added IMPP to HOL
authoroheimb
Mon Jan 31 18:30:35 2000 +0100 (2000-01-31)
changeset 8177e59e93ad85eb
parent 8176 db112d36a426
child 8178 a6a4fb7b819b
added IMPP to HOL
src/HOL/IMPP/Com.ML
src/HOL/IMPP/Com.thy
src/HOL/IMPP/EvenOdd.ML
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Hoare.ML
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Misc.ML
src/HOL/IMPP/Misc.thy
src/HOL/IMPP/Natural.ML
src/HOL/IMPP/Natural.thy
src/HOL/IMPP/README.html
src/HOL/IMPP/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMPP/Com.ML	Mon Jan 31 18:30:35 2000 +0100
     1.3 @@ -0,0 +1,24 @@
     1.4 +Goalw [dom_def] "m a = Some b ==> a : dom m";
     1.5 +by Auto_tac;
     1.6 +qed "domI";
     1.7 +
     1.8 +Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
     1.9 +by Auto_tac;
    1.10 +qed "domD";
    1.11 +AddSDs [domD];
    1.12 +
    1.13 +Goalw [body_def] "finite (dom body)";
    1.14 +br finite_dom_map_of 1;
    1.15 +qed "finite_dom_body";
    1.16 +
    1.17 +Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
    1.18 +bd map_of_SomeD 1;
    1.19 +by (Fast_tac 1);
    1.20 +qed "WT_bodiesD";
    1.21 +
    1.22 +val WTs_elim_cases = map WTs.mk_cases
    1.23 +   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
    1.24 +    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
    1.25 +    "WT (BODY P)", "WT (X:=CALL P(a))"];
    1.26 +
    1.27 +AddSEs WTs_elim_cases;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMPP/Com.thy	Mon Jan 31 18:30:35 2000 +0100
     2.3 @@ -0,0 +1,81 @@
     2.4 +(*  Title:    HOL/IMPP/Com.thy
     2.5 +    ID:       $Id$
     2.6 +    Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
     2.7 +    Copyright 1999 TUM
     2.8 +
     2.9 +Semantics of arithmetic and boolean expressions, Syntax of commands
    2.10 +*)
    2.11 +
    2.12 +Com = Main +
    2.13 +
    2.14 +types	 val = nat   (* for the meta theory, this may be anything, but with
    2.15 +                        current Isabelle, types cannot be refined later *)
    2.16 +types	 glb
    2.17 +         loc
    2.18 +arities	 (*val,*)glb,loc :: term
    2.19 +consts   Arg, Res :: loc
    2.20 +
    2.21 +datatype vname  = Glb glb | Loc loc
    2.22 +types	 globs  = glb => val
    2.23 +	 locals = loc => val
    2.24 +datatype state  = st globs locals
    2.25 +(* for the meta theory, the following would be sufficient:
    2.26 +types    state
    2.27 +arities  state::term
    2.28 +consts   st:: [globs , locals] => state
    2.29 +*)
    2.30 +types	 aexp   = state => val
    2.31 +	 bexp   = state => bool
    2.32 +
    2.33 +types	pname
    2.34 +arities	pname  :: term
    2.35 +
    2.36 +datatype com
    2.37 +      = SKIP
    2.38 +      | Ass   vname aexp	("_:==_"	        [65, 65    ] 60)
    2.39 +      | Local loc aexp com	("LOCAL _:=_ IN _"	[65,  0, 61] 60)
    2.40 +      | Semi  com  com		("_;; _"	        [59, 60    ] 59)
    2.41 +      | Cond  bexp com com	("IF _ THEN _ ELSE _"	[65, 60, 61] 60)
    2.42 +      | While bexp com		("WHILE _ DO _"		[65,     61] 60)
    2.43 +      | BODY  pname
    2.44 +      | Call  vname pname aexp	("_:=CALL _'(_')"	[65, 65,  0] 60)
    2.45 +
    2.46 +consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
    2.47 +       body   :: " pname ~=> com"
    2.48 +defs   body_def  "body == map_of bodies"
    2.49 +
    2.50 +
    2.51 +(* Well-typedness: all procedures called must exist *)
    2.52 +consts WTs :: com set
    2.53 +syntax WT  :: com => bool
    2.54 +translations "WT c" == "c : WTs"
    2.55 +
    2.56 +inductive WTs intrs
    2.57 +
    2.58 +    Skip    "WT SKIP"
    2.59 +
    2.60 +    Assign  "WT (X :== a)"
    2.61 +
    2.62 +    Local   "WT c ==>
    2.63 +             WT (LOCAL Y := a IN c)"
    2.64 +
    2.65 +    Semi    "[| WT c0; WT c1 |] ==>
    2.66 +             WT (c0;; c1)"
    2.67 +
    2.68 +    If      "[| WT c0; WT c1 |] ==>
    2.69 +             WT (IF b THEN c0 ELSE c1)"
    2.70 +
    2.71 +    While   "WT c ==>
    2.72 +             WT (WHILE b DO c)"
    2.73 +
    2.74 +    Body    "body pn ~= None ==>
    2.75 +             WT (BODY pn)"
    2.76 +
    2.77 +    Call    "WT (BODY pn) ==>
    2.78 +             WT (X:=CALL pn(a))"
    2.79 +
    2.80 +constdefs
    2.81 +  WT_bodies :: bool
    2.82 + "WT_bodies == !(pn,b):set bodies. WT b"
    2.83 +
    2.84 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Mon Jan 31 18:30:35 2000 +0100
     3.3 @@ -0,0 +1,111 @@
     3.4 +(*  Title:      HOL/IMPP/EvenOdd.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     David von Oheimb
     3.7 +    Copyright   1999 TUM
     3.8 +*)
     3.9 +
    3.10 +section "even"; 
    3.11 +
    3.12 +Goalw [even_def] "even 0";
    3.13 +by (Simp_tac 1);
    3.14 +qed "even_0";
    3.15 +Addsimps [even_0];
    3.16 +
    3.17 +Goalw [even_def] "even 1 = False";
    3.18 +by (Clarsimp_tac 1);
    3.19 +bd dvd_imp_le 1;
    3.20 +by Auto_tac;
    3.21 +qed "not_even_1";
    3.22 +Addsimps [not_even_1];
    3.23 +
    3.24 +Goalw [even_def] "even (Suc (Suc n)) = even n";
    3.25 +by (subgoal_tac "Suc (Suc n) = n+2" 1);
    3.26 +by  (Simp_tac 2);
    3.27 +be ssubst 1;
    3.28 +br dvd_reduce 1;
    3.29 +qed "even_step";
    3.30 +Addsimps[even_step];
    3.31 +
    3.32 +
    3.33 +section "Arg, Res";
    3.34 +
    3.35 +Addsimps[Arg_neq_Res,Arg_neq_Res RS not_sym];
    3.36 +Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym];
    3.37 +
    3.38 +Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)";
    3.39 +br refl 1;
    3.40 +qed "Z_eq_Arg_plus_def2";
    3.41 +
    3.42 +Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))";
    3.43 +br refl 1;
    3.44 +qed "Res_ok_def2";
    3.45 +
    3.46 +val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]);
    3.47 +
    3.48 +Goalw [body_def, bodies_def] "body Odd = Some odd";
    3.49 +by Auto_tac;
    3.50 +qed "body_Odd";
    3.51 +Goalw [body_def, bodies_def] "body Even = Some evn";
    3.52 +by Auto_tac;
    3.53 +qed "body_Even";
    3.54 +Addsimps[body_Odd, body_Even];
    3.55 +
    3.56 +section "verification";
    3.57 +
    3.58 +Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. odd .{Res_ok}";
    3.59 +br hoare_derivs.If 1;
    3.60 +br  (hoare_derivs.Ass RS conseq1) 1;
    3.61 +by  (clarsimp_tac Arg_Res_css 1);
    3.62 +br export_s 1;
    3.63 +br (hoare_derivs.Call RS conseq1) 1;
    3.64 +by  (res_inst_tac [("P","Z=Arg+2")] conseq12 1);
    3.65 +br   single_asm 1;
    3.66 +by (auto_tac Arg_Res_css);
    3.67 +qed "Odd_lemma";
    3.68 +
    3.69 +Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}";
    3.70 +br hoare_derivs.If 1;
    3.71 +br  (hoare_derivs.Ass RS conseq1) 1;
    3.72 +by  (clarsimp_tac Arg_Res_css 1);
    3.73 +br hoare_derivs.Comp 1;
    3.74 +br  hoare_derivs.Ass 2;
    3.75 +by (Clarsimp_tac 1);
    3.76 +by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
    3.77 +br  export_s 1;
    3.78 +by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
    3.79 +		   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
    3.80 +br   (single_asm RS conseq2) 1;
    3.81 +by   (clarsimp_tac Arg_Res_css 1);
    3.82 +by  (force_tac Arg_Res_css 1);
    3.83 +br export_s 1;
    3.84 +by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
    3.85 +		  ("Q1","%Z s. even Z = (s<Arg>=0)")]
    3.86 +		 (Call_invariant RS conseq12) 1);
    3.87 +br  (single_asm RS conseq2) 1;
    3.88 +by  (clarsimp_tac Arg_Res_css 1);
    3.89 +by (force_tac Arg_Res_css 1);
    3.90 +qed "Even_lemma";
    3.91 +
    3.92 +
    3.93 +Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
    3.94 +br BodyN 1;
    3.95 +by (Simp_tac 1);
    3.96 +br (Even_lemma RS hoare_derivs.cut) 1;
    3.97 +br BodyN 1;
    3.98 +by (Simp_tac 1);
    3.99 +br (Odd_lemma RS thin) 1;
   3.100 +by (Simp_tac 1);
   3.101 +qed "Even_ok_N";
   3.102 +
   3.103 +Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
   3.104 +br conseq1 1;
   3.105 +by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), 
   3.106 +      ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
   3.107 +      ("Q","%pn. Res_ok")] Body1 1);
   3.108 +by    Auto_tac;
   3.109 +br hoare_derivs.insert 1;
   3.110 +br  (Odd_lemma RS thin) 1;
   3.111 +by  (Simp_tac 1);
   3.112 +br (Even_lemma RS thin) 1;
   3.113 +by (Simp_tac 1);
   3.114 +qed "Even_ok_S";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Mon Jan 31 18:30:35 2000 +0100
     4.3 @@ -0,0 +1,42 @@
     4.4 +(*  Title:      HOL/IMPP/EvenOdd.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     David von Oheimb
     4.7 +    Copyright   1999 TUM
     4.8 +
     4.9 +Example of mutually recursive procedures verified with Hoare logic
    4.10 +*)
    4.11 +
    4.12 +EvenOdd = Misc +
    4.13 +
    4.14 +constdefs even :: nat => bool
    4.15 +  "even n == 2 dvd n"
    4.16 +
    4.17 +consts
    4.18 +  Even, Odd :: pname
    4.19 +rules 
    4.20 +  Even_neq_Odd "Even ~= Odd"
    4.21 +  Arg_neq_Res  "Arg  ~= Res"
    4.22 +
    4.23 +constdefs
    4.24 +  evn :: com
    4.25 + "evn == IF (%s. s<Arg>=0)
    4.26 +         THEN Loc Res:==(%s. 0)
    4.27 +         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
    4.28 +              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
    4.29 +              Loc Res:==(%s. s<Res> * s<Arg>))"
    4.30 +  odd :: com
    4.31 + "odd == IF (%s. s<Arg>=0)
    4.32 +         THEN Loc Res:==(%s. 1)
    4.33 +         ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))"
    4.34 +
    4.35 +defs
    4.36 +  bodies_def "bodies == [(Even,evn),(Odd,odd)]"
    4.37 +  
    4.38 +consts
    4.39 +  Z_eq_Arg_plus   :: nat => nat assn ("Z=Arg+_" [50]50)
    4.40 + "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
    4.41 +defs
    4.42 +  Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
    4.43 +  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res>=0)"
    4.44 +
    4.45 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/IMPP/Hoare.ML	Mon Jan 31 18:30:35 2000 +0100
     5.3 @@ -0,0 +1,407 @@
     5.4 +(*  Title:      HOL/IMPP/Hoare.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     David von Oheimb
     5.7 +    Copyright   1999 TUM
     5.8 +
     5.9 +Soundness and relative completeness of Hoare rules wrt operational semantics
    5.10 +*)
    5.11 +
    5.12 +Goalw [state_not_singleton_def] 
    5.13 +	"state_not_singleton ==> !t. (!s::state. s = t) --> False";
    5.14 +by (Clarify_tac 1);
    5.15 +by (case_tac "ta = t" 1);
    5.16 +by  (ALLGOALS (blast_tac (HOL_cs addDs [not_sym])));
    5.17 +qed "single_stateE";
    5.18 +
    5.19 +Addsimps[peek_and_def];
    5.20 +
    5.21 +
    5.22 +section "validity";
    5.23 +
    5.24 +Goalw [triple_valid_def] 
    5.25 +  "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
    5.26 +by Auto_tac;
    5.27 +qed "triple_valid_def2";
    5.28 +
    5.29 +Goal "|=0:{P}. BODY pn .{Q}";
    5.30 +by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
    5.31 +by (Clarsimp_tac 1);
    5.32 +qed "Body_triple_valid_0";
    5.33 +
    5.34 +(* only ==> direction required *)
    5.35 +Goal "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}";
    5.36 +by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
    5.37 +by (Force_tac 1);
    5.38 +qed "Body_triple_valid_Suc";
    5.39 +
    5.40 +Goalw [triple_valid_def] "|=Suc n:t --> |=n:t";
    5.41 +by (induct_tac "t" 1);
    5.42 +by (Simp_tac 1);
    5.43 +by (fast_tac (claset() addIs [evaln_Suc]) 1);
    5.44 +qed_spec_mp "triple_valid_Suc";
    5.45 +
    5.46 +Goal "||=Suc n:ts ==> ||=n:ts";
    5.47 +by (fast_tac (claset() addIs [triple_valid_Suc]) 1);
    5.48 +qed "triples_valid_Suc";
    5.49 +
    5.50 +
    5.51 +section "derived rules";
    5.52 +
    5.53 +Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \
    5.54 +\                        (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \
    5.55 +\      ==> G|-{P}.c.{Q}";
    5.56 +br hoare_derivs.conseq 1;
    5.57 +by (Blast_tac 1);
    5.58 +qed "conseq12";
    5.59 +
    5.60 +Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}";
    5.61 +be conseq12 1;
    5.62 +by (Fast_tac 1);
    5.63 +qed "conseq1";
    5.64 +
    5.65 +Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}";
    5.66 +be conseq12 1;
    5.67 +by (Fast_tac 1);
    5.68 +qed "conseq2";
    5.69 +
    5.70 +Goal "[| G Un (%p. {P p}.      BODY p  .{Q p})``Procs  \
    5.71 +\         ||- (%p. {P p}. the (body p) .{Q p})``Procs; \
    5.72 +\   pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
    5.73 +bd hoare_derivs.Body 1;
    5.74 +be hoare_derivs.weaken 1;
    5.75 +by (Fast_tac 1);
    5.76 +qed "Body1";
    5.77 +
    5.78 +Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> \
    5.79 +\ G|-{P}. BODY pn .{Q}";
    5.80 +br Body1 1;
    5.81 +br  singletonI 2;
    5.82 +by (Clarsimp_tac 1);
    5.83 +qed "BodyN";
    5.84 +
    5.85 +Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}";
    5.86 +br hoare_derivs.conseq 1;
    5.87 +by (Fast_tac 1);
    5.88 +qed "escape";
    5.89 +
    5.90 +Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}";
    5.91 +br hoare_derivs.conseq 1;
    5.92 +by (fast_tac (claset() addDs (premises())) 1);
    5.93 +qed "constant";
    5.94 +
    5.95 +Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}";
    5.96 +br (hoare_derivs.Loop RS conseq2) 1;
    5.97 +by  (ALLGOALS Simp_tac);
    5.98 +br hoare_derivs.conseq 1;
    5.99 +by (Fast_tac 1);
   5.100 +qed "LoopF";
   5.101 +
   5.102 +(*
   5.103 +Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
   5.104 +be hoare_derivs.cut 1;
   5.105 +be hoare_derivs.asm 1;
   5.106 +qed "thin";
   5.107 +*)
   5.108 +Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
   5.109 +by (etac hoare_derivs.induct 1);
   5.110 +by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
   5.111 +br		  hoare_derivs.empty 1;
   5.112 +by               (eatac hoare_derivs.insert 1 1);
   5.113 +by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
   5.114 +by             (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
   5.115 +by            (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
   5.116 +by           (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
   5.117 +	             smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
   5.118 +by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac] 7); 
   5.119 +by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intrs)
   5.120 +	              THEN_ALL_NEW Fast_tac));
   5.121 +qed_spec_mp "thin";
   5.122 +
   5.123 +Goal "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}";
   5.124 +br BodyN 1;
   5.125 +be thin 1;
   5.126 +by Auto_tac;
   5.127 +qed "weak_Body";
   5.128 +
   5.129 +Goal "G||-insert t ts ==> G|-t & G||-ts";
   5.130 +by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
   5.131 +qed "derivs_insertD";
   5.132 +
   5.133 +Goal "[| finite U; \
   5.134 +\ !p. G |-     {P' p}.c0 p.{Q' p}       --> G |-     {P p}.c0 p.{Q p} |] ==> \
   5.135 +\     G||-(%p. {P' p}.c0 p.{Q' p}) `` U --> G||-(%p. {P p}.c0 p.{Q p}) `` U";
   5.136 +be finite_induct 1;
   5.137 +by (ALLGOALS Clarsimp_tac);
   5.138 +bd derivs_insertD 1;
   5.139 +br hoare_derivs.insert 1;
   5.140 +by  Auto_tac;
   5.141 +qed_spec_mp "finite_pointwise";
   5.142 +
   5.143 +
   5.144 +section "soundness";
   5.145 +
   5.146 +Goalw [hoare_valids_def]
   5.147 + "G|={P &> b}. c .{P} ==> \
   5.148 +\ G|={P}. WHILE b DO c .{P &> (Not o b)}";
   5.149 +by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
   5.150 +br allI 1;
   5.151 +by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \
   5.152 +\ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1);
   5.153 +by  (EVERY'[etac thin_rl, Fast_tac] 1);
   5.154 +by (EVERY'[REPEAT o rtac allI, rtac impI] 1);
   5.155 +by ((etac evaln.induct THEN_ALL_NEW Simp_tac) 1);
   5.156 +by  (ALLGOALS Fast_tac);
   5.157 +qed "Loop_sound_lemma";
   5.158 +
   5.159 +Goalw [hoare_valids_def]
   5.160 +   "[| G Un (%pn. {P pn}.      BODY pn  .{Q pn})``Procs \
   5.161 +\        ||=(%pn. {P pn}. the (body pn) .{Q pn})``Procs |] ==> \
   5.162 +\       G||=(%pn. {P pn}.      BODY pn  .{Q pn})``Procs";
   5.163 +br allI 1;
   5.164 +by (induct_tac "n" 1);
   5.165 +by  (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
   5.166 +by (Clarsimp_tac 1);
   5.167 +bd triples_valid_Suc 1;
   5.168 +by (mp_tac 1);
   5.169 +by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
   5.170 +by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1);
   5.171 +by (fast_tac (claset() addSIs [Body_triple_valid_Suc RS iffD1]) 1);
   5.172 +qed "Body_sound_lemma";
   5.173 +
   5.174 +Goal "G||-ts ==> G||=ts";
   5.175 +be hoare_derivs.induct 1;
   5.176 +by              (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma]
   5.177 +                         THEN_ALL_NEW atac));
   5.178 +by            (rewtac hoare_valids_def);
   5.179 +by            (Blast_tac 1);
   5.180 +by           (Blast_tac 1);
   5.181 +by          (Blast_tac 1); (* asm *)
   5.182 +by         (Blast_tac 1); (* cut *)
   5.183 +by        (Blast_tac 1); (* weaken *)
   5.184 +by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", 
   5.185 +	                   Clarsimp_tac, REPEAT o smp_tac 1]));
   5.186 +by       (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
   5.187 +by       (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
   5.188 +by      (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
   5.189 +by   (Force_tac 3); (* Call *)
   5.190 +by  (eresolve_tac evaln_elim_cases 2); (* If *)
   5.191 +by   (TRYALL Blast_tac);
   5.192 +qed "hoare_sound";
   5.193 +
   5.194 +
   5.195 +section "completeness";
   5.196 +
   5.197 +(* Both versions *)
   5.198 +
   5.199 +(*unused*)
   5.200 +Goalw [MGT_def] "G|-MGT c ==> \
   5.201 +\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}";
   5.202 +be conseq12 1;
   5.203 +by Auto_tac;
   5.204 +qed "MGT_alternI";
   5.205 +
   5.206 +(* requires com_det *)
   5.207 +Goalw [MGT_def] "state_not_singleton ==> \
   5.208 +\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c";
   5.209 +be conseq12 1;
   5.210 +by Auto_tac;
   5.211 +by (case_tac "? t. <c,?s> -c-> t" 1);
   5.212 +by  (fast_tac (claset() addEs [com_det]) 1);
   5.213 +by (Clarsimp_tac 1);
   5.214 +bd single_stateE 1;
   5.215 +by (Blast_tac 1);
   5.216 +qed "MGT_alternD";
   5.217 +
   5.218 +Goalw [MGT_def] 
   5.219 + "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
   5.220 +be conseq12 1;
   5.221 +by (clarsimp_tac (claset(), simpset() addsimps 
   5.222 +  [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
   5.223 +qed "MGF_complete";
   5.224 +
   5.225 +val WTs_elim_cases = map WTs.mk_cases
   5.226 +   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
   5.227 +    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
   5.228 +    "WT (BODY P)", "WT (X:=CALL P(a))"];
   5.229 +
   5.230 +AddSEs WTs_elim_cases;
   5.231 +(* requires com_det, escape (i.e. hoare_derivs.conseq) *)
   5.232 +Goal "state_not_singleton ==> \
   5.233 +\ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
   5.234 +by (induct_tac "c" 1);
   5.235 +by        (ALLGOALS Clarsimp_tac);
   5.236 +by        (fast_tac (claset() addIs [domI]) 7);
   5.237 +be       MGT_alternD 6;
   5.238 +by       (rewtac MGT_def);
   5.239 +by       (EVERY'[dtac bspec, etac domI] 7);
   5.240 +by       (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
   5.241 +	     [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
   5.242 +	     (hoare_derivs.Call RS conseq1), etac conseq12] 7);
   5.243 +by        (ALLGOALS (etac thin_rl));
   5.244 +br        (hoare_derivs.Skip RS conseq2) 1;
   5.245 +br        (hoare_derivs.Ass RS conseq1) 2;
   5.246 +by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
   5.247 +	          [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] 
   5.248 +		  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
   5.249 +by         (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
   5.250 +by         ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
   5.251 +by          (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
   5.252 +by           Auto_tac;
   5.253 +qed_spec_mp "MGF_lemma1";
   5.254 +
   5.255 +(* Version: nested single recursion *)
   5.256 +
   5.257 +Goal "[| !!G ts. ts <= G ==> P G ts;\
   5.258 +\ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\
   5.259 +\         !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \
   5.260 +\         !!pn. pn : U ==> wt (the (body pn)); \
   5.261 +\         finite U; uG = mgt_call``U |] ==> \
   5.262 +\ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})";
   5.263 +by (cut_facts_tac (premises()) 1);
   5.264 +by (induct_tac "n" 1);
   5.265 +by  (ALLGOALS Clarsimp_tac);
   5.266 +bd  card_seteq 1;
   5.267 +by    (Asm_simp_tac 1);
   5.268 +be   finite_imageI 1;
   5.269 +by  (Asm_full_simp_tac 1);
   5.270 +by  (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
   5.271 +br  ballI 1;
   5.272 +by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
   5.273 +by  (Fast_tac 1);
   5.274 +by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
   5.275 +br ballI 1;
   5.276 +by (case_tac "mgt_call pn : G" 1);
   5.277 +by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
   5.278 +by  (Fast_tac 1);
   5.279 +by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
   5.280 +byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4];
   5.281 +by   (eresolve_tac (tl(tl(tl(premises())))) 4);
   5.282 +by   (Fast_tac 1);
   5.283 +be  Suc_leD 1;
   5.284 +bd finite_subset 1;
   5.285 +be  finite_imageI 1;
   5.286 +by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1);
   5.287 +qed_spec_mp "nesting_lemma";
   5.288 +
   5.289 +Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> \
   5.290 +\ G|-{=}.BODY pn.{->}";
   5.291 +br BodyN 1;
   5.292 +be conseq2 1;
   5.293 +by (Force_tac 1);
   5.294 +qed "MGT_BodyN";
   5.295 +
   5.296 +(* requires BodyN, com_det *)
   5.297 +Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
   5.298 +by (res_inst_tac [("P","%G ts. G||-ts"),("U","dom body")] nesting_lemma 1);
   5.299 +be          hoare_derivs.asm 1;
   5.300 +be         MGT_BodyN 1;
   5.301 +br        finite_dom_body 3;
   5.302 +be       MGF_lemma1 1;
   5.303 +ba        2;
   5.304 +by       (Blast_tac 1);
   5.305 +by      (Clarsimp_tac 1);
   5.306 +by     (eatac WT_bodiesD 1 1);
   5.307 +br     le_refl 3;
   5.308 +by    Auto_tac;
   5.309 +qed "MGF";
   5.310 +
   5.311 +
   5.312 +(* Version: simultaneous recursion in call rule *)
   5.313 +
   5.314 +(* finiteness not really necessary here *)
   5.315 +Goalw [MGT_def]     "[| G Un (%pn. {=}.      BODY pn  .{->})``Procs \
   5.316 +\                         ||-(%pn. {=}. the (body pn) .{->})``Procs; \
   5.317 +\ finite Procs |] ==>   G ||-(%pn. {=}.      BODY pn  .{->})``Procs";
   5.318 +br hoare_derivs.Body 1;
   5.319 +be finite_pointwise 1;
   5.320 +ba  2;
   5.321 +by (Clarify_tac 1);
   5.322 +be  conseq2 1;
   5.323 +by Auto_tac;
   5.324 +qed "MGT_Body";
   5.325 +
   5.326 +(* requires empty, insert, com_det *)
   5.327 +Goal "[| state_not_singleton; WT_bodies; \
   5.328 +\ F<=(%pn. {=}.the (body pn).{->})``dom body |] ==> \
   5.329 +\    (%pn. {=}.     BODY pn .{->})``dom body||-F";
   5.330 +by (ftac finite_subset 1);
   5.331 +br  (finite_dom_body RS finite_imageI) 1;
   5.332 +by (rotate_tac 2 1);
   5.333 +by (make_imp_tac 1);
   5.334 +be finite_induct 1;
   5.335 +by  (ALLGOALS (clarsimp_tac (
   5.336 +	claset() addSIs [hoare_derivs.empty,hoare_derivs.insert],
   5.337 +	simpset() delsimps [range_composition])));
   5.338 +be MGF_lemma1 1;
   5.339 +by  (fast_tac (claset() addDs [WT_bodiesD]) 2);
   5.340 +by (Clarsimp_tac 1);
   5.341 +br hoare_derivs.asm 1;
   5.342 +by (fast_tac (claset() addIs [domI]) 1);
   5.343 +qed_spec_mp "MGF_lemma2_simult";
   5.344 +
   5.345 +(* requires Body, empty, insert, com_det *)
   5.346 +Goal "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c";
   5.347 +br MGF_lemma1 1;
   5.348 +ba   1;
   5.349 +ba  2;
   5.350 +by (Clarsimp_tac 1);
   5.351 +by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})``dom body" 1);
   5.352 +be  hoare_derivs.weaken 1;
   5.353 +by  (fast_tac (claset() addIs [domI]) 1);
   5.354 +br (finite_dom_body RSN (2,MGT_Body)) 1;
   5.355 +by (Simp_tac 1);
   5.356 +by (eatac MGF_lemma2_simult 1 1);
   5.357 +br subset_refl 1;
   5.358 +qed "MGF";
   5.359 +
   5.360 +(* requires Body+empty+insert / BodyN, com_det *)
   5.361 +bind_thm ("hoare_complete", MGF RS MGF_complete); 
   5.362 +
   5.363 +section "unused derived rules";
   5.364 +
   5.365 +Goal "G|-{%Z s. False}.c.{Q}";
   5.366 +br hoare_derivs.conseq 1;
   5.367 +by (Fast_tac 1);
   5.368 +qed "falseE";
   5.369 +
   5.370 +Goal "G|-{P}.c.{%Z s. True}";
   5.371 +br hoare_derivs.conseq 1;
   5.372 +by (fast_tac (claset() addSIs [falseE]) 1);
   5.373 +qed "trueI";
   5.374 +
   5.375 +Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \
   5.376 +\       ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}";
   5.377 +br hoare_derivs.conseq 1;
   5.378 +by (fast_tac (claset() addEs [conseq12]) 1);
   5.379 +qed "disj"; (* analogue conj non-derivable *)
   5.380 +
   5.381 +Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}";
   5.382 +br conseq12 1;
   5.383 +br  hoare_derivs.Skip 1;
   5.384 +by (Fast_tac 1);
   5.385 +qed "hoare_SkipI";
   5.386 +
   5.387 +
   5.388 +section "useful derived rules";
   5.389 +
   5.390 +Goal "{t}|-t";
   5.391 +br hoare_derivs.asm 1;
   5.392 +br subset_refl 1;
   5.393 +qed "single_asm";
   5.394 +
   5.395 +Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
   5.396 +br hoare_derivs.conseq 1;
   5.397 +by (Clarsimp_tac 1);
   5.398 +by (cut_facts_tac (premises()) 1);
   5.399 +by (Fast_tac 1);
   5.400 +qed "export_s";
   5.401 +
   5.402 +
   5.403 +Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> \
   5.404 +\   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}";
   5.405 +br export_s 1;
   5.406 +br hoare_derivs.Local 1;
   5.407 +be conseq2 1;
   5.408 +be spec 1;
   5.409 +qed "weak_Local";
   5.410 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/IMPP/Hoare.thy	Mon Jan 31 18:30:35 2000 +0100
     6.3 @@ -0,0 +1,99 @@
     6.4 +(*  Title:      HOL/IMPP/Hoare.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     David von Oheimb
     6.7 +    Copyright   1999 TUM
     6.8 +
     6.9 +Inductive definition of Hoare logic for partial correctness
    6.10 +Completeness is taken relative to completeness of the underlying logic
    6.11 +Two versions of completeness proof:
    6.12 +  nested single recursion vs. simultaneous recursion in call rule
    6.13 +*)
    6.14 +
    6.15 +Hoare = Natural + 
    6.16 +
    6.17 +types 'a assn = "'a => state => bool"
    6.18 +translations
    6.19 +      "a assn"   <= (type)"a => state => bool"
    6.20 +
    6.21 +constdefs
    6.22 +  state_not_singleton :: bool
    6.23 + "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *)
    6.24 +
    6.25 +  peek_and    :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)
    6.26 + "peek_and P p == %Z s. P Z s & p s"
    6.27 +
    6.28 +datatype 'a triple =
    6.29 +    triple ('a assn) com ('a assn)         ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
    6.30 +  
    6.31 +consts
    6.32 +  triple_valid ::            nat => 'a triple     => bool ( "|=_:_" [0 , 58] 57)
    6.33 +  hoare_valids ::  'a triple set => 'a triple set => bool ("_||=_"  [58, 58] 57)
    6.34 +  hoare_derivs ::"('a triple set *  'a triple set)   set"
    6.35 +syntax
    6.36 +  triples_valid::            nat => 'a triple set => bool ("||=_:_" [0 , 58] 57)
    6.37 +  hoare_valid  ::  'a triple set => 'a triple     => bool ("_|=_"   [58, 58] 57)
    6.38 +"@hoare_derivs"::  'a triple set => 'a triple set => bool ("_||-_"  [58, 58] 57)
    6.39 +"@hoare_deriv" ::  'a triple set => 'a triple     => bool ("_|-_"   [58, 58] 57)
    6.40 +
    6.41 +defs triple_valid_def  "|=n:t  ==  case t of {P}.c.{Q} =>
    6.42 +		                !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
    6.43 +translations          "||=n:G" == "Ball G (triple_valid n)"
    6.44 +defs hoare_valids_def"G||=ts   ==  !n. ||=n:G --> ||=n:ts"
    6.45 +translations         "G |=t  " == " G||={t}"
    6.46 +                     "G||-ts"  == "(G,ts) : hoare_derivs"
    6.47 +                     "G |-t"   == " G||-{t}"
    6.48 +
    6.49 +(* Most General Triples *)
    6.50 +constdefs MGT    :: com => state triple              ("{=}._.{->}" [60] 58)
    6.51 +         "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}"
    6.52 +
    6.53 +inductive hoare_derivs intrs
    6.54 +  
    6.55 +  empty    "G||-{}"
    6.56 +  insert"[| G |-t;  G||-ts |]
    6.57 +	==> G||-insert t ts"
    6.58 +
    6.59 +  asm	   "ts <= G ==>
    6.60 +	    G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
    6.61 +
    6.62 +  cut   "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
    6.63 +
    6.64 +  weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
    6.65 +
    6.66 +  conseq"!Z s. P  Z  s --> (? P' Q'. G|-{P'}.c.{Q'} &
    6.67 +                                  (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
    6.68 +         ==> G|-{P}.c.{Q}"
    6.69 +
    6.70 +
    6.71 +  Skip	"G|-{P}. SKIP .{P}"
    6.72 +
    6.73 +  Ass	"G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
    6.74 +
    6.75 +  Local	"G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
    6.76 +     ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
    6.77 +
    6.78 +  Comp	"[| G|-{P}.c.{Q};
    6.79 +	    G|-{Q}.d.{R} |]
    6.80 +	==> G|-{P}. (c;;d) .{R}"
    6.81 +
    6.82 +  If	"[| G|-{P &>        b }.c.{Q};
    6.83 +	    G|-{P &> (Not o b)}.d.{Q} |]
    6.84 +	==> G|-{P}. IF b THEN c ELSE d .{Q}"
    6.85 +
    6.86 +  Loop  "G|-{P &> b}.c.{P} ==>
    6.87 +	 G|-{P}. WHILE b DO c .{P &> (Not o b)}"
    6.88 +
    6.89 +(*
    6.90 +  BodyN	"(insert ({P}. BODY pn  .{Q}) G)
    6.91 +	  |-{P}.  the (body pn) .{Q} ==>
    6.92 +	 G|-{P}.       BODY pn  .{Q}"
    6.93 +*)
    6.94 +  Body	"[| G Un (%p. {P p}.      BODY p  .{Q p})``Procs
    6.95 +	      ||-(%p. {P p}. the (body p) .{Q p})``Procs |]
    6.96 +	==>  G||-(%p. {P p}.      BODY p  .{Q p})``Procs"
    6.97 +
    6.98 +  Call	   "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
    6.99 +	==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
   6.100 +	    X:=CALL pn(a) .{Q}"
   6.101 +
   6.102 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/IMPP/Misc.ML	Mon Jan 31 18:30:35 2000 +0100
     7.3 @@ -0,0 +1,135 @@
     7.4 +(*  Title:      HOL/IMPP/Misc.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     David von Oheimb
     7.7 +    Copyright   1999 TUM
     7.8 +*)
     7.9 +
    7.10 +section "state access";
    7.11 +
    7.12 +Goalw [getlocs_def] "getlocs (st g l) = l";
    7.13 +by (Simp_tac 1);
    7.14 +qed "getlocs_def2";
    7.15 +
    7.16 +Goalw [update_def] "s[Loc Y::=s<Y>] = s";
    7.17 +by (induct_tac "s" 1);
    7.18 +by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
    7.19 +br ext 1;
    7.20 +by (Simp_tac 1);
    7.21 +qed "update_Loc_idem2";
    7.22 +Addsimps[update_Loc_idem2];
    7.23 +
    7.24 +Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]";
    7.25 +by (induct_tac "X" 1);
    7.26 +by  Auto_tac;
    7.27 +by  (ALLGOALS (induct_tac "s"));
    7.28 +by  Auto_tac;
    7.29 +by  (ALLGOALS (rtac ext));
    7.30 +by  Auto_tac;
    7.31 +qed "update_overwrt";
    7.32 +Addsimps[update_overwrt];
    7.33 +
    7.34 +Goalw [update_def]"(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)";
    7.35 +by (induct_tac "s" 1);
    7.36 +by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
    7.37 +qed "getlocs_Loc_update";
    7.38 +Addsimps[getlocs_Loc_update];
    7.39 +
    7.40 +Goalw [update_def] "getlocs (s[Glb Y::=k]) = getlocs s";
    7.41 +by (induct_tac "s" 1);
    7.42 +by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
    7.43 +qed "getlocs_Glb_update";
    7.44 +Addsimps[getlocs_Glb_update];
    7.45 +
    7.46 +Goalw [setlocs_def] "getlocs (setlocs s l) = l";
    7.47 +by (induct_tac "s" 1);
    7.48 +by Auto_tac;
    7.49 +by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
    7.50 +qed "getlocs_setlocs";
    7.51 +Addsimps[getlocs_setlocs];
    7.52 +
    7.53 +Goal "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])";
    7.54 +by (induct_tac "Y" 1);
    7.55 +br ext 2;
    7.56 +by Auto_tac;
    7.57 +qed "getlocs_setlocs_lemma";
    7.58 +
    7.59 +(*unused*)
    7.60 +Goalw [hoare_valids_def] 
    7.61 +"!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
    7.62 +\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}";
    7.63 +by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
    7.64 +by (Clarsimp_tac 1);
    7.65 +by (dres_inst_tac [("x","s<Y>")] spec 1);
    7.66 +by (smp_tac 1 1);
    7.67 +bd spec 1;
    7.68 +by (dres_inst_tac [("x","s[Loc Y::=a s]")] spec 1);
    7.69 +by (Full_simp_tac 1);
    7.70 +by (mp_tac 1);
    7.71 +by (smp_tac 1 1);
    7.72 +by (Simp_tac 1);
    7.73 +qed "classic_Local_valid";
    7.74 +
    7.75 +Goal "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
    7.76 +\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}";
    7.77 +br export_s 1;
    7.78 +(*variant 1*)
    7.79 +br (hoare_derivs.Local RS conseq1) 1;
    7.80 +be  spec 1;
    7.81 +by (Force_tac 1);
    7.82 +(*variant 2
    7.83 +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);
    7.84 +by  (Clarsimp_tac 2);
    7.85 +br hoare_derivs.Local 1;
    7.86 +be spec 1;
    7.87 +*)
    7.88 +qed "classic_Local";
    7.89 +
    7.90 +Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
    7.91 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
    7.92 +br classic_Local 1;
    7.93 +by (ALLGOALS Clarsimp_tac);
    7.94 +be conseq12 1;
    7.95 +by (Clarsimp_tac 1);
    7.96 +bd sym 1;
    7.97 +by (Asm_full_simp_tac 1);
    7.98 +qed "classic_Local_indep";
    7.99 +
   7.100 +Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
   7.101 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
   7.102 +br export_s 1;
   7.103 +br hoare_derivs.Local 1;
   7.104 +by (Clarsimp_tac 1);
   7.105 +qed "Local_indep";
   7.106 +
   7.107 +Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
   7.108 +\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
   7.109 +br weak_Local 1;
   7.110 +by (ALLGOALS Clarsimp_tac);
   7.111 +qed "weak_Local_indep";
   7.112 +
   7.113 +
   7.114 +Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
   7.115 +br export_s 1;
   7.116 +by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<Y> = s<Y>")] (conseq12) 1);
   7.117 +by  (Clarsimp_tac 2);
   7.118 +br hoare_derivs.Local 1;
   7.119 +by (Clarsimp_tac 1);
   7.120 +br trueI 1;
   7.121 +qed "export_Local_invariant";
   7.122 +
   7.123 +Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
   7.124 +br classic_Local 1;
   7.125 +by (Clarsimp_tac 1);
   7.126 +br (trueI RS conseq12) 1;
   7.127 +by (Clarsimp_tac 1);
   7.128 +qed "classic_Local_invariant";
   7.129 +
   7.130 +Goal "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==> \
   7.131 +\ G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}. \
   7.132 +\ X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}";
   7.133 +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);
   7.134 +by  (asm_simp_tac  (simpset() addsimps [getlocs_setlocs_lemma]) 1);
   7.135 +by (Force_tac 1);
   7.136 +qed "Call_invariant";
   7.137 +
   7.138 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/IMPP/Misc.thy	Mon Jan 31 18:30:35 2000 +0100
     8.3 @@ -0,0 +1,19 @@
     8.4 +(*  Title:      HOL/IMPP/Misc.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     David von Oheimb
     8.7 +    Copyright   1999 TUM
     8.8 +
     8.9 +Several examples for Hoare logic
    8.10 +*)
    8.11 +Misc = Hoare +
    8.12 +
    8.13 +defs
    8.14 +  newlocs_def "newlocs       == %x. arbitrary"
    8.15 +  setlocs_def "setlocs s l'  == case s of st g l => st g l'"
    8.16 +  getlocs_def "getlocs s     == case s of st g l => l"
    8.17 +   update_def "update s vn v == case vn of
    8.18 +                              Glb gn => (case s of st g l => st (g(gn:=v)) l)
    8.19 +                            | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    8.20 +
    8.21 +end
    8.22 +  
    8.23 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/IMPP/Natural.ML	Mon Jan 31 18:30:35 2000 +0100
     9.3 @@ -0,0 +1,77 @@
     9.4 +(*  Title:      HOL/IMPP/Natural.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     David von Oheimb, TUM
     9.7 +    Copyright   1999 TUM
     9.8 +*)
     9.9 +
    9.10 +open Natural;
    9.11 +
    9.12 +AddIs evalc.intrs;
    9.13 +AddIs evaln.intrs;
    9.14 +
    9.15 +val evalc_elim_cases = map evalc.mk_cases
    9.16 +   ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t", 
    9.17 +    "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t",
    9.18 +    "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"];
    9.19 +val evaln_elim_cases = map evaln.mk_cases
    9.20 +   ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t",
    9.21 +    "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t",
    9.22 +    "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"];
    9.23 +val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
    9.24 +val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t";
    9.25 +
    9.26 +AddSEs evalc_elim_cases;
    9.27 +AddSEs evaln_elim_cases;
    9.28 +
    9.29 +(* evaluation of com is deterministic *)
    9.30 +Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    9.31 +be evalc.induct 1;
    9.32 +by (thin_tac "<?c,s1> -c-> s2" 8);
    9.33 +(*blast_tac needs Unify.search_bound := 40*)
    9.34 +by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
    9.35 +qed_spec_mp "com_det";
    9.36 +
    9.37 +Goal "<c,s> -n-> t ==> <c,s> -c-> t";
    9.38 +be evaln.induct 1;
    9.39 +by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
    9.40 +qed "evaln_evalc";
    9.41 +
    9.42 +goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)";
    9.43 +by (induct_tac "m'" 1);
    9.44 +by  Auto_tac;
    9.45 +qed_spec_mp "Suc_le_D";
    9.46 +
    9.47 +Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
    9.48 +by (cut_facts_tac (premises()) 1);
    9.49 +by (ftac Suc_le_D 1);
    9.50 +by (Clarify_tac 1);
    9.51 +by (eresolve_tac (premises()) 1);
    9.52 +qed "Suc_le_D_lemma";
    9.53 +
    9.54 +Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
    9.55 +be evaln.induct 1;
    9.56 +by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
    9.57 +by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
    9.58 +qed_spec_mp "evaln_nonstrict";
    9.59 +
    9.60 +Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
    9.61 +be evaln_nonstrict 1;
    9.62 +by Auto_tac;
    9.63 +qed "evaln_Suc";
    9.64 +
    9.65 +Goal "[| <c1,s1> -n1-> t1;  <c2,s2> -n2-> t2 |] ==> \
    9.66 +\   ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2";
    9.67 +by (cut_facts_tac [read_instantiate [("m","n1"),("n","n2")] nat_le_linear] 1);
    9.68 +by (blast_tac (claset() addDs [evaln_nonstrict]) 1);
    9.69 +qed "evaln_max2";
    9.70 +
    9.71 +Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t";
    9.72 +be evalc.induct 1;
    9.73 +by (ALLGOALS (REPEAT o etac exE));
    9.74 +by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
    9.75 +by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
    9.76 +qed "evalc_evaln";
    9.77 +
    9.78 +Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
    9.79 +by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1);
    9.80 +qed "eval_eq";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/IMPP/Natural.thy	Mon Jan 31 18:30:35 2000 +0100
    10.3 @@ -0,0 +1,89 @@
    10.4 +(*  Title:      HOL/IMPP/Natural.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
    10.7 +    Copyright   1999 TUM
    10.8 +
    10.9 +Natural semantics of commands
   10.10 +*)
   10.11 +
   10.12 +Natural = Com + 
   10.13 +
   10.14 +(** Execution of commands **)
   10.15 +consts	 evalc :: "(com * state *       state) set"
   10.16 +       "@evalc":: [com,state,    state] => bool	("<_,_>/ -c-> _" [0,0,  51] 51)
   10.17 +	 evaln :: "(com * state * nat * state) set"
   10.18 +       "@evaln":: [com,state,nat,state] => bool	("<_,_>/ -_-> _" [0,0,0,51] 51)
   10.19 +
   10.20 +translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
   10.21 +              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
   10.22 +
   10.23 +consts
   10.24 +  newlocs :: locals
   10.25 +  setlocs :: state => locals => state
   10.26 +  getlocs :: state => locals
   10.27 +  update  :: state => vname => val => state	("_/[_/::=/_]" [900,0,0] 900)
   10.28 +syntax (* IN Natural.thy *)
   10.29 +  loc :: state => locals    ("_<_>" [75,0] 75)
   10.30 +translations
   10.31 +  "s<X>" == "getlocs s X"
   10.32 +
   10.33 +inductive evalc
   10.34 +  intrs
   10.35 +    Skip    "<SKIP,s> -c-> s"
   10.36 +
   10.37 +    Assign  "<X :== a,s> -c-> s[X::=a s]"
   10.38 +
   10.39 +    Local   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
   10.40 +             <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
   10.41 +
   10.42 +    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
   10.43 +             <c0;; c1, s0> -c-> s2"
   10.44 +
   10.45 +    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
   10.46 +             <IF b THEN c0 ELSE c1, s> -c-> s1"
   10.47 +
   10.48 +    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
   10.49 +             <IF b THEN c0 ELSE c1, s> -c-> s1"
   10.50 +
   10.51 +    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
   10.52 +
   10.53 +    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
   10.54 +                <WHILE b DO c, s0> -c-> s2"
   10.55 +
   10.56 +    Body       "<the (body pn), s0> -c-> s1 ==>
   10.57 +                <BODY pn, s0> -c-> s1"
   10.58 +
   10.59 +    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
   10.60 +                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
   10.61 +                                         [X::=s1<Res>]"
   10.62 +
   10.63 +inductive evaln
   10.64 +  intrs
   10.65 +    Skip    "<SKIP,s> -n-> s"
   10.66 +
   10.67 +    Assign  "<X :== a,s> -n-> s[X::=a s]"
   10.68 +
   10.69 +    Local   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
   10.70 +             <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
   10.71 +
   10.72 +    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
   10.73 +             <c0;; c1, s0> -n-> s2"
   10.74 +
   10.75 +    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
   10.76 +             <IF b THEN c0 ELSE c1, s> -n-> s1"
   10.77 +
   10.78 +    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
   10.79 +             <IF b THEN c0 ELSE c1, s> -n-> s1"
   10.80 +
   10.81 +    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
   10.82 +
   10.83 +    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
   10.84 +                <WHILE b DO c, s0> -n-> s2"
   10.85 +
   10.86 +    Body       "<the (body pn), s0> -    n-> s1 ==>
   10.87 +                <BODY pn, s0> -Suc n-> s1"
   10.88 +
   10.89 +    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
   10.90 +                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
   10.91 +                                         [X::=s1<Res>]"
   10.92 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/IMPP/README.html	Mon Jan 31 18:30:35 2000 +0100
    11.3 @@ -0,0 +1,13 @@
    11.4 +<!-- $Id$ -->
    11.5 +<HTML><HEAD>
    11.6 +<TITLE>HOL/IMPP/README</TITLE>
    11.7 +</HEAD><BODY>
    11.8 +
    11.9 +<H2>IMPP--An imperative language with procedures</H2>
   11.10 +
   11.11 +This is an extension of <A HREF="../IMP/">IMP</A> with local variables
   11.12 +and mutually recursive procedures. For documentation see
   11.13 +<A HREF="http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html">
   11.14 +Hoare Logic for Mutual Recursion and Local Variables</A>.
   11.15 +
   11.16 +</BODY></HTML>
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/IMPP/ROOT.ML	Mon Jan 31 18:30:35 2000 +0100
    12.3 @@ -0,0 +1,9 @@
    12.4 +(*  Title:      HOL/IMPP/ROOT.ML
    12.5 +    ID:         $Id$
    12.6 +    Author:     David von Oheimb
    12.7 +    Copyright   1999 TUM
    12.8 +*)
    12.9 +
   12.10 +writeln"Root file for HOL/IMPP";
   12.11 +
   12.12 +use_thy "EvenOdd";
    13.1 --- a/src/HOL/IsaMakefile	Mon Jan 31 16:19:51 2000 +0100
    13.2 +++ b/src/HOL/IsaMakefile	Mon Jan 31 18:30:35 2000 +0100
    13.3 @@ -8,7 +8,7 @@
    13.4  
    13.5  default: HOL
    13.6  images: HOL HOL-Real TLA
    13.7 -test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
    13.8 +test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
    13.9    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
   13.10    HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   13.11    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \