--- a/src/HOL/IMPP/Com.ML Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Com.ML Sat Sep 17 20:14:30 2005 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
Goalw [body_def] "finite (dom body)";
@@ -9,9 +11,4 @@
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;
--- a/src/HOL/IMPP/Com.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Com.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,80 +2,89 @@
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 +
+header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
-types val = nat (* for the meta theory, this may be anything, but with
+theory Com
+imports Main
+begin
+
+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 :: type
-consts Arg, Res :: loc
+typedecl glb
+typedecl loc
+
+consts
+ Arg :: loc
+ Res :: loc
datatype vname = Glb glb | Loc loc
-types globs = glb => val
- locals = loc => val
+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::type
-consts st:: [globs , locals] => state
+typedecl state
+consts st :: "[globs , locals] => state"
*)
-types aexp = state => val
- bexp = state => bool
+types aexp = "state => val"
+ bexp = "state => bool"
-types pname
-arities pname :: type
+typedecl pname
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)
+ | 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)
+ | 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"
+defs body_def: "body == map_of bodies"
(* Well-typedness: all procedures called must exist *)
-consts WTs :: com set
-syntax WT :: com => bool
+consts WTs :: "com set"
+syntax WT :: "com => bool"
translations "WT c" == "c : WTs"
-inductive WTs intrs
+inductive WTs intros
- Skip "WT SKIP"
+ Skip: "WT SKIP"
- Assign "WT (X :== a)"
+ Assign: "WT (X :== a)"
- Local "WT c ==>
- WT (LOCAL Y := a IN c)"
+ Local: "WT c ==>
+ WT (LOCAL Y := a IN c)"
- Semi "[| WT c0; WT c1 |] ==>
- WT (c0;; c1)"
+ Semi: "[| WT c0; WT c1 |] ==>
+ WT (c0;; c1)"
- If "[| WT c0; WT c1 |] ==>
- WT (IF b THEN c0 ELSE c1)"
+ If: "[| WT c0; WT c1 |] ==>
+ WT (IF b THEN c0 ELSE c1)"
- While "WT c ==>
- WT (WHILE b DO c)"
+ While: "WT c ==>
+ WT (WHILE b DO c)"
- Body "body pn ~= None ==>
- WT (BODY pn)"
+ Body: "body pn ~= None ==>
+ WT (BODY pn)"
- Call "WT (BODY pn) ==>
- WT (X:=CALL pn(a))"
+ Call: "WT (BODY pn) ==>
+ WT (X:=CALL pn(a))"
+
+inductive_cases WTs_elim_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))"
constdefs
WT_bodies :: bool
- "WT_bodies == !(pn,b):set bodies. WT b"
+ "WT_bodies == !(pn,b):set bodies. WT b"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/IMPP/EvenOdd.ML Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML Sat Sep 17 20:14:30 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1999 TUM
*)
-section "even";
+section "even";
Goalw [even_def] "even 0";
by (Simp_tac 1);
@@ -71,14 +71,14 @@
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);
+ ("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);
+ ("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);
@@ -97,7 +97,7 @@
Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
by (rtac conseq1 1);
-by (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
+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;
--- a/src/HOL/IMPP/EvenOdd.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,20 +2,24 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 TUM
-
-Example of mutually recursive procedures verified with Hoare logic
*)
-EvenOdd = Misc +
+header {* Example of mutually recursive procedures verified with Hoare logic *}
-constdefs even :: nat => bool
+theory EvenOdd
+imports Misc
+begin
+
+constdefs
+ even :: "nat => bool"
"even n == 2 dvd n"
consts
- Even, Odd :: pname
-rules
- Even_neq_Odd "Even ~= Odd"
- Arg_neq_Res "Arg ~= Res"
+ Even :: pname
+ Odd :: pname
+axioms
+ Even_neq_Odd: "Even ~= Odd"
+ Arg_neq_Res: "Arg ~= Res"
constdefs
evn :: com
@@ -30,13 +34,15 @@
ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
defs
- bodies_def "bodies == [(Even,evn),(Odd,odd)]"
-
+ 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")
+ 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)"
+ 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 ()) *}
end
--- a/src/HOL/IMPP/Hoare.ML Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Hoare.ML Sat Sep 17 20:14:30 2005 +0200
@@ -6,8 +6,8 @@
Soundness and relative completeness of Hoare rules wrt operational semantics
*)
-Goalw [state_not_singleton_def]
- "state_not_singleton ==> !t. (!s::state. s = t) --> False";
+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])));
@@ -18,7 +18,7 @@
section "validity";
-Goalw [triple_valid_def]
+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";
@@ -105,16 +105,16 @@
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 (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.intrs)
- THEN_ALL_NEW Fast_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}";
@@ -178,8 +178,8 @@
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 (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 *)
@@ -212,18 +212,13 @@
by (Blast_tac 1);
qed "MGT_alternD";
-Goalw [MGT_def]
+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
+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 ==> \
@@ -234,15 +229,15 @@
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 (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'[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);
@@ -278,7 +273,7 @@
by (Fast_tac 1);
by (dtac finite_subset 1);
by (etac finite_imageI 1);
-by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
by (arith_tac 1);
qed_spec_mp "nesting_lemma";
@@ -329,8 +324,8 @@
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])));
+ 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);
@@ -354,7 +349,7 @@
qed "MGF'";
(* requires Body+empty+insert / BodyN, com_det *)
-bind_thm ("hoare_complete", MGF' RS MGF_complete);
+bind_thm ("hoare_complete", MGF' RS MGF_complete);
section "unused derived rules";
--- a/src/HOL/IMPP/Hoare.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Hoare.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,98 +2,106 @@
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 +
+header {* Inductive definition of Hoare logic for partial correctness *}
+
+theory Hoare
+imports Natural
+begin
+
+text {*
+ Completeness is taken relative to completeness of the underlying logic.
+
+ Two versions of completeness proof: nested single recursion
+ vs. simultaneous recursion in call rule
+*}
types 'a assn = "'a => state => bool"
translations
- "a assn" <= (type)"a => state => bool"
+ "a assn" <= (type)"a => state => bool"
constdefs
state_not_singleton :: bool
- "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *)
+ "state_not_singleton == \<exists>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"
+ "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)
-
+ 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"
+ 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)
+ 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')"
+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"
+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)
+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"
+inductive hoare_derivs intros
+
+ 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 *)
+ 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 *)
+ cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
- weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
+ 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}"
+ 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}"
+ Skip: "G|-{P}. SKIP .{P}"
- Ass "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{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}"
+ 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}"
+ 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}"
+ 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)}"
+ 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}"
+ 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"
+ 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}"
+ 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}"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/IMPP/Misc.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Misc.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,18 +2,22 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 TUM
+*)
-Several examples for Hoare logic
-*)
-Misc = Hoare +
+header {* Several examples for Hoare logic *}
+
+theory Misc
+imports Hoare
+begin
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)))"
+ 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)))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-
\ No newline at end of file
--- a/src/HOL/IMPP/Natural.ML Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Natural.ML Sat Sep 17 20:14:30 2005 +0200
@@ -4,21 +4,8 @@
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";
+AddIs evalc.intros;
+AddIs evaln.intros;
AddSEs evalc_elim_cases;
AddSEs evaln_elim_cases;
@@ -33,7 +20,7 @@
Goal "<c,s> -n-> t ==> <c,s> -c-> t";
by (etac evaln.induct 1);
-by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
+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'";
@@ -46,7 +33,7 @@
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.intrs THEN_ALL_NEW atac));
+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'";
@@ -64,7 +51,7 @@
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.intrs THEN_ALL_NEW atac));
+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)";
--- a/src/HOL/IMPP/Natural.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Natural.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,88 +2,111 @@
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 +
+header {* Natural semantics of commands *}
+
+theory Natural
+imports Com
+begin
(** 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)
+consts
+ evalc :: "(com * state * state) set"
+ evaln :: "(com * state * nat * state) set"
-translations "<c,s> -c-> s'" == "(c,s, s') : evalc"
- "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
+syntax
+ "@evalc":: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51)
+ "@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)
+ 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)
+ loc :: "state => locals" ("_<_>" [75,0] 75)
translations
"s<X>" == "getlocs s X"
inductive evalc
- intrs
- Skip "<SKIP,s> -c-> s"
+ intros
+ Skip: "<SKIP,s> -c-> s"
- Assign "<X :== a,s> -c-> s[X::=a 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>]"
+ 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"
+ 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"
+ 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"
+ 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"
+ 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"
+ 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"
+ 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>]"
+ 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"
+ intros
+ Skip: "<SKIP,s> -n-> s"
+
+ Assign: "<X :== a,s> -n-> s[X::=a 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"
- Local "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
- <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
+ IfTrue: "[| b s; <c0,s> -n-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -n-> s1"
- Semi "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
- <c0;; c1, s0> -n-> s2"
+ IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
+ <IF b THEN c0 ELSE c1, s> -n-> s1"
- IfTrue "[| b s; <c0,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"
- IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
- <IF b THEN c0 ELSE c1, s> -n-> s1"
+ Body: "<the (body pn), s0> - n-> s1 ==>
+ <BODY pn, s0> -Suc n-> s1"
- WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"
+ 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>]"
- 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"
+inductive_cases evalc_elim_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"
- 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>]"
+inductive_cases evaln_elim_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"
+
+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 ()) *}
+
end