--- a/src/HOL/MicroJava/BV/Err.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Tue Apr 02 13:47:01 2002 +0200
@@ -135,20 +135,24 @@
"~(Err <_(le r) x)"
by (simp add: lesssub_def lesub_def le_def split: err.split)
-lemma semilat_errI [intro]:
- "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+lemma semilat_errI [intro]: includes semilat
+shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+apply(insert semilat)
apply (unfold semilat_Def closed_def plussub_def lesub_def
lift2_def Err.le_def err_def)
apply (simp split: err.split)
done
-lemma err_semilat_eslI [intro, simp]:
- "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
+lemma err_semilat_eslI_aux:
+includes semilat shows "err_semilat(esl(A,r,f))"
apply (unfold sl_def esl_def)
-apply (simp (no_asm_simp) only: split_tupled_all)
-apply (simp add: semilat_errI)
+apply (simp add: semilat_errI[OF semilat])
done
+lemma err_semilat_eslI [intro, simp]:
+ "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
+by(simp add: err_semilat_eslI_aux split_tupled_all)
+
lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: err.split)
@@ -222,27 +226,29 @@
lemma semilat_le_err_Err_plus [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
- by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+ by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
+ semilat.le_iff_plus_unchanged2 [THEN iffD1])
lemma semilat_le_err_plus_Err [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
- by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+ by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
+ semilat.le_iff_plus_unchanged2 [THEN iffD1])
lemma semilat_le_err_OK1:
"\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
\<Longrightarrow> x <=_r z";
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
-apply simp
-done
+apply (simp add:semilat.ub1)
+done
lemma semilat_le_err_OK2:
"\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
\<Longrightarrow> y <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
-apply simp
-done
+apply (simp add:semilat.ub2)
+done
lemma eq_order_le:
"\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
@@ -257,14 +263,14 @@
have plus_le_conv3: "\<And>A x y z f r.
\<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
\<Longrightarrow> x <=_r z \<and> y <=_r z"
- by (rule plus_le_conv [THEN iffD1])
+ by (rule semilat.plus_le_conv [THEN iffD1])
case rule_context
thus ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule OK_le_err_OK [THEN iffD2])
- apply (drule semilat_lub)
+ apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
apply assumption
apply assumption
apply simp
@@ -276,10 +282,10 @@
apply (rename_tac z)
apply (subgoal_tac "OK z: err A")
apply (drule eq_order_le)
- apply blast
+ apply (erule semilat.orderI)
apply (blast dest: plus_le_conv3)
apply (erule subst)
- apply (blast intro: closedD)
+ apply (blast intro: semilat.closedI closedD)
done
qed
--- a/src/HOL/MicroJava/BV/JType.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Tue Apr 02 13:47:01 2002 +0200
@@ -279,15 +279,15 @@
have
"(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and>
(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
- by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
+ by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split)
- moreover
+ moreover
from wf_prog single_valued acyclic
have
"\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G).
x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
- by (unfold lift2_def plussub_def lesub_def le_def)
+ by (unfold lift2_def plussub_def lesub_def Err.le_def)
(auto intro: sup_subtype_smallest sup_exists split: err.split)
ultimately
--- a/src/HOL/MicroJava/BV/JVM.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Apr 02 13:47:01 2002 +0200
@@ -288,8 +288,8 @@
apply (rule err_semilat_upto_esl)
apply (rule err_semilat_JType_esl, assumption+)
apply (rule err_semilat_eslI)
- apply (rule semilat_Listn_sl)
- apply (rule err_semilat_JType_esl, assumption+)
+ apply (rule Listn_sl)
+ apply (rule err_semilat_JType_esl, assumption+)
done
lemma sl_triple_conv:
--- a/src/HOL/MicroJava/BV/Kildall.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Apr 02 13:47:01 2002 +0200
@@ -43,36 +43,34 @@
"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
-lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
+lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
-lemma nth_merges:
- "\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A;
- \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
+lemma (in semilat) nth_merges:
+ "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
(merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
- (is "\<And>ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
+ (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp
fix ss p' ps'
- assume sl: "semilat (A, r, f)"
assume ss: "ss \<in> list n A"
assume l: "p < length ss"
assume "?steptype (p'#ps')"
then obtain a b where
p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?steptype ps'"
by (cases p', auto)
- assume "\<And>ss. semilat (A,r,f) \<Longrightarrow> p < length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
+ assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
- from sl ss ab
+ from ss ab
have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
moreover
from calculation
have "p < length (ss[a := b +_f ss!a])" by simp
ultimately
have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
- with p' l
+ with p' l
show "?P ss (p'#ps')" by simp
qed
@@ -84,47 +82,43 @@
by (induct_tac ps, auto)
-lemma merges_preserves_type_lemma:
- "semilat(A,r,f) \<Longrightarrow>
- \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
- \<longrightarrow> merges f ps xs \<in> list n A"
- apply (frule semilatDclosedI)
- apply (unfold closed_def)
- apply (induct_tac ps)
- apply simp
- apply clarsimp
- done
+lemma (in semilat) merges_preserves_type_lemma:
+shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+ \<longrightarrow> merges f ps xs \<in> list n A"
+apply (insert closedI)
+apply (unfold closed_def)
+apply (induct_tac ps)
+ apply simp
+apply clarsimp
+done
-lemma merges_preserves_type [simp]:
- "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
+lemma (in semilat) merges_preserves_type [simp]:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
\<Longrightarrow> merges f ps xs \<in> list n A"
- by (simp add: merges_preserves_type_lemma)
-
-lemma merges_incr_lemma:
- "semilat(A,r,f) \<Longrightarrow>
- \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
- apply (induct_tac ps)
- apply simp
+by (simp add: merges_preserves_type_lemma)
+
+lemma (in semilat) merges_incr_lemma:
+ "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
+apply (induct_tac ps)
+ apply simp
+apply simp
+apply clarify
+apply (rule order_trans)
apply simp
- apply clarify
- apply (rule order_trans)
- apply simp
- apply (erule list_update_incr)
- apply assumption
- apply simp
- apply simp
- apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
- done
+ apply (erule list_update_incr)
+ apply simp
+ apply simp
+apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
+done
-lemma merges_incr:
- "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk>
+lemma (in semilat) merges_incr:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk>
\<Longrightarrow> xs <=[r] merges f ps xs"
by (simp add: merges_incr_lemma)
-lemma merges_same_conv [rule_format]:
- "semilat(A,r,f) \<Longrightarrow>
- (\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>
+lemma (in semilat) merges_same_conv [rule_format]:
+ "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>
(merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
apply (induct_tac ps)
apply simp
@@ -135,7 +129,6 @@
apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
apply (force dest!: le_listD simp add: nth_list_update)
apply (erule subst, rule merges_incr)
- apply assumption
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
apply clarify
apply (rule conjI)
@@ -158,24 +151,22 @@
done
-lemma list_update_le_listI [rule_format]:
+lemma (in semilat) list_update_le_listI [rule_format]:
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
- x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
- xs[p := x +_f xs!p] <=[r] ys"
+ x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
+ apply(insert semilat)
apply (unfold Listn.le_def lesub_def semilat_def)
apply (simp add: list_all2_conv_all_nth nth_list_update)
done
-lemma merges_pres_le_ub:
- "\<lbrakk> semilat(A,r,f); set ts <= A; set ss <= A;
- \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts;
- ss <=[r] ts \<rbrakk>
+lemma (in semilat) merges_pres_le_ub:
+shows "\<lbrakk> set ts <= A; set ss <= A;
+ \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
\<Longrightarrow> merges f ps ss <=[r] ts"
proof -
- { fix A r f t ts ps
+ { fix t ts ps
have
- "\<And>qs. \<lbrakk> semilat(A,r,f); set ts <= A;
- \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts \<rbrakk> \<Longrightarrow>
+ "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
set qs <= set ps \<longrightarrow>
(\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
apply (induct_tac qs)
@@ -218,8 +209,8 @@
(** iter **)
-lemma stable_pres_lemma:
- "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n;
+lemma (in semilat) stable_pres_lemma:
+shows "\<lbrakk>pres_type step n A; bounded step n;
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
\<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
\<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;
@@ -237,8 +228,7 @@
apply simp
apply simp
apply clarify
- apply (subst nth_merges)
- apply assumption
+ apply (subst nth_merges)
apply simp
apply (blast dest: boundedD)
apply assumption
@@ -248,10 +238,11 @@
apply (erule pres_typeD)
prefer 3 apply assumption
apply simp
- apply simp
- apply (frule nth_merges [of _ _ _ q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
- prefer 2 apply assumption
- apply simp
+ apply simp
+apply(subgoal_tac "q < length ss")
+prefer 2 apply simp
+ apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
+apply assumption
apply clarify
apply (rule conjI)
apply (blast dest: boundedD)
@@ -281,8 +272,8 @@
apply (rule order_trans)
apply simp
defer
- apply (rule ub2)
- apply assumption
+ apply (rule pp_ub2)(*
+ apply assumption*)
apply simp
apply clarify
apply simp
@@ -294,16 +285,15 @@
apply (blast intro: listE_nth_in dest: boundedD)
apply blast
done
-
-
-lemma merges_bounded_lemma:
- "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n;
- \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
- ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
+
+
+lemma (in semilat) merges_bounded_lemma:
+ "\<lbrakk> mono r step n A; bounded step n;
+ \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
+ ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
\<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
apply (unfold stable_def)
apply (rule merges_pres_le_ub)
- apply assumption
apply simp
apply simp
prefer 2 apply assumption
@@ -326,10 +316,11 @@
apply (blast intro: order_trans)
done
-lemma termination_lemma:
- "\<lbrakk> semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow>
+lemma termination_lemma: includes semilat
+shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow>
ss <[r] merges f qs ss \<or>
merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
+apply(insert semilat)
apply (unfold lesssub_def)
apply (simp (no_asm_simp) add: merges_incr)
apply (rule impI)
@@ -346,14 +337,15 @@
apply clarsimp
done
-lemma iter_properties[rule_format]:
- "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
+lemma iter_properties[rule_format]: includes semilat
+shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
\<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
iter f step ss0 w0 = (ss',w')
\<longrightarrow>
ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
+apply(insert semilat)
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
@@ -363,7 +355,7 @@
in while_rule)
-- "Invariant holds initially:"
-apply (simp add:stables_def)
+apply (simp add:stables_def)
-- "Invariant is preserved:"
apply(simp add: stables_def split_paired_all)
@@ -385,8 +377,8 @@
apply blast
apply simp
apply (rule conjI)
- apply (erule merges_preserves_type)
- apply blast
+ apply (rule merges_preserves_type)
+ apply blast
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
@@ -396,10 +388,10 @@
apply (erule listE_nth_in)
apply blast
apply blast
-apply (rule conjI)
- apply clarify
+apply (rule conjI)
+ apply clarify
apply (blast intro!: stable_pres_lemma)
-apply (rule conjI)
+apply (rule conjI)
apply (blast intro!: merges_incr intro: le_list_trans)
apply (rule conjI)
apply clarsimp
@@ -408,11 +400,11 @@
-- "Postcondition holds upon termination:"
-apply(clarsimp simp add: stables_def split_paired_all)
+apply(clarsimp simp add: stables_def split_paired_all)
-- "Well-foundedness of the termination relation:"
apply (rule wf_lex_prod)
- apply (drule (1) semilatDorderI [THEN acc_le_listI])
+ apply (insert orderI [THEN acc_le_listI])
apply (simp only: acc_def lesssub_def)
apply (rule wf_finite_psubset)
@@ -434,7 +426,7 @@
apply blast
apply (subst decomp_propa)
apply blast
-apply clarify
+apply clarify
apply (simp del: listE_length
add: lex_prod_def finite_psubset_def
bounded_nat_set_is_finite)
@@ -444,11 +436,11 @@
apply assumption
apply clarsimp
apply (blast dest!: boundedD)
-done
+done
-lemma kildall_properties:
- "\<lbrakk> semilat(A,r,f); acc r; pres_type step n A; mono r step n A;
+lemma kildall_properties: includes semilat
+shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
kildall r f step ss0 \<in> list n A \<and>
stables r step (kildall r f step ss0) \<and>
@@ -459,16 +451,14 @@
apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply(simp)
apply (rule iter_properties)
-apply (simp_all add: unstables_def stable_def)
-done
+by (simp_all add: unstables_def stable_def)
+
-lemma is_bcv_kildall:
- "\<lbrakk> semilat(A,r,f); acc r; top r T;
- pres_type step n A; bounded step n;
- mono r step n A \<rbrakk>
+lemma is_bcv_kildall: includes semilat
+shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
\<Longrightarrow> is_bcv r T step n A (kildall r f step)"
apply(unfold is_bcv_def wt_step_def)
-apply(insert kildall_properties[of A])
+apply(insert semilat kildall_properties[of A])
apply(simp add:stables_def)
apply clarify
apply(subgoal_tac "kildall r f step ss \<in> list n A")
@@ -476,9 +466,9 @@
apply (rule iffI)
apply (rule_tac x = "kildall r f step ss" in bexI)
apply (rule conjI)
- apply blast
+ apply (blast)
apply (simp (no_asm_simp))
- apply assumption
+ apply(assumption)
apply clarify
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
apply simp
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Apr 02 13:47:01 2002 +0200
@@ -110,8 +110,8 @@
moreover
have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto
from eosl x map1
- have "\<forall>x \<in> set (?map ss1). x \<le>|r (?sum ss1)"
- by clarify (rule ub1, simp add: Err.sl_def)
+ have "\<forall>x \<in> set (?map ss1). x \<le>|r (?sum ss1)"
+ by clarify (rule semilat.pp_ub1, simp add: Err.sl_def)
with sum have "\<forall>x \<in> set (?map ss1). x \<le>|r (OK s1)" by simp
with less have "\<forall>x \<in> set (?map ss2). x \<le>|r (OK s1)"
apply clarify
@@ -127,7 +127,7 @@
done
moreover
from eosl map1 x have "x \<le>|r (?sum ss1)"
- by - (rule ub2, simp add: Err.sl_def)
+ by - (rule semilat.pp_ub2, simp add: Err.sl_def)
with sum have "x \<le>|r (OK s1)" by simp
moreover {
have "set (?map ss2) \<subseteq> snd`(set ss2)" by auto
@@ -135,7 +135,7 @@
finally have "set (?map ss2) \<subseteq> err (opt A)" . }
ultimately
have "?sum ss2 \<le>|r (OK s1)" using eosl x
- by - (rule lub, simp add: Err.sl_def)
+ by - (rule semilat.pp_lub, simp add: Err.sl_def)
also obtain s2 where sum2: "?sum ss2 = s2" by blast
finally have "s2 \<le>|r (OK s1)" .
with sum2 have "\<exists>s2. ?sum ss2 = s2 \<and> s2 \<le>|r (OK s1)" by blast
@@ -295,7 +295,8 @@
have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"
by (cases "cert!Suc pc") (simp, blast dest: fitsD2)
ultimately
- have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)" by (rule lub)
+ have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"
+ by (rule semilat.pp_lub)
thus ?thesis by auto
qed
ultimately
@@ -386,7 +387,7 @@
have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"
by (cases "cert!Suc pc") (simp, blast dest: fitsD2)
ultimately
- have "?sum \<le>|r OK (phi!Suc pc)" by (rule lub)
+ have "?sum \<le>|r OK (phi!Suc pc)" by (rule semilat.pp_lub)
}
finally show ?thesis .
qed
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Apr 02 13:47:01 2002 +0200
@@ -105,7 +105,7 @@
"err_semilat (A,r,f) \<Longrightarrow> order r"
apply (simp add: Err.sl_def)
apply (rule order_le_err [THEN iffD1])
- apply (rule semilatDorderI)
+ apply (rule semilat.orderI)
apply assumption
done
@@ -175,7 +175,8 @@
also have "\<dots> = ?if ls ?if'"
proof -
from l have "s' \<in> err (opt A)" by simp
- with x semi have "(s' +|f x) \<in> err (opt A)" by (fast intro: closedD)
+ with x semi have "(s' +|f x) \<in> err (opt A)"
+ by (fast intro: semilat.closedI closedD)
with x have "?if' \<in> err (opt A)" by auto
hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
qed
--- a/src/HOL/MicroJava/BV/Listn.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Tue Apr 02 13:47:01 2002 +0200
@@ -283,30 +283,30 @@
done
-lemma plus_list_ub1 [rule_format]:
- "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+lemma (in semilat) plus_list_ub1 [rule_format]:
+ "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
\<Longrightarrow> xs <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
-lemma plus_list_ub2:
- "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+lemma (in semilat) plus_list_ub2:
+ "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
\<Longrightarrow> ys <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
-done
+done
-lemma plus_list_lub [rule_format]:
- "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A
+lemma (in semilat) plus_list_lub [rule_format]:
+shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A
\<longrightarrow> size xs = n & size ys = n \<longrightarrow>
xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
-done
+done
-lemma list_update_incr [rule_format]:
- "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow>
+lemma (in semilat) list_update_incr [rule_format]:
+ "x:A \<Longrightarrow> set xs <= A \<longrightarrow>
(!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
@@ -315,7 +315,7 @@
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp add: nth_Cons split: nat.split)
-done
+done
lemma acc_le_listI [intro!]:
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
@@ -376,22 +376,23 @@
apply (simp add: in_list_Suc_iff)
apply clarify
apply simp
-done
+done
-lemma semilat_Listn_sl:
- "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
+lemma Listn_sl_aux:
+includes semilat shows "semilat (Listn.sl n (A,r,f))"
apply (unfold Listn.sl_def)
-apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm) only: semilat_Def split_conv)
apply (rule conjI)
apply simp
apply (rule conjI)
- apply (simp only: semilatDclosedI closed_listI)
+ apply (simp only: closedI closed_listI)
apply (simp (no_asm) only: list_def)
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
-done
+done
+lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
+ by(simp add: Listn_sl_aux split_tupled_all)
lemma coalesce_in_err_list [rule_format]:
"!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
@@ -443,7 +444,7 @@
apply (erule thin_rl)
apply (erule thin_rl)
apply force
-done
+done
lemma coalesce_eq_OK_ub_D [rule_format]:
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
@@ -500,7 +501,7 @@
apply (simp add: in_list_Suc_iff)
apply clarify
apply (simp add: plussub_def closed_err_lift2_conv)
-done
+done
lemma closed_lift2_sup:
"closed (err A) (lift2 f) \<Longrightarrow>
@@ -515,9 +516,9 @@
apply (unfold Err.sl_def)
apply (simp only: split_conv)
apply (simp (no_asm) only: semilat_Def plussub_def)
-apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
apply (rule conjI)
- apply (drule semilatDorderI)
+ apply (drule semilat.orderI)
apply simp
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
--- a/src/HOL/MicroJava/BV/Product.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Tue Apr 02 13:47:01 2002 +0200
@@ -78,14 +78,14 @@
have plus_le_conv2:
"\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
- by (rule plus_le_conv [THEN iffD1])
+ by (rule semilat.plus_le_conv [THEN iffD1])
case rule_context
thus ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule OK_le_err_OK [THEN iffD2])
- apply (drule semilat_lub)
+ apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
apply assumption
apply assumption
apply simp
@@ -101,7 +101,7 @@
apply simp
apply blast
apply simp
- apply (blast dest: semilatDorderI order_refl)
+ apply (blast dest: semilat.orderI order_refl)
apply blast
apply (erule subst)
apply (unfold semilat_def err_def closed_def)
@@ -115,15 +115,15 @@
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
apply (simp (no_asm) only: semilat_Def)
-apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
simp add: lift2_def split: err.split)
-apply (blast dest: semilatDorderI)
-apply (blast dest: semilatDorderI)
+apply (blast dest: semilat.orderI)
+apply (blast dest: semilat.orderI)
apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
apply simp
apply simp
apply simp
@@ -132,7 +132,7 @@
apply simp
apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
apply simp
apply simp
apply simp
--- a/src/HOL/MicroJava/BV/Semilat.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Tue Apr 02 13:47:01 2002 +0200
@@ -61,8 +61,13 @@
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-"some_lub r x y == SOME z. is_lub r x y z"
+"some_lub r x y == SOME z. is_lub r x y z";
+locale semilat =
+ fixes A :: "'a set"
+ and r :: "'a ord"
+ and f :: "'a binop"
+ assumes semilat: "semilat(A,r,f)"
lemma order_refl [simp, intro]:
"order r \<Longrightarrow> x <=_r x";
@@ -71,7 +76,7 @@
lemma order_antisym:
"\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
apply (unfold order_def)
-apply (simp (no_asm_simp))
+apply (simp (no_asm_simp))
done
lemma order_trans:
@@ -109,48 +114,44 @@
apply (rule refl [THEN eq_reflection])
done
-lemma semilatDorderI [simp, intro]:
- "semilat(A,r,f) \<Longrightarrow> order r"
- by (simp add: semilat_Def)
+lemma (in semilat) orderI [simp, intro]:
+ "order r"
+ by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) closedI [simp, intro]:
+ "closed A f"
+ by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) ub1 [simp]:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
+ by (insert semilat) (unfold semilat_Def, simp)
+
+lemma (in semilat) ub2 [simp]:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
+ by (insert semilat) (unfold semilat_Def, simp)
-lemma semilatDclosedI [simp, intro]:
- "semilat(A,r,f) \<Longrightarrow> closed A f"
-apply (unfold semilat_Def)
+lemma (in semilat) lub [simp]:
+ "\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
+ by (insert semilat) (unfold semilat_Def, simp)
+
+
+lemma (in semilat) plus_le_conv [simp]:
+ "\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+apply (blast intro: ub1 ub2 lub order_trans)
+done
+
+lemma (in semilat) le_iff_plus_unchanged:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
+apply (rule iffI)
+ apply (blast intro: order_antisym lub order_refl ub2);
+apply (erule subst)
apply simp
done
-lemma semilat_ub1 [simp]:
- "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
- by (unfold semilat_Def, simp)
-
-lemma semilat_ub2 [simp]:
- "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
- by (unfold semilat_Def, simp)
-
-lemma semilat_lub [simp]:
- "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
- by (unfold semilat_Def, simp)
-
-
-lemma plus_le_conv [simp]:
- "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk>
- \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
-apply (unfold semilat_Def)
-apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
-done
-
-lemma le_iff_plus_unchanged:
- "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
+lemma (in semilat) le_iff_plus_unchanged2:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
apply (rule iffI)
- apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
-apply (erule subst)
-apply simp
-done
-
-lemma le_iff_plus_unchanged2:
- "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
-apply (rule iffI)
- apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
+ apply (blast intro: order_antisym lub order_refl ub1)
apply (erule subst)
apply simp
done
@@ -160,23 +161,22 @@
"\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
apply (unfold closed_def)
apply blast
-done
+done
lemma closed_UNIV [simp]: "closed UNIV f"
by (simp add: closed_def)
-lemma plus_assoc [simp]:
- assumes semi: "semilat (A,r,f)"
+lemma (in semilat) plus_assoc [simp]:
assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
shows "a +_f (b +_f c) = a +_f b +_f c"
proof -
have order: "order r" ..
note order_trans [OF order,trans]
- note closedD [OF semilatDclosedI [OF semi], intro]
- note semilat_ub1 [OF semi, intro]
- note semilat_ub2 [OF semi, intro]
- note semilat_lub [OF _ _ semi, intro]
+ note closedD [OF closedI, intro]
+ note ub1 [intro]
+ note ub2 [intro]
+ note lub [intro]
from a b have ab: "a +_f b \<in> A" ..
from this c have abc: "(a +_f b) +_f c \<in> A" ..
@@ -186,7 +186,7 @@
from order show ?thesis
proof (rule order_antisym)
show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
- proof -
+ proof -
from a b have "a <=_r a +_f b" ..
also from ab c have "\<dots> <=_r \<dots> +_f c" ..
finally have "a<": "a <=_r (a +_f b) +_f c" .
@@ -212,28 +212,24 @@
qed
qed
-lemma plus_com_lemma:
- "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
+lemma (in semilat) plus_com_lemma:
+ "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
proof -
- assume semi: "semilat (A,r,f)" and a: "a \<in> A" and b: "b \<in> A"
- from semi b a have "a <=_r b +_f a" by (rule semilat_ub2)
+ assume a: "a \<in> A" and b: "b \<in> A"
+ from b a have "a <=_r b +_f a" by (rule ub2)
moreover
- from semi b a have "b <=_r b +_f a" by (rule semilat_ub1)
+ from b a have "b <=_r b +_f a" by (rule ub1)
moreover
- note semi a b
+ note a b
moreover
- from semi b a have "b +_f a \<in> A" by (rule closedD [OF semilatDclosedI])
+ from b a have "b +_f a \<in> A" by (rule closedD [OF closedI])
ultimately
- show ?thesis by (rule semilat_lub)
+ show ?thesis by (rule lub)
qed
-lemma plus_commutative:
- "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
- apply (frule semilatDorderI)
- apply (erule order_antisym)
- apply (rule plus_com_lemma, assumption+)
- apply (rule plus_com_lemma, assumption+)
- done
+lemma (in semilat) plus_commutative:
+ "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
+by(blast intro: order_antisym plus_com_lemma)
lemma is_lubD:
"is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Tue Apr 02 13:47:01 2002 +0200
@@ -62,79 +62,71 @@
done
-lemma plusplus_closed:
- "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
+lemma plusplus_closed: includes semilat shows
+ "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
proof (induct x)
show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
fix y x xs
- assume sl: "semilat (A, r, f)" and y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
- assume IH: "\<And>y. \<lbrakk>semilat (A, r, f); set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
- from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
- from sl x y have "(x +_f y) \<in> A" by (simp add: closedD)
- with sl xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+ assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
+ assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
+ from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
+ from semilat x y have "(x +_f y) \<in> A" by (simp add: closedD)
+ with semilat xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
thus "(x#xs) ++_f y \<in> A" by simp
qed
-lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+lemma (in semilat) pp_ub2:
+ "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
proof (induct x)
- show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp
+ from semilat show "\<And>y. y <=_r [] ++_f y" by simp
fix y a l
- assume sl: "semilat (A, r, f)"
assume y: "y \<in> A"
assume "set (a#l) \<subseteq> A"
- then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
- assume "\<And>y. \<lbrakk>semilat (A, r, f); set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
+ then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
+ assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
- from sl have "order r" .. note order_trans [OF this, trans]
-
- from sl a y have "y <=_r a +_f y" by (rule semilat_ub2)
- also
- from sl a y have "a +_f y \<in> A" by (simp add: closedD)
+ have "order r" .. note order_trans [OF this, trans]
+
+ from a y have "y <=_r a +_f y" by (rule ub2)
+ also from a y have "a +_f y \<in> A" by (simp add: closedD)
hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
- finally
- have "y <=_r l ++_f (a +_f y)" .
+ finally have "y <=_r l ++_f (a +_f y)" .
thus "y <=_r (a#l) ++_f y" by simp
qed
-lemma ub1:
- "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+lemma (in semilat) pp_ub1:
+shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
proof (induct ls)
show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
-
+
fix y s ls
- assume sl: "semilat (A, r, f)"
- hence "order r" .. note order_trans [OF this, trans]
+ have "order r" .. note order_trans [OF this, trans]
assume "set (s#ls) \<subseteq> A"
then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
assume y: "y \<in> A"
assume
- "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+ "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
assume "x \<in> set (s#ls)"
then obtain xls: "x = s \<or> x \<in> set ls" by simp
moreover {
assume xs: "x = s"
- from sl s y have "s <=_r s +_f y" by (rule semilat_ub1)
- also
- from sl s y have "s +_f y \<in> A" by (simp add: closedD)
- with sl ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule ub2)
- finally
- have "s <=_r ls ++_f (s +_f y)" .
+ from s y have "s <=_r s +_f y" by (rule ub1)
+ also from s y have "s +_f y \<in> A" by (simp add: closedD)
+ with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
+ finally have "s <=_r ls ++_f (s +_f y)" .
with xs have "x <=_r ls ++_f (s +_f y)" by simp
}
moreover {
assume "x \<in> set ls"
hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
- moreover
- from sl s y
- have "s +_f y \<in> A" by (simp add: closedD)
- ultimately
- have "x <=_r ls ++_f (s +_f y)" .
+ moreover from s y have "s +_f y \<in> A" by (simp add: closedD)
+ ultimately have "x <=_r ls ++_f (s +_f y)" .
}
ultimately
have "x <=_r ls ++_f (s +_f y)" by blast
@@ -142,8 +134,8 @@
qed
-lemma lub:
- assumes sl: "semilat (A, r, f)" and "z \<in> A"
+lemma (in semilat) pp_lub:
+ assumes "z \<in> A"
shows
"\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z"
proof (induct xs)
@@ -153,25 +145,25 @@
then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
assume "\<forall>x \<in> set (l#ls). x <=_r z"
then obtain "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto
- assume "y <=_r z" have "l +_f y <=_r z" by (rule semilat_lub)
+ assume "y <=_r z" have "l +_f y <=_r z" by (rule lub)
moreover
- from sl l y have "l +_f y \<in> A" by (fast intro: closedD)
+ from l y have "l +_f y \<in> A" by (fast intro: closedD)
moreover
assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z
\<Longrightarrow> ls ++_f y <=_r z"
ultimately
- have "ls ++_f (l +_f y) <=_r z" using ls lsz by - assumption
+ have "ls ++_f (l +_f y) <=_r z" by - (insert ls lsz)
thus "(l#ls) ++_f y <=_r z" by simp
qed
-lemma ub1':
- "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
+lemma ub1': includes semilat
+shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
\<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
proof -
let "b <=_r ?map ++_f y" = ?thesis
- assume "semilat (A, r, f)" "y \<in> A"
+ assume "y \<in> A"
moreover
assume "\<forall>(p,s) \<in> set S. s \<in> A"
hence "set ?map \<subseteq> A" by auto
@@ -179,7 +171,7 @@
assume "(a,b) \<in> set S"
hence "b \<in> set ?map" by (induct S, auto)
ultimately
- show ?thesis by - (rule ub1)
+ show ?thesis by - (rule pp_ub1)
qed