# HG changeset patch # User wenzelm # Date 1188378628 -7200 # Node ID 41c81e23c08ddaf8c91d4a4aaa2b452f11757405 # Parent 01fd2863d7c8b2a4941d07c3d6a62a357810ed56 removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system); diff -r 01fd2863d7c8 -r 41c81e23c08d src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Wed Aug 29 10:20:22 2007 +0200 +++ b/src/HOL/Hoare/Hoare.thy Wed Aug 29 11:10:28 2007 +0200 @@ -10,7 +10,7 @@ *) theory Hoare imports Main -uses ("hoare.ML") begin +begin types 'a bexp = "'a set" @@ -225,7 +225,167 @@ done -use "hoare.ML" +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} + +ML {* +(*** 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 **) +(*****************************************************************************) + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + + +ML {* +(**Simp_tacs**) + +val before_set2pred_simp_tac = + (simp_tac (HOL_basic_ss addsimps [@{thm Collect_conj_eq} RS sym, @{thm 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; +*} method_setup vcg = {* Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *} diff -r 01fd2863d7c8 -r 41c81e23c08d src/HOL/Hoare/HoareAbort.thy --- a/src/HOL/Hoare/HoareAbort.thy Wed Aug 29 10:20:22 2007 +0200 +++ b/src/HOL/Hoare/HoareAbort.thy Wed Aug 29 11:10:28 2007 +0200 @@ -7,7 +7,7 @@ *) theory HoareAbort imports Main -uses ("hoareAbort.ML") begin +begin types 'a bexp = "'a set" @@ -235,7 +235,169 @@ lemma AbortRule: "p \ {s. False} \ Valid p Abort q" by(auto simp:Valid_def) -use "hoareAbort.ML" + +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} + +ML {* +(*** 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 **) +(*****************************************************************************) + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + + +ML {* +(**Simp_tacs**) + +val before_set2pred_simp_tac = + (simp_tac (HOL_basic_ss addsimps [@{thm Collect_conj_eq} RS sym, @{thm 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, + rtac @{thm AbortRule} 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; +*} method_setup vcg = {* Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *} diff -r 01fd2863d7c8 -r 41c81e23c08d src/HOL/Hoare/hoare.ML --- a/src/HOL/Hoare/hoare.ML Wed Aug 29 10:20:22 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,171 +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. -*) - -val SkipRule = thm"SkipRule"; -val BasicRule = thm"BasicRule"; -val SeqRule = thm"SeqRule"; -val CondRule = thm"CondRule"; -val WhileRule = thm"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; - -(** 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 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 01fd2863d7c8 -r 41c81e23c08d src/HOL/Hoare/hoareAbort.ML --- a/src/HOL/Hoare/hoareAbort.ML Wed Aug 29 10:20:22 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,173 +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. -*) - -val SkipRule = thm"SkipRule"; -val BasicRule = thm"BasicRule"; -val AbortRule = thm"AbortRule"; -val SeqRule = thm"SeqRule"; -val CondRule = thm"CondRule"; -val WhileRule = thm"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; - -(** 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 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, - rtac AbortRule 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 01fd2863d7c8 -r 41c81e23c08d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Aug 29 10:20:22 2007 +0200 +++ b/src/HOL/IsaMakefile Wed Aug 29 11:10:28 2007 +0200 @@ -369,10 +369,10 @@ HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \ - Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \ + Hoare/Examples.thy Hoare/Hoare.thy \ Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \ Hoare/ROOT.ML Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ - Hoare/hoareAbort.ML Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \ + Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \ Hoare/Separation.thy Hoare/SepLogHeap.thy \ Hoare/document/root.tex Hoare/document/root.bib @$(ISATOOL) usedir $(OUT)/HOL Hoare @@ -667,7 +667,7 @@ ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \ ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \ ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \ - ex/Refute_Examples.thy ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \ + ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \ ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \ ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy diff -r 01fd2863d7c8 -r 41c81e23c08d src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Wed Aug 29 10:20:22 2007 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Aug 29 11:10:28 2007 +0200 @@ -10,7 +10,7 @@ theory SVC_Oracle imports Main -uses "svc_funcs.ML" ("svc_oracle.ML") +uses "svc_funcs.ML" begin consts @@ -22,6 +22,108 @@ oracle svc_oracle ("term") = Svc.oracle -use "svc_oracle.ML" +ML {* +(* +Installing the oracle for SVC (Stanford Validity Checker) + +The following code merely CALLS the oracle; + the soundness-critical functions are at svc_funcs.ML + +Based upon the work of Søren T. Heilmann +*) + + +(*Generalize an Isabelle formula, replacing by Vars + all subterms not intelligible to SVC.*) +fun svc_abstract t = + let + (*The oracle's result is given to the subgoal using compose_tac because + its premises are matched against the assumptions rather than used + to make subgoals. Therefore , abstraction must copy the parameters + precisely and make them available to all generated Vars.*) + val params = Term.strip_all_vars t + and body = Term.strip_all_body t + val Us = map #2 params + val nPar = length params + val vname = ref "V_a" + val pairs = ref ([] : (term*term) list) + fun insert t = + let val T = fastype_of t + val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) + in vname := Symbol.bump_string (!vname); + pairs := (t, v) :: !pairs; + v + end; + fun replace t = + case t of + Free _ => t (*but not existing Vars, lest the names clash*) + | Bound _ => t + | _ => (case AList.lookup Pattern.aeconv (!pairs) t of + SOME v => v + | NONE => insert t) + (*abstraction of a numeric literal*) + fun lit (t as Const(@{const_name HOL.zero}, _)) = t + | lit (t as Const(@{const_name HOL.one}, _)) = t + | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t + | lit t = replace t + (*abstraction of a real/rational expression*) + fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x) + | rat t = lit t + (*abstraction of an integer expression: no div, mod*) + fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x) + | int t = lit t + (*abstraction of a natural number expression: no minus*) + fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) + | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) + | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) + | nat t = lit t + (*abstraction of a relation: =, <, <=*) + fun rel (T, c $ x $ y) = + if T = HOLogic.realT then c $ (rat x) $ (rat y) + else if T = HOLogic.intT then c $ (int x) $ (int y) + else if T = HOLogic.natT then c $ (nat x) $ (nat y) + else if T = HOLogic.boolT then c $ (fm x) $ (fm y) + else replace (c $ x $ y) (*non-numeric comparison*) + (*abstraction of a formula*) + and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q) + | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q) + | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q) + | fm ((c as Const("Not", _)) $ p) = c $ (fm p) + | fm ((c as Const("True", _))) = c + | fm ((c as Const("False", _))) = c + | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) + | fm (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) + | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) + | fm t = replace t + (*entry point, and abstraction of a meta-formula*) + fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p) + | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) + | mt t = fm t (*it might be a formula*) + in (list_all (params, mt body), !pairs) end; + + +(*Present the entire subgoal to the oracle, assumptions and all, but possibly + abstracted. Use via compose_tac, which performs no lifting but will + instantiate variables.*) + +fun svc_tac i st = + let + val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i) + val th = svc_oracle (Thm.theory_of_thm st) abs_goal + in compose_tac (false, th, 0) i st end + handle TERM _ => no_tac st; + + +(*check if user has SVC installed*) +fun svc_enabled () = getenv "SVC_HOME" <> ""; +fun if_svc_enabled f x = if svc_enabled () then f x else (); +*} end diff -r 01fd2863d7c8 -r 41c81e23c08d src/HOL/ex/svc_oracle.ML --- a/src/HOL/ex/svc_oracle.ML Wed Aug 29 10:20:22 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -(* Title: HOL/SVC_Oracle.ML - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1999 University of Cambridge - -Installing the oracle for SVC (Stanford Validity Checker) - -The following code merely CALLS the oracle; - the soundness-critical functions are at HOL/Tools/svc_funcs.ML - -Based upon the work of Soren T. Heilmann -*) - - -(*Generalize an Isabelle formula, replacing by Vars - all subterms not intelligible to SVC.*) -fun svc_abstract t = - let - (*The oracle's result is given to the subgoal using compose_tac because - its premises are matched against the assumptions rather than used - to make subgoals. Therefore , abstraction must copy the parameters - precisely and make them available to all generated Vars.*) - val params = Term.strip_all_vars t - and body = Term.strip_all_body t - val Us = map #2 params - val nPar = length params - val vname = ref "V_a" - val pairs = ref ([] : (term*term) list) - fun insert t = - let val T = fastype_of t - val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) - in vname := Symbol.bump_string (!vname); - pairs := (t, v) :: !pairs; - v - end; - fun replace t = - case t of - Free _ => t (*but not existing Vars, lest the names clash*) - | Bound _ => t - | _ => (case AList.lookup Pattern.aeconv (!pairs) t of - SOME v => v - | NONE => insert t) - (*abstraction of a numeric literal*) - fun lit (t as Const(@{const_name HOL.zero}, _)) = t - | lit (t as Const(@{const_name HOL.one}, _)) = t - | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t - | lit t = replace t - (*abstraction of a real/rational expression*) - fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x) - | rat t = lit t - (*abstraction of an integer expression: no div, mod*) - fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x) - | int t = lit t - (*abstraction of a natural number expression: no minus*) - fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) - | nat t = lit t - (*abstraction of a relation: =, <, <=*) - fun rel (T, c $ x $ y) = - if T = HOLogic.realT then c $ (rat x) $ (rat y) - else if T = HOLogic.intT then c $ (int x) $ (int y) - else if T = HOLogic.natT then c $ (nat x) $ (nat y) - else if T = HOLogic.boolT then c $ (fm x) $ (fm y) - else replace (c $ x $ y) (*non-numeric comparison*) - (*abstraction of a formula*) - and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q) - | fm ((c as Const("Not", _)) $ p) = c $ (fm p) - | fm ((c as Const("True", _))) = c - | fm ((c as Const("False", _))) = c - | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm t = replace t - (*entry point, and abstraction of a meta-formula*) - fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p) - | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) - | mt t = fm t (*it might be a formula*) - in (list_all (params, mt body), !pairs) end; - - -(*Present the entire subgoal to the oracle, assumptions and all, but possibly - abstracted. Use via compose_tac, which performs no lifting but will - instantiate variables.*) - -fun svc_tac i st = - let - val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i) - val th = svc_oracle (Thm.theory_of_thm st) abs_goal - in compose_tac (false, th, 0) i st end - handle TERM _ => no_tac st; - - -(*check if user has SVC installed*) -fun svc_enabled () = getenv "SVC_HOME" <> ""; -fun if_svc_enabled f x = if svc_enabled () then f x else ();