# HG changeset patch # User nipkow # Date 1036587698 -3600 # Node ID 631460c31a1f8efa456b869d85dd517e8879cd50 # Parent 3e48dcd25746c6c8ac4cf004e2872fbc32178aa8 a new pointer example and some syntactic sugar diff -r 3e48dcd25746 -r 631460c31a1f src/HOL/Hoare/Hoare.ML --- a/src/HOL/Hoare/Hoare.ML Tue Nov 05 15:59:17 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,217 +0,0 @@ -(* Title: HOL/Hoare/Hoare.ML - ID: $Id$ - Author: Leonor Prensa Nieto & Tobias Nipkow - Copyright 1998 TUM - -Derivation of the proof rules and, most importantly, the VCG tactic. -*) - -(*** The proof rules ***) - -Goalw [thm "Valid_def"] "p <= q ==> Valid p (Basic id) q"; -by (Auto_tac); -qed "SkipRule"; - -Goalw [thm "Valid_def"] "p <= {s. (f s):q} ==> Valid p (Basic f) q"; -by (Auto_tac); -qed "BasicRule"; - -Goalw [thm "Valid_def"] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R"; -by (Asm_simp_tac 1); -by (Blast_tac 1); -qed "SeqRule"; - -Goalw [thm "Valid_def"] - "p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \ -\ ==> Valid w c1 q ==> Valid w' c2 q \ -\ ==> Valid p (Cond b c1 c2) q"; -by (Asm_simp_tac 1); -by (Blast_tac 1); -qed "CondRule"; - -Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \ -\ ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b"; -by (induct_tac "n" 1); - by (Asm_simp_tac 1); -by (Simp_tac 1); -by (Blast_tac 1); -val lemma = result() RS spec RS spec RS mp RS mp; - -Goalw [thm "Valid_def"] - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \ -\ ==> Valid p (While b j c) q"; -by (Asm_simp_tac 1); -by (Clarify_tac 1); -by (dtac lemma 1); -by (assume_tac 2); -by (Blast_tac 1); -by (Blast_tac 1); -qed "WhileRule'"; - -Goal - "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \ -\ ==> Valid p (While b i c) q"; -by (rtac WhileRule' 1); -by (ALLGOALS assume_tac); -qed "WhileRule"; - -(*** The tactics ***) - -(*****************************************************************************) -(** The function Mset makes the theorem **) -(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) -(** where (x1,...,xn) are the variables of the particular program we are **) -(** working on at the moment of the call **) -(*****************************************************************************) - -local open HOLogic in - -(** maps (%x1 ... xn. t) to [x1,...,xn] **) -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] - | abs2list _ = []; - -(** maps {(x1,...,xn). t} to [x1,...,xn] **) -fun mk_vars (Const ("Collect",_) $ T) = abs2list T - | mk_vars _ = []; - -(** abstraction of body over a tuple formed from a list of free variables. -Types are also built **) -fun mk_abstupleC [] body = absfree ("x", unitT, body) - | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v - in if w=[] then absfree (n, T, body) - else let val z = mk_abstupleC w body; - val T2 = case z of Abs(_,T,_) => T - | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T; - in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) - $ absfree (n, T, z) end end; - -(** maps [x1,...,xn] to (x1,...,xn) and types**) -fun mk_bodyC [] = HOLogic.unit - | mk_bodyC (x::xs) = if xs=[] then x - else let val (n, T) = dest_Free x ; - val z = mk_bodyC xs; - val T2 = case z of Free(_, T) => T - | Const ("Pair", Type ("fun", [_, Type - ("fun", [_, T])])) $ _ $ _ => T; - in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end; - -fun dest_Goal (Const ("Goal", _) $ P) = P; - -(** maps a goal of the form: - 1. [| P |] ==> |- VARS x1 ... xn. {._.} _ {._.} or to [x1,...,xn]**) -fun get_vars thm = let val c = dest_Goal (concl_of (thm)); - val d = Logic.strip_assums_concl c; - val Const _ $ pre $ _ $ _ = dest_Trueprop d; - in mk_vars pre end; - - -(** Makes Collect with type **) -fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm - in Collect_const t $ trm end; - -fun inclt ty = Const ("op <=", [ty,ty] ---> boolT); - -(** Makes "Mset <= t" **) -fun Mset_incl t = let val MsetT = fastype_of t - in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end; - - -fun Mset thm = let val vars = get_vars(thm); - val varsT = fastype_of (mk_bodyC vars); - val big_Collect = mk_CollectC (mk_abstupleC vars - (Free ("P",varsT --> boolT) $ mk_bodyC vars)); - val small_Collect = mk_CollectC (Abs("x",varsT, - Free ("P",varsT --> boolT) $ Bound 0)); - val impl = implies $ (Mset_incl big_Collect) $ - (Mset_incl small_Collect); - in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; - -end; - - -(*****************************************************************************) -(** Simplifying: **) -(** Some useful lemmata, lists and simplification tactics to control which **) -(** theorems are used to simplify at each moment, so that the original **) -(** input does not suffer any unexpected transformation **) -(*****************************************************************************) - -Goal "-(Collect b) = {x. ~(b x)}"; -by (Fast_tac 1); -qed "Compl_Collect"; - - -(**Simp_tacs**) - -val before_set2pred_simp_tac = - (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect])); - -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv])); - -(*****************************************************************************) -(** set2pred transforms sets inclusion into predicates implication, **) -(** maintaining the original variable names. **) -(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) -(** Subgoals containing intersections (A Int B) or complement sets (-A) **) -(** are first simplified by "before_set2pred_simp_tac", that returns only **) -(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) -(** transformed. **) -(** This transformation may solve very easy subgoals due to a ligth **) -(** simplification done by (split_all_tac) **) -(*****************************************************************************) - -fun set2pred i thm = let fun mk_string [] = "" - | mk_string (x::xs) = x^" "^mk_string xs; - val vars=get_vars(thm); - val var_string = mk_string (map (fst o dest_Free) vars); - in ((before_set2pred_simp_tac i) THEN_MAYBE - (EVERY [rtac subsetI i, - rtac CollectI i, - dtac CollectD i, - (TRY(split_all_tac i)) THEN_MAYBE - ((rename_tac var_string i) THEN - (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm - end; - -(*****************************************************************************) -(** BasicSimpTac is called to simplify all verification conditions. It does **) -(** a light simplification by applying "mem_Collect_eq", then it calls **) -(** MaxSimpTac, which solves subgoals of the form "A <= A", **) -(** and transforms any other into predicates, applying then **) -(** the tactic chosen by the user, which may solve the subgoal completely. **) -(*****************************************************************************) - -fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac]; - -fun BasicSimpTac tac = - simp_tac - (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc]) - THEN_MAYBE' MaxSimpTac tac; - -(** HoareRuleTac **) - -fun WlpTac Mlem tac i = rtac SeqRule i THEN HoareRuleTac Mlem tac false (i+1) -and HoareRuleTac Mlem tac pre_cond i st = st |> - (*abstraction over st prevents looping*) - ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i) - ORELSE - (FIRST[rtac SkipRule i, - EVERY[rtac BasicRule i, - rtac Mlem i, - split_simp_tac i], - EVERY[rtac CondRule i, - HoareRuleTac Mlem tac false (i+2), - HoareRuleTac Mlem tac false (i+1)], - EVERY[rtac WhileRule i, - BasicSimpTac tac (i+2), - HoareRuleTac Mlem tac true (i+1)] ] - THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) )); - - -(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **) -(** the final verification conditions **) - -fun hoare_tac tac i thm = - let val Mlem = Mset(thm) - in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end; diff -r 3e48dcd25746 -r 631460c31a1f src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Tue Nov 05 15:59:17 2002 +0100 +++ b/src/HOL/Hoare/Hoare.thy Wed Nov 06 14:01:38 2002 +0100 @@ -10,7 +10,7 @@ *) theory Hoare = Main -files ("Hoare.ML"): +files ("hoare.ML"): types 'a bexp = "'a set" @@ -193,7 +193,7 @@ print_translation {* [("Valid", spec_tr')] *} -use "Hoare.ML" +use "hoare.ML" method_setup vcg = {* Method.no_args diff -r 3e48dcd25746 -r 631460c31a1f src/HOL/Hoare/Pointers.thy --- a/src/HOL/Hoare/Pointers.thy Tue Nov 05 15:59:17 2002 +0100 +++ b/src/HOL/Hoare/Pointers.thy Wed Nov 06 14:01:38 2002 +0100 @@ -16,6 +16,30 @@ theory Pointers = Hoare: +(* field access and update *) +syntax + "@faccess" :: "'a option => ('a \ 'v option) => 'v" + ("_^:_" [65,1000] 65) + "@fassign" :: "'p option => id => 'v => 's com" + ("(2_^._ :=/ _)" [70,1000,65] 61) +translations + "p^:f" == "f(the p)" + "p^.f := e" => "f := fun_upd f (the p) e" + + +text{* An example due to Suzuki: *} + +lemma "|- VARS v n. + {w = Some w0 & x = Some x0 & y = Some y0 & z = Some z0 & + distinct[w0,x0,y0,z0]} + w^.v := (1::int); w^.n := x; + x^.v := 2; x^.n := y; + y^.v := 3; y^.n := z; + z^.v := 4; x^.n := z + {w^:n^:n^:v = 4}" +by vcg_simp + + section"The heap" subsection"Paths in the heap" @@ -33,12 +57,18 @@ done lemma [simp]: "path h (Some a) as z = - (as = [] \ z = Some a \ (\bs. as = a#bs \ path h (h a) bs z))" + (as = [] \ z = Some a \ (\bs. as = a#bs \ path h (h a) bs z))" apply(case_tac as) apply fastsimp apply fastsimp done +lemma [simp]: "\x. path f x (as@bs) z = (\y. path f x as y \ path f y bs z)" +by(induct as, simp+) + +lemma [simp]: "\x. u \ set as \ path (f(u\v)) x as y = path f x as y" +by(induct as, simp, simp add:eq_sym_conv) + subsection "Lists on the heap" constdefs @@ -66,13 +96,13 @@ lemma list_app: "\x. list h x (as@bs) = (\y. path h x as y \ list h y bs)" by(induct as, simp, clarsimp) -lemma list_hd_not_in_tl: "list h (h a) as \ a \ set as" +lemma list_hd_not_in_tl[simp]: "list h (h a) as \ a \ set as" apply (clarsimp simp add:in_set_conv_decomp) apply(frule list_app[THEN iffD1]) apply(fastsimp dest:list_app[THEN iffD1] list_unique) done -lemma list_distinct: "\x. list h x as \ distinct as" +lemma list_distinct[simp]: "\x. list h x as \ distinct as" apply(induct as, simp) apply(fastsimp dest:list_hd_not_in_tl) done @@ -101,7 +131,7 @@ WHILE p ~= None INV {\As' Bs'. list tl p As' \ list tl q Bs' \ set As' \ set Bs' = {} \ rev As' @ Bs' = rev As @ Bs} - DO r := p; p := tl(the p); tl := tl(the r := q); q := r OD + DO r := p; p := p^:tl; r^.tl := q; q := r OD {list tl q (rev As @ Bs)}" apply vcg_simp @@ -113,7 +143,6 @@ apply clarify apply(rename_tac As' b Bs') -apply(frule list_distinct) apply clarsimp apply(rename_tac As'') apply(rule_tac x = As'' in exI) @@ -132,9 +161,9 @@ lemma "|- VARS tl p. {list tl p As \ X \ set As} - WHILE p ~= None & p ~= Some X - INV {p ~= None & (\As'. list tl p As' \ X \ set As')} - DO p := tl(the p) OD + WHILE p \ None \ p \ Some X + INV {p \ None \ (\As'. list tl p As' \ X \ set As')} + DO p := p^:tl OD {p = Some X}" apply vcg_simp apply(case_tac p) @@ -150,9 +179,9 @@ lemma "|- VARS tl p. {path tl p As (Some X)} - WHILE p ~= None & p ~= Some X - INV {p ~= None & (\As'. path tl p As' (Some X))} - DO p := tl(the p) OD + WHILE p \ None \ p \ Some X + INV {p \ None \ (\As'. path tl p As' (Some X))} + DO p := p^:tl OD {p = Some X}" apply vcg_simp apply(case_tac p) @@ -183,9 +212,9 @@ lemma "|- VARS tl p. {Some X \ ({(Some x,tl x) |x. True}^* `` {p})} - WHILE p ~= None & p ~= Some X - INV {p ~= None & Some X \ ({(Some x,tl x) |x. True}^* `` {p})} - DO p := tl(the p) OD + WHILE p \ None \ p \ Some X + INV {p \ None \ Some X \ ({(Some x,tl x) |x. True}^* `` {p})} + DO p := p^:tl OD {p = Some X}" apply vcg_simp apply(case_tac p) @@ -201,10 +230,10 @@ text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*} lemma "|- VARS tl p. - {p ~= None & X \ ({(x,y). tl x = Some y}^* `` {the p})} - WHILE p ~= None & p ~= Some X - INV {p ~= None & X \ ({(x,y). tl x = Some y}^* `` {the p})} - DO p := tl(the p) OD + {p \ None \ X \ ({(x,y). tl x = Some y}^* `` {the p})} + WHILE p \ None \ p \ Some X + INV {p \ None \ X \ ({(x,y). tl x = Some y}^* `` {the p})} + DO p := p^:tl OD {p = Some X}" apply vcg_simp apply clarsimp @@ -214,4 +243,116 @@ apply clarsimp done +subsection{*Merging two lists*} + +consts merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" + +recdef merge "measure(%(xs,ys,f). size xs + size ys)" +"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) + else y # merge(x#xs,ys,f))" +"merge(x#xs,[],f) = x # merge(xs,[],f)" +"merge([],y#ys,f) = y # merge([],ys,f)" +"merge([],[],f) = []" + +lemma imp_disjCL: "(P|Q \ R) = ((P \ R) \ (~P \ Q \ R))" +by blast + +declare imp_disjL[simp del] imp_disjCL[simp] + +lemma "|- VARS hd tl p q r s. + {list tl p Ps \ list tl q Qs \ set Ps \ set Qs = {} \ + (p \ None \ q \ None)} + IF q = None \ p \ None \ p^:hd \ q^:hd + THEN r := p; p := p^:tl ELSE r := q; q := q^:tl FI; + s := r; + WHILE p \ None \ q \ None + INV {EX rs ps qs a. path tl r rs s \ list tl p ps \ list tl q qs \ + distinct(a # ps @ qs @ rs) \ s = Some a \ + merge(Ps,Qs,\x y. hd x \ hd y) = + rs @ a # merge(ps,qs,\x y. hd x \ hd y) \ + (tl a = p \ tl a = q)} + DO IF q = None \ p \ None \ p^:hd \ q^:hd + THEN s^.tl := p; p := p^:tl ELSE s^.tl := q; q := q^:tl FI; + s := s^:tl + OD + {list tl r (merge(Ps,Qs,\x y. hd x \ hd y))}" +apply vcg_simp + +apply clarsimp +apply(rule conjI) +apply clarsimp +apply(rule exI, rule conjI, rule disjI1, rule refl) +apply (fastsimp) +apply(rule conjI) +apply clarsimp +apply(rule exI, rule conjI, rule disjI1, rule refl) +apply clarsimp +apply(rule exI) +apply(rule conjI) +apply assumption +apply(rule exI) +apply(rule conjI) +apply(rule exI) +apply(rule conjI) +apply(rule refl) +apply assumption +apply (fastsimp) +apply(case_tac p) +apply clarsimp +apply(rule exI, rule conjI, rule disjI1, rule refl) +apply (fastsimp) +apply clarsimp +apply(rule exI, rule conjI, rule disjI1, rule refl) +apply(rule exI) +apply(rule conjI) +apply(rule exI) +apply(rule conjI) +apply(rule refl) +apply assumption +apply (fastsimp) + +apply clarsimp +apply(rule conjI) +apply clarsimp +apply(rule_tac x = "rs @ [a]" in exI) +apply simp +apply(rule_tac x = "bs" in exI) +apply (fastsimp simp:eq_sym_conv) + +apply(rule conjI) +apply clarsimp +apply(rule_tac x = "rs @ [a]" in exI) +apply simp +apply(rule_tac x = "bs" in exI) +apply(rule conjI) +apply (simp add:eq_sym_conv) +apply(rule exI) +apply(rule conjI) +apply(rule_tac x = bsa in exI) +apply(rule conjI) +apply(rule refl) +apply (simp add:eq_sym_conv) +apply (fastsimp simp:eq_sym_conv) +apply(case_tac p) +apply clarsimp +apply(rule_tac x = "rs @ [a]" in exI) +apply simp +apply(rule_tac x = "bs" in exI) +apply (fastsimp simp:eq_sym_conv) + +apply clarsimp +apply(rule_tac x = "rs @ [a]" in exI) +apply simp +apply(rule exI) +apply(rule conjI) +apply(rule_tac x = bs in exI) +apply(rule conjI) +apply(rule refl) +apply (simp add:eq_sym_conv) +apply(rule_tac x = bsa in exI) +apply (fastsimp simp:eq_sym_conv) + +apply(clarsimp simp add:list_app) +done + end diff -r 3e48dcd25746 -r 631460c31a1f src/HOL/Hoare/hoare.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/hoare.ML Wed Nov 06 14:01:38 2002 +0100 @@ -0,0 +1,217 @@ +(* Title: HOL/Hoare/Hoare.ML + ID: $Id$ + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM + +Derivation of the proof rules and, most importantly, the VCG tactic. +*) + +(*** The proof rules ***) + +Goalw [thm "Valid_def"] "p <= q ==> Valid p (Basic id) q"; +by (Auto_tac); +qed "SkipRule"; + +Goalw [thm "Valid_def"] "p <= {s. (f s):q} ==> Valid p (Basic f) q"; +by (Auto_tac); +qed "BasicRule"; + +Goalw [thm "Valid_def"] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R"; +by (Asm_simp_tac 1); +by (Blast_tac 1); +qed "SeqRule"; + +Goalw [thm "Valid_def"] + "p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \ +\ ==> Valid w c1 q ==> Valid w' c2 q \ +\ ==> Valid p (Cond b c1 c2) q"; +by (Asm_simp_tac 1); +by (Blast_tac 1); +qed "CondRule"; + +Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \ +\ ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b"; +by (induct_tac "n" 1); + by (Asm_simp_tac 1); +by (Simp_tac 1); +by (Blast_tac 1); +val lemma = result() RS spec RS spec RS mp RS mp; + +Goalw [thm "Valid_def"] + "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \ +\ ==> Valid p (While b j c) q"; +by (Asm_simp_tac 1); +by (Clarify_tac 1); +by (dtac lemma 1); +by (assume_tac 2); +by (Blast_tac 1); +by (Blast_tac 1); +qed "WhileRule'"; + +Goal + "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \ +\ ==> Valid p (While b i c) q"; +by (rtac WhileRule' 1); +by (ALLGOALS assume_tac); +qed "WhileRule"; + +(*** The tactics ***) + +(*****************************************************************************) +(** The function Mset makes the theorem **) +(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) +(** where (x1,...,xn) are the variables of the particular program we are **) +(** working on at the moment of the call **) +(*****************************************************************************) + +local open HOLogic in + +(** maps (%x1 ... xn. t) to [x1,...,xn] **) +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; + +(** maps {(x1,...,xn). t} to [x1,...,xn] **) +fun mk_vars (Const ("Collect",_) $ T) = abs2list T + | mk_vars _ = []; + +(** abstraction of body over a tuple formed from a list of free variables. +Types are also built **) +fun mk_abstupleC [] body = absfree ("x", unitT, body) + | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v + in if w=[] then absfree (n, T, body) + else let val z = mk_abstupleC w body; + val T2 = case z of Abs(_,T,_) => T + | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T; + in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) + $ absfree (n, T, z) end end; + +(** maps [x1,...,xn] to (x1,...,xn) and types**) +fun mk_bodyC [] = HOLogic.unit + | mk_bodyC (x::xs) = if xs=[] then x + else let val (n, T) = dest_Free x ; + val z = mk_bodyC xs; + val T2 = case z of Free(_, T) => T + | Const ("Pair", Type ("fun", [_, Type + ("fun", [_, T])])) $ _ $ _ => T; + in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end; + +fun dest_Goal (Const ("Goal", _) $ P) = P; + +(** maps a goal of the form: + 1. [| P |] ==> |- VARS x1 ... xn. {._.} _ {._.} or to [x1,...,xn]**) +fun get_vars thm = let val c = dest_Goal (concl_of (thm)); + val d = Logic.strip_assums_concl c; + val Const _ $ pre $ _ $ _ = dest_Trueprop d; + in mk_vars pre end; + + +(** Makes Collect with type **) +fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm + in Collect_const t $ trm end; + +fun inclt ty = Const ("op <=", [ty,ty] ---> boolT); + +(** Makes "Mset <= t" **) +fun Mset_incl t = let val MsetT = fastype_of t + in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end; + + +fun Mset thm = let val vars = get_vars(thm); + val varsT = fastype_of (mk_bodyC vars); + val big_Collect = mk_CollectC (mk_abstupleC vars + (Free ("P",varsT --> boolT) $ mk_bodyC vars)); + val small_Collect = mk_CollectC (Abs("x",varsT, + Free ("P",varsT --> boolT) $ Bound 0)); + val impl = implies $ (Mset_incl big_Collect) $ + (Mset_incl small_Collect); + in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; + +end; + + +(*****************************************************************************) +(** Simplifying: **) +(** Some useful lemmata, lists and simplification tactics to control which **) +(** theorems are used to simplify at each moment, so that the original **) +(** input does not suffer any unexpected transformation **) +(*****************************************************************************) + +Goal "-(Collect b) = {x. ~(b x)}"; +by (Fast_tac 1); +qed "Compl_Collect"; + + +(**Simp_tacs**) + +val before_set2pred_simp_tac = + (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect])); + +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv])); + +(*****************************************************************************) +(** set2pred transforms sets inclusion into predicates implication, **) +(** maintaining the original variable names. **) +(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) +(** Subgoals containing intersections (A Int B) or complement sets (-A) **) +(** are first simplified by "before_set2pred_simp_tac", that returns only **) +(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) +(** transformed. **) +(** This transformation may solve very easy subgoals due to a ligth **) +(** simplification done by (split_all_tac) **) +(*****************************************************************************) + +fun set2pred i thm = let fun mk_string [] = "" + | mk_string (x::xs) = x^" "^mk_string xs; + val vars=get_vars(thm); + val var_string = mk_string (map (fst o dest_Free) vars); + in ((before_set2pred_simp_tac i) THEN_MAYBE + (EVERY [rtac subsetI i, + rtac CollectI i, + dtac CollectD i, + (TRY(split_all_tac i)) THEN_MAYBE + ((rename_tac var_string i) THEN + (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm + end; + +(*****************************************************************************) +(** BasicSimpTac is called to simplify all verification conditions. It does **) +(** a light simplification by applying "mem_Collect_eq", then it calls **) +(** MaxSimpTac, which solves subgoals of the form "A <= A", **) +(** and transforms any other into predicates, applying then **) +(** the tactic chosen by the user, which may solve the subgoal completely. **) +(*****************************************************************************) + +fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac]; + +fun BasicSimpTac tac = + simp_tac + (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc]) + THEN_MAYBE' MaxSimpTac tac; + +(** HoareRuleTac **) + +fun WlpTac Mlem tac i = rtac SeqRule i THEN HoareRuleTac Mlem tac false (i+1) +and HoareRuleTac Mlem tac pre_cond i st = st |> + (*abstraction over st prevents looping*) + ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i) + ORELSE + (FIRST[rtac SkipRule i, + EVERY[rtac BasicRule i, + rtac Mlem i, + split_simp_tac i], + EVERY[rtac CondRule i, + HoareRuleTac Mlem tac false (i+2), + HoareRuleTac Mlem tac false (i+1)], + EVERY[rtac WhileRule i, + BasicSimpTac tac (i+2), + HoareRuleTac Mlem tac true (i+1)] ] + THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) )); + + +(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **) +(** the final verification conditions **) + +fun hoare_tac tac i thm = + let val Mlem = Mset(thm) + in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;