--- a/src/HOL/IMPP/Com.ML Wed Jun 07 01:06:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* $Id$ *)
-
-val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
-
-Goalw [body_def] "finite (dom body)";
-by (rtac (thm"finite_dom_map_of") 1);
-qed "finite_dom_body";
-
-Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
-by (dtac (thm"map_of_SomeD") 1);
-by (Fast_tac 1);
-qed "WT_bodiesD";
-
-AddSEs WTs_elim_cases;
--- a/src/HOL/IMPP/Com.thy Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/Com.thy Wed Jun 07 01:51:22 2006 +0200
@@ -85,6 +85,20 @@
WT_bodies :: bool
"WT_bodies == !(pn,b):set bodies. WT b"
-ML {* use_legacy_bindings (the_context ()) *}
+
+ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *}
+
+lemma finite_dom_body: "finite (dom body)"
+apply (unfold body_def)
+apply (rule finite_dom_map_of)
+done
+
+lemma WT_bodiesD: "[| WT_bodies; body pn = Some b |] ==> WT b"
+apply (unfold WT_bodies_def body_def)
+apply (drule map_of_SomeD)
+apply fast
+done
+
+declare WTs_elim_cases [elim!]
end
--- a/src/HOL/IMPP/EvenOdd.ML Wed Jun 07 01:06:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Title: HOL/IMPP/EvenOdd.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TUM
-*)
-
-section "even";
-
-Goalw [even_def] "even 0";
-by (Simp_tac 1);
-qed "even_0";
-Addsimps [even_0];
-
-Goalw [even_def] "even (Suc 0) = False";
-by (Simp_tac 1);
-qed "not_even_1";
-Addsimps [not_even_1];
-
-Goalw [even_def] "even (Suc (Suc n)) = even n";
-by (subgoal_tac "Suc (Suc n) = n+2" 1);
-by (Simp_tac 2);
-by (etac ssubst 1);
-by (rtac dvd_reduce 1);
-qed "even_step";
-Addsimps[even_step];
-
-
-section "Arg, Res";
-
-Addsimps[Arg_neq_Res,Arg_neq_Res RS not_sym];
-Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym];
-
-Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)";
-by (rtac refl 1);
-qed "Z_eq_Arg_plus_def2";
-
-Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))";
-by (rtac refl 1);
-qed "Res_ok_def2";
-
-val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]);
-
-Goalw [body_def, bodies_def] "body Odd = Some odd";
-by Auto_tac;
-qed "body_Odd";
-Goalw [body_def, bodies_def] "body Even = Some evn";
-by Auto_tac;
-qed "body_Even";
-Addsimps[body_Odd, body_Even];
-
-section "verification";
-
-Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}";
-by (rtac hoare_derivs.If 1);
-by (rtac (hoare_derivs.Ass RS conseq1) 1);
-by (clarsimp_tac Arg_Res_css 1);
-by (rtac export_s 1);
-by (rtac (hoare_derivs.Call RS conseq1) 1);
-by (res_inst_tac [("P","Z=Arg+Suc (Suc 0)")] conseq12 1);
-by (rtac single_asm 1);
-by (auto_tac Arg_Res_css);
-qed "Odd_lemma";
-
-Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}";
-by (rtac hoare_derivs.If 1);
-by (rtac (hoare_derivs.Ass RS conseq1) 1);
-by (clarsimp_tac Arg_Res_css 1);
-by (rtac hoare_derivs.Comp 1);
-by (rtac hoare_derivs.Ass 2);
-by (Clarsimp_tac 1);
-by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
-by (rtac export_s 1);
-by (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
- ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
-by (rtac (single_asm RS conseq2) 1);
-by (clarsimp_tac Arg_Res_css 1);
-by (force_tac Arg_Res_css 1);
-by (rtac export_s 1);
-by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
- ("Q1","%Z s. even Z = (s<Arg> = 0)")]
- (Call_invariant RS conseq12) 1);
-by (rtac (single_asm RS conseq2) 1);
-by (clarsimp_tac Arg_Res_css 1);
-by (force_tac Arg_Res_css 1);
-qed "Even_lemma";
-
-
-Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
-by (rtac BodyN 1);
-by (Simp_tac 1);
-by (rtac (Even_lemma RS hoare_derivs.cut) 1);
-by (rtac BodyN 1);
-by (Simp_tac 1);
-by (rtac (Odd_lemma RS thin) 1);
-by (Simp_tac 1);
-qed "Even_ok_N";
-
-Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
-by (rtac conseq1 1);
-by (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
- ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
- ("Q","%pn. Res_ok")] Body1 1);
-by Auto_tac;
-by (rtac hoare_derivs.insert 1);
-by (rtac (Odd_lemma RS thin) 1);
-by (Simp_tac 1);
-by (rtac (Even_lemma RS thin) 1);
-by (Simp_tac 1);
-qed "Even_ok_S";
--- a/src/HOL/IMPP/EvenOdd.thy Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy Wed Jun 07 01:51:22 2006 +0200
@@ -43,6 +43,112 @@
Z_eq_Arg_plus_def: "Z=Arg+n == %Z s. Z = s<Arg>+n"
Res_ok_def: "Res_ok == %Z s. even Z = (s<Res> = 0)"
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection "even"
+
+lemma even_0 [simp]: "even 0"
+apply (unfold even_def)
+apply simp
+done
+
+lemma not_even_1 [simp]: "even (Suc 0) = False"
+apply (unfold even_def)
+apply simp
+done
+
+lemma even_step [simp]: "even (Suc (Suc n)) = even n"
+apply (unfold even_def)
+apply (subgoal_tac "Suc (Suc n) = n+2")
+prefer 2
+apply simp
+apply (erule ssubst)
+apply (rule dvd_reduce)
+done
+
+
+subsection "Arg, Res"
+
+declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
+declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
+
+lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
+apply (unfold Z_eq_Arg_plus_def)
+apply (rule refl)
+done
+
+lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
+apply (unfold Res_ok_def)
+apply (rule refl)
+done
+
+lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
+
+lemma body_Odd [simp]: "body Odd = Some odd"
+apply (unfold body_def bodies_def)
+apply auto
+done
+
+lemma body_Even [simp]: "body Even = Some evn"
+apply (unfold body_def bodies_def)
+apply auto
+done
+
+
+subsection "verification"
+
+lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
+apply (unfold odd_def)
+apply (rule hoare_derivs.If)
+apply (rule hoare_derivs.Ass [THEN conseq1])
+apply (clarsimp simp: Arg_Res_simps)
+apply (rule export_s)
+apply (rule hoare_derivs.Call [THEN conseq1])
+apply (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
+apply (rule single_asm)
+apply (auto simp: Arg_Res_simps)
+done
+
+lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
+apply (unfold evn_def)
+apply (rule hoare_derivs.If)
+apply (rule hoare_derivs.Ass [THEN conseq1])
+apply (clarsimp simp: Arg_Res_simps)
+apply (rule hoare_derivs.Comp)
+apply (rule_tac [2] hoare_derivs.Ass)
+apply clarsimp
+apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp)
+apply (rule export_s)
+apply (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
+apply (rule single_asm [THEN conseq2])
+apply (clarsimp simp: Arg_Res_simps)
+apply (force simp: Arg_Res_simps)
+apply (rule export_s)
+apply (rule_tac I1 = "%Z l. even Z = (l Res = 0) " and Q1 = "%Z s. even Z = (s<Arg> = 0) " in Call_invariant [THEN conseq12])
+apply (rule single_asm [THEN conseq2])
+apply (clarsimp simp: Arg_Res_simps)
+apply (force simp: Arg_Res_simps)
+done
+
+
+lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
+apply (rule BodyN)
+apply (simp (no_asm))
+apply (rule Even_lemma [THEN hoare_derivs.cut])
+apply (rule BodyN)
+apply (simp (no_asm))
+apply (rule Odd_lemma [THEN thin])
+apply (simp (no_asm))
+done
+
+lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
+apply (rule conseq1)
+apply (rule_tac Procs = "{Odd, Even}" and pn = "Even" and P = "%pn. Z=Arg+ (if pn = Odd then 1 else 0) " and Q = "%pn. Res_ok" in Body1)
+apply auto
+apply (rule hoare_derivs.insert)
+apply (rule Odd_lemma [THEN thin])
+apply (simp (no_asm))
+apply (rule Even_lemma [THEN thin])
+apply (simp (no_asm))
+done
end
--- a/src/HOL/IMPP/Hoare.ML Wed Jun 07 01:06:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(* Title: HOL/IMPP/Hoare.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TUM
-
-Soundness and relative completeness of Hoare rules wrt operational semantics
-*)
-
-Goalw [state_not_singleton_def]
- "state_not_singleton ==> !t. (!s::state. s = t) --> False";
-by (Clarify_tac 1);
-by (case_tac "ta = t" 1);
-by (ALLGOALS (blast_tac (HOL_cs addDs [not_sym])));
-qed "single_stateE";
-
-Addsimps[peek_and_def];
-
-
-section "validity";
-
-Goalw [triple_valid_def]
- "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
-by Auto_tac;
-qed "triple_valid_def2";
-
-Goal "|=0:{P}. BODY pn .{Q}";
-by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
-by (Clarsimp_tac 1);
-qed "Body_triple_valid_0";
-
-(* only ==> direction required *)
-Goal "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}";
-by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
-by (Force_tac 1);
-qed "Body_triple_valid_Suc";
-
-Goalw [triple_valid_def] "|=Suc n:t --> |=n:t";
-by (induct_tac "t" 1);
-by (Simp_tac 1);
-by (fast_tac (claset() addIs [evaln_Suc]) 1);
-qed_spec_mp "triple_valid_Suc";
-
-Goal "||=Suc n:ts ==> ||=n:ts";
-by (fast_tac (claset() addIs [triple_valid_Suc]) 1);
-qed "triples_valid_Suc";
-
-
-section "derived rules";
-
-Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \
-\ (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \
-\ ==> G|-{P}.c.{Q}";
-by (rtac hoare_derivs.conseq 1);
-by (Blast_tac 1);
-qed "conseq12";
-
-Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}";
-by (etac conseq12 1);
-by (Fast_tac 1);
-qed "conseq1";
-
-Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}";
-by (etac conseq12 1);
-by (Fast_tac 1);
-qed "conseq2";
-
-Goal "[| G Un (%p. {P p}. BODY p .{Q p})`Procs \
-\ ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
-\ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
-by (dtac hoare_derivs.Body 1);
-by (etac hoare_derivs.weaken 1);
-by (Fast_tac 1);
-qed "Body1";
-
-Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> \
-\ G|-{P}. BODY pn .{Q}";
-by (rtac Body1 1);
-by (rtac singletonI 2);
-by (Clarsimp_tac 1);
-qed "BodyN";
-
-Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}";
-by (rtac hoare_derivs.conseq 1);
-by (Fast_tac 1);
-qed "escape";
-
-Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}";
-by (rtac hoare_derivs.conseq 1);
-by (fast_tac (claset() addDs (premises())) 1);
-qed "constant";
-
-Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}";
-by (rtac (hoare_derivs.Loop RS conseq2) 1);
-by (ALLGOALS Simp_tac);
-by (rtac hoare_derivs.conseq 1);
-by (Fast_tac 1);
-qed "LoopF";
-
-(*
-Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
-by (etac hoare_derivs.cut 1);
-by (etac hoare_derivs.asm 1);
-qed "thin";
-*)
-Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
-by (etac hoare_derivs.induct 1);
-by (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
-by (rtac hoare_derivs.empty 1);
-by (eatac hoare_derivs.insert 1 1);
-by (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
-by (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
-by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
-by (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
- smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
-by (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7);
-by (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intros)
- THEN_ALL_NEW Fast_tac));
-qed_spec_mp "thin";
-
-Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
-by (rtac BodyN 1);
-by (etac thin 1);
-by Auto_tac;
-qed "weak_Body";
-
-Goal "G||-insert t ts ==> G|-t & G||-ts";
-by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
-qed "derivs_insertD";
-
-Goal "[| finite U; \
-\ !p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> \
-\ G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
-by (etac finite_induct 1);
-by (ALLGOALS Clarsimp_tac);
-by (dtac derivs_insertD 1);
-by (rtac hoare_derivs.insert 1);
-by Auto_tac;
-qed_spec_mp "finite_pointwise";
-
-
-section "soundness";
-
-Goalw [hoare_valids_def]
- "G|={P &> b}. c .{P} ==> \
-\ G|={P}. WHILE b DO c .{P &> (Not o b)}";
-by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
-by (rtac allI 1);
-by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \
-\ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1);
-by (EVERY'[etac thin_rl, Fast_tac] 1);
-by (EVERY'[REPEAT o rtac allI, rtac impI] 1);
-by ((etac evaln.induct THEN_ALL_NEW Simp_tac) 1);
-by (ALLGOALS Fast_tac);
-qed "Loop_sound_lemma";
-
-Goalw [hoare_valids_def]
- "[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs \
-\ ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> \
-\ G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs";
-by (rtac allI 1);
-by (induct_tac "n" 1);
-by (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
-by (Clarsimp_tac 1);
-by (dtac triples_valid_Suc 1);
-by (mp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
-by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1);
-by (fast_tac (claset() addSIs [Body_triple_valid_Suc RS iffD1]) 1);
-qed "Body_sound_lemma";
-
-Goal "G||-ts ==> G||=ts";
-by (etac hoare_derivs.induct 1);
-by (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma]
- THEN_ALL_NEW atac));
-by (rewtac hoare_valids_def);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1); (* asm *)
-by (Blast_tac 1); (* cut *)
-by (Blast_tac 1); (* weaken *)
-by (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs",
- Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
-by (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
-by (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
-by (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
-by (Force_tac 3); (* Call *)
-by (eresolve_tac evaln_elim_cases 2); (* If *)
-by (TRYALL Blast_tac);
-qed "hoare_sound";
-
-
-section "completeness";
-
-(* Both versions *)
-
-(*unused*)
-Goalw [MGT_def] "G|-MGT c ==> \
-\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}";
-by (etac conseq12 1);
-by Auto_tac;
-qed "MGT_alternI";
-
-(* requires com_det *)
-Goalw [MGT_def] "state_not_singleton ==> \
-\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c";
-by (etac conseq12 1);
-by Auto_tac;
-by (case_tac "? t. <c,?s> -c-> t" 1);
-by (fast_tac (claset() addEs [com_det]) 1);
-by (Clarsimp_tac 1);
-by (dtac single_stateE 1);
-by (Blast_tac 1);
-qed "MGT_alternD";
-
-Goalw [MGT_def]
- "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
-by (etac conseq12 1);
-by (clarsimp_tac (claset(), simpset() addsimps
- [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
-qed "MGF_complete";
-
-AddSEs WTs_elim_cases;
-AddIffs [not_None_eq];
-(* requires com_det, escape (i.e. hoare_derivs.conseq) *)
-Goal "state_not_singleton ==> \
-\ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
-by (induct_tac "c" 1);
-by (ALLGOALS Clarsimp_tac);
-by (fast_tac (claset() addIs [(thm"domI")]) 7);
-by (etac MGT_alternD 6);
-by (rewtac MGT_def);
-by (EVERY'[dtac bspec, etac (thm"domI")] 7);
-by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
- [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
- (hoare_derivs.Call RS conseq1), etac conseq12] 7);
-by (ALLGOALS (etac thin_rl));
-by (rtac (hoare_derivs.Skip RS conseq2) 1);
-by (rtac (hoare_derivs.Ass RS conseq1) 2);
-by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac
- [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")]
- (hoare_derivs.Local RS conseq1), etac conseq12] 3);
-by (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
-by ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
-by (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
-by Auto_tac;
-qed_spec_mp "MGF_lemma1";
-
-(* Version: nested single recursion *)
-
-Goal "[| !!G ts. ts <= G ==> P G ts;\
-\ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\
-\ !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \
-\ !!pn. pn : U ==> wt (the (body pn)); \
-\ finite U; uG = mgt_call`U |] ==> \
-\ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})";
-by (cut_facts_tac (premises()) 1);
-by (induct_tac "n" 1);
-by (ALLGOALS Clarsimp_tac);
-by (subgoal_tac "G = mgt_call ` U" 1);
-by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
-by (Asm_full_simp_tac 1);
-by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
-by (rtac ballI 1);
-by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
-by (Fast_tac 1);
-by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
-by (rtac ballI 1);
-by (case_tac "mgt_call pn : G" 1);
-by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
-by (Fast_tac 1);
-by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
-by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]);
-by (eresolve_tac (tl(tl(tl(premises())))) 3);
-by (Fast_tac 1);
-by (dtac finite_subset 1);
-by (etac finite_imageI 1);
-by (Asm_simp_tac 1);
-by (arith_tac 1);
-qed_spec_mp "nesting_lemma";
-
-Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
-\ G|-{=}.BODY pn.{->}";
-by (rtac BodyN 1);
-by (etac conseq2 1);
-by (Force_tac 1);
-qed "MGT_BodyN";
-
-(* requires BodyN, com_det *)
-Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
-by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1);
-by (etac hoare_derivs.asm 1);
-by (etac MGT_BodyN 1);
-by (rtac finite_dom_body 3);
-by (etac MGF_lemma1 1);
-by (assume_tac 2);
-by (Blast_tac 1);
-by (Clarsimp_tac 1);
-by (eatac WT_bodiesD 1 1);
-by (rtac le_refl 3);
-by Auto_tac;
-qed "MGF";
-
-
-(* Version: simultaneous recursion in call rule *)
-
-(* finiteness not really necessary here *)
-Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})`Procs \
-\ ||-(%pn. {=}. the (body pn) .{->})`Procs; \
-\ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs";
-by (rtac hoare_derivs.Body 1);
-by (etac finite_pointwise 1);
-by (assume_tac 2);
-by (Clarify_tac 1);
-by (etac conseq2 1);
-by Auto_tac;
-qed "MGT_Body";
-
-(* requires empty, insert, com_det *)
-Goal "[| state_not_singleton; WT_bodies; \
-\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
-\ (%pn. {=}. BODY pn .{->})`dom body||-F";
-by (ftac finite_subset 1);
-by (rtac (finite_dom_body RS finite_imageI) 1);
-by (rotate_tac 2 1);
-by (make_imp_tac 1);
-by (etac finite_induct 1);
-by (ALLGOALS (clarsimp_tac (
- claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
- simpset() delsimps [range_composition])));
-by (etac MGF_lemma1 1);
-by (fast_tac (claset() addDs [WT_bodiesD]) 2);
-by (Clarsimp_tac 1);
-by (rtac hoare_derivs.asm 1);
-by (fast_tac (claset() addIs [(thm"domI")]) 1);
-qed_spec_mp "MGF_lemma2_simult";
-
-(* requires Body, empty, insert, com_det *)
-Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
-by (rtac MGF_lemma1 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (Clarsimp_tac 1);
-by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
-by (etac hoare_derivs.weaken 1);
-by (fast_tac (claset() addIs [(thm"domI")]) 1);
-by (rtac (finite_dom_body RSN (2,MGT_Body)) 1);
-by (Simp_tac 1);
-by (eatac MGF_lemma2_simult 1 1);
-by (rtac subset_refl 1);
-qed "MGF'";
-
-(* requires Body+empty+insert / BodyN, com_det *)
-bind_thm ("hoare_complete", MGF' RS MGF_complete);
-
-section "unused derived rules";
-
-Goal "G|-{%Z s. False}.c.{Q}";
-by (rtac hoare_derivs.conseq 1);
-by (Fast_tac 1);
-qed "falseE";
-
-Goal "G|-{P}.c.{%Z s. True}";
-by (rtac hoare_derivs.conseq 1);
-by (fast_tac (claset() addSIs [falseE]) 1);
-qed "trueI";
-
-Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \
-\ ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}";
-by (rtac hoare_derivs.conseq 1);
-by (fast_tac (claset() addEs [conseq12]) 1);
-qed "disj"; (* analogue conj non-derivable *)
-
-Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}";
-by (rtac conseq12 1);
-by (rtac hoare_derivs.Skip 1);
-by (Fast_tac 1);
-qed "hoare_SkipI";
-
-
-section "useful derived rules";
-
-Goal "{t}|-t";
-by (rtac hoare_derivs.asm 1);
-by (rtac subset_refl 1);
-qed "single_asm";
-
-Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
-by (rtac hoare_derivs.conseq 1);
-by (Clarsimp_tac 1);
-by (cut_facts_tac (premises()) 1);
-by (Fast_tac 1);
-qed "export_s";
-
-
-Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}";
-by (rtac export_s 1);
-by (rtac hoare_derivs.Local 1);
-by (etac conseq2 1);
-by (etac spec 1);
-qed "weak_Local";
-
-(*
-Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}";
-by (induct_tac "c" 1);
-by Auto_tac;
-by (rtac conseq1 1);
-by (rtac hoare_derivs.Skip 1);
-force 1;
-by (rtac conseq1 1);
-by (rtac hoare_derivs.Ass 1);
-force 1;
-by (defer_tac 1);
-###
-by (rtac hoare_derivs.Comp 1);
-by (dtac spec 2);
-by (dtac spec 2);
-by (assume_tac 2);
-by (etac conseq1 2);
-by (Clarsimp_tac 2);
-force 1;
-*)
--- a/src/HOL/IMPP/Hoare.thy Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/Hoare.thy Wed Jun 07 01:51:22 2006 +0200
@@ -102,6 +102,429 @@
==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
X:=CALL pn(a) .{Q}"
-ML {* use_legacy_bindings (the_context ()) *}
+
+section {* Soundness and relative completeness of Hoare rules wrt operational semantics *}
+
+lemma single_stateE:
+ "state_not_singleton ==> !t. (!s::state. s = t) --> False"
+apply (unfold state_not_singleton_def)
+apply clarify
+apply (case_tac "ta = t")
+apply blast
+apply (blast dest: not_sym)
+done
+
+declare peek_and_def [simp]
+
+
+subsection "validity"
+
+lemma triple_valid_def2:
+ "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))"
+apply (unfold triple_valid_def)
+apply auto
+done
+
+lemma Body_triple_valid_0: "|=0:{P}. BODY pn .{Q}"
+apply (simp (no_asm) add: triple_valid_def2)
+apply clarsimp
+done
+
+(* only ==> direction required *)
+lemma Body_triple_valid_Suc: "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}"
+apply (simp (no_asm) add: triple_valid_def2)
+apply force
+done
+
+lemma triple_valid_Suc [rule_format (no_asm)]: "|=Suc n:t --> |=n:t"
+apply (unfold triple_valid_def)
+apply (induct_tac t)
+apply simp
+apply (fast intro: evaln_Suc)
+done
+
+lemma triples_valid_Suc: "||=Suc n:ts ==> ||=n:ts"
+apply (fast intro: triple_valid_Suc)
+done
+
+
+subsection "derived rules"
+
+lemma conseq12: "[| G|-{P'}.c.{Q'}; !Z s. P Z s -->
+ (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |]
+ ==> G|-{P}.c.{Q}"
+apply (rule hoare_derivs.conseq)
+apply blast
+done
+
+lemma conseq1: "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}"
+apply (erule conseq12)
+apply fast
+done
+
+lemma conseq2: "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}"
+apply (erule conseq12)
+apply fast
+done
+
+lemma Body1: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs
+ ||- (%p. {P p}. the (body p) .{Q p})`Procs;
+ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}"
+apply (drule hoare_derivs.Body)
+apply (erule hoare_derivs.weaken)
+apply fast
+done
+
+lemma BodyN: "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==>
+ G|-{P}. BODY pn .{Q}"
+apply (rule Body1)
+apply (rule_tac [2] singletonI)
+apply clarsimp
+done
+
+lemma escape: "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}"
+apply (rule hoare_derivs.conseq)
+apply fast
+done
+
+lemma constant: "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}"
+apply (rule hoare_derivs.conseq)
+apply fast
+done
+
+lemma LoopF: "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}"
+apply (rule hoare_derivs.Loop [THEN conseq2])
+apply (simp_all (no_asm))
+apply (rule hoare_derivs.conseq)
+apply fast
+done
+
+(*
+Goal "[| G'||-ts; G' <= G |] ==> G||-ts"
+by (etac hoare_derivs.cut 1);
+by (etac hoare_derivs.asm 1);
+qed "thin";
+*)
+lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
+apply (erule hoare_derivs.induct)
+apply (tactic {* ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]) *})
+apply (rule hoare_derivs.empty)
+apply (erule (1) hoare_derivs.insert)
+apply (fast intro: hoare_derivs.asm)
+apply (fast intro: hoare_derivs.cut)
+apply (fast intro: hoare_derivs.weaken)
+apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
+prefer 7
+apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
+done
+
+lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
+apply (rule BodyN)
+apply (erule thin)
+apply auto
+done
+
+lemma derivs_insertD: "G||-insert t ts ==> G|-t & G||-ts"
+apply (fast intro: hoare_derivs.weaken)
+done
+
+lemma finite_pointwise [rule_format (no_asm)]: "[| finite U;
+ !p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==>
+ G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U"
+apply (erule finite_induct)
+apply simp
+apply clarsimp
+apply (drule derivs_insertD)
+apply (rule hoare_derivs.insert)
+apply auto
+done
+
+
+subsection "soundness"
+
+lemma Loop_sound_lemma:
+ "G|={P &> b}. c .{P} ==>
+ G|={P}. WHILE b DO c .{P &> (Not o b)}"
+apply (unfold hoare_valids_def)
+apply (simp (no_asm_use) add: triple_valid_def2)
+apply (rule allI)
+apply (subgoal_tac "!d s s'. <d,s> -n-> s' --> d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s') ")
+apply (erule thin_rl, fast)
+apply ((rule allI)+, rule impI)
+apply (erule evaln.induct)
+apply (simp_all (no_asm))
+apply fast
+apply fast
+done
+
+lemma Body_sound_lemma:
+ "[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs
+ ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==>
+ G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs"
+apply (unfold hoare_valids_def)
+apply (rule allI)
+apply (induct_tac n)
+apply (fast intro: Body_triple_valid_0)
+apply clarsimp
+apply (drule triples_valid_Suc)
+apply (erule (1) notE impE)
+apply (simp add: ball_Un)
+apply (drule spec, erule impE, erule conjI, assumption)
+apply (fast intro!: Body_triple_valid_Suc [THEN iffD1])
+done
+
+lemma hoare_sound: "G||-ts ==> G||=ts"
+apply (erule hoare_derivs.induct)
+apply (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *})
+apply (unfold hoare_valids_def)
+apply blast
+apply blast
+apply (blast) (* asm *)
+apply (blast) (* cut *)
+apply (blast) (* weaken *)
+apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *})
+apply (simp_all (no_asm_use) add: triple_valid_def2)
+apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
+apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
+prefer 3 apply (force) (* Call *)
+apply (erule_tac [2] evaln_elim_cases) (* If *)
+apply blast+
+done
+
+
+section "completeness"
+
+(* Both versions *)
+
+(*unused*)
+lemma MGT_alternI: "G|-MGT c ==>
+ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}"
+apply (unfold MGT_def)
+apply (erule conseq12)
+apply auto
+done
+
+(* requires com_det *)
+lemma MGT_alternD: "state_not_singleton ==>
+ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c"
+apply (unfold MGT_def)
+apply (erule conseq12)
+apply auto
+apply (case_tac "? t. <c,?s> -c-> t")
+apply (fast elim: com_det)
+apply clarsimp
+apply (drule single_stateE)
+apply blast
+done
+
+lemma MGF_complete:
+ "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}"
+apply (unfold MGT_def)
+apply (erule conseq12)
+apply (clarsimp simp add: hoare_valids_def eval_eq triple_valid_def2)
+done
+
+declare WTs_elim_cases [elim!]
+declare not_None_eq [iff]
+(* requires com_det, escape (i.e. hoare_derivs.conseq) *)
+lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
+ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
+apply (induct_tac c)
+apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+prefer 7 apply (fast intro: domI)
+apply (erule_tac [6] MGT_alternD)
+apply (unfold MGT_def)
+apply (drule_tac [7] bspec, erule_tac [7] domI)
+apply (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
+ rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
+apply (erule_tac [!] thin_rl)
+apply (rule hoare_derivs.Skip [THEN conseq2])
+apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
+apply (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
+ rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
+ erule_tac [3] conseq12)
+apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
+apply (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *})
+apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
+apply auto
+done
+
+(* Version: nested single recursion *)
+
+lemma nesting_lemma [rule_format]:
+ assumes "!!G ts. ts <= G ==> P G ts"
+ and "!!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn}"
+ and "!!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}"
+ and "!!pn. pn : U ==> wt (the (body pn))"
+ shows "finite U ==> uG = mgt_call`U ==>
+ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
+apply (induct_tac n)
+apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply (subgoal_tac "G = mgt_call ` U")
+prefer 2
+apply (simp add: card_seteq finite_imageI)
+apply simp
+apply (erule prems(3-)) (*MGF_lemma1*)
+apply (rule ballI)
+apply (rule prems) (*hoare_derivs.asm*)
+apply fast
+apply (erule prems(3-)) (*MGF_lemma1*)
+apply (rule ballI)
+apply (case_tac "mgt_call pn : G")
+apply (rule prems) (*hoare_derivs.asm*)
+apply fast
+apply (rule prems(2-)) (*MGT_BodyN*)
+apply (drule spec, erule impE, erule_tac [2] impE, drule_tac [3] spec, erule_tac [3] mp)
+apply (erule_tac [3] prems(4-))
+apply fast
+apply (drule finite_subset)
+apply (erule finite_imageI)
+apply (simp (no_asm_simp))
+apply arith
+done
+
+lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>
+ G|-{=}.BODY pn.{->}"
+apply (unfold MGT_def)
+apply (rule BodyN)
+apply (erule conseq2)
+apply force
+done
+
+(* requires BodyN, com_det *)
+lemma MGF: "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"
+apply (rule_tac P = "%G ts. G||-ts" and U = "dom body" in nesting_lemma)
+apply (erule hoare_derivs.asm)
+apply (erule MGT_BodyN)
+apply (rule_tac [3] finite_dom_body)
+apply (erule MGF_lemma1)
+prefer 2 apply (assumption)
+apply blast
+apply clarsimp
+apply (erule (1) WT_bodiesD)
+apply (rule_tac [3] le_refl)
+apply auto
+done
+
+
+(* Version: simultaneous recursion in call rule *)
+
+(* finiteness not really necessary here *)
+lemma MGT_Body: "[| G Un (%pn. {=}. BODY pn .{->})`Procs
+ ||-(%pn. {=}. the (body pn) .{->})`Procs;
+ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs"
+apply (unfold MGT_def)
+apply (rule hoare_derivs.Body)
+apply (erule finite_pointwise)
+prefer 2 apply (assumption)
+apply clarify
+apply (erule conseq2)
+apply auto
+done
+
+(* requires empty, insert, com_det *)
+lemma MGF_lemma2_simult [rule_format (no_asm)]: "[| state_not_singleton; WT_bodies;
+ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==>
+ (%pn. {=}. BODY pn .{->})`dom body||-F"
+apply (frule finite_subset)
+apply (rule finite_dom_body [THEN finite_imageI])
+apply (rotate_tac 2)
+apply (tactic "make_imp_tac 1")
+apply (erule finite_induct)
+apply (clarsimp intro!: hoare_derivs.empty)
+apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition)
+apply (erule MGF_lemma1)
+prefer 2 apply (fast dest: WT_bodiesD)
+apply clarsimp
+apply (rule hoare_derivs.asm)
+apply (fast intro: domI)
+done
+
+(* requires Body, empty, insert, com_det *)
+lemma MGF': "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c"
+apply (rule MGF_lemma1)
+apply assumption
+prefer 2 apply (assumption)
+apply clarsimp
+apply (subgoal_tac "{}||- (%pn. {=}. BODY pn .{->}) `dom body")
+apply (erule hoare_derivs.weaken)
+apply (fast intro: domI)
+apply (rule finite_dom_body [THEN [2] MGT_Body])
+apply (simp (no_asm))
+apply (erule (1) MGF_lemma2_simult)
+apply (rule subset_refl)
+done
+
+(* requires Body+empty+insert / BodyN, com_det *)
+lemmas hoare_complete = MGF' [THEN MGF_complete, standard]
+
+
+subsection "unused derived rules"
+
+lemma falseE: "G|-{%Z s. False}.c.{Q}"
+apply (rule hoare_derivs.conseq)
+apply fast
+done
+
+lemma trueI: "G|-{P}.c.{%Z s. True}"
+apply (rule hoare_derivs.conseq)
+apply (fast intro!: falseE)
+done
+
+lemma disj: "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |]
+ ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}"
+apply (rule hoare_derivs.conseq)
+apply (fast elim: conseq12)
+done (* analogue conj non-derivable *)
+
+lemma hoare_SkipI: "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}"
+apply (rule conseq12)
+apply (rule hoare_derivs.Skip)
+apply fast
+done
+
+
+subsection "useful derived rules"
+
+lemma single_asm: "{t}|-t"
+apply (rule hoare_derivs.asm)
+apply (rule subset_refl)
+done
+
+lemma export_s: "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}"
+apply (rule hoare_derivs.conseq)
+apply auto
+done
+
+
+lemma weak_Local: "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==>
+ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}"
+apply (rule export_s)
+apply (rule hoare_derivs.Local)
+apply (erule conseq2)
+apply (erule spec)
+done
+
+(*
+Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}"
+by (induct_tac "c" 1);
+by Auto_tac;
+by (rtac conseq1 1);
+by (rtac hoare_derivs.Skip 1);
+force 1;
+by (rtac conseq1 1);
+by (rtac hoare_derivs.Ass 1);
+force 1;
+by (defer_tac 1);
+###
+by (rtac hoare_derivs.Comp 1);
+by (dtac spec 2);
+by (dtac spec 2);
+by (assume_tac 2);
+by (etac conseq1 2);
+by (Clarsimp_tac 2);
+force 1;
+*)
end
--- a/src/HOL/IMPP/Misc.ML Wed Jun 07 01:06:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-(* Title: HOL/IMPP/Misc.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TUM
-*)
-
-section "state access";
-
-Goalw [getlocs_def] "getlocs (st g l) = l";
-by (Simp_tac 1);
-qed "getlocs_def2";
-
-Goalw [update_def] "s[Loc Y::=s<Y>] = s";
-by (induct_tac "s" 1);
-by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
-qed "update_Loc_idem2";
-Addsimps[update_Loc_idem2];
-
-Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]";
-by (induct_tac "X" 1);
-by Auto_tac;
-by (ALLGOALS (induct_tac "s"));
-by Auto_tac;
-by (ALLGOALS (rtac ext));
-by Auto_tac;
-qed "update_overwrt";
-Addsimps[update_overwrt];
-
-Goalw [update_def]"(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)";
-by (induct_tac "s" 1);
-by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
-qed "getlocs_Loc_update";
-Addsimps[getlocs_Loc_update];
-
-Goalw [update_def] "getlocs (s[Glb Y::=k]) = getlocs s";
-by (induct_tac "s" 1);
-by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
-qed "getlocs_Glb_update";
-Addsimps[getlocs_Glb_update];
-
-Goalw [setlocs_def] "getlocs (setlocs s l) = l";
-by (induct_tac "s" 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
-qed "getlocs_setlocs";
-Addsimps[getlocs_setlocs];
-
-Goal "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])";
-by (induct_tac "Y" 1);
-by (rtac ext 2);
-by Auto_tac;
-qed "getlocs_setlocs_lemma";
-
-(*unused*)
-Goalw [hoare_valids_def]
-"!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
-\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}";
-by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
-by (Clarsimp_tac 1);
-by (dres_inst_tac [("x","s<Y>")] spec 1);
-by (smp_tac 1 1);
-by (dtac spec 1);
-by (dres_inst_tac [("x","s[Loc Y::=a s]")] spec 1);
-by (Full_simp_tac 1);
-by (mp_tac 1);
-by (smp_tac 1 1);
-by (Simp_tac 1);
-qed "classic_Local_valid";
-
-Goal "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
-\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}";
-by (rtac export_s 1);
-(*variant 1*)
-by (rtac (hoare_derivs.Local RS conseq1) 1);
-by (etac spec 1);
-by (Force_tac 1);
-(*variant 2
-by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] conseq1 1);
-by (Clarsimp_tac 2);
-by (rtac hoare_derivs.Local 1);
-by (etac spec 1);
-*)
-qed "classic_Local";
-
-Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
-by (rtac classic_Local 1);
-by (ALLGOALS Clarsimp_tac);
-by (etac conseq12 1);
-by (Clarsimp_tac 1);
-by (dtac sym 1);
-by (Asm_full_simp_tac 1);
-qed "classic_Local_indep";
-
-Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
-by (rtac export_s 1);
-by (rtac hoare_derivs.Local 1);
-by (Clarsimp_tac 1);
-qed "Local_indep";
-
-Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
-by (rtac weak_Local 1);
-by (ALLGOALS Clarsimp_tac);
-qed "weak_Local_indep";
-
-
-Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
-by (rtac export_s 1);
-by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<Y> = s<Y>")] (conseq12) 1);
-by (Clarsimp_tac 2);
-by (rtac hoare_derivs.Local 1);
-by (Clarsimp_tac 1);
-by (rtac trueI 1);
-qed "export_Local_invariant";
-
-Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
-by (rtac classic_Local 1);
-by (Clarsimp_tac 1);
-by (rtac (trueI RS conseq12) 1);
-by (Clarsimp_tac 1);
-qed "classic_Local_invariant";
-
-Goal "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==> \
-\ G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}. \
-\ X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}";
-by (res_inst_tac [("s'1","s'"),("Q'","%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s")] (hoare_derivs.Call RS conseq12) 1);
-by (asm_simp_tac (simpset() addsimps [getlocs_setlocs_lemma]) 1);
-by (Force_tac 1);
-qed "Call_invariant";
-
-
--- a/src/HOL/IMPP/Misc.thy Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/Misc.thy Wed Jun 07 01:51:22 2006 +0200
@@ -18,6 +18,134 @@
Glb gn => (case s of st g l => st (g(gn:=v)) l)
| Loc ln => (case s of st g l => st g (l(ln:=v)))"
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection "state access"
+
+lemma getlocs_def2: "getlocs (st g l) = l"
+apply (unfold getlocs_def)
+apply simp
+done
+
+lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]"
+apply (unfold update_def)
+apply (induct_tac X)
+apply auto
+apply (induct_tac [!] s)
+apply auto
+done
+
+lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l"
+apply (unfold setlocs_def)
+apply (induct_tac s)
+apply auto
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])"
+apply (induct_tac Y)
+apply (rule_tac [2] ext)
+apply auto
+done
+
+(*unused*)
+lemma classic_Local_valid:
+"!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.
+ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}"
+apply (unfold hoare_valids_def)
+apply (simp (no_asm_use) add: triple_valid_def2)
+apply clarsimp
+apply (drule_tac x = "s<Y>" in spec)
+apply (tactic "smp_tac 1 1")
+apply (drule spec)
+apply (drule_tac x = "s[Loc Y::=a s]" in spec)
+apply (simp (no_asm_use))
+apply (erule (1) notE impE)
+apply (tactic "smp_tac 1 1")
+apply simp
+done
+
+lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.
+ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}"
+apply (rule export_s)
+(*variant 1*)
+apply (rule hoare_derivs.Local [THEN conseq1])
+apply (erule spec)
+apply force
+(*variant 2
+by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] conseq1 1)
+by (Clarsimp_tac 2);
+by (rtac hoare_derivs.Local 1);
+by (etac spec 1);
+*)
+done
+
+lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>
+ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
+apply (rule classic_Local)
+apply clarsimp
+apply (erule conseq12)
+apply clarsimp
+apply (drule sym)
+apply simp
+done
+
+lemma Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>
+ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
+apply (rule export_s)
+apply (rule hoare_derivs.Local)
+apply clarsimp
+done
+
+lemma weak_Local_indep: "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>
+ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
+apply (rule weak_Local)
+apply auto
+done
+
+
+lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
+apply (rule export_s)
+apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12)
+prefer 2
+apply clarsimp
+apply (rule hoare_derivs.Local)
+apply clarsimp
+apply (rule trueI)
+done
+
+lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
+apply (rule classic_Local)
+apply clarsimp
+apply (rule trueI [THEN conseq12])
+apply clarsimp
+done
+
+lemma Call_invariant: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==>
+ G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}.
+ X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}"
+apply (rule_tac s'1 = "s'" and
+ Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in
+ hoare_derivs.Call [THEN conseq12])
+apply (simp (no_asm_simp) add: getlocs_setlocs_lemma)
+apply force
+done
end
--- a/src/HOL/IMPP/Natural.ML Wed Jun 07 01:06:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: HOL/IMPP/Natural.ML
- ID: $Id$
- Author: David von Oheimb, TUM
- Copyright 1999 TUM
-*)
-
-AddIs evalc.intros;
-AddIs evaln.intros;
-
-AddSEs evalc_elim_cases;
-AddSEs evaln_elim_cases;
-
-(* evaluation of com is deterministic *)
-Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
-by (etac evalc.induct 1);
-by (thin_tac "<?c,s1> -c-> s2" 8);
-(*blast_tac needs Unify.search_bound := 40*)
-by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
-qed_spec_mp "com_det";
-
-Goal "<c,s> -n-> t ==> <c,s> -c-> t";
-by (etac evaln.induct 1);
-by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac));
-qed "evaln_evalc";
-
-Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
-by (cut_facts_tac (premises()) 1);
-by (ftac Suc_le_D 1);
-by (Clarify_tac 1);
-by (eresolve_tac (premises()) 1);
-qed "Suc_le_D_lemma";
-
-Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
-by (etac evaln.induct 1);
-by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
-by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac));
-qed_spec_mp "evaln_nonstrict";
-
-Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
-by (etac evaln_nonstrict 1);
-by Auto_tac;
-qed "evaln_Suc";
-
-Goal "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==> \
-\ ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2";
-by (cut_facts_tac [read_instantiate [("m","n1"),("n","n2")] nat_le_linear] 1);
-by (blast_tac (claset() addDs [evaln_nonstrict]) 1);
-qed "evaln_max2";
-
-Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t";
-by (etac evalc.induct 1);
-by (ALLGOALS (REPEAT o etac exE));
-by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
-by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac));
-qed "evalc_evaln";
-
-Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
-by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1);
-qed "eval_eq";
--- a/src/HOL/IMPP/Natural.thy Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/Natural.thy Wed Jun 07 01:51:22 2006 +0200
@@ -107,6 +107,56 @@
inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
-ML {* use_legacy_bindings (the_context ()) *}
+declare evalc.intros [intro]
+declare evaln.intros [intro]
+
+declare evalc_elim_cases [elim!]
+declare evaln_elim_cases [elim!]
+
+(* evaluation of com is deterministic *)
+lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
+apply (erule evalc.induct)
+apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
+(*blast_tac needs Unify.search_bound := 40*)
+apply (best elim: evalc_WHILE_case)+
+done
+
+lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
+apply (erule evaln.induct)
+apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
+done
+
+lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
+apply (frule Suc_le_D)
+apply blast
+done
+
+lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
+apply (erule evaln.induct)
+apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
+done
+
+lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
+apply (erule evaln_nonstrict)
+apply auto
+done
+
+lemma evaln_max2: "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==>
+ ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"
+apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
+apply (blast dest: evaln_nonstrict)
+done
+
+lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
+apply (erule evalc.induct)
+apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
+apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
+apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
+done
+
+lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
+apply (fast elim: evalc_evaln evaln_evalc)
+done
end
--- a/src/HOL/IsaMakefile Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 07 01:51:22 2006 +0200
@@ -252,9 +252,8 @@
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
-$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \
- IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \
- IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML
+$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
+ IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
@$(ISATOOL) usedir $(OUT)/HOL IMPP