# HG changeset patch # User nipkow # Date 908371591 -7200 # Node ID 7c2ddbaf8b8c67d2f42c3d70eb844fa413b7e79a # Parent b872b209db69397a0af869e9d60229162c0907da New many-sorted version. diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/Examples.ML --- a/src/HOL/Hoare/Examples.ML Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/Examples.ML Wed Oct 14 15:26:31 1998 +0200 @@ -1,94 +1,178 @@ (* Title: HOL/Hoare/Examples.thy ID: $Id$ - Author: Norbert Galm - Copyright 1995 TUM - -Various arithmetic examples. + Author: Norbert Galm & Tobias Nipkow + Copyright 1998 TUM *) -open Examples; +(*** ARITHMETIC ***) (*** multiplication by successive addition ***) -Goal - "{m=0 & s=0} \ -\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\ -\ {s = a*b}"; -by (hoare_tac 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); +Goal "|- VARS m s. \ +\ {m=0 & s=0} \ +\ WHILE m~=a \ +\ INV {s=m*b} \ +\ DO s := s+b; m := m+1 OD \ +\ {s = a*b}"; +by(hoare_tac (Asm_full_simp_tac) 1); qed "multiply_by_add"; - (*** Euclid's algorithm for GCD ***) -Goal -" {0 A!j ~= 0} \ +\ DO i := i+1 OD \ +\ {(i < length A --> A!i = 0) & \ +\ (i = length A --> (!j. j < length A --> A!j ~= 0))}"; +by (hoare_tac Asm_full_simp_tac 1); +by(blast_tac (claset() addSEs [less_SucE]) 1); +qed "zero_search"; + +(* +The `partition' procedure for quicksort. +`A' is the array to be sorted (modelled as a list). +Elements of A must be of class order to infer at the end +that the elements between u and l are equal to pivot. + +Ambiguity warnings of parser are due to := being used +both for assignment and list update. +*) +Goal +"[| leq == %A i. !k. k A!k <= pivot; \ +\ geq == %A i. !k. i pivot <= A!k |] ==> \ +\ |- VARS A u l.\ +\ {0 < length(A::('a::order)list)} \ +\ l := 0; u := length A - 1; \ +\ WHILE l <= u \ +\ INV {leq A l & geq A u & u A!k = pivot) & geq A l}"; +(* expand and delete abbreviations first *) +by(asm_simp_tac HOL_basic_ss 1); +by(REPEAT(etac thin_rl 1)); +by (hoare_tac Asm_full_simp_tac 1); + by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); + by(Clarify_tac 1); + by(asm_full_simp_tac (simpset() addsimps [nth_list_update] + addSolver cut_trans_tac) 1); + by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1); + br conjI 1; + by(Clarify_tac 1); + bd (pred_less_imp_le RS le_imp_less_Suc) 1; + by(blast_tac (claset() addSEs [less_SucE]) 1); + br less_imp_diff_less 1; + by(Blast_tac 1); + by(Clarify_tac 1); + by(asm_simp_tac (simpset() addsimps [nth_list_update] + addSolver cut_trans_tac) 1); + by(Clarify_tac 1); + by(trans_tac 1); +by(Clarify_tac 1); +by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); +br conjI 1; + by(Clarify_tac 1); + br order_antisym 1; + by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); + by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); +by(Clarify_tac 1); +by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); +qed "Partition"; diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/Examples.thy --- a/src/HOL/Hoare/Examples.thy Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/Examples.thy Wed Oct 14 15:26:31 1998 +0200 @@ -1,9 +1,9 @@ (* Title: HOL/Hoare/Examples.thy ID: $Id$ Author: Norbert Galm - Copyright 1995 TUM + Copyright 1998 TUM -Various arithmetic examples. +Various examples. *) Examples = Hoare + Arith2 diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/Hoare.ML --- a/src/HOL/Hoare/Hoare.ML Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/Hoare.ML Wed Oct 14 15:26:31 1998 +0200 @@ -1,226 +1,210 @@ (* Title: HOL/Hoare/Hoare.ML ID: $Id$ - Author: Norbert Galm & Tobias Nipkow - Copyright 1995 TUM + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM -The verification condition generation tactics. +Derivation of the proof rules and, most importantly, the VCG tactic. *) -open Hoare; - -(*** Hoare rules ***) +(*** The proof rules ***) -val SkipRule = prove_goalw thy [Spec_def,Skip_def] - "(!!s. p(s) ==> q(s)) ==> Spec p Skip q" - (fn prems => [fast_tac (claset() addIs prems) 1]); +Goalw [Valid_def] "p <= q ==> Valid p SKIP q"; +by(Auto_tac); +qed "SkipRule"; -val AssignRule = prove_goalw thy [Spec_def,Assign_def] - "(!!s. p s ==> q(%x. if x=v then e s else s x)) ==> Spec p (Assign v e) q" - (fn prems => [fast_tac (claset() addIs prems) 1]); +Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q"; +by(Auto_tac); +qed "BasicRule"; -val SeqRule = prove_goalw thy [Spec_def,Seq_def] - "[| Spec p c (%s. q s); Spec (%s. q s) c' r |] ==> Spec p (Seq c c') r" - (fn prems => [cut_facts_tac prems 1, Fast_tac 1]); +Goalw [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"; -val IfRule = prove_goalw thy [Spec_def,Cond_def] - "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \ -\ Spec (%s. q s) c r; Spec (%s. q' s) c' r |] \ -\ ==> Spec p (Cond b c c') r" - (fn [prem1,prem2,prem3] => - [REPEAT (rtac allI 1), - REPEAT (rtac impI 1), - dtac prem1 1, - cut_facts_tac [prem2,prem3] 1, - fast_tac (claset() addIs [prem1]) 1]); - -val strenthen_pre = prove_goalw thy [Spec_def] - "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q" - (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1, - fast_tac (claset() addIs [prem1]) 1]); +Goalw [Valid_def] + "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \ +\ Valid w c1 q; Valid w' c2 q |] \ +\ ==> Valid p (IF b THEN c1 ELSE c2 FI) q"; +by(Asm_simp_tac 1); +by(Blast_tac 1); +qed "CondRule"; -val lemma = prove_goalw thy [Spec_def,While_def] - "[| Spec (%s. I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \ -\ ==> Spec I (While b I c) q" - (fn [prem1,prem2] => - [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2, - etac thin_rl 1, res_inst_tac[("x","s")]spec 1, - res_inst_tac[("x","s'")]spec 1, induct_tac "n" 1, - Simp_tac 1, - fast_tac (claset() addIs [prem2]) 1, - simp_tac (simpset() addsimps [Seq_def]) 1, - cut_facts_tac [prem1] 1, fast_tac (claset() addIs [prem2]) 1]); +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; -val WhileRule = lemma RSN (2,strenthen_pre); +Goalw [Valid_def] + "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \ +\ ==> Valid p (WHILE b INV {i} DO c OD) q"; +by(Asm_simp_tac 1); +by(Clarify_tac 1); +bd lemma 1; +ba 2; +by(Blast_tac 1); +by(Blast_tac 1); +qed "WhileRule"; - -(*** meta_spec used in StateElimTac ***) +(*** The tactics ***) -val meta_spec = prove_goal HOL.thy - "(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))" - (fn prems => [resolve_tac prems 1]); - - -(**************************************************************************************************) -(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***) -(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)" ***) -(**************************************************************************************************) +(*****************************************************************************) +(** 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. For instance, (found,x,y) are **) +(** the variables of the Zero Search program. **) +(*****************************************************************************) -(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen - mit Namen von in nach um *) +local open HOLogic in -fun rename_abs (von,nach,Abs (s,t,trm)) = - if von=s - then Abs (nach,t,rename_abs (von,nach,trm)) - else Abs (s,t,rename_abs (von,nach,trm)) - | rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2) - | rename_abs (_,_,trm) =trm; +(** 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 _ = []; -(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen - mit Namen von in nach um. Vorgehen: - - Term t zu thoerem bestimmen - - Term t' zu t durch Umbenennen der Namen generieren - - Certified Term ct' zu t' erstellen - - Thoerem ct'==ct' anlegen - - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct' - abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *) - -fun ren_abs_thm (von,nach,theorem) = - equal_elim - (reflexive (cterm_of (#sign (rep_thm theorem)) - (rename_abs (von,nach,#prop (rep_thm theorem))))) - theorem; - +(** 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; -(****************************************************************************) -(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***) -(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***) -(*** - Instanziieren von freien Variablen im Theorem ***) -(*** - Composing des Subgoals mit dem Theorem ***) -(****************************************************************************) +(** maps [x1,...,xn] to (x1,...,xn) and types**) +fun mk_bodyC [] = Const ("()", unitT) + | 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; -(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden - - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *) +fun dest_Goal (Const ("Goal", _) $ P) = P; -fun comp_inst_ren_tac rens insts theorem i = - let fun compose_inst_ren_tac [] insts theorem i = - compose_tac (false, - cterm_instantiate insts theorem,nprems_of theorem) i - | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = - compose_inst_ren_tac rl insts - (ren_abs_thm (von,nach,theorem)) i - in compose_inst_ren_tac rens insts theorem i end; +(** 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; -(*************************************************************** *********) -(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***) -(*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***) -(****************************************************************************) +(** 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; + -(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen - aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an. - Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a") - wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) +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); + val cimpl = cterm_of (#sign (rep_thm thm)) impl + in prove_goalw_cterm [] cimpl (fn prems => + [cut_facts_tac prems 1,Blast_tac 1]) end; -fun pvars_of_term (name,trm) = - let fun add_vars (name,Free (s,t) $ trm,vl) = - if name=s then if trm mem vl then vl else trm::vl - else add_vars (name,trm,vl) - | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) - | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) - | add_vars (_,_,vl) =vl - in add_vars (name,trm,[]) end; +end; -(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i - - v::vl:(term) list Liste der zu eliminierenden Programmvariablen - - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird - z.B.: "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))" - - namexAll:string Name von ^ (hier "x") - - varx:term Term zu ^ (hier Var(("x",0),...)) - - varP:term Term zu ^ (hier Var(("P",0),...)) - - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) +(*****************************************************************************) +(** 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 **) +(*****************************************************************************) + +val Compl_Collect = prove_goal thy "-(Collect b) = {x. ~(b x)}" + (fn _ => [Fast_tac 1]); + +(**Simp_tacs**) - Vorgehen: - - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: - - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt - z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich - meta_spec zu "(!! s a. PROP P(s,a)) ==> (!! s. PROP P(s,x(s)))" - - Instanziierungen in meta_spec: - varx wird mit "%s:(type_pvar) state. s(pvar)" instanziiert - varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": - - zu Subgoal "!!s. s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": - trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) - - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: - trm1 = "s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber xs: - trm2 = "%xs. s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber restliche Vorkommen von s: - trm3 = "%s xs. s(Suc(0)) = xs ==> xs = 1" - - instanziiere varP mit trm3 -*) +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])); + +(*****************************************************************************) +(** 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) **) +(*****************************************************************************) -(* StateElimTac: tactic to eliminate all program variable from subgoal i - - applies to subgoals of the form "!!s:('a) state. P(s)", - i.e. the term Const("all",_) $ Abs ("s",pvar --> 'a,_) - - meta_spec has the form "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))" -*) +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]) 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]; -val StateElimTac = SUBGOAL (fn (Bi,i) => - let val Const _ $ Abs (_,Type ("fun",[_,type_pvar]),trm) = Bi - val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ - (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = - #prop (rep_thm meta_spec) - fun vtac v i st = st |> - let val cterm = cterm_of (#sign (rep_thm st)) - val (_,_,_ $ Abs (_,_,trm),_) = dest_state (st,i); - val (sname,trm0) = variant_abs ("s",dummyT,trm); - val xsname = variant_name ("xs",trm0); - val trm1 = subst_term (Free (sname,dummyT) $ v, - Syntax.free xsname,trm0) - val trm2 = Abs ("xs", type_pvar, - abstract_over (Syntax.free xsname,trm1)) - in - comp_inst_ren_tac - [(namexAll,pvar2pvarID v)] - [(cterm varx, - cterm (Abs ("s",Type ("nat",[]) --> type_pvar, - Bound 0 $ v))), - (cterm varP, - cterm (Abs ("s", Type ("nat",[]) --> type_pvar, - abstract_over (Free (sname,dummyT),trm2))))] - meta_spec i - end - fun vars_tac [] i = all_tac - | vars_tac (v::vl) i = vtac v i THEN vars_tac vl i - in - vars_tac (pvars_of_term (variant_abs ("s",dummyT,trm))) i - end); +fun BasicSimpTac tac = + simp_tac (HOL_basic_ss addsimps [mem_Collect_eq,split]) + 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)) )); -(*** tactics for verification condition generation ***) - -(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall - von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann - generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen - Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *) - -fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false) -and HoareRuleTac i pre_cond st = st |> - (*abstraction over st prevents looping*) - ( (WlpTac i THEN HoareRuleTac i pre_cond) - ORELSE - (FIRST[rtac SkipRule i, - rtac AssignRule i, - EVERY[rtac IfRule i, - HoareRuleTac (i+2) false, - HoareRuleTac (i+1) false], - EVERY[rtac WhileRule i, - Asm_full_simp_tac (i+2), - HoareRuleTac (i+1) true]] - THEN - (if pre_cond then (Asm_full_simp_tac i) else (atac i))) ); - -val hoare_tac = - SELECT_GOAL - (EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]); - +(** 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 b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/Hoare.thy Wed Oct 14 15:26:31 1998 +0200 @@ -1,196 +1,193 @@ (* Title: HOL/Hoare/Hoare.thy ID: $Id$ - Author: Norbert Galm & Tobias Nipkow - Copyright 1995 TUM + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM Sugared semantic embedding of Hoare logic. +Strictly speaking a shallow embedding (as implemented by Norbert Galm +following Mike Gordon) would suffice. Maybe the datatype com comes in useful +later. *) -Hoare = Arith + +Hoare = Main + types - pvar = nat (* encoding of program variables ( < 26! ) *) - 'a state = pvar => 'a (* program state *) - 'a exp = 'a state => 'a (* denotation of expressions *) - 'a bexp = 'a state => bool (* denotation of boolean expressions *) - 'a com = 'a state => 'a state => bool (* denotation of programs *) + 'a bexp = 'a set + 'a assn = 'a set + 'a fexp = 'a =>'a + +datatype + 'a com = Basic ('a fexp) + | Seq ('a com) ('a com) ("(_;/_)" [61,60] 60) + | Cond ('a bexp) ('a com) ('a com) ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + | While ('a bexp) ('a assn) ('a com) ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +syntax + "@assign" :: id => 'b => 'a com ("(2_ :=/ _ )" [70,65] 61) + "@annskip" :: 'a com ("SKIP") + +translations + "SKIP" == "Basic id" + +types 'a sem = 'a => 'a => bool + +consts iter :: nat => 'a bexp => 'a sem => 'a sem +primrec +"iter 0 b S = (%s s'. s ~: b & (s=s'))" +"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))" + +consts Sem :: 'a com => 'a sem +primrec +"Sem(Basic f) s s' = (s' = f s)" +"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" +"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & + (s ~: b --> Sem c2 s s'))" +"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" + +constdefs Valid :: ['a bexp, 'a com, 'a bexp] => bool + "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" -(* program syntax *) - nonterminals - prog + vars syntax - "@Skip" :: prog ("SKIP") - "@Assign" :: [id, 'a] => prog ("_ := _") - "@Seq" :: [prog, prog] => prog ("_;//_" [0,1000] 999) - "@If" :: [bool, prog, prog] => prog ("IF _//THEN// (_)//ELSE// (_)//END") - "@While" :: [bool, bool, prog] => prog ("WHILE _//DO {_}// (_)//END") - "@Spec" :: [bool, prog, bool] => bool ("{_}//_//{_}") - - -(* denotational semantics *) - -constdefs - Skip :: 'a com - "Skip s s' == (s=s')" - - Assign :: [pvar, 'a exp] => 'a com - "Assign v e s s' == (s' = (%x. if x=v then e(s) else s(x)))" + "" :: "id => vars" ("_") + "_vars" :: "[id, vars] => vars" ("_ _") - Seq :: ['a com, 'a com] => 'a com - "Seq c c' s s' == ? s''. c s s'' & c' s'' s'" - - Cond :: ['a bexp, 'a com, 'a com] => 'a com - "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')" - -consts - Iter :: [nat, 'a bexp, 'a com] => 'a com - -primrec - "Iter 0 b c = (%s s'.~b(s) & (s=s'))" - "Iter (Suc n) b c = (%s s'. b(s) & Seq c (Iter n b c) s s')" - -constdefs - While :: ['a bexp, 'a bexp, 'a com] => 'a com - "While b I c s s' == ? n. Iter n b c s s'" - - Spec :: ['a bexp, 'a com, 'a bexp] => bool - "Spec p c q == !s s'. c s s' --> p s --> q s'" +syntax + "@hoare_vars" :: [vars, 'a assn,'a com,'a assn] => bool + ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50) +syntax ("" output) + "@hoare" :: ['a assn,'a com,'a assn] => bool + ("|- {_} // _ // {_}" [0,55,0] 50) end ML - -(*** term manipulation ***) - -(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante, - freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *) +(** parse translations **) -fun name_in_term (name,Const (s,t)) = (name=s) - | name_in_term (name,Free (s,t)) = (name=s) - | name_in_term (name,Var (ix,t)) = (name= string_of_indexname ix) - | name_in_term (name,Abs (s,t,trm)) = (name=s) orelse - (name_in_term (name,trm)) - | name_in_term (name,trm1 $ trm2) = (name_in_term (name,trm1)) orelse - (name_in_term (name,trm2)) - | name_in_term (_,_) = false; - -(* variant_name:string (name:string,trm:term) liefert einen von name - abgewandelten Namen (durch Anhaengen von genuegend vielen "_"), der nicht - in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es auch Namen - von scheme-Variablen und von Lambda-Abstraktionen in trm *) +fun mk_abstuple [] body = absfree ("x", dummyT, body) + | mk_abstuple [v] body = absfree ((fst o dest_Free) v, dummyT, body) + | mk_abstuple (v::w) body = Syntax.const "split" $ + absfree ((fst o dest_Free) v, dummyT, mk_abstuple w body); -(*This could be done more simply by calling Term.variant, supplying a list of - all free, bound and scheme variables in the term.*) -fun variant_name (name,trm) = if name_in_term (name,trm) - then variant_name (name ^ "_",trm) - else name; - -(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus -trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt -wurden *) + +fun mk_fbody v e [] = Syntax.const "()" + | mk_fbody v e [x] = if v=x then e else x + | mk_fbody v e (x::xs) = Syntax.const "Pair" $ (if v=x then e else x) $ + mk_fbody v e xs; -fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm) - then nach - else Abs (s,t,subst_term (von,nach,trm)) - | subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2 - then nach - else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2) - | subst_term (von,nach,trm) =if von=trm - then nach - else trm; +fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs); -(* Translation between program vars ("a" - "z") and their encoding as - natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *) +(* bexp_tr & assn_tr *) +(*all meta-variables for bexp except for TRUE and FALSE are translated as if they + were boolean expressions*) + +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" + | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b; + +fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r; -fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z"; +(* com_tr *) + +fun assign_tr [Free (V,_),E] xs = Syntax.const "Basic" $ + mk_fexp (Free(V,dummyT)) E xs + | assign_tr ts _ = raise TERM ("assign_tr", ts); -fun pvarID2pvar s = - let fun rest2pvar (i,arg) = - if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg) - in rest2pvar(ord s - ord "a", Syntax.const "0") end; +fun com_tr (Const("@assign",_) $ Free (V,_) $ E) xs = + assign_tr [Free (V,dummyT),E] xs + | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f + | com_tr (Const ("Seq",_) $ c1 $ c2) xs = Syntax.const "Seq" $ + com_tr c1 xs $ com_tr c2 xs + | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs = Syntax.const "Cond" $ + bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const ("While",_) $ b $ I $ c) xs = Syntax.const "While" $ + bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr trm _ = trm; + +(* triple_tr *) -fun pvar2pvarID trm = - let - fun rest2pvarID (Const("0",_),i) =chr (i + ord "a") - | rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1) - in - rest2pvarID (trm,0) - end; +fun vars_tr (x as Free _) = [x] + | vars_tr (Const ("_vars", _) $ (x as Free _) $ vars) = x :: vars_tr vars + | vars_tr t = raise TERM ("vars_tr", [t]); + +fun hoare_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const "Valid" $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); + + + +val parse_translation = [("@hoare_vars", hoare_vars_tr)]; -(*** parse translations: syntax -> semantics ***) +(*****************************************************************************) + +(*** print translations ***) -(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID - darstellen, durch name $ pvarID2pvar(pvarID). Beispiel: - bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *) +fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) = + subst_bound (Syntax.free v, dest_abstuple body) + | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) + | dest_abstuple trm = trm; -fun term_tr (name,Free (s,t)) = if is_pvarID s - then Syntax.free name $ pvarID2pvar s - else Free (s,t) - | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm)) - | term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2) - | term_tr (name,trm) = trm; +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; -fun bool_tr B = - let val name = variant_name("s",B) - in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end; +fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t + | mk_ts (Abs(x,_,t)) = mk_ts t + | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b) + | mk_ts t = [t]; -fun exp_tr E = - let val name = variant_name("s",E) - in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end; +fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = + ((Syntax.free x)::(abs2list t), mk_ts t) + | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) + | mk_vts t = raise Match; + +fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" )) + | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs + else (true, (v, subst_bounds (xs,t))); + +fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true + | is_f (Abs(x,_,t)) = true + | is_f t = false; + +(* assn_tr' & bexp_tr'*) + +fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T + | assn_tr' (Const ("op Int",_) $ (Const ("Collect",_) $ T1) $ + (Const ("Collect",_) $ T2)) = + Syntax.const "op Int" $ dest_abstuple T1 $ dest_abstuple T2 + | assn_tr' t = t; -fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip" - | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) = - if is_pvarID V - then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E - else error("Not a valid program variable: " ^ quote V) - | prog_tr (Const ("@Seq",_) $ C $ C') = - Syntax.const "Seq" $ prog_tr C $ prog_tr C' - | prog_tr (Const ("@If",_) $ B $ C $ C') = - Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C' - | prog_tr (Const ("@While",_) $ B $ INV $ C) = - Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C; +fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T + | bexp_tr' t = t; + +(*com_tr' *) -fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q; +fun mk_assign f = + let val (vs, ts) = mk_vts f; + val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) + in if ch then Syntax.const "@assign" $ fst(which) $ snd(which) + else Syntax.const "@skip" end; -val parse_translation = [("@Spec",spec_tr)]; +fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f + else Syntax.const "Basic" $ f + | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $ + com_tr' c1 $ com_tr' c2 + | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $ + bexp_tr' b $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $ + bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' t = t; -(*** print translations: semantics -> syntax ***) - -(* Note: does not mark tokens *) - -(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch - entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel: - bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *) - -fun term_tr' (name,Free (s,t) $ trm) = - if name=s then Syntax.free (pvar2pvarID trm) - else Free (s,t) $ term_tr' (name,trm) - | term_tr' (name,Abs (s,t,trm)) = Abs (s,t,term_tr' (name,trm)) - | term_tr' (name,trm1 $ trm2) = term_tr' (name,trm1) $ term_tr' (name,trm2) - | term_tr' (name,trm) = trm; - -fun bexp_tr' (Abs(_,_,b)) = term_tr' (variant_abs ("s",dummyT,b)); - -fun exp_tr' (Abs(_,_,e)) = term_tr' (variant_abs ("s",dummyT,e)); - -fun com_tr' (Const ("Skip",_)) = Syntax.const "@Skip" - | com_tr' (Const ("Assign",_) $ v $ e) = - Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e - | com_tr' (Const ("Seq",_) $ c $ c') = - Syntax.const "@Seq" $ com_tr' c $ com_tr' c' - | com_tr' (Const ("Cond",_) $ b $ c $ c') = - Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c' - | com_tr' (Const ("While",_) $ b $ inv $ c) = - Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c; - -fun spec_tr' [p,c,q] = - Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q; - -val print_translation = [("Spec",spec_tr')]; +fun spec_tr' [p, c, q] = + Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q + +val print_translation = [("Valid", spec_tr')]; diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/List_Examples.ML --- a/src/HOL/Hoare/List_Examples.ML Wed Oct 14 11:51:11 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -Goal -"{x=X} \ -\ y := []; \ -\ WHILE x ~= [] \ -\ DO { rev(x)@y = rev(X)} \ -\ y := hd x # y; x := tl x \ -\ END \ -\{y=rev(X)}"; -by (hoare_tac 1); -by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); -by Safe_tac; -by (Asm_full_simp_tac 1); -qed "imperative_reverse"; - -Goal -"{x=X & y = Y} \ -\ x := rev(x); \ -\ WHILE x ~= [] \ -\ DO { rev(x)@y = X@Y} \ -\ y := hd x # y; x := tl x \ -\ END \ -\{y = X@Y}"; -by (hoare_tac 1); -by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); -by Safe_tac; -by (Asm_full_simp_tac 1); -qed "imperative_append"; diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/List_Examples.thy --- a/src/HOL/Hoare/List_Examples.thy Wed Oct 14 11:51:11 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -List_Examples = Hoare + List diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/README.html --- a/src/HOL/Hoare/README.html Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/README.html Wed Oct 14 15:26:31 1998 +0200 @@ -1,6 +1,59 @@ HOL/Hoare/ReadMe -

