--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Com.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,24 @@
+Goalw [dom_def] "m a = Some b ==> a : dom m";
+by Auto_tac;
+qed "domI";
+
+Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
+by Auto_tac;
+qed "domD";
+AddSDs [domD];
+
+Goalw [body_def] "finite (dom body)";
+br finite_dom_map_of 1;
+qed "finite_dom_body";
+
+Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
+bd map_of_SomeD 1;
+by (Fast_tac 1);
+qed "WT_bodiesD";
+
+val WTs_elim_cases = map WTs.mk_cases
+ ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)",
+ "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
+ "WT (BODY P)", "WT (X:=CALL P(a))"];
+
+AddSEs WTs_elim_cases;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Com.thy Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,81 @@
+(* Title: HOL/IMPP/Com.thy
+ ID: $Id$
+ Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
+ Copyright 1999 TUM
+
+Semantics of arithmetic and boolean expressions, Syntax of commands
+*)
+
+Com = Main +
+
+types val = nat (* for the meta theory, this may be anything, but with
+ current Isabelle, types cannot be refined later *)
+types glb
+ loc
+arities (*val,*)glb,loc :: term
+consts Arg, Res :: loc
+
+datatype vname = Glb glb | Loc loc
+types globs = glb => val
+ locals = loc => val
+datatype state = st globs locals
+(* for the meta theory, the following would be sufficient:
+types state
+arities state::term
+consts st:: [globs , locals] => state
+*)
+types aexp = state => val
+ bexp = state => bool
+
+types pname
+arities pname :: term
+
+datatype com
+ = SKIP
+ | Ass vname aexp ("_:==_" [65, 65 ] 60)
+ | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60)
+ | Semi com com ("_;; _" [59, 60 ] 59)
+ | Cond bexp com com ("IF _ THEN _ ELSE _" [65, 60, 61] 60)
+ | While bexp com ("WHILE _ DO _" [65, 61] 60)
+ | BODY pname
+ | Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60)
+
+consts bodies :: "(pname * com) list"(* finitely many procedure definitions *)
+ body :: " pname ~=> com"
+defs body_def "body == map_of bodies"
+
+
+(* Well-typedness: all procedures called must exist *)
+consts WTs :: com set
+syntax WT :: com => bool
+translations "WT c" == "c : WTs"
+
+inductive WTs intrs
+
+ Skip "WT SKIP"
+
+ Assign "WT (X :== a)"
+
+ Local "WT c ==>
+ WT (LOCAL Y := a IN c)"
+
+ Semi "[| WT c0; WT c1 |] ==>
+ WT (c0;; c1)"
+
+ If "[| WT c0; WT c1 |] ==>
+ WT (IF b THEN c0 ELSE c1)"
+
+ While "WT c ==>
+ WT (WHILE b DO c)"
+
+ Body "body pn ~= None ==>
+ WT (BODY pn)"
+
+ Call "WT (BODY pn) ==>
+ WT (X:=CALL pn(a))"
+
+constdefs
+ WT_bodies :: bool
+ "WT_bodies == !(pn,b):set bodies. WT b"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/EvenOdd.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,111 @@
+(* 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 1 = False";
+by (Clarsimp_tac 1);
+bd dvd_imp_le 1;
+by Auto_tac;
+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);
+be ssubst 1;
+br 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)";
+br refl 1;
+qed "Z_eq_Arg_plus_def2";
+
+Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))";
+br 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+1}. odd .{Res_ok}";
+br hoare_derivs.If 1;
+br (hoare_derivs.Ass RS conseq1) 1;
+by (clarsimp_tac Arg_Res_css 1);
+br export_s 1;
+br (hoare_derivs.Call RS conseq1) 1;
+by (res_inst_tac [("P","Z=Arg+2")] conseq12 1);
+br 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}";
+br hoare_derivs.If 1;
+br (hoare_derivs.Ass RS conseq1) 1;
+by (clarsimp_tac Arg_Res_css 1);
+br hoare_derivs.Comp 1;
+br 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);
+br export_s 1;
+by (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
+ ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
+br (single_asm RS conseq2) 1;
+by (clarsimp_tac Arg_Res_css 1);
+by (force_tac Arg_Res_css 1);
+br 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);
+br (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}";
+br BodyN 1;
+by (Simp_tac 1);
+br (Even_lemma RS hoare_derivs.cut) 1;
+br BodyN 1;
+by (Simp_tac 1);
+br (Odd_lemma RS thin) 1;
+by (Simp_tac 1);
+qed "Even_ok_N";
+
+Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
+br 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;
+br hoare_derivs.insert 1;
+br (Odd_lemma RS thin) 1;
+by (Simp_tac 1);
+br (Even_lemma RS thin) 1;
+by (Simp_tac 1);
+qed "Even_ok_S";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/EvenOdd.thy Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,42 @@
+(* Title: HOL/IMPP/EvenOdd.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TUM
+
+Example of mutually recursive procedures verified with Hoare logic
+*)
+
+EvenOdd = Misc +
+
+constdefs even :: nat => bool
+ "even n == 2 dvd n"
+
+consts
+ Even, Odd :: pname
+rules
+ Even_neq_Odd "Even ~= Odd"
+ Arg_neq_Res "Arg ~= Res"
+
+constdefs
+ evn :: com
+ "evn == IF (%s. s<Arg>=0)
+ THEN Loc Res:==(%s. 0)
+ ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
+ Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
+ Loc Res:==(%s. s<Res> * s<Arg>))"
+ odd :: com
+ "odd == IF (%s. s<Arg>=0)
+ THEN Loc Res:==(%s. 1)
+ ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))"
+
+defs
+ bodies_def "bodies == [(Even,evn),(Odd,odd)]"
+
+consts
+ Z_eq_Arg_plus :: nat => nat assn ("Z=Arg+_" [50]50)
+ "even_Z=(Res=0)" :: nat assn ("Res'_ok")
+defs
+ 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)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Hoare.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,407 @@
+(* 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}";
+br 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}";
+be 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}";
+be 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}";
+bd hoare_derivs.Body 1;
+be 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}";
+br Body1 1;
+br 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}";
+br 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}";
+br 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}";
+br (hoare_derivs.Loop RS conseq2) 1;
+by (ALLGOALS Simp_tac);
+br hoare_derivs.conseq 1;
+by (Fast_tac 1);
+qed "LoopF";
+
+(*
+Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
+be hoare_derivs.cut 1;
+be 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]));
+br 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.intrs)
+ THEN_ALL_NEW Fast_tac));
+qed_spec_mp "thin";
+
+Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
+br BodyN 1;
+be 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";
+be finite_induct 1;
+by (ALLGOALS Clarsimp_tac);
+bd derivs_insertD 1;
+br 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);
+br 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";
+br allI 1;
+by (induct_tac "n" 1);
+by (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
+by (Clarsimp_tac 1);
+bd 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";
+be 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",
+ Clarsimp_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}";
+be 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";
+be 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);
+bd 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}";
+be conseq12 1;
+by (clarsimp_tac (claset(), simpset() addsimps
+ [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
+qed "MGF_complete";
+
+val WTs_elim_cases = map WTs.mk_cases
+ ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)",
+ "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
+ "WT (BODY P)", "WT (X:=CALL P(a))"];
+
+AddSEs WTs_elim_cases;
+(* 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 [domI]) 7);
+be MGT_alternD 6;
+by (rewtac MGT_def);
+by (EVERY'[dtac bspec, etac 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));
+br (hoare_derivs.Skip RS conseq2) 1;
+br (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);
+bd card_seteq 1;
+by (Asm_simp_tac 1);
+be finite_imageI 1;
+by (Asm_full_simp_tac 1);
+by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
+br ballI 1;
+by (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
+by (Fast_tac 1);
+by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
+br 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);
+byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4];
+by (eresolve_tac (tl(tl(tl(premises())))) 4);
+by (Fast_tac 1);
+be Suc_leD 1;
+bd finite_subset 1;
+be finite_imageI 1;
+by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1);
+qed_spec_mp "nesting_lemma";
+
+Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
+\ G|-{=}.BODY pn.{->}";
+br BodyN 1;
+be 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);
+be hoare_derivs.asm 1;
+be MGT_BodyN 1;
+br finite_dom_body 3;
+be MGF_lemma1 1;
+ba 2;
+by (Blast_tac 1);
+by (Clarsimp_tac 1);
+by (eatac WT_bodiesD 1 1);
+br 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";
+br hoare_derivs.Body 1;
+be finite_pointwise 1;
+ba 2;
+by (Clarify_tac 1);
+be 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);
+br (finite_dom_body RS finite_imageI) 1;
+by (rotate_tac 2 1);
+by (make_imp_tac 1);
+be finite_induct 1;
+by (ALLGOALS (clarsimp_tac (
+ claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
+ simpset() delsimps [range_composition])));
+be MGF_lemma1 1;
+by (fast_tac (claset() addDs [WT_bodiesD]) 2);
+by (Clarsimp_tac 1);
+br hoare_derivs.asm 1;
+by (fast_tac (claset() addIs [domI]) 1);
+qed_spec_mp "MGF_lemma2_simult";
+
+(* requires Body, empty, insert, com_det *)
+Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
+br MGF_lemma1 1;
+ba 1;
+ba 2;
+by (Clarsimp_tac 1);
+by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})``dom body" 1);
+be hoare_derivs.weaken 1;
+by (fast_tac (claset() addIs [domI]) 1);
+br (finite_dom_body RSN (2,MGT_Body)) 1;
+by (Simp_tac 1);
+by (eatac MGF_lemma2_simult 1 1);
+br 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}";
+br hoare_derivs.conseq 1;
+by (Fast_tac 1);
+qed "falseE";
+
+Goal "G|-{P}.c.{%Z s. True}";
+br 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}";
+br 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}";
+br conseq12 1;
+br hoare_derivs.Skip 1;
+by (Fast_tac 1);
+qed "hoare_SkipI";
+
+
+section "useful derived rules";
+
+Goal "{t}|-t";
+br hoare_derivs.asm 1;
+br subset_refl 1;
+qed "single_asm";
+
+Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
+br 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}";
+br export_s 1;
+br hoare_derivs.Local 1;
+be conseq2 1;
+be spec 1;
+qed "weak_Local";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Hoare.thy Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,99 @@
+(* Title: HOL/IMPP/Hoare.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TUM
+
+Inductive definition of Hoare logic for partial correctness
+Completeness is taken relative to completeness of the underlying logic
+Two versions of completeness proof:
+ nested single recursion vs. simultaneous recursion in call rule
+*)
+
+Hoare = Natural +
+
+types 'a assn = "'a => state => bool"
+translations
+ "a assn" <= (type)"a => state => bool"
+
+constdefs
+ state_not_singleton :: bool
+ "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *)
+
+ peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)
+ "peek_and P p == %Z s. P Z s & p s"
+
+datatype 'a triple =
+ triple ('a assn) com ('a assn) ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
+
+consts
+ triple_valid :: nat => 'a triple => bool ( "|=_:_" [0 , 58] 57)
+ hoare_valids :: 'a triple set => 'a triple set => bool ("_||=_" [58, 58] 57)
+ hoare_derivs ::"('a triple set * 'a triple set) set"
+syntax
+ triples_valid:: nat => 'a triple set => bool ("||=_:_" [0 , 58] 57)
+ hoare_valid :: 'a triple set => 'a triple => bool ("_|=_" [58, 58] 57)
+"@hoare_derivs":: 'a triple set => 'a triple set => bool ("_||-_" [58, 58] 57)
+"@hoare_deriv" :: 'a triple set => 'a triple => bool ("_|-_" [58, 58] 57)
+
+defs triple_valid_def "|=n:t == case t of {P}.c.{Q} =>
+ !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
+translations "||=n:G" == "Ball G (triple_valid n)"
+defs hoare_valids_def"G||=ts == !n. ||=n:G --> ||=n:ts"
+translations "G |=t " == " G||={t}"
+ "G||-ts" == "(G,ts) : hoare_derivs"
+ "G |-t" == " G||-{t}"
+
+(* Most General Triples *)
+constdefs MGT :: com => state triple ("{=}._.{->}" [60] 58)
+ "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}"
+
+inductive hoare_derivs intrs
+
+ empty "G||-{}"
+ insert"[| G |-t; G||-ts |]
+ ==> G||-insert t ts"
+
+ asm "ts <= G ==>
+ G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
+
+ cut "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
+
+ weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
+
+ conseq"!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} &
+ (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
+ ==> G|-{P}.c.{Q}"
+
+
+ Skip "G|-{P}. SKIP .{P}"
+
+ Ass "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
+
+ Local "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
+ ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
+
+ Comp "[| G|-{P}.c.{Q};
+ G|-{Q}.d.{R} |]
+ ==> G|-{P}. (c;;d) .{R}"
+
+ If "[| G|-{P &> b }.c.{Q};
+ G|-{P &> (Not o b)}.d.{Q} |]
+ ==> G|-{P}. IF b THEN c ELSE d .{Q}"
+
+ Loop "G|-{P &> b}.c.{P} ==>
+ G|-{P}. WHILE b DO c .{P &> (Not o b)}"
+
+(*
+ BodyN "(insert ({P}. BODY pn .{Q}) G)
+ |-{P}. the (body pn) .{Q} ==>
+ G|-{P}. BODY pn .{Q}"
+*)
+ Body "[| G Un (%p. {P p}. BODY p .{Q p})``Procs
+ ||-(%p. {P p}. the (body p) .{Q p})``Procs |]
+ ==> G||-(%p. {P p}. BODY p .{Q p})``Procs"
+
+ Call "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
+ ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
+ X:=CALL pn(a) .{Q}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Misc.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,135 @@
+(* 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);
+br ext 1;
+by (Simp_tac 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);
+br 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);
+bd 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}";
+br export_s 1;
+(*variant 1*)
+br (hoare_derivs.Local RS conseq1) 1;
+be 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);
+br hoare_derivs.Local 1;
+be 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}";
+br classic_Local 1;
+by (ALLGOALS Clarsimp_tac);
+be conseq12 1;
+by (Clarsimp_tac 1);
+bd 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}";
+br export_s 1;
+br 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}";
+br 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>}";
+br 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);
+br hoare_derivs.Local 1;
+by (Clarsimp_tac 1);
+br trueI 1;
+qed "export_Local_invariant";
+
+Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
+br classic_Local 1;
+by (Clarsimp_tac 1);
+br (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";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Misc.thy Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,19 @@
+(* Title: HOL/IMPP/Misc.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TUM
+
+Several examples for Hoare logic
+*)
+Misc = Hoare +
+
+defs
+ newlocs_def "newlocs == %x. arbitrary"
+ setlocs_def "setlocs s l' == case s of st g l => st g l'"
+ getlocs_def "getlocs s == case s of st g l => l"
+ update_def "update s vn v == case vn of
+ 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)))"
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Natural.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,77 @@
+(* Title: HOL/IMPP/Natural.ML
+ ID: $Id$
+ Author: David von Oheimb, TUM
+ Copyright 1999 TUM
+*)
+
+open Natural;
+
+AddIs evalc.intrs;
+AddIs evaln.intrs;
+
+val evalc_elim_cases = map evalc.mk_cases
+ ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t",
+ "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t",
+ "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"];
+val evaln_elim_cases = map evaln.mk_cases
+ ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t",
+ "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t",
+ "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"];
+val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
+val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t";
+
+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)";
+be 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";
+be evaln.induct 1;
+by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
+qed "evaln_evalc";
+
+goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)";
+by (induct_tac "m'" 1);
+by Auto_tac;
+qed_spec_mp "Suc_le_D";
+
+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";
+be 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.intrs THEN_ALL_NEW atac));
+qed_spec_mp "evaln_nonstrict";
+
+Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
+be 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";
+be 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.intrs 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";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/Natural.thy Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,89 @@
+(* Title: HOL/IMPP/Natural.thy
+ ID: $Id$
+ Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
+ Copyright 1999 TUM
+
+Natural semantics of commands
+*)
+
+Natural = Com +
+
+(** Execution of commands **)
+consts evalc :: "(com * state * state) set"
+ "@evalc":: [com,state, state] => bool ("<_,_>/ -c-> _" [0,0, 51] 51)
+ evaln :: "(com * state * nat * state) set"
+ "@evaln":: [com,state,nat,state] => bool ("<_,_>/ -_-> _" [0,0,0,51] 51)
+
+translations "<c,s> -c-> s'" == "(c,s, s') : evalc"
+ "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
+
+consts
+ newlocs :: locals
+ setlocs :: state => locals => state
+ getlocs :: state => locals
+ update :: state => vname => val => state ("_/[_/::=/_]" [900,0,0] 900)
+syntax (* IN Natural.thy *)
+ loc :: state => locals ("_<_>" [75,0] 75)
+translations
+ "s<X>" == "getlocs s X"
+
+inductive evalc
+ intrs
+ Skip "<SKIP,s> -c-> s"
+
+ Assign "<X :== a,s> -c-> s[X::=a s]"
+
+ Local "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
+ <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
+
+ Semi "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
+ <c0;; c1, s0> -c-> s2"
+
+ IfTrue "[| b s; <c0,s> -c-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -c-> s1"
+
+ IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -c-> s1"
+
+ WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
+
+ WhileTrue "[| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 |] ==>
+ <WHILE b DO c, s0> -c-> s2"
+
+ Body "<the (body pn), s0> -c-> s1 ==>
+ <BODY pn, s0> -c-> s1"
+
+ Call "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
+ <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
+ [X::=s1<Res>]"
+
+inductive evaln
+ intrs
+ Skip "<SKIP,s> -n-> s"
+
+ Assign "<X :== a,s> -n-> s[X::=a s]"
+
+ Local "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
+ <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+
+ Semi "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
+ <c0;; c1, s0> -n-> s2"
+
+ IfTrue "[| b s; <c0,s> -n-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -n-> s1"
+
+ IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -n-> s1"
+
+ WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
+
+ WhileTrue "[| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 |] ==>
+ <WHILE b DO c, s0> -n-> s2"
+
+ Body "<the (body pn), s0> - n-> s1 ==>
+ <BODY pn, s0> -Suc n-> s1"
+
+ Call "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
+ <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
+ [X::=s1<Res>]"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/README.html Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,13 @@
+<!-- $Id$ -->
+<HTML><HEAD>
+<TITLE>HOL/IMPP/README</TITLE>
+</HEAD><BODY>
+
+<H2>IMPP--An imperative language with procedures</H2>
+
+This is an extension of <A HREF="../IMP/">IMP</A> with local variables
+and mutually recursive procedures. For documentation see
+<A HREF="http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html">
+Hoare Logic for Mutual Recursion and Local Variables</A>.
+
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/ROOT.ML Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,9 @@
+(* Title: HOL/IMPP/ROOT.ML
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 TUM
+*)
+
+writeln"Root file for HOL/IMPP";
+
+use_thy "EvenOdd";
--- a/src/HOL/IsaMakefile Mon Jan 31 16:19:51 2000 +0100
+++ b/src/HOL/IsaMakefile Mon Jan 31 18:30:35 2000 +0100
@@ -8,7 +8,7 @@
default: HOL
images: HOL HOL-Real TLA
-test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
+test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \