Read about our upcoming Code of Conduct on this issue

Commit e4bd8fd9 authored by haftmann's avatar haftmann
Browse files

avoid name clash

parent 1a42ddd5dbbc
......@@ -121,7 +121,7 @@ proof unfold_locales
also have "... \<le> top * --x * top"
by (simp add: minarc_below mult_isotone)
finally show "top * x * top = top"
using 1 antisym by simp
using 1 order.antisym by simp
qed
lemma minarc_bot:
......
......@@ -387,7 +387,7 @@ proof
also have "... = (if i = ?h \<and> j = i then h (i,j) + (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) else h (i,j) + zero)"
by simp
also have "... \<le> (if i = ?h \<and> j = i then h (i,j) + (\<Sum>\<^sub>k \<Sum>\<^sub>l g (k,l)) else h (i,j) + zero)"
using 4 inf.eq_iff by auto
using 4 order.eq_iff by auto
also have "... = h (i,j) + (if i = ?h \<and> j = i then \<Sum>\<^sub>k \<Sum>\<^sub>l g (k,l) else zero)"
by simp
finally show "h (i,j) + (sum\<^sub>M f) (i,j) \<le> h (i,j) + (sum\<^sub>M g) (i,j)"
......@@ -715,7 +715,7 @@ lemma regular_bot_top_2:
sublocale heyting: heyting_stone_algebra where implies = "\<lambda>x y . if x \<le> y then top else y"
apply unfold_locales
apply (simp add: antisym)
apply (simp add: order.antisym)
by auto
end
......
......@@ -72,7 +72,7 @@ proof (intro_classes, unfold_locales; unfold compare_complex_def)
assume "?c (Re x, Im x) (Re y, Im y) = Lt"
"?c (Re y, Im y) (Re z, Im z) = Lt"
thus "?c (Re x, Im x) (Re z, Im z) = Lt"
by (rule trans)
by (rule comp_trans)
}
{
assume "?c (Re x, Im x) (Re y, Im y) = Eq"
......
......@@ -103,16 +103,16 @@ lemma a_idem [simp]: "ad x \<cdot> ad x = ad x"
by (metis a_d_closed d1_a)
lemma meet_ord: "ad x \<le> ad y \<longleftrightarrow> ad x \<cdot> ad y = ad x"
by (metis a_d_closed a_subid_aux d1_a antisym mult_1_right mult_isol)
by (metis a_d_closed a_subid_aux d1_a order.antisym mult_1_right mult_isol)
lemma d_wloc: "x \<cdot> y = 0 \<longleftrightarrow> x \<cdot> d y = 0"
by (metis a_subid_aux d1_a dom_op_def add_ub antisym as1 as2 mult_1_right mult_assoc)
by (metis a_subid_aux d1_a dom_op_def add_ub order.antisym as1 as2 mult_1_right mult_assoc)
lemma gla_1: "ad x \<cdot> y = 0 \<Longrightarrow> ad x \<le> ad y"
by (metis a_subid_aux d_wloc dom_op_def add_zerol as3 distrib_left mult_1_right)
lemma a2_eq [simp]: "ad (x \<cdot> d y) = ad (x \<cdot> y)"
by (metis a_mul_d d1_a dom_op_def gla_1 add_ub antisym as1 as2 mult_assoc)
by (metis a_mul_d d1_a dom_op_def gla_1 add_ub order.antisym as1 as2 mult_assoc)
lemma a_supdist: "ad (x + y) \<le> ad x"
by (metis add_commute gla_1 add_ub add_zerol as1 distrib_left less_eq_def)
......@@ -130,7 +130,7 @@ proof -
finally have "ad x \<cdot> ad y \<le> ad y \<cdot> ad x"
by simp }
thus ?thesis
by (simp add: antisym)
by (simp add: order.antisym)
qed
lemma a_closed [simp]: "d (ad x \<cdot> ad y) = ad x \<cdot> ad y"
......@@ -146,7 +146,7 @@ proof -
qed
lemma a_exp [simp]: "ad (ad x \<cdot> y) = d x + ad y"
proof (rule antisym)
proof (rule order.antisym)
have "ad (ad x \<cdot> y) \<cdot> ad x \<cdot> d y = 0"
using d_wloc mult_assoc by fastforce
hence a: "ad (ad x \<cdot> y) \<cdot> d y \<le> d x"
......@@ -175,7 +175,7 @@ proof -
qed
lemma a4: "ad (x + y) = ad x \<cdot> ad y"
proof (rule antisym)
proof (rule order.antisym)
show "ad (x + y) \<le> ad x \<cdot> ad y"
by (metis a_supdist add_commute mult_isor meet_ord)
hence "ad x \<cdot> ad y = ad x \<cdot> ad y + ad (x + y)"
......
......@@ -115,7 +115,7 @@ proof -
qed
lemma fdia_arden_eq: "\<nabla>x = 0 \<Longrightarrow> d p = d q + |x\<rangle> p \<Longrightarrow> d p = |x\<^sup>\<star>\<rangle> q"
by (simp add: fdia_arden dka.fdia_star_induct_eq eq_iff)
by (simp add: fdia_arden dka.fdia_star_induct_eq order.eq_iff)
lemma fdia_arden_iff: "\<nabla>x = 0 \<Longrightarrow> (d p = d q + |x\<rangle> p \<longleftrightarrow> d p = |x\<^sup>\<star>\<rangle> q)"
by (metis fdia_arden_eq dka.fdia_d_simp dka.fdia_star_unfold_var)
......@@ -137,7 +137,7 @@ proof -
qed
lemma fbox_arden_eq: "\<nabla>x = 0 \<Longrightarrow> d q \<cdot> |x] p = d p \<Longrightarrow> |x\<^sup>\<star>] q = d p"
by (simp add: fbox_arden antisym fbox_star_induct_eq)
by (simp add: fbox_arden order.antisym fbox_star_induct_eq)
lemma fbox_arden_iff: "\<nabla>x = 0 \<Longrightarrow> (d p = d q \<cdot> |x] p \<longleftrightarrow> d p = |x\<^sup>\<star>] q)"
by (metis fbox_arden_eq fbox_simp fbox_star_unfold_var)
......
......@@ -112,7 +112,7 @@ lemma a_d_iff: "a x = 1 \<sqinter> -(x \<cdot> \<top>)"
by (clarsimp simp: a_def dblo.d_def inf_sup_distrib1)
lemma topr: "-(x \<cdot> \<top>) \<cdot> \<top> = -(x \<cdot> \<top>)"
proof (rule antisym)
proof (rule order.antisym)
show "-(x \<cdot> \<top>) \<le> -(x \<cdot> \<top>) \<cdot> \<top>"
by (metis mult_isol_var mult_oner order_refl top_greatest)
have "-(x \<cdot> \<top>) \<sqinter> (x \<cdot> \<top>) = \<bottom>"
......@@ -180,7 +180,7 @@ lemma ar_r_iff: "ar x = 1 \<sqinter> -(\<top> \<cdot> x)"
by (simp add: ar_def inf_sup_distrib1 r_def)
lemma topl: "\<top>\<cdot>(-(\<top> \<cdot> x)) = -(\<top> \<cdot> x)"
proof (rule antisym)
proof (rule order.antisym)
show "\<top> \<cdot> - (\<top> \<cdot> x) \<le> - (\<top> \<cdot> x)"
by (metis bot_annir' compl_inf_bot inf_bot_iff_le ldv')
show "- (\<top> \<cdot> x) \<le> \<top> \<cdot> - (\<top> \<cdot> x)"
......@@ -254,7 +254,7 @@ sublocale dioid_one_zero "(\<squnion>)" "(\<cdot>)" "1" "\<bottom>" "(\<le>)" "(
by (standard, simp add: le_iff_sup, auto)
lemma Sup_sup_pred: "x \<squnion> Sup{y. P y} = Sup{y. y = x \<or> P y}"
apply (rule antisym)
apply (rule order.antisym)
apply (simp add: Collect_mono Sup_subset_mono Sup_upper)
using Sup_least Sup_upper le_supI2 by fastforce
......
......@@ -22,7 +22,7 @@ next
from this have "mset_set (set_mset (M + {#x#})) = mset_set (set_mset M)"
by (simp add: insert_absorb)
from this add.hyps show ?thesis
using subset_mset.order.trans by fastforce
using subset_mset.trans by fastforce
next
assume "\<not> x \<in># M"
from this add.hyps have "{#x#} + mset_set (set_mset M) \<subseteq># M + {#x#}"
......
......@@ -109,7 +109,7 @@ proof (rule ccontr)
with \<open>chain C\<close> \<open>C \<noteq> {}\<close> have "chain (C - A)" "C - A \<noteq> {}"
by (auto intro: chain_Diff)
moreover have "Sup C = Sup (C - A)"
proof (safe intro!: antisym ccpo_Sup_least \<open>chain C\<close> chain_Diff)
proof (safe intro!: order.antisym ccpo_Sup_least \<open>chain C\<close> chain_Diff)
fix c assume "c \<in> C"
with * obtain c' where "c' \<in> C" "c \<le> c'" "c' \<notin> A"
by auto
......
......@@ -189,7 +189,7 @@ qed
lemma ldistinct_lmerge:
"\<lbrakk> lsorted xs; lsorted ys; ldistinct xs; ldistinct ys \<rbrakk>
\<Longrightarrow> ldistinct (lmerge xs ys)"
by(coinduction arbitrary: xs ys)(auto 4 3 simp add: lhd_lmerge ltl_lmerge not_lnull_conv lsorted_LCons not_less dest!: in_lset_lmergeD dest: antisym)
by(coinduction arbitrary: xs ys)(auto 4 3 simp add: lhd_lmerge ltl_lmerge not_lnull_conv lsorted_LCons not_less dest!: in_lset_lmergeD dest: order.antisym)
end
......
......@@ -50,7 +50,7 @@ lemma (in ccpo) Sup_Un_less:
assumes chain: "Complete_Partial_Order.chain (\<le>) (A \<union> B)"
and AB: "\<forall>x\<in>A. \<exists>y\<in>B. x \<le> y"
shows "Sup (A \<union> B) = Sup B"
proof(rule antisym)
proof(rule order.antisym)
from chain have chain': "Complete_Partial_Order.chain (\<le>) B"
by(blast intro: chain_subset)
show "Sup (A \<union> B) \<le> Sup B" using chain
......
......@@ -59,7 +59,7 @@ proof (rule order_class.order.antisym)
by (simp add: complete_lattice_class.INF_lower complete_lattice_class.le_INF_iff)
next
have "\<And>k. \<exists>i j. f (i + j) \<le> f k"
by (metis add.left_neutral order_class.eq_iff)
by (metis Nat.add_0_right order_refl)
then have "\<And>k. \<exists>i. (\<Sqinter>j. f (i + j)) \<le> f k"
by (meson UNIV_I complete_lattice_class.INF_lower2)
then show "(\<Sqinter>i j. f (i + j)) \<le> (\<Sqinter>k. f k)"
......
......@@ -157,7 +157,7 @@ proof -
have "linorder.sorted (\<sqsubseteq>) (map fst (map (\<lambda>(c, d). ((a, c), f a b c d)) ys))"
using ys by(induct ys) auto
thus ?case using x Cons
by(fastforce simp add: set_alist_product a.not_less dest: bspec a.antisym intro: rev_image_eqI)
by(fastforce simp add: set_alist_product a.not_less dest: bspec a.order_antisym intro: rev_image_eqI)
qed
qed
......
......@@ -105,7 +105,7 @@ next
by fastforce
ultimately show ?case by(simp add: "4.IH")
next
case 5 thus ?case by(simp add: not_less eq_iff)
case 5 thus ?case by(simp add: not_less order_eq_iff)
qed
lemma sorted_quicksort [simp]: "sorted (quicksort xs)"
......@@ -1222,10 +1222,10 @@ context linorder begin
lemma sorted_list_subset_correct:
"\<lbrakk> sorted xs; distinct xs; sorted ys; distinct ys \<rbrakk>
\<Longrightarrow> sorted_list_subset (=) xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
apply(induct "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" xs ys rule: sorted_list_subset.induct)
apply(auto 6 2)
apply auto
by (metis eq_iff insert_iff subsetD)
apply(induct "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" xs ys rule: sorted_list_subset.induct)
apply(auto 6 2)
using order_antisym apply auto
done
end
......
......@@ -1060,8 +1060,8 @@ next
case Cons
show ?thesis using assms unfolding Cons exhaustive.simps
apply(subst exhaustive_above_iff)
apply(auto simp add: less_le proper_interval_simps not_less)
by (metis List.set_simps(2) UNIV_I eq_iff set_ConsD)
apply(auto simp add: less_le proper_interval_simps not_less intro: order_antisym)
done
qed
theorem proper_interval_set_aux:
......
......@@ -1144,7 +1144,7 @@ proof(intro mcontI contI)
moreover
have "ord' (lub' (f ` Y)) (f (lub Y))" using chain'
by(rule ccpo'.ccpo_Sup_least)(blast intro: monotoneD[OF mono] ccpo.ccpo_Sup_upper[OF ccpo chain])
ultimately show "f (lub Y) = lub' (f ` Y)" by(rule ccpo'.antisym)
ultimately show "f (lub Y) = lub' (f ` Y)" by(rule ccpo'.order.antisym)
qed(fact mono)
lemma rel_fun_curry: includes lifting_syntax shows
......@@ -1248,7 +1248,7 @@ proof -
interpret c1: ccpo lub1 leq1 "mk_less leq1" by fact
interpret c2: ccpo lub2 leq2 "mk_less leq2" by fact
show ?thesis
proof(rule c1.antisym)
proof(rule c1.order.antisym)
have fg: "monotone leq2 leq2 (\<lambda>x. f (g x))" using f g by(rule monotone2monotone) simp_all
have gf: "monotone leq1 leq1 (\<lambda>x. g (f x))" using g f by(rule monotone2monotone) simp_all
show "leq1 (c1.fixp (\<lambda>x. g (f x))) (g (c2.fixp (\<lambda>x. f (g x))))" using gf
......
......@@ -56,7 +56,7 @@ locale comparator =
fixes comp :: "'a comparator"
assumes sym: "invert_order (comp x y) = comp y x"
and weak_eq: "comp x y = Eq \<Longrightarrow> x = y"
and trans: "comp x y = Lt \<Longrightarrow> comp y z = Lt \<Longrightarrow> comp x z = Lt"
and comp_trans: "comp x y = Lt \<Longrightarrow> comp y z = Lt \<Longrightarrow> comp x z = Lt"
begin
lemma eq: "(comp x y = Eq) = (x = y)"
......@@ -72,20 +72,33 @@ lemma comp_same [simp]:
abbreviation "lt \<equiv> lt_of_comp comp"
abbreviation "le \<equiv> le_of_comp comp"
lemma linorder: "class.linorder le lt"
sublocale ordering le lt
proof
note [simp] = lt_of_comp_def le_of_comp_def
fix x y z :: 'a
show "lt x y = (le x y \<and> \<not> le y x)"
using sym [of x y] by (cases "comp x y") (simp_all)
show "le x y \<or> le y x"
using sym [of x y] by (cases "comp x y") (simp_all)
show "le x x" using eq [of x x] by (simp)
show "le x y \<Longrightarrow> le y x \<Longrightarrow> x = y"
using sym [of x y] by (cases "comp x y") (simp_all add: eq)
show "le x y \<Longrightarrow> le y z \<Longrightarrow> le x z"
by (cases "comp x y" "comp y z" rule: order.exhaust [case_product order.exhaust])
(auto dest: trans simp: eq)
(auto dest: comp_trans simp: eq)
show "le x y \<Longrightarrow> le y x \<Longrightarrow> x = y"
using sym [of x y] by (cases "comp x y") (simp_all add: eq)
show "lt x y \<longleftrightarrow> le x y \<and> x \<noteq> y"
using eq [of x y] by (cases "comp x y") (simp_all)
qed
lemma linorder: "class.linorder le lt"
proof (rule class.linorder.intro)
interpret order le lt
using ordering_axioms by (rule ordering_orderI)
show \<open>class.order le lt\<close>
by (fact order_axioms)
show \<open>class.linorder_axioms le\<close>
proof
note [simp] = lt_of_comp_def le_of_comp_def
fix x y :: 'a
show "le x y \<or> le y x"
using sym [of x y] by (cases "comp x y") (simp_all)
qed
qed
sublocale linorder le lt
......
......@@ -205,7 +205,7 @@ proof -
fix x y z
assume "acomp x y \<noteq> Gt" "acomp y z \<noteq> Gt"
thus "acomp x z \<noteq> Gt \<and> (acomp x y = Lt \<or> acomp y z = Lt \<longrightarrow> acomp x z = Lt)"
using trans [of x y z] and eq [of x y] and eq [of y z]
using comp_trans [of x y z] and eq [of x y] and eq [of y z]
by (cases "acomp x y" "acomp y z" rule: order.exhaust [case_product order.exhaust]) auto
qed
qed
......
......@@ -36,7 +36,7 @@ qed
lemma add_nonneg_eq_0_iff:
assumes x: "0 \<le> x" and y: "0 \<le> y"
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
by (metis add.comm_neutral add.left_neutral add_left_mono antisym x y)
by (metis local.add_0_left local.add_0_right local.add_left_mono local.antisym_conv x y)
lemma add_incr: "0\<le>b \<Longrightarrow> a \<le> a+b"
by (metis add.comm_neutral add_left_mono)
......
......@@ -199,7 +199,7 @@ begin
using assms proof induction
case (liveSimple' n v)
from liveSimple'.prems have "vs' = [v]"
by (metis append_Nil butlast.simps(2) suffixI suffix_order.antisym suffix_unsnoc)
by (metis append_Nil butlast.simps(2) suffixI suffix_order.order_antisym suffix_unsnoc)
with liveSimple'.hyps show ?case by (auto intro: liveVal'.liveSimple')
next
case (livePhi' v vs v')
......
......@@ -55,7 +55,7 @@ lemma strict_prefix_butlast:
using assms unfolding append_butlast_last_id[symmetric] by (auto simp add:less_le butlast_strict_prefix prefix_order.le_less_trans)
lemma prefix_tl_subset: "prefix xs ys \<Longrightarrow> set (tl xs) \<subseteq> set (tl ys)"
by (metis Nil_tl prefix_bot.bot.extremum prefix_def set_mono_prefix tl_append2)
by (metis Nil_tl prefix_bot.extremum prefix_def set_mono_prefix tl_append2)
lemma suffix_tl_subset: "suffix xs ys \<Longrightarrow> set (tl xs) \<subseteq> set (tl ys)"
by (metis append_Nil suffix_def set_mono_suffix suffix_tl suffix_order.order_trans tl_append2)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment