# HG changeset patch # User wenzelm # Date 1188398768 -7200 # Node ID a297ae4ff188dc67366cf62fe354d20b1cb7b5bd # Parent 33da394f0888cd1133b3b083b0c058174e693dfe added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy); diff -r 33da394f0888 -r a297ae4ff188 src/HOL/Hoare/hoare_tac.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/hoare_tac.ML Wed Aug 29 16:46:08 2007 +0200 @@ -0,0 +1,165 @@ +(* Title: HOL/Hoare/hoare_tac.ML + ID: $Id$ + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM + +Derivation of the proof rules and, most importantly, the VCG tactic. +*) + +(*** 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; + +(** maps a goal of the form: + 1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) +fun get_vars thm = let val c = Logic.unprotect (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 (@{const_name HOL.less_eq}, [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 Goal.prove (ProofContext.init (Thm.theory_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 val var_names = map (fst o dest_Free) (get_vars thm) 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_params_tac var_names 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 @{thm 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 @{thm SkipRule} i, + EVERY[rtac @{thm BasicRule} i, + rtac Mlem i, + split_simp_tac i], + EVERY[rtac @{thm CondRule} i, + HoareRuleTac Mlem tac false (i+2), + HoareRuleTac Mlem tac false (i+1)], + EVERY[rtac @{thm 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;