src/HOL/Hoare/hoare.ML
 author nipkow Tue Mar 11 15:04:24 2003 +0100 (2003-03-11) changeset 13857 11d7c5a8dbb7 parent 13737 e564c3d2d174 child 15531 08c8dad8e399 permissions -rw-r--r--
*** empty log message ***
 nipkow@13696 ` 1` ```(* Title: HOL/Hoare/Hoare.ML ``` nipkow@13696 ` 2` ``` ID: \$Id\$ ``` nipkow@13696 ` 3` ``` Author: Leonor Prensa Nieto & Tobias Nipkow ``` nipkow@13696 ` 4` ``` Copyright 1998 TUM ``` nipkow@13696 ` 5` nipkow@13696 ` 6` ```Derivation of the proof rules and, most importantly, the VCG tactic. ``` nipkow@13696 ` 7` ```*) ``` nipkow@13696 ` 8` nipkow@13857 ` 9` ```val SkipRule = thm"SkipRule"; ``` nipkow@13857 ` 10` ```val BasicRule = thm"BasicRule"; ``` nipkow@13857 ` 11` ```val SeqRule = thm"SeqRule"; ``` nipkow@13857 ` 12` ```val CondRule = thm"CondRule"; ``` nipkow@13857 ` 13` ```val WhileRule = thm"WhileRule"; ``` nipkow@13696 ` 14` nipkow@13696 ` 15` ```(*** The tactics ***) ``` nipkow@13696 ` 16` nipkow@13696 ` 17` ```(*****************************************************************************) ``` nipkow@13696 ` 18` ```(** The function Mset makes the theorem **) ``` nipkow@13696 ` 19` ```(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) ``` nipkow@13696 ` 20` ```(** where (x1,...,xn) are the variables of the particular program we are **) ``` nipkow@13696 ` 21` ```(** working on at the moment of the call **) ``` nipkow@13696 ` 22` ```(*****************************************************************************) ``` nipkow@13696 ` 23` nipkow@13696 ` 24` ```local open HOLogic in ``` nipkow@13696 ` 25` nipkow@13696 ` 26` ```(** maps (%x1 ... xn. t) to [x1,...,xn] **) ``` nipkow@13696 ` 27` ```fun abs2list (Const ("split",_) \$ (Abs(x,T,t))) = Free (x, T)::abs2list t ``` nipkow@13696 ` 28` ``` | abs2list (Abs(x,T,t)) = [Free (x, T)] ``` nipkow@13696 ` 29` ``` | abs2list _ = []; ``` nipkow@13696 ` 30` nipkow@13696 ` 31` ```(** maps {(x1,...,xn). t} to [x1,...,xn] **) ``` nipkow@13696 ` 32` ```fun mk_vars (Const ("Collect",_) \$ T) = abs2list T ``` nipkow@13696 ` 33` ``` | mk_vars _ = []; ``` nipkow@13696 ` 34` nipkow@13696 ` 35` ```(** abstraction of body over a tuple formed from a list of free variables. ``` nipkow@13696 ` 36` ```Types are also built **) ``` nipkow@13696 ` 37` ```fun mk_abstupleC [] body = absfree ("x", unitT, body) ``` nipkow@13696 ` 38` ``` | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v ``` nipkow@13696 ` 39` ``` in if w=[] then absfree (n, T, body) ``` nipkow@13696 ` 40` ``` else let val z = mk_abstupleC w body; ``` nipkow@13696 ` 41` ``` val T2 = case z of Abs(_,T,_) => T ``` nipkow@13696 ` 42` ``` | Const (_, Type (_,[_, Type (_,[T,_])])) \$ _ => T; ``` nipkow@13696 ` 43` ``` in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) ``` nipkow@13696 ` 44` ``` \$ absfree (n, T, z) end end; ``` nipkow@13696 ` 45` nipkow@13696 ` 46` ```(** maps [x1,...,xn] to (x1,...,xn) and types**) ``` nipkow@13696 ` 47` ```fun mk_bodyC [] = HOLogic.unit ``` nipkow@13696 ` 48` ``` | mk_bodyC (x::xs) = if xs=[] then x ``` nipkow@13696 ` 49` ``` else let val (n, T) = dest_Free x ; ``` nipkow@13696 ` 50` ``` val z = mk_bodyC xs; ``` nipkow@13696 ` 51` ``` val T2 = case z of Free(_, T) => T ``` nipkow@13696 ` 52` ``` | Const ("Pair", Type ("fun", [_, Type ``` nipkow@13696 ` 53` ``` ("fun", [_, T])])) \$ _ \$ _ => T; ``` nipkow@13696 ` 54` ``` in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) \$ x \$ z end; ``` nipkow@13696 ` 55` nipkow@13696 ` 56` ```fun dest_Goal (Const ("Goal", _) \$ P) = P; ``` nipkow@13696 ` 57` nipkow@13696 ` 58` ```(** maps a goal of the form: ``` nipkow@13737 ` 59` ``` 1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) ``` nipkow@13696 ` 60` ```fun get_vars thm = let val c = dest_Goal (concl_of (thm)); ``` nipkow@13696 ` 61` ``` val d = Logic.strip_assums_concl c; ``` nipkow@13696 ` 62` ``` val Const _ \$ pre \$ _ \$ _ = dest_Trueprop d; ``` nipkow@13696 ` 63` ``` in mk_vars pre end; ``` nipkow@13696 ` 64` nipkow@13696 ` 65` nipkow@13696 ` 66` ```(** Makes Collect with type **) ``` nipkow@13696 ` 67` ```fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm ``` nipkow@13696 ` 68` ``` in Collect_const t \$ trm end; ``` nipkow@13696 ` 69` nipkow@13696 ` 70` ```fun inclt ty = Const ("op <=", [ty,ty] ---> boolT); ``` nipkow@13696 ` 71` nipkow@13696 ` 72` ```(** Makes "Mset <= t" **) ``` nipkow@13696 ` 73` ```fun Mset_incl t = let val MsetT = fastype_of t ``` nipkow@13696 ` 74` ``` in mk_Trueprop ((inclt MsetT) \$ Free ("Mset", MsetT) \$ t) end; ``` nipkow@13696 ` 75` nipkow@13696 ` 76` nipkow@13696 ` 77` ```fun Mset thm = let val vars = get_vars(thm); ``` nipkow@13696 ` 78` ``` val varsT = fastype_of (mk_bodyC vars); ``` nipkow@13696 ` 79` ``` val big_Collect = mk_CollectC (mk_abstupleC vars ``` nipkow@13696 ` 80` ``` (Free ("P",varsT --> boolT) \$ mk_bodyC vars)); ``` nipkow@13696 ` 81` ``` val small_Collect = mk_CollectC (Abs("x",varsT, ``` nipkow@13696 ` 82` ``` Free ("P",varsT --> boolT) \$ Bound 0)); ``` nipkow@13696 ` 83` ``` val impl = implies \$ (Mset_incl big_Collect) \$ ``` nipkow@13696 ` 84` ``` (Mset_incl small_Collect); ``` nipkow@13696 ` 85` ``` in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end; ``` nipkow@13696 ` 86` nipkow@13696 ` 87` ```end; ``` nipkow@13696 ` 88` nipkow@13696 ` 89` nipkow@13696 ` 90` ```(*****************************************************************************) ``` nipkow@13696 ` 91` ```(** Simplifying: **) ``` nipkow@13696 ` 92` ```(** Some useful lemmata, lists and simplification tactics to control which **) ``` nipkow@13696 ` 93` ```(** theorems are used to simplify at each moment, so that the original **) ``` nipkow@13696 ` 94` ```(** input does not suffer any unexpected transformation **) ``` nipkow@13696 ` 95` ```(*****************************************************************************) ``` nipkow@13696 ` 96` nipkow@13696 ` 97` ```Goal "-(Collect b) = {x. ~(b x)}"; ``` nipkow@13696 ` 98` ```by (Fast_tac 1); ``` nipkow@13696 ` 99` ```qed "Compl_Collect"; ``` nipkow@13696 ` 100` nipkow@13696 ` 101` nipkow@13696 ` 102` ```(**Simp_tacs**) ``` nipkow@13696 ` 103` nipkow@13696 ` 104` ```val before_set2pred_simp_tac = ``` nipkow@13696 ` 105` ``` (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect])); ``` nipkow@13696 ` 106` nipkow@13696 ` 107` ```val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv])); ``` nipkow@13696 ` 108` nipkow@13696 ` 109` ```(*****************************************************************************) ``` nipkow@13696 ` 110` ```(** set2pred transforms sets inclusion into predicates implication, **) ``` nipkow@13696 ` 111` ```(** maintaining the original variable names. **) ``` nipkow@13696 ` 112` ```(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) ``` nipkow@13696 ` 113` ```(** Subgoals containing intersections (A Int B) or complement sets (-A) **) ``` nipkow@13696 ` 114` ```(** are first simplified by "before_set2pred_simp_tac", that returns only **) ``` nipkow@13696 ` 115` ```(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) ``` nipkow@13696 ` 116` ```(** transformed. **) ``` nipkow@13696 ` 117` ```(** This transformation may solve very easy subgoals due to a ligth **) ``` nipkow@13696 ` 118` ```(** simplification done by (split_all_tac) **) ``` nipkow@13696 ` 119` ```(*****************************************************************************) ``` nipkow@13696 ` 120` nipkow@13696 ` 121` ```fun set2pred i thm = let fun mk_string [] = "" ``` nipkow@13696 ` 122` ``` | mk_string (x::xs) = x^" "^mk_string xs; ``` nipkow@13696 ` 123` ``` val vars=get_vars(thm); ``` nipkow@13696 ` 124` ``` val var_string = mk_string (map (fst o dest_Free) vars); ``` nipkow@13696 ` 125` ``` in ((before_set2pred_simp_tac i) THEN_MAYBE ``` nipkow@13696 ` 126` ``` (EVERY [rtac subsetI i, ``` nipkow@13696 ` 127` ``` rtac CollectI i, ``` nipkow@13696 ` 128` ``` dtac CollectD i, ``` nipkow@13696 ` 129` ``` (TRY(split_all_tac i)) THEN_MAYBE ``` nipkow@13696 ` 130` ``` ((rename_tac var_string i) THEN ``` nipkow@13696 ` 131` ``` (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm ``` nipkow@13696 ` 132` ``` end; ``` nipkow@13696 ` 133` nipkow@13696 ` 134` ```(*****************************************************************************) ``` nipkow@13696 ` 135` ```(** BasicSimpTac is called to simplify all verification conditions. It does **) ``` nipkow@13696 ` 136` ```(** a light simplification by applying "mem_Collect_eq", then it calls **) ``` nipkow@13696 ` 137` ```(** MaxSimpTac, which solves subgoals of the form "A <= A", **) ``` nipkow@13696 ` 138` ```(** and transforms any other into predicates, applying then **) ``` nipkow@13696 ` 139` ```(** the tactic chosen by the user, which may solve the subgoal completely. **) ``` nipkow@13696 ` 140` ```(*****************************************************************************) ``` nipkow@13696 ` 141` nipkow@13696 ` 142` ```fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac]; ``` nipkow@13696 ` 143` nipkow@13696 ` 144` ```fun BasicSimpTac tac = ``` nipkow@13696 ` 145` ``` simp_tac ``` nipkow@13696 ` 146` ``` (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc]) ``` nipkow@13696 ` 147` ``` THEN_MAYBE' MaxSimpTac tac; ``` nipkow@13696 ` 148` nipkow@13696 ` 149` ```(** HoareRuleTac **) ``` nipkow@13696 ` 150` nipkow@13857 ` 151` ```fun WlpTac Mlem tac i = ``` nipkow@13857 ` 152` ``` rtac SeqRule i THEN HoareRuleTac Mlem tac false (i+1) ``` nipkow@13696 ` 153` ```and HoareRuleTac Mlem tac pre_cond i st = st |> ``` nipkow@13696 ` 154` ``` (*abstraction over st prevents looping*) ``` nipkow@13696 ` 155` ``` ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i) ``` nipkow@13696 ` 156` ``` ORELSE ``` nipkow@13696 ` 157` ``` (FIRST[rtac SkipRule i, ``` nipkow@13696 ` 158` ``` EVERY[rtac BasicRule i, ``` nipkow@13696 ` 159` ``` rtac Mlem i, ``` nipkow@13696 ` 160` ``` split_simp_tac i], ``` nipkow@13696 ` 161` ``` EVERY[rtac CondRule i, ``` nipkow@13696 ` 162` ``` HoareRuleTac Mlem tac false (i+2), ``` nipkow@13696 ` 163` ``` HoareRuleTac Mlem tac false (i+1)], ``` nipkow@13696 ` 164` ``` EVERY[rtac WhileRule i, ``` nipkow@13696 ` 165` ``` BasicSimpTac tac (i+2), ``` nipkow@13696 ` 166` ``` HoareRuleTac Mlem tac true (i+1)] ] ``` nipkow@13696 ` 167` ``` THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) )); ``` nipkow@13696 ` 168` nipkow@13696 ` 169` nipkow@13696 ` 170` ```(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **) ``` nipkow@13696 ` 171` ```(** the final verification conditions **) ``` nipkow@13696 ` 172` ``` ``` nipkow@13696 ` 173` ```fun hoare_tac tac i thm = ``` nipkow@13696 ` 174` ``` let val Mlem = Mset(thm) ``` nipkow@13696 ` 175` ``` in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end; ```