# HG changeset patch # User nipkow # Date 1325177020 -3600 # Node ID 698de142f6f9ff6c99c9cf559d321de1876a133c # Parent 313be214e40a1e4d7866e5b6c59b6745e63e2bd2 tuned diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0.thy --- a/src/HOL/IMP/Abs_Int0.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0.thy Thu Dec 29 17:43:40 2011 +0100 @@ -13,12 +13,12 @@ begin fun aval' :: "aexp \ 'a st \ 'a" where -"aval' (N n) _ = num' n" | +"aval' (N n) S = num' n" | "aval' (V x) S = lookup S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" lemma aval'_sound: "s : \\<^isub>f S \ aval a s : \(aval' a S)" -by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def) +by (induct a) (auto simp: gamma_num' gamma_plus' \_st_def lookup_def) end @@ -46,22 +46,22 @@ text{* Soundness: *} -lemma in_rep_update: +lemma in_gamma_update: "\ s : \\<^isub>f S; i : \ a \ \ s(x := i) : \\<^isub>f(update S x a)" -by(simp add: rep_st_def lookup_update) +by(simp add: \_st_def lookup_update) text{* The soundness proofs are textually identical to the ones for the step function operating on states as functions. *} lemma step_preserves_le2: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ \ step S cs \ \\<^isub>c (step' sa ca)" proof(induction c arbitrary: cs ca S sa) case SKIP thus ?case by(auto simp:strip_eq_SKIP) next case Assign thus ?case - by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update + by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update split: option.splits del:subsetD) next case Semi thus ?case apply (auto simp: strip_eq_Semi) @@ -70,29 +70,29 @@ case (If b c1 c2) then obtain cs1 cs2 ca1 ca2 P Pa where "cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}" - "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" + "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2" by (fastforce simp: strip_eq_If) - moreover have "post cs1 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom) - moreover have "post cs2 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom) + moreover have "post cs1 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) + moreover have "post cs2 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff) next case (While b c1) then obtain cs1 ca1 I P Ia Pa where "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}" - "I \ \\<^isub>u Ia" "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" + "I \ \\<^isub>o Ia" "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "strip cs1 = c1" "strip ca1 = c1" by (fastforce simp: strip_eq_While) - moreover have "S \ post cs1 \ \\<^isub>u (sa \ post ca1)" - using `S \ \\<^isub>u sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans) + moreover have "S \ post cs1 \ \\<^isub>o (sa \ post ca1)" + using `S \ \\<^isub>o sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] + by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) ultimately show ?case by (simp add: While.IH subset_iff) qed lemma step_preserves_le: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c \ \ step S cs \ \\<^isub>c(step' sa ca)" by (metis le_strip step_preserves_le2 strip_acom) @@ -106,12 +106,12 @@ proof(rule lfp_lowerbound[simplified,OF 3]) show "step UNIV (\\<^isub>c (step' \ c')) \ \\<^isub>c (step' \ c')" proof(rule step_preserves_le[OF _ _ 3]) - show "UNIV \ \\<^isub>u \" by simp - show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_rep_c[OF 2]) + show "UNIV \ \\<^isub>o \" by simp + show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_gamma_c[OF 2]) qed qed from this 2 show "lfp c (step UNIV) \ \\<^isub>c c'" - by (blast intro: mono_rep_c order_trans) + by (blast intro: mono_gamma_c order_trans) qed end diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0_const.thy --- a/src/HOL/IMP/Abs_Int0_const.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0_const.thy Thu Dec 29 17:43:40 2011 +0100 @@ -8,9 +8,9 @@ datatype cval = Const val | Any -fun rep_cval where -"rep_cval (Const n) = {n}" | -"rep_cval (Any) = UNIV" +fun \_cval where +"\_cval (Const n) = {n}" | +"\_cval (Any) = UNIV" fun plus_cval where "plus_cval (Const m) (Const n) = Const(m+n)" | @@ -52,7 +52,7 @@ end -interpretation Val_abs rep_cval Const plus_cval +interpretation Val_abs \_cval Const plus_cval defines aval'_const is aval' proof case goal1 thus ?case @@ -66,7 +66,7 @@ by(auto simp: plus_cval_cases split: cval.split) qed -interpretation Abs_Int rep_cval Const plus_cval +interpretation Abs_Int \_cval Const plus_cval defines AI_const is AI and step_const is step' proof qed @@ -74,7 +74,7 @@ text{* Monotonicity: *} -interpretation Abs_Int_mono rep_cval Const plus_cval +interpretation Abs_Int_mono \_cval Const plus_cval proof case goal1 thus ?case by(auto simp: plus_cval_cases split: cval.split) diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int0_fun.thy --- a/src/HOL/IMP/Abs_Int0_fun.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Dec 29 17:43:40 2011 +0100 @@ -132,7 +132,7 @@ "None \ y = y" | "x \ None = x" -lemma [simp]: "x \ None = x" +lemma join_None2[simp]: "x \ None = x" by (cases x) simp_all definition "\ = Some \" @@ -224,23 +224,23 @@ subsection "Abstract Interpretation" -definition rep_fun :: "('a \ 'b set) \ ('c \ 'a) \ ('c \ 'b)set" where -"rep_fun rep F = {f. \x. f x \ rep(F x)}" +definition \_fun :: "('a \ 'b set) \ ('c \ 'a) \ ('c \ 'b)set" where +"\_fun \ F = {f. \x. f x \ \(F x)}" -fun rep_option :: "('a \ 'b set) \ 'a option \ 'b set" where -"rep_option rep None = {}" | -"rep_option rep (Some a) = rep a" +fun \_option :: "('a \ 'b set) \ 'a option \ 'b set" where +"\_option \ None = {}" | +"\_option \ (Some a) = \ a" text{* The interface for abstract values: *} locale Val_abs = -fixes rep :: "'a::SL_top \ val set" ("\") - assumes mono_rep: "a \ b \ \ a \ \ b" - and rep_Top[simp]: "\ \ = UNIV" +fixes \ :: "'a::SL_top \ val set" + assumes mono_gamma: "a \ b \ \ a \ \ b" + and gamma_Top[simp]: "\ \ = UNIV" fixes num' :: "val \ 'a" and plus' :: "'a \ 'a \ 'a" - assumes rep_num': "n : \(num' n)" - and rep_plus': + assumes gamma_num': "n : \(num' n)" + and gamma_plus': "n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \(plus' a1 a2)" type_synonym 'a st = "(vname \ 'a)" @@ -249,7 +249,7 @@ begin fun aval' :: "aexp \ 'a st \ 'a" where -"aval' (N n) _ = num' n" | +"aval' (N n) S = num' n" | "aval' (V x) S = S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" @@ -272,51 +272,51 @@ by(induct c arbitrary: S) (simp_all add: Let_def) -abbreviation rep_f :: "'a st \ state set" ("\\<^isub>f") -where "\\<^isub>f == rep_fun \" +abbreviation \\<^isub>f :: "'a st \ state set" +where "\\<^isub>f == \_fun \" -abbreviation rep_u :: "'a st option \ state set" ("\\<^isub>u") -where "\\<^isub>u == rep_option \\<^isub>f" +abbreviation \\<^isub>o :: "'a st option \ state set" +where "\\<^isub>o == \_option \\<^isub>f" -abbreviation rep_c :: "'a st option acom \ state set acom" ("\\<^isub>c") -where "\\<^isub>c == map_acom \\<^isub>u" +abbreviation \\<^isub>c :: "'a st option acom \ state set acom" +where "\\<^isub>c == map_acom \\<^isub>o" -lemma rep_f_Top[simp]: "\\<^isub>f Top = UNIV" -by(simp add: Top_fun_def rep_fun_def) +lemma gamma_f_Top[simp]: "\\<^isub>f Top = UNIV" +by(simp add: Top_fun_def \_fun_def) -lemma rep_u_Top[simp]: "\\<^isub>u Top = UNIV" +lemma gamma_o_Top[simp]: "\\<^isub>o Top = UNIV" by (simp add: Top_option_def) (* FIXME (maybe also le \ sqle?) *) -lemma mono_rep_f: "f \ g \ \\<^isub>f f \ \\<^isub>f g" -by(auto simp: le_fun_def rep_fun_def dest: mono_rep) +lemma mono_gamma_f: "f \ g \ \\<^isub>f f \ \\<^isub>f g" +by(auto simp: le_fun_def \_fun_def dest: mono_gamma) -lemma mono_rep_u: - "sa \ sa' \ \\<^isub>u sa \ \\<^isub>u sa'" -by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f) +lemma mono_gamma_o: + "sa \ sa' \ \\<^isub>o sa \ \\<^isub>o sa'" +by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) -lemma mono_rep_c: "ca \ ca' \ \\<^isub>c ca \ \\<^isub>c ca'" -by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u) +lemma mono_gamma_c: "ca \ ca' \ \\<^isub>c ca \ \\<^isub>c ca'" +by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) text{* Soundness: *} lemma aval'_sound: "s : \\<^isub>f S \ aval a s : \(aval' a S)" -by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def) +by (induct a) (auto simp: gamma_num' gamma_plus' \_fun_def) -lemma in_rep_update: +lemma in_gamma_update: "\ s : \\<^isub>f S; i : \ a \ \ s(x := i) : \\<^isub>f(S(x := a))" -by(simp add: rep_fun_def) +by(simp add: \_fun_def) lemma step_preserves_le2: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ \ step S cs \ \\<^isub>c (step' sa ca)" proof(induction c arbitrary: cs ca S sa) case SKIP thus ?case by(auto simp:strip_eq_SKIP) next case Assign thus ?case - by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update + by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update split: option.splits del:subsetD) next case Semi thus ?case apply (auto simp: strip_eq_Semi) @@ -325,29 +325,29 @@ case (If b c1 c2) then obtain cs1 cs2 ca1 ca2 P Pa where "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}" - "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" + "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2" by (fastforce simp: strip_eq_If) - moreover have "post cs1 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom) - moreover have "post cs2 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom) - ultimately show ?case using `S \ \\<^isub>u sa` by (simp add: If.IH subset_iff) + moreover have "post cs1 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) + moreover have "post cs2 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) + ultimately show ?case using `S \ \\<^isub>o sa` by (simp add: If.IH subset_iff) next case (While b c1) then obtain cs1 ca1 I P Ia Pa where "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}" - "I \ \\<^isub>u Ia" "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" + "I \ \\<^isub>o Ia" "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "strip cs1 = c1" "strip ca1 = c1" by (fastforce simp: strip_eq_While) - moreover have "S \ post cs1 \ \\<^isub>u (sa \ post ca1)" - using `S \ \\<^isub>u sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans) + moreover have "S \ post cs1 \ \\<^isub>o (sa \ post ca1)" + using `S \ \\<^isub>o sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] + by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) ultimately show ?case by (simp add: While.IH subset_iff) qed lemma step_preserves_le: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c \ \ step S cs \ \\<^isub>c(step' sa ca)" by (metis le_strip step_preserves_le2 strip_acom) @@ -361,12 +361,12 @@ proof(rule lfp_lowerbound[simplified,OF 3]) show "step UNIV (\\<^isub>c (step' \ c')) \ \\<^isub>c (step' \ c')" proof(rule step_preserves_le[OF _ _ 3]) - show "UNIV \ \\<^isub>u \" by simp - show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_rep_c[OF 2]) + show "UNIV \ \\<^isub>o \" by simp + show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_gamma_c[OF 2]) qed qed from this 2 show "lfp c (step UNIV) \ \\<^isub>c c'" - by (blast intro: mono_rep_c order_trans) + by (blast intro: mono_gamma_c order_trans) qed end diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int1.thy --- a/src/HOL/IMP/Abs_Int1.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Thu Dec 29 17:43:40 2011 +0100 @@ -37,24 +37,24 @@ end -locale Val_abs1_rep = - Val_abs rep num' plus' - for rep :: "'a::L_top_bot \ val set" ("\") and num' plus' + -assumes inter_rep_subset_rep_meet: - "rep a1 \ rep a2 \ rep(a1 \ a2)" -and rep_Bot[simp]: "rep \ = {}" +locale Val_abs1_gamma = + Val_abs \ num' plus' + for \ :: "'a::L_top_bot \ val set" and num' plus' + +assumes inter_gamma_subset_gamma_meet: + "\ a1 \ \ a2 \ \(a1 \ a2)" +and gamma_Bot[simp]: "\ \ = {}" begin -lemma in_rep_meet: "x : \ a1 \ x : \ a2 \ x : \(a1 \ a2)" -by (metis IntI inter_rep_subset_rep_meet set_mp) +lemma in_gamma_meet: "x : \ a1 \ x : \ a2 \ x : \(a1 \ a2)" +by (metis IntI inter_gamma_subset_gamma_meet set_mp) -lemma rep_meet[simp]: "\(a1 \ a2) = \ a1 \ \ a2" -by (metis equalityI inter_rep_subset_rep_meet le_inf_iff mono_rep meet_le1 meet_le2) +lemma gamma_meet[simp]: "\(a1 \ a2) = \ a1 \ \ a2" +by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2) end -locale Val_abs1 = Val_abs1_rep + +locale Val_abs1 = Val_abs1_gamma + fixes filter_plus' :: "'a \ 'a \ 'a \ 'a * 'a" and filter_less' :: "bool \ 'a \ 'a \ 'a * 'a" assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \ @@ -66,14 +66,14 @@ locale Abs_Int1 = Val_abs1 begin -lemma in_rep_join_UpI: "s : \\<^isub>u S1 | s : \\<^isub>u S2 \ s : \\<^isub>u(S1 \ S2)" -by (metis (no_types) join_ge1 join_ge2 mono_rep_u set_rev_mp) +lemma in_gamma_join_UpI: "s : \\<^isub>o S1 \ s : \\<^isub>o S2 \ s : \\<^isub>o(S1 \ S2)" +by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp) fun aval'' :: "aexp \ 'a st option \ 'a" where "aval'' e None = \" | "aval'' e (Some sa) = aval' e sa" -lemma aval''_sound: "s : \\<^isub>u S \ aval a s : \(aval'' a S)" +lemma aval''_sound: "s : \\<^isub>o S \ aval a s : \(aval'' a S)" by(cases S)(simp add: aval'_sound)+ subsubsection "Backward analysis" @@ -107,31 +107,31 @@ (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S) in afilter e1 res1 (afilter e2 res2 S))" -lemma afilter_sound: "s : \\<^isub>u S \ aval e s : \ a \ s : \\<^isub>u (afilter e a S)" +lemma afilter_sound: "s : \\<^isub>o S \ aval e s : \ a \ s : \\<^isub>o (afilter e a S)" proof(induction e arbitrary: a S) case N thus ?case by simp next case (V x) - obtain S' where "S = Some S'" and "s : \\<^isub>f S'" using `s : \\<^isub>u S` - by(auto simp: in_rep_up_iff) - moreover hence "s x : \ (lookup S' x)" by(simp add: rep_st_def) + obtain S' where "S = Some S'" and "s : \\<^isub>f S'" using `s : \\<^isub>o S` + by(auto simp: in_gamma_option_iff) + moreover hence "s x : \ (lookup S' x)" by(simp add: \_st_def) moreover have "s x : \ a" using V by simp ultimately show ?case using V(1) - by(simp add: lookup_update Let_def rep_st_def) - (metis mono_rep emptyE in_rep_meet rep_Bot subset_empty) + by(simp add: lookup_update Let_def \_st_def) + (metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty) next case (Plus e1 e2) thus ?case using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]] by (auto split: prod.split) qed -lemma bfilter_sound: "s : \\<^isub>u S \ bv = bval b s \ s : \\<^isub>u(bfilter b bv S)" +lemma bfilter_sound: "s : \\<^isub>o S \ bv = bval b s \ s : \\<^isub>o(bfilter b bv S)" proof(induction b arbitrary: S bv) case Bc thus ?case by simp next case (Not b) thus ?case by simp next - case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI) + case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI) next case (Less e1 e2) thus ?case by (auto split: prod.split) @@ -162,20 +162,20 @@ subsubsection "Soundness" -lemma in_rep_update: +lemma in_gamma_update: "\ s : \\<^isub>f S; i : \ a \ \ s(x := i) : \\<^isub>f(update S x a)" -by(simp add: rep_st_def lookup_update) +by(simp add: \_st_def lookup_update) lemma step_preserves_le2: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c; strip ca = c \ \ step S cs \ \\<^isub>c (step' sa ca)" proof(induction c arbitrary: cs ca S sa) case SKIP thus ?case by(auto simp:strip_eq_SKIP) next case Assign thus ?case - by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update + by (fastforce simp: strip_eq_Assign intro: aval'_sound in_gamma_update split: option.splits del:subsetD) next case Semi thus ?case apply (auto simp: strip_eq_Semi) @@ -184,30 +184,30 @@ case (If b c1 c2) then obtain cs1 cs2 ca1 ca2 P Pa where "cs= IF b THEN cs1 ELSE cs2 {P}" "ca= IF b THEN ca1 ELSE ca2 {Pa}" - "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" + "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "cs2 \ \\<^isub>c ca2" "strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2" by (fastforce simp: strip_eq_If) - moreover have "post cs1 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom) - moreover have "post cs2 \ \\<^isub>u(post ca1 \ post ca2)" - by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom) - ultimately show ?case using `S \ \\<^isub>u sa` + moreover have "post cs1 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs1 \ \\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) + moreover have "post cs2 \ \\<^isub>o(post ca1 \ post ca2)" + by (metis (no_types) `cs2 \ \\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) + ultimately show ?case using `S \ \\<^isub>o sa` by (simp add: If.IH subset_iff bfilter_sound) next case (While b c1) then obtain cs1 ca1 I P Ia Pa where "cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}" - "I \ \\<^isub>u Ia" "P \ \\<^isub>u Pa" "cs1 \ \\<^isub>c ca1" + "I \ \\<^isub>o Ia" "P \ \\<^isub>o Pa" "cs1 \ \\<^isub>c ca1" "strip cs1 = c1" "strip ca1 = c1" by (fastforce simp: strip_eq_While) - moreover have "S \ post cs1 \ \\<^isub>u (sa \ post ca1)" - using `S \ \\<^isub>u sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans) + moreover have "S \ post cs1 \ \\<^isub>o (sa \ post ca1)" + using `S \ \\<^isub>o sa` le_post[OF `cs1 \ \\<^isub>c ca1`, simplified] + by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound) qed lemma step_preserves_le: - "\ S \ \\<^isub>u sa; cs \ \\<^isub>c ca; strip cs = c \ + "\ S \ \\<^isub>o sa; cs \ \\<^isub>c ca; strip cs = c \ \ step S cs \ \\<^isub>c(step' sa ca)" by (metis le_strip step_preserves_le2 strip_acom) @@ -221,12 +221,12 @@ proof(rule lfp_lowerbound[simplified,OF 3]) show "step UNIV (\\<^isub>c (step' \ c')) \ \\<^isub>c (step' \ c')" proof(rule step_preserves_le[OF _ _ 3]) - show "UNIV \ \\<^isub>u \" by simp - show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_rep_c[OF 2]) + show "UNIV \ \\<^isub>o \" by simp + show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_gamma_c[OF 2]) qed qed from this 2 show "lfp c (step UNIV) \ \\<^isub>c c'" - by (blast intro: mono_rep_c order_trans) + by (blast intro: mono_gamma_c order_trans) qed end @@ -255,7 +255,7 @@ lemma mono_afilter: "r \ r' \ S \ S' \ afilter e r S \ afilter e r' S'" apply(induction e arbitrary: r r' S S') apply(auto simp: Let_def split: option.splits prod.splits) -apply (metis mono_rep subsetD) +apply (metis mono_gamma subsetD) apply(drule_tac x = "list" in mono_lookup) apply (metis mono_meet le_trans) apply (metis mono_meet mono_lookup mono_update) diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int1_ivl.thy --- a/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy Thu Dec 29 17:43:40 2011 +0100 @@ -8,7 +8,7 @@ datatype ivl = I "int option" "int option" -definition "rep_ivl i = (case i of +definition "\_ivl i = (case i of I (Some l) (Some h) \ {l..h} | I (Some l) None \ {l..} | I None (Some h) \ {..h} | @@ -26,14 +26,14 @@ definition "num_ivl n = {n\n}" definition - [code_abbrev]: "contained_in i k \ k \ rep_ivl i" + [code_abbrev]: "contained_in i k \ k \ \_ivl i" lemma contained_in_simps [code]: "contained_in (I (Some l) (Some h)) k \ l \ k \ k \ h" "contained_in (I (Some l) None) k \ l \ k" "contained_in (I None (Some h)) k \ k \ h" "contained_in (I None None) k \ True" - by (simp_all add: contained_in_def rep_ivl_def) + by (simp_all add: contained_in_def \_ivl_def) instantiation option :: (plus)plus begin @@ -56,8 +56,8 @@ (case l of Some l \ (case h of Some h \ h False) | None \ False)" by(auto split:option.split) -lemma [simp]: "is_empty i \ rep_ivl i = {}" -by(auto simp add: rep_ivl_def split: ivl.split option.split) +lemma [simp]: "is_empty i \ \_ivl i = {}" +by(auto simp add: \_ivl_def split: ivl.split option.split) definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else case (i1,i2) of (I l1 h1, I l2 h2) \ I (l1+l2) (h1+h2))" @@ -154,9 +154,9 @@ definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else case (i1,i2) of (I l1 h1, I l2 h2) \ I (l1-h2) (h1-l2))" -lemma rep_minus_ivl: - "n1 : rep_ivl i1 \ n2 : rep_ivl i2 \ n1-n2 : rep_ivl(minus_ivl i1 i2)" -by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits) +lemma gamma_minus_ivl: + "n1 : \_ivl i1 \ n2 : \_ivl i2 \ n1-n2 : \_ivl(minus_ivl i1 i2)" +by(auto simp add: minus_ivl_def \_ivl_def split: ivl.splits option.splits) definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*) @@ -170,26 +170,26 @@ I (max_option False (l1 + Some 1) l2) h2) else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" -interpretation Val_abs rep_ivl num_ivl plus_ivl +interpretation Val_abs \_ivl num_ivl plus_ivl defines aval_ivl is aval' proof case goal1 thus ?case - by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) + by(auto simp: \_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) next - case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def) + case goal2 show ?case by(simp add: \_ivl_def Top_ivl_def) next - case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def) + case goal3 thus ?case by(simp add: \_ivl_def num_ivl_def) next case goal4 thus ?case - by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits) + by(auto simp add: \_ivl_def plus_ivl_def split: ivl.split option.splits) qed -interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl +interpretation Val_abs1_gamma \_ivl num_ivl plus_ivl proof case goal1 thus ?case - by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) + by(auto simp add: \_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) next - case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def) + case goal2 show ?case by(auto simp add: bot_ivl_def \_ivl_def empty_def) qed lemma mono_minus_ivl: @@ -202,19 +202,19 @@ interpretation - Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl + Val_abs1 \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl proof case goal1 thus ?case by(auto simp add: filter_plus_ivl_def) - (metis rep_minus_ivl add_diff_cancel add_commute)+ + (metis gamma_minus_ivl add_diff_cancel add_commute)+ next case goal2 thus ?case by(cases a1, cases a2, - auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) + auto simp: \_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) qed interpretation - Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl + Abs_Int1 \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl defines afilter_ivl is afilter and bfilter_ivl is bfilter and step_ivl is step' @@ -226,7 +226,7 @@ text{* Monotonicity: *} interpretation - Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl + Abs_Int1_mono \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl proof case goal1 thus ?case by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits) diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_Int2.thy --- a/src/HOL/IMP/Abs_Int2.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_Int2.thy Thu Dec 29 17:43:40 2011 +0100 @@ -180,7 +180,7 @@ apply(auto simp add: pfp_WN_def prefp_def split: option.splits) by (metis (no_types) strip_lpfpc strip_map2_acom strip_while) -locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \ val set" +locale Abs_Int2 = Abs_Int1_mono \ for \ :: "'a::{WN,L_top_bot} \ val set" begin definition AI_WN :: "com \ 'a st option acom option" where @@ -196,18 +196,18 @@ proof(rule lfp_lowerbound[simplified,OF 3]) show "step UNIV (\\<^isub>c (step' \ c')) \ \\<^isub>c (step' \ c')" proof(rule step_preserves_le[OF _ _ 3]) - show "UNIV \ \\<^isub>u \" by simp - show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_rep_c[OF 2]) + show "UNIV \ \\<^isub>o \" by simp + show "\\<^isub>c (step' \ c') \ \\<^isub>c c'" by(rule mono_gamma_c[OF 2]) qed qed from this 2 show "lfp c (step UNIV) \ \\<^isub>c c'" - by (blast intro: mono_rep_c order_trans) + by (blast intro: mono_gamma_c order_trans) qed end interpretation - Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl + Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \_ivl defines AI_ivl' is AI_WN proof qed diff -r 313be214e40a -r 698de142f6f9 src/HOL/IMP/Abs_State.thy --- a/src/HOL/IMP/Abs_State.thy Thu Dec 29 14:44:44 2011 +0100 +++ b/src/HOL/IMP/Abs_State.thy Thu Dec 29 17:43:40 2011 +0100 @@ -30,7 +30,7 @@ lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" by(rule ext)(auto simp: lookup_def update_def) -definition "rep_st rep F = {f. \x. f x \ rep(lookup F x)}" +definition "\_st \ F = {f. \x. f x \ \(lookup F x)}" instantiation st :: (SL_top) SL_top begin @@ -61,35 +61,36 @@ context Val_abs begin -abbreviation rep_f :: "'a st \ state set" ("\\<^isub>f") -where "\\<^isub>f == rep_st rep" +abbreviation \\<^isub>f :: "'a st \ state set" +where "\\<^isub>f == \_st \" -abbreviation rep_u :: "'a st option \ state set" ("\\<^isub>u") -where "\\<^isub>u == rep_option \\<^isub>f" +abbreviation \\<^isub>o :: "'a st option \ state set" +where "\\<^isub>o == \_option \\<^isub>f" -abbreviation rep_c :: "'a st option acom \ state set acom" ("\\<^isub>c") -where "\\<^isub>c == map_acom \\<^isub>u" +abbreviation \\<^isub>c :: "'a st option acom \ state set acom" +where "\\<^isub>c == map_acom \\<^isub>o" -lemma rep_f_Top[simp]: "rep_f Top = UNIV" -by(auto simp: Top_st_def rep_st_def lookup_def) +lemma gamma_f_Top[simp]: "\\<^isub>f Top = UNIV" +by(auto simp: Top_st_def \_st_def lookup_def) -lemma rep_u_Top[simp]: "rep_u Top = UNIV" +lemma gamma_o_Top[simp]: "\\<^isub>o Top = UNIV" by (simp add: Top_option_def) (* FIXME (maybe also le \ sqle?) *) -lemma mono_rep_f: "f \ g \ \\<^isub>f f \ \\<^isub>f g" -apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits) -by (metis UNIV_I mono_rep rep_Top subsetD) +lemma mono_gamma_f: "f \ g \ \\<^isub>f f \ \\<^isub>f g" +apply(simp add:\_st_def subset_iff lookup_def le_st_def split: if_splits) +by (metis UNIV_I mono_gamma gamma_Top subsetD) -lemma mono_rep_u: - "sa \ sa' \ \\<^isub>u sa \ \\<^isub>u sa'" -by(induction sa sa' rule: le_option.induct)(simp_all add: mono_rep_f) +lemma mono_gamma_o: + "sa \ sa' \ \\<^isub>o sa \ \\<^isub>o sa'" +by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) -lemma mono_rep_c: "ca \ ca' \ \\<^isub>c ca \ \\<^isub>c ca'" -by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_rep_u) +lemma mono_gamma_c: "ca \ ca' \ \\<^isub>c ca \ \\<^isub>c ca'" +by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) -lemma in_rep_up_iff: "x : rep_option r u \ (\u'. u = Some u' \ x : r u')" +lemma in_gamma_option_iff: + "x : \_option r u \ (\u'. u = Some u' \ x : r u')" by (cases u) auto end