Commit d30c1114 authored by haftmann's avatar haftmann
Browse files

dedicated locale for preorder and abstract bdd operation

parent 908f7c03d556
......@@ -50,7 +50,7 @@ lemma add_ub: "x \<le> x + y"
by (metis add_assoc add_idem less_eq_def)
lemma add_lub: "x + y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
by (metis add_assoc add_commute less_eq_def order.ordering_axioms ordering.refl)
by (metis add_assoc add_ub add.left_commute less_eq_def)
......@@ -282,7 +282,7 @@ proof -
hence "d p \<le> wp ((d r \<cdot> x)\<^sup>\<star>) p"
using wp_star_induct_var by blast
thus ?thesis
by (metis order.ordering_axioms ordering.trans while_def wp_weaken)
by (simp add: while_def) (use local.dual_order.trans wp_weaken in fastforce)
lemma wp_while_inv: "d p \<le> d i \<Longrightarrow> d i \<cdot> ad r \<le> d q \<Longrightarrow> d i \<cdot> d r \<le> wp x i \<Longrightarrow> d p \<le> wp (while r inv i do x od) q"
......@@ -530,6 +530,3 @@ lemma var_swap_ref_var:
using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkad.R_skip by fastforce
......@@ -51,7 +51,7 @@ lemma add_iso: "x \<le> y \<Longrightarrow> x + z \<le> y + z"
by (metis (no_types, lifting) abel_semigroup.commute add.abel_semigroup_axioms add.semigroup_axioms add_idem less_eq_def semigroup.assoc)
lemma add_lub: "x + y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
by (metis add_assoc add_commute less_eq_def order.ordering_axioms ordering.refl)
by (metis add_assoc add.left_commute add_idem less_eq_def)
......@@ -363,5 +363,3 @@ lemma var_swap_ref_var:
using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkat.R_skip by fastforce
......@@ -16,11 +16,11 @@ setup \<open>Consts.add_const_data ("NUMC", UtilArith.is_numc)\<close>
subsection \<open>Results in class order or preorder\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.order_class.order.trans} [with_filt (not_type_filter "a" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.order_class.order.strict_trans} [with_filt (not_type_filter "a" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.order_le_less_trans} [with_filt (not_type_filter "x" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.order_less_le_trans} [with_filt (not_type_filter "x" natT)]\<close>
setup \<open>add_resolve_prfstep @{thm Orderings.order_class.order.irrefl}\<close>
setup \<open>add_forward_prfstep_cond @{thm order.trans} [with_filt (not_type_filter "a" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm order.strict_trans} [with_filt (not_type_filter "a" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm order_le_less_trans} [with_filt (not_type_filter "x" natT)]\<close>
setup \<open>add_forward_prfstep_cond @{thm order_less_le_trans} [with_filt (not_type_filter "x" natT)]\<close>
setup \<open>add_resolve_prfstep @{thm order.irrefl}\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.le_neq_trans} [with_cond "?a \<noteq> ?b"]\<close>
setup \<open>add_forward_prfstep_cond @{thm Orderings.order_antisym} [with_filt (order_filter "x" "y"), with_cond "?x \<noteq> ?y"]\<close>
......@@ -979,21 +979,6 @@ text \<open>
more easily facilitate simultaneously working with both an order and its dual.
subsubsection \<open>Dual ordering\<close>
context ordering
abbreviation greater_eq :: "'a\<Rightarrow>'a\<Rightarrow>bool" (infix "\<succeq>" 50)
where "greater_eq a b \<equiv> less_eq b a"
abbreviation greater :: "'a\<Rightarrow>'a\<Rightarrow>bool" (infix "\<succ>" 50)
where "greater a b \<equiv> less b a"
lemma dual: "ordering greater_eq greater"
using strict_iff_order refl antisym trans by unfold_locales fastforce
end (* context ordering *)
subsubsection \<open>Morphisms of posets\<close>
locale OrderingSetMap =
......@@ -1009,27 +994,18 @@ locale OrderingSetMap =
lemma comp:
assumes "OrderingSetMap less_eq' less' less_eq'' less'' Q g" "f`P \<subseteq> Q"
assumes "OrderingSetMap less_eq' less' less_eq'' less'' Q g"
"f`P \<subseteq> Q"
shows "OrderingSetMap less_eq less less_eq'' less'' P (g\<circ>f)"
proof (
intro_locales, rule OrderingSetMap.axioms(2), rule assms(1), unfold_locales
from assms(2)
show "\<And>a b. a \<in> P \<Longrightarrow> b \<in> P \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> less_eq'' ((g \<circ> f) a) ((g \<circ> f) b)"
using ordsetmap OrderingSetMap.ordsetmap[OF assms(1)]
by force
proof -
from assms(1) interpret I: OrderingSetMap less_eq' less' less_eq'' less'' Q g .
show ?thesis
by standard (use assms(2) in \<open>auto intro: ordsetmap I.ordsetmap\<close>)
lemma subset: "Q\<subseteq>P \<Longrightarrow> OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<^bold>\<le>*) (\<^bold><*) Q f"
using ordsetmap by unfold_locales fast
lemma dual:
"OrderingSetMap domain.greater_eq domain.greater
codomain.greater_eq codomain.greater P f"
proof (intro_locales, rule domain.dual, rule codomain.dual, unfold_locales)
from ordsetmap show "\<And>a b. a\<in>P \<Longrightarrow> b\<in>P \<Longrightarrow> a\<succeq>b \<Longrightarrow> f b \<^bold>\<le>* f a" by fast
end (* context OrderingSetMap *)
locale OrderingSetIso = OrderingSetMap less_eq less less_eq' less' P f
......@@ -1113,12 +1089,19 @@ lemma iso_subset:
by (blast intro: OrderingSetMap.isoI)
lemma iso_dual:
"OrderingSetIso domain.greater_eq domain.greater
codomain.greater_eq codomain.greater P f"
by (
rule OrderingSetMap.isoI, rule OrderingSetMap.dual, unfold_locales,
rule inj, rule rev_ordsetmap
\<open>OrderingSetIso (\<lambda>a b. less_eq b a) (\<lambda>a b. less b a)
(\<lambda>a b. less_eq' b a) (\<lambda>a b. less' b a) P f\<close>
apply (rule OrderingSetMap.isoI)
apply unfold_locales
using inj
apply (auto simp add: domain.refl codomain.refl
domain.irrefl codomain.irrefl
domain.order_iff_strict codomain.order_iff_strict
ordsetmap_strict rev_ordsetmap_strict inj_onD
intro: domain.trans codomain.trans
domain.strict_trans codomain.strict_trans
domain.antisym codomain.antisym)
end (* context OrderingSetIso *)
......@@ -1031,7 +1031,7 @@ proof -
moreover have "llength t>0"
proof -
from \<open>x < llength (\<pi>\<^bsub>c\<^esub>(t))\<close> have "llength (\<pi>\<^bsub>c\<^esub>(t))>0" by auto
thus ?thesis using proj_llength Orderings.order_class.order.strict_trans2 by blast
thus ?thesis using proj_llength order.strict_trans2 by blast
ultimately show "llength t - 1 < llength t" by (metis One_nat_def \<open>lfinite t\<close> diff_Suc_less
enat_ord_simps(2) idiff_enat_enat lfinite_conv_llength_enat one_enat_def zero_enat_def)
......@@ -1800,8 +1800,8 @@ proof -
have "finite ?K" by auto
with not_empty_K have *:
"\<forall> k' < k. cyc_free_subs n {0..k'} m"
unfolding k_def
by simp (meson order_class.dual_order.trans preorder_class.less_le_not_le)
by (auto simp add: k_def not_le)
(meson less_imp_le_nat local.leI order_less_irrefl preorder_class.order_trans)
from linorder_class.Min_in[OF \<open>finite ?K\<close> \<open>?K \<noteq> {}\<close>] have
"\<not> cyc_free_subs n {0..k} m" "k \<le> n"
unfolding k_def by auto
......@@ -92,10 +92,7 @@ proof -
moreover from mnh2 have "unat x < unat (65536::128 word)" by(rule Word.unat_mono)
ultimately have x: "unat x < 65536" by simp
with mnh3 have "unat x < 2 ^ (m - n)"
apply(rule_tac b=65535 in Orderings.order_class.order.strict_trans1)
using power_2_16_nat apply blast
using power_2_16_nat [of \<open>m - n\<close>] by simp
with assms(2) show ?thesis by(subst word_less_nat_alt) simp
hence mnhelper2: "(of_bl::bool list \<Rightarrow> 128 word) (to_bl b) < 2 ^ (m - n)"
......@@ -1057,11 +1057,11 @@ text \<open>
class le_eqvt = order +
assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))"
class le_eqvt = pt +
assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y :: 'a :: {order, pt})))"
class inf_eqvt = Inf +
assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, complete_lattice}) set))"
class inf_eqvt = pt +
assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X :: 'a :: {complete_lattice, pt} set))"
instantiation bool :: le_eqvt
......@@ -74,12 +74,8 @@ proof -
finally show "Re (exp (Complex wR \<theta>)) = Re z" .
moreover have "-pi<\<theta>" "\<theta>\<le>pi"
unfolding \<theta>_def
subgoal by (auto intro:order_class.order.strict_trans[OF _ arctan_lbound])
apply (rule preorder_class.less_imp_le)
by (auto intro:order_class.order.strict_trans[OF arctan_ubound])
using arctan_lbound [of \<open>Im z / Re z\<close>] arctan_ubound [of \<open>Im z / Re z\<close>]
by (simp_all add: \<theta>_def)
ultimately have "Ln z = Complex wR \<theta>" using Ln_unique by auto
then show ?thesis using that unfolding \<theta>_def by auto
......@@ -691,8 +687,7 @@ proof -
finally have *:"dist x y = \<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar>" .
then have "\<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar> < e" using \<open>dist x y<e\<close> by auto
then have "\<bar>k+k1-k2\<bar>*\<bar>\<delta>\<bar> < \<bar>\<delta>\<bar>"
apply (elim order_class.dual_order.strict_trans1[rotated])
unfolding e_def by auto
by (simp add: e_def split: if_splits)
then have "\<bar>k+k1-k2\<bar> = 0" unfolding e_def using \<open>\<delta>\<noteq>0\<close> by force
then have "dist x y=0" using * by auto
then show ?thesis by auto
Supports Markdown
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