Semantic Embedding of Hoare Logic

+

Hoare Logic for a Simple WHILE Language

+ +

The language and logic

+ +This directory contains an implementation of Hoare logic for a simple WHILE +language. The are +
    +
  • SKIP +
  • _ := _ +
  • _ ; _ +
  • IF _ THEN _ ELSE _ FI +
  • WHILE _ INV {_} DO _ OD +
+Note that each WHILE-loop must be annotated with an invariant. +

+ +After loading theory Hoare, you can state goals of the form +

+|- VARS x y ... . {P} prog {Q}
+
+where prog is a program in the above language, P is the +precondition, Q the postcondition, and x y ... is the +list of all program variables in prog. The latter list must +be nonempty and it must include all variables that occur on the left-hand +side of an assignment in prof. Example: +
+|- VARS x. {x = a} x := x+1 {x = a+1}
+
+The (normal) variable a is merely used to record the initial +value of x and is not a program variable. Pre and postconditions +can be arbitrary HOL formulae mentioning both program variables and normal +variables. +

+ +The implementation hides reasoning in Hoare logic completely and provides a +tactic hoare_tac for generating the verification conditions in ordinary +logic: +

+by(hoare_tac tac i);
+
+applies the tactic to subgoal i and applies the parameter +tac to all generated verification conditions. A typical call is +
+by(hoare_tac Asm_full_simp_tac 1);
+
+which, given the example goal above, solves it completely. +

+ +IMPORTANT: +This is a logic of partial correctness. You can only prove that your program +does the right thing if it terminates, but not that it +terminates. + +

Notes on the implementation

This directory contains a sugared shallow semantic embedding of Hoare logic for a while language. The implementation closely follows

diff -r b872b209db69 -r 7c2ddbaf8b8c src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Wed Oct 14 11:51:11 1998 +0200 +++ b/src/HOL/Hoare/ROOT.ML Wed Oct 14 15:26:31 1998 +0200 @@ -1,10 +1,9 @@ (* Title: HOL/IMP/ROOT.ML ID: $Id$ Author: Tobias Nipkow - Copyright 1995 TUM + Copyright 1998 TUM *) HOL_build_completed; (*Make examples fail if HOL did*) use_thy "Examples"; -use_thy "List_Examples";