removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
authorwenzelm
Wed Aug 29 11:10:28 2007 +0200 (2007-08-29)
changeset 2447041c81e23c08d
parent 24469 01fd2863d7c8
child 24471 d7cf53c1085f
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/IsaMakefile
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_oracle.ML
     1.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Aug 29 10:20:22 2007 +0200
     1.2 +++ b/src/HOL/Hoare/Hoare.thy	Wed Aug 29 11:10:28 2007 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  *)
     1.5  
     1.6  theory Hoare  imports Main
     1.7 -uses ("hoare.ML") begin
     1.8 +begin
     1.9  
    1.10  types
    1.11      'a bexp = "'a set"
    1.12 @@ -225,7 +225,167 @@
    1.13  done
    1.14  
    1.15  
    1.16 -use "hoare.ML"
    1.17 +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *}
    1.18 +
    1.19 +ML {*
    1.20 +(*** The tactics ***)
    1.21 +
    1.22 +(*****************************************************************************)
    1.23 +(** The function Mset makes the theorem                                     **)
    1.24 +(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
    1.25 +(** where (x1,...,xn) are the variables of the particular program we are    **)
    1.26 +(** working on at the moment of the call                                    **)
    1.27 +(*****************************************************************************)
    1.28 +
    1.29 +local open HOLogic in
    1.30 +
    1.31 +(** maps (%x1 ... xn. t) to [x1,...,xn] **)
    1.32 +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    1.33 +  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    1.34 +  | abs2list _ = [];
    1.35 +
    1.36 +(** maps {(x1,...,xn). t} to [x1,...,xn] **)
    1.37 +fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    1.38 +  | mk_vars _ = [];
    1.39 +
    1.40 +(** abstraction of body over a tuple formed from a list of free variables. 
    1.41 +Types are also built **)
    1.42 +fun mk_abstupleC []     body = absfree ("x", unitT, body)
    1.43 +  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    1.44 +                               in if w=[] then absfree (n, T, body)
    1.45 +        else let val z  = mk_abstupleC w body;
    1.46 +                 val T2 = case z of Abs(_,T,_) => T
    1.47 +                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    1.48 +       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    1.49 +          $ absfree (n, T, z) end end;
    1.50 +
    1.51 +(** maps [x1,...,xn] to (x1,...,xn) and types**)
    1.52 +fun mk_bodyC []      = HOLogic.unit
    1.53 +  | mk_bodyC (x::xs) = if xs=[] then x 
    1.54 +               else let val (n, T) = dest_Free x ;
    1.55 +                        val z = mk_bodyC xs;
    1.56 +                        val T2 = case z of Free(_, T) => T
    1.57 +                                         | Const ("Pair", Type ("fun", [_, Type
    1.58 +                                            ("fun", [_, T])])) $ _ $ _ => T;
    1.59 +                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    1.60 +
    1.61 +(** maps a goal of the form:
    1.62 +        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    1.63 +fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    1.64 +                        val d = Logic.strip_assums_concl c;
    1.65 +                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    1.66 +      in mk_vars pre end;
    1.67 +
    1.68 +
    1.69 +(** Makes Collect with type **)
    1.70 +fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    1.71 +                      in Collect_const t $ trm end;
    1.72 +
    1.73 +fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
    1.74 +
    1.75 +(** Makes "Mset <= t" **)
    1.76 +fun Mset_incl t = let val MsetT = fastype_of t 
    1.77 +                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    1.78 +
    1.79 +
    1.80 +fun Mset thm = let val vars = get_vars(thm);
    1.81 +                   val varsT = fastype_of (mk_bodyC vars);
    1.82 +                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    1.83 +                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    1.84 +                   val small_Collect = mk_CollectC (Abs("x",varsT,
    1.85 +                           Free ("P",varsT --> boolT) $ Bound 0));
    1.86 +                   val impl = implies $ (Mset_incl big_Collect) $ 
    1.87 +                                          (Mset_incl small_Collect);
    1.88 +   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    1.89 +
    1.90 +end;
    1.91 +*}
    1.92 +
    1.93 +(*****************************************************************************)
    1.94 +(** Simplifying:                                                            **)
    1.95 +(** Some useful lemmata, lists and simplification tactics to control which  **)
    1.96 +(** theorems are used to simplify at each moment, so that the original      **)
    1.97 +(** input does not suffer any unexpected transformation                     **)
    1.98 +(*****************************************************************************)
    1.99 +
   1.100 +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
   1.101 +  by blast
   1.102 +
   1.103 +
   1.104 +ML {*
   1.105 +(**Simp_tacs**)
   1.106 +
   1.107 +val before_set2pred_simp_tac =
   1.108 +  (simp_tac (HOL_basic_ss addsimps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]));
   1.109 +
   1.110 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
   1.111 +
   1.112 +(*****************************************************************************)
   1.113 +(** set2pred transforms sets inclusion into predicates implication,         **)
   1.114 +(** maintaining the original variable names.                                **)
   1.115 +(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   1.116 +(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   1.117 +(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
   1.118 +(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
   1.119 +(** transformed.                                                            **)
   1.120 +(** This transformation may solve very easy subgoals due to a ligth         **)
   1.121 +(** simplification done by (split_all_tac)                                  **)
   1.122 +(*****************************************************************************)
   1.123 +
   1.124 +fun set2pred i thm =
   1.125 +  let val var_names = map (fst o dest_Free) (get_vars thm) in
   1.126 +    ((before_set2pred_simp_tac i) THEN_MAYBE
   1.127 +     (EVERY [rtac subsetI i, 
   1.128 +             rtac CollectI i,
   1.129 +             dtac CollectD i,
   1.130 +             (TRY(split_all_tac i)) THEN_MAYBE
   1.131 +             ((rename_params_tac var_names i) THEN
   1.132 +              (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   1.133 +  end;
   1.134 +
   1.135 +(*****************************************************************************)
   1.136 +(** BasicSimpTac is called to simplify all verification conditions. It does **)
   1.137 +(** a light simplification by applying "mem_Collect_eq", then it calls      **)
   1.138 +(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
   1.139 +(** and transforms any other into predicates, applying then                 **)
   1.140 +(** the tactic chosen by the user, which may solve the subgoal completely.  **)
   1.141 +(*****************************************************************************)
   1.142 +
   1.143 +fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   1.144 +
   1.145 +fun BasicSimpTac tac =
   1.146 +  simp_tac
   1.147 +    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   1.148 +  THEN_MAYBE' MaxSimpTac tac;
   1.149 +
   1.150 +(** HoareRuleTac **)
   1.151 +
   1.152 +fun WlpTac Mlem tac i =
   1.153 +  rtac @{thm SeqRule} i THEN  HoareRuleTac Mlem tac false (i+1)
   1.154 +and HoareRuleTac Mlem tac pre_cond i st = st |>
   1.155 +        (*abstraction over st prevents looping*)
   1.156 +    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   1.157 +      ORELSE
   1.158 +      (FIRST[rtac @{thm SkipRule} i,
   1.159 +             EVERY[rtac @{thm BasicRule} i,
   1.160 +                   rtac Mlem i,
   1.161 +                   split_simp_tac i],
   1.162 +             EVERY[rtac @{thm CondRule} i,
   1.163 +                   HoareRuleTac Mlem tac false (i+2),
   1.164 +                   HoareRuleTac Mlem tac false (i+1)],
   1.165 +             EVERY[rtac @{thm WhileRule} i,
   1.166 +                   BasicSimpTac tac (i+2),
   1.167 +                   HoareRuleTac Mlem tac true (i+1)] ] 
   1.168 +       THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) ));
   1.169 +
   1.170 +
   1.171 +(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   1.172 +(** the final verification conditions                                       **)
   1.173 + 
   1.174 +fun hoare_tac tac i thm =
   1.175 +  let val Mlem = Mset(thm)
   1.176 +  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
   1.177 +*}
   1.178  
   1.179  method_setup vcg = {*
   1.180    Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *}
     2.1 --- a/src/HOL/Hoare/HoareAbort.thy	Wed Aug 29 10:20:22 2007 +0200
     2.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Wed Aug 29 11:10:28 2007 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  *)
     2.5  
     2.6  theory HoareAbort  imports Main
     2.7 -uses ("hoareAbort.ML") begin
     2.8 +begin
     2.9  
    2.10  types
    2.11      'a bexp = "'a set"
    2.12 @@ -235,7 +235,169 @@
    2.13  lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
    2.14  by(auto simp:Valid_def)
    2.15  
    2.16 -use "hoareAbort.ML"
    2.17 +
    2.18 +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *}
    2.19 +
    2.20 +ML {*
    2.21 +(*** The tactics ***)
    2.22 +
    2.23 +(*****************************************************************************)
    2.24 +(** The function Mset makes the theorem                                     **)
    2.25 +(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
    2.26 +(** where (x1,...,xn) are the variables of the particular program we are    **)
    2.27 +(** working on at the moment of the call                                    **)
    2.28 +(*****************************************************************************)
    2.29 +
    2.30 +local open HOLogic in
    2.31 +
    2.32 +(** maps (%x1 ... xn. t) to [x1,...,xn] **)
    2.33 +fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    2.34 +  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    2.35 +  | abs2list _ = [];
    2.36 +
    2.37 +(** maps {(x1,...,xn). t} to [x1,...,xn] **)
    2.38 +fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    2.39 +  | mk_vars _ = [];
    2.40 +
    2.41 +(** abstraction of body over a tuple formed from a list of free variables. 
    2.42 +Types are also built **)
    2.43 +fun mk_abstupleC []     body = absfree ("x", unitT, body)
    2.44 +  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    2.45 +                               in if w=[] then absfree (n, T, body)
    2.46 +        else let val z  = mk_abstupleC w body;
    2.47 +                 val T2 = case z of Abs(_,T,_) => T
    2.48 +                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    2.49 +       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    2.50 +          $ absfree (n, T, z) end end;
    2.51 +
    2.52 +(** maps [x1,...,xn] to (x1,...,xn) and types**)
    2.53 +fun mk_bodyC []      = HOLogic.unit
    2.54 +  | mk_bodyC (x::xs) = if xs=[] then x 
    2.55 +               else let val (n, T) = dest_Free x ;
    2.56 +                        val z = mk_bodyC xs;
    2.57 +                        val T2 = case z of Free(_, T) => T
    2.58 +                                         | Const ("Pair", Type ("fun", [_, Type
    2.59 +                                            ("fun", [_, T])])) $ _ $ _ => T;
    2.60 +                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    2.61 +
    2.62 +(** maps a goal of the form:
    2.63 +        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    2.64 +fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    2.65 +                        val d = Logic.strip_assums_concl c;
    2.66 +                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    2.67 +      in mk_vars pre end;
    2.68 +
    2.69 +
    2.70 +(** Makes Collect with type **)
    2.71 +fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    2.72 +                      in Collect_const t $ trm end;
    2.73 +
    2.74 +fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
    2.75 +
    2.76 +(** Makes "Mset <= t" **)
    2.77 +fun Mset_incl t = let val MsetT = fastype_of t 
    2.78 +                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    2.79 +
    2.80 +
    2.81 +fun Mset thm = let val vars = get_vars(thm);
    2.82 +                   val varsT = fastype_of (mk_bodyC vars);
    2.83 +                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    2.84 +                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    2.85 +                   val small_Collect = mk_CollectC (Abs("x",varsT,
    2.86 +                           Free ("P",varsT --> boolT) $ Bound 0));
    2.87 +                   val impl = implies $ (Mset_incl big_Collect) $ 
    2.88 +                                          (Mset_incl small_Collect);
    2.89 +   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    2.90 +
    2.91 +end;
    2.92 +*}
    2.93 +
    2.94 +(*****************************************************************************)
    2.95 +(** Simplifying:                                                            **)
    2.96 +(** Some useful lemmata, lists and simplification tactics to control which  **)
    2.97 +(** theorems are used to simplify at each moment, so that the original      **)
    2.98 +(** input does not suffer any unexpected transformation                     **)
    2.99 +(*****************************************************************************)
   2.100 +
   2.101 +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
   2.102 +  by blast
   2.103 +
   2.104 +
   2.105 +ML {*
   2.106 +(**Simp_tacs**)
   2.107 +
   2.108 +val before_set2pred_simp_tac =
   2.109 +  (simp_tac (HOL_basic_ss addsimps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]));
   2.110 +
   2.111 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
   2.112 +
   2.113 +(*****************************************************************************)
   2.114 +(** set2pred transforms sets inclusion into predicates implication,         **)
   2.115 +(** maintaining the original variable names.                                **)
   2.116 +(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   2.117 +(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   2.118 +(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
   2.119 +(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
   2.120 +(** transformed.                                                            **)
   2.121 +(** This transformation may solve very easy subgoals due to a ligth         **)
   2.122 +(** simplification done by (split_all_tac)                                  **)
   2.123 +(*****************************************************************************)
   2.124 +
   2.125 +fun set2pred i thm =
   2.126 +  let val var_names = map (fst o dest_Free) (get_vars thm) in
   2.127 +    ((before_set2pred_simp_tac i) THEN_MAYBE
   2.128 +      (EVERY [rtac subsetI i, 
   2.129 +              rtac CollectI i,
   2.130 +              dtac CollectD i,
   2.131 +              (TRY(split_all_tac i)) THEN_MAYBE
   2.132 +              ((rename_params_tac var_names i) THEN
   2.133 +               (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   2.134 +  end;
   2.135 +
   2.136 +(*****************************************************************************)
   2.137 +(** BasicSimpTac is called to simplify all verification conditions. It does **)
   2.138 +(** a light simplification by applying "mem_Collect_eq", then it calls      **)
   2.139 +(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
   2.140 +(** and transforms any other into predicates, applying then                 **)
   2.141 +(** the tactic chosen by the user, which may solve the subgoal completely.  **)
   2.142 +(*****************************************************************************)
   2.143 +
   2.144 +fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   2.145 +
   2.146 +fun BasicSimpTac tac =
   2.147 +  simp_tac
   2.148 +    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   2.149 +  THEN_MAYBE' MaxSimpTac tac;
   2.150 +
   2.151 +(** HoareRuleTac **)
   2.152 +
   2.153 +fun WlpTac Mlem tac i =
   2.154 +  rtac @{thm SeqRule} i THEN  HoareRuleTac Mlem tac false (i+1)
   2.155 +and HoareRuleTac Mlem tac pre_cond i st = st |>
   2.156 +        (*abstraction over st prevents looping*)
   2.157 +    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   2.158 +      ORELSE
   2.159 +      (FIRST[rtac @{thm SkipRule} i,
   2.160 +             rtac @{thm AbortRule} i,
   2.161 +             EVERY[rtac @{thm BasicRule} i,
   2.162 +                   rtac Mlem i,
   2.163 +                   split_simp_tac i],
   2.164 +             EVERY[rtac @{thm CondRule} i,
   2.165 +                   HoareRuleTac Mlem tac false (i+2),
   2.166 +                   HoareRuleTac Mlem tac false (i+1)],
   2.167 +             EVERY[rtac @{thm WhileRule} i,
   2.168 +                   BasicSimpTac tac (i+2),
   2.169 +                   HoareRuleTac Mlem tac true (i+1)] ] 
   2.170 +       THEN (if pre_cond then (BasicSimpTac tac i) else rtac subset_refl i) ));
   2.171 +
   2.172 +
   2.173 +(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   2.174 +(** the final verification conditions                                       **)
   2.175 + 
   2.176 +fun hoare_tac tac i thm =
   2.177 +  let val Mlem = Mset(thm)
   2.178 +  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
   2.179 +*}
   2.180  
   2.181  method_setup vcg = {*
   2.182    Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *}
     3.1 --- a/src/HOL/Hoare/hoare.ML	Wed Aug 29 10:20:22 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,171 +0,0 @@
     3.4 -(*  Title:      HOL/Hoare/Hoare.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Leonor Prensa Nieto & Tobias Nipkow
     3.7 -    Copyright   1998 TUM
     3.8 -
     3.9 -Derivation of the proof rules and, most importantly, the VCG tactic.
    3.10 -*)
    3.11 -
    3.12 -val SkipRule = thm"SkipRule";
    3.13 -val BasicRule = thm"BasicRule";
    3.14 -val SeqRule = thm"SeqRule";
    3.15 -val CondRule = thm"CondRule";
    3.16 -val WhileRule = thm"WhileRule";
    3.17 -
    3.18 -(*** The tactics ***)
    3.19 -
    3.20 -(*****************************************************************************)
    3.21 -(** The function Mset makes the theorem                                     **)
    3.22 -(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
    3.23 -(** where (x1,...,xn) are the variables of the particular program we are    **)
    3.24 -(** working on at the moment of the call                                    **)
    3.25 -(*****************************************************************************)
    3.26 -
    3.27 -local open HOLogic in
    3.28 -
    3.29 -(** maps (%x1 ... xn. t) to [x1,...,xn] **)
    3.30 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    3.31 -  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    3.32 -  | abs2list _ = [];
    3.33 -
    3.34 -(** maps {(x1,...,xn). t} to [x1,...,xn] **)
    3.35 -fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    3.36 -  | mk_vars _ = [];
    3.37 -
    3.38 -(** abstraction of body over a tuple formed from a list of free variables. 
    3.39 -Types are also built **)
    3.40 -fun mk_abstupleC []     body = absfree ("x", unitT, body)
    3.41 -  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    3.42 -                               in if w=[] then absfree (n, T, body)
    3.43 -        else let val z  = mk_abstupleC w body;
    3.44 -                 val T2 = case z of Abs(_,T,_) => T
    3.45 -                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    3.46 -       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    3.47 -          $ absfree (n, T, z) end end;
    3.48 -
    3.49 -(** maps [x1,...,xn] to (x1,...,xn) and types**)
    3.50 -fun mk_bodyC []      = HOLogic.unit
    3.51 -  | mk_bodyC (x::xs) = if xs=[] then x 
    3.52 -               else let val (n, T) = dest_Free x ;
    3.53 -                        val z = mk_bodyC xs;
    3.54 -                        val T2 = case z of Free(_, T) => T
    3.55 -                                         | Const ("Pair", Type ("fun", [_, Type
    3.56 -                                            ("fun", [_, T])])) $ _ $ _ => T;
    3.57 -                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    3.58 -
    3.59 -(** maps a goal of the form:
    3.60 -        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    3.61 -fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    3.62 -                        val d = Logic.strip_assums_concl c;
    3.63 -                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    3.64 -      in mk_vars pre end;
    3.65 -
    3.66 -
    3.67 -(** Makes Collect with type **)
    3.68 -fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    3.69 -                      in Collect_const t $ trm end;
    3.70 -
    3.71 -fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
    3.72 -
    3.73 -(** Makes "Mset <= t" **)
    3.74 -fun Mset_incl t = let val MsetT = fastype_of t 
    3.75 -                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    3.76 -
    3.77 -
    3.78 -fun Mset thm = let val vars = get_vars(thm);
    3.79 -                   val varsT = fastype_of (mk_bodyC vars);
    3.80 -                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    3.81 -                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    3.82 -                   val small_Collect = mk_CollectC (Abs("x",varsT,
    3.83 -                           Free ("P",varsT --> boolT) $ Bound 0));
    3.84 -                   val impl = implies $ (Mset_incl big_Collect) $ 
    3.85 -                                          (Mset_incl small_Collect);
    3.86 -   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    3.87 -
    3.88 -end;
    3.89 -
    3.90 -
    3.91 -(*****************************************************************************)
    3.92 -(** Simplifying:                                                            **)
    3.93 -(** Some useful lemmata, lists and simplification tactics to control which  **)
    3.94 -(** theorems are used to simplify at each moment, so that the original      **)
    3.95 -(** input does not suffer any unexpected transformation                     **)
    3.96 -(*****************************************************************************)
    3.97 -
    3.98 -Goal "-(Collect b) = {x. ~(b x)}";
    3.99 -by (Fast_tac 1);
   3.100 -qed "Compl_Collect";
   3.101 -
   3.102 -
   3.103 -(**Simp_tacs**)
   3.104 -
   3.105 -val before_set2pred_simp_tac =
   3.106 -  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
   3.107 -
   3.108 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
   3.109 -
   3.110 -(*****************************************************************************)
   3.111 -(** set2pred transforms sets inclusion into predicates implication,         **)
   3.112 -(** maintaining the original variable names.                                **)
   3.113 -(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   3.114 -(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   3.115 -(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
   3.116 -(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
   3.117 -(** transformed.                                                            **)
   3.118 -(** This transformation may solve very easy subgoals due to a ligth         **)
   3.119 -(** simplification done by (split_all_tac)                                  **)
   3.120 -(*****************************************************************************)
   3.121 -
   3.122 -fun set2pred i thm =
   3.123 -  let val var_names = map (fst o dest_Free) (get_vars thm) in
   3.124 -    ((before_set2pred_simp_tac i) THEN_MAYBE
   3.125 -     (EVERY [rtac subsetI i, 
   3.126 -             rtac CollectI i,
   3.127 -             dtac CollectD i,
   3.128 -             (TRY(split_all_tac i)) THEN_MAYBE
   3.129 -             ((rename_params_tac var_names i) THEN
   3.130 -              (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   3.131 -  end;
   3.132 -
   3.133 -(*****************************************************************************)
   3.134 -(** BasicSimpTac is called to simplify all verification conditions. It does **)
   3.135 -(** a light simplification by applying "mem_Collect_eq", then it calls      **)
   3.136 -(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
   3.137 -(** and transforms any other into predicates, applying then                 **)
   3.138 -(** the tactic chosen by the user, which may solve the subgoal completely.  **)
   3.139 -(*****************************************************************************)
   3.140 -
   3.141 -fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   3.142 -
   3.143 -fun BasicSimpTac tac =
   3.144 -  simp_tac
   3.145 -    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   3.146 -  THEN_MAYBE' MaxSimpTac tac;
   3.147 -
   3.148 -(** HoareRuleTac **)
   3.149 -
   3.150 -fun WlpTac Mlem tac i =
   3.151 -  rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
   3.152 -and HoareRuleTac Mlem tac pre_cond i st = st |>
   3.153 -        (*abstraction over st prevents looping*)
   3.154 -    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   3.155 -      ORELSE
   3.156 -      (FIRST[rtac SkipRule i,
   3.157 -             EVERY[rtac BasicRule i,
   3.158 -                   rtac Mlem i,
   3.159 -                   split_simp_tac i],
   3.160 -             EVERY[rtac CondRule i,
   3.161 -                   HoareRuleTac Mlem tac false (i+2),
   3.162 -                   HoareRuleTac Mlem tac false (i+1)],
   3.163 -             EVERY[rtac WhileRule i,
   3.164 -                   BasicSimpTac tac (i+2),
   3.165 -                   HoareRuleTac Mlem tac true (i+1)] ] 
   3.166 -       THEN (if pre_cond then (BasicSimpTac tac i) else (rtac subset_refl i)) ));
   3.167 -
   3.168 -
   3.169 -(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   3.170 -(** the final verification conditions                                       **)
   3.171 - 
   3.172 -fun hoare_tac tac i thm =
   3.173 -  let val Mlem = Mset(thm)
   3.174 -  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
     4.1 --- a/src/HOL/Hoare/hoareAbort.ML	Wed Aug 29 10:20:22 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,173 +0,0 @@
     4.4 -(*  Title:      HOL/Hoare/Hoare.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Leonor Prensa Nieto & Tobias Nipkow
     4.7 -    Copyright   1998 TUM
     4.8 -
     4.9 -Derivation of the proof rules and, most importantly, the VCG tactic.
    4.10 -*)
    4.11 -
    4.12 -val SkipRule = thm"SkipRule";
    4.13 -val BasicRule = thm"BasicRule";
    4.14 -val AbortRule = thm"AbortRule";
    4.15 -val SeqRule = thm"SeqRule";
    4.16 -val CondRule = thm"CondRule";
    4.17 -val WhileRule = thm"WhileRule";
    4.18 -
    4.19 -(*** The tactics ***)
    4.20 -
    4.21 -(*****************************************************************************)
    4.22 -(** The function Mset makes the theorem                                     **)
    4.23 -(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
    4.24 -(** where (x1,...,xn) are the variables of the particular program we are    **)
    4.25 -(** working on at the moment of the call                                    **)
    4.26 -(*****************************************************************************)
    4.27 -
    4.28 -local open HOLogic in
    4.29 -
    4.30 -(** maps (%x1 ... xn. t) to [x1,...,xn] **)
    4.31 -fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    4.32 -  | abs2list (Abs(x,T,t)) = [Free (x, T)]
    4.33 -  | abs2list _ = [];
    4.34 -
    4.35 -(** maps {(x1,...,xn). t} to [x1,...,xn] **)
    4.36 -fun mk_vars (Const ("Collect",_) $ T) = abs2list T
    4.37 -  | mk_vars _ = [];
    4.38 -
    4.39 -(** abstraction of body over a tuple formed from a list of free variables. 
    4.40 -Types are also built **)
    4.41 -fun mk_abstupleC []     body = absfree ("x", unitT, body)
    4.42 -  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
    4.43 -                               in if w=[] then absfree (n, T, body)
    4.44 -        else let val z  = mk_abstupleC w body;
    4.45 -                 val T2 = case z of Abs(_,T,_) => T
    4.46 -                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    4.47 -       in Const ("split", (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) 
    4.48 -          $ absfree (n, T, z) end end;
    4.49 -
    4.50 -(** maps [x1,...,xn] to (x1,...,xn) and types**)
    4.51 -fun mk_bodyC []      = HOLogic.unit
    4.52 -  | mk_bodyC (x::xs) = if xs=[] then x 
    4.53 -               else let val (n, T) = dest_Free x ;
    4.54 -                        val z = mk_bodyC xs;
    4.55 -                        val T2 = case z of Free(_, T) => T
    4.56 -                                         | Const ("Pair", Type ("fun", [_, Type
    4.57 -                                            ("fun", [_, T])])) $ _ $ _ => T;
    4.58 -                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    4.59 -
    4.60 -(** maps a goal of the form:
    4.61 -        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    4.62 -fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    4.63 -                        val d = Logic.strip_assums_concl c;
    4.64 -                        val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    4.65 -      in mk_vars pre end;
    4.66 -
    4.67 -
    4.68 -(** Makes Collect with type **)
    4.69 -fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
    4.70 -                      in Collect_const t $ trm end;
    4.71 -
    4.72 -fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
    4.73 -
    4.74 -(** Makes "Mset <= t" **)
    4.75 -fun Mset_incl t = let val MsetT = fastype_of t 
    4.76 -                 in mk_Trueprop ((inclt MsetT) $ Free ("Mset", MsetT) $ t) end;
    4.77 -
    4.78 -
    4.79 -fun Mset thm = let val vars = get_vars(thm);
    4.80 -                   val varsT = fastype_of (mk_bodyC vars);
    4.81 -                   val big_Collect = mk_CollectC (mk_abstupleC vars 
    4.82 -                         (Free ("P",varsT --> boolT) $ mk_bodyC vars));
    4.83 -                   val small_Collect = mk_CollectC (Abs("x",varsT,
    4.84 -                           Free ("P",varsT --> boolT) $ Bound 0));
    4.85 -                   val impl = implies $ (Mset_incl big_Collect) $ 
    4.86 -                                          (Mset_incl small_Collect);
    4.87 -   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    4.88 -
    4.89 -end;
    4.90 -
    4.91 -
    4.92 -(*****************************************************************************)
    4.93 -(** Simplifying:                                                            **)
    4.94 -(** Some useful lemmata, lists and simplification tactics to control which  **)
    4.95 -(** theorems are used to simplify at each moment, so that the original      **)
    4.96 -(** input does not suffer any unexpected transformation                     **)
    4.97 -(*****************************************************************************)
    4.98 -
    4.99 -Goal "-(Collect b) = {x. ~(b x)}";
   4.100 -by (Fast_tac 1);
   4.101 -qed "Compl_Collect";
   4.102 -
   4.103 -
   4.104 -(**Simp_tacs**)
   4.105 -
   4.106 -val before_set2pred_simp_tac =
   4.107 -  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
   4.108 -
   4.109 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
   4.110 -
   4.111 -(*****************************************************************************)
   4.112 -(** set2pred transforms sets inclusion into predicates implication,         **)
   4.113 -(** maintaining the original variable names.                                **)
   4.114 -(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
   4.115 -(** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
   4.116 -(** are first simplified by "before_set2pred_simp_tac", that returns only   **)
   4.117 -(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
   4.118 -(** transformed.                                                            **)
   4.119 -(** This transformation may solve very easy subgoals due to a ligth         **)
   4.120 -(** simplification done by (split_all_tac)                                  **)
   4.121 -(*****************************************************************************)
   4.122 -
   4.123 -fun set2pred i thm =
   4.124 -  let val var_names = map (fst o dest_Free) (get_vars thm) in
   4.125 -    ((before_set2pred_simp_tac i) THEN_MAYBE
   4.126 -      (EVERY [rtac subsetI i, 
   4.127 -              rtac CollectI i,
   4.128 -              dtac CollectD i,
   4.129 -              (TRY(split_all_tac i)) THEN_MAYBE
   4.130 -              ((rename_params_tac var_names i) THEN
   4.131 -               (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   4.132 -  end;
   4.133 -
   4.134 -(*****************************************************************************)
   4.135 -(** BasicSimpTac is called to simplify all verification conditions. It does **)
   4.136 -(** a light simplification by applying "mem_Collect_eq", then it calls      **)
   4.137 -(** MaxSimpTac, which solves subgoals of the form "A <= A",                 **)
   4.138 -(** and transforms any other into predicates, applying then                 **)
   4.139 -(** the tactic chosen by the user, which may solve the subgoal completely.  **)
   4.140 -(*****************************************************************************)
   4.141 -
   4.142 -fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
   4.143 -
   4.144 -fun BasicSimpTac tac =
   4.145 -  simp_tac
   4.146 -    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   4.147 -  THEN_MAYBE' MaxSimpTac tac;
   4.148 -
   4.149 -(** HoareRuleTac **)
   4.150 -
   4.151 -fun WlpTac Mlem tac i =
   4.152 -  rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)
   4.153 -and HoareRuleTac Mlem tac pre_cond i st = st |>
   4.154 -        (*abstraction over st prevents looping*)
   4.155 -    ( (WlpTac Mlem tac i THEN HoareRuleTac Mlem tac pre_cond i)
   4.156 -      ORELSE
   4.157 -      (FIRST[rtac SkipRule i,
   4.158 -             rtac AbortRule i,
   4.159 -             EVERY[rtac BasicRule i,
   4.160 -                   rtac Mlem i,
   4.161 -                   split_simp_tac i],
   4.162 -             EVERY[rtac CondRule i,
   4.163 -                   HoareRuleTac Mlem tac false (i+2),
   4.164 -                   HoareRuleTac Mlem tac false (i+1)],
   4.165 -             EVERY[rtac WhileRule i,
   4.166 -                   BasicSimpTac tac (i+2),
   4.167 -                   HoareRuleTac Mlem tac true (i+1)] ] 
   4.168 -       THEN (if pre_cond then (BasicSimpTac tac i) else rtac subset_refl i) ));
   4.169 -
   4.170 -
   4.171 -(** tac:(int -> tactic) is the tactic the user chooses to solve or simplify **)
   4.172 -(** the final verification conditions                                       **)
   4.173 - 
   4.174 -fun hoare_tac tac i thm =
   4.175 -  let val Mlem = Mset(thm)
   4.176 -  in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
     5.1 --- a/src/HOL/IsaMakefile	Wed Aug 29 10:20:22 2007 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Wed Aug 29 11:10:28 2007 +0200
     5.3 @@ -369,10 +369,10 @@
     5.4  HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
     5.5  
     5.6  $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
     5.7 -  Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
     5.8 +  Hoare/Examples.thy Hoare/Hoare.thy \
     5.9    Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
    5.10    Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
    5.11 -  Hoare/hoareAbort.ML Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
    5.12 +  Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
    5.13    Hoare/Separation.thy Hoare/SepLogHeap.thy \
    5.14    Hoare/document/root.tex Hoare/document/root.bib
    5.15  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    5.16 @@ -667,7 +667,7 @@
    5.17    ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
    5.18    ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
    5.19    ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
    5.20 -  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
    5.21 +  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
    5.22    ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
    5.23    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \
    5.24    ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
     6.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Aug 29 10:20:22 2007 +0200
     6.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Aug 29 11:10:28 2007 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  theory SVC_Oracle
     6.6  imports Main
     6.7 -uses "svc_funcs.ML" ("svc_oracle.ML")
     6.8 +uses "svc_funcs.ML"
     6.9  begin
    6.10  
    6.11  consts
    6.12 @@ -22,6 +22,108 @@
    6.13  oracle
    6.14    svc_oracle ("term") = Svc.oracle
    6.15  
    6.16 -use "svc_oracle.ML"
    6.17 +ML {*
    6.18 +(*
    6.19 +Installing the oracle for SVC (Stanford Validity Checker)
    6.20 +
    6.21 +The following code merely CALLS the oracle;
    6.22 +  the soundness-critical functions are at svc_funcs.ML
    6.23 +
    6.24 +Based upon the work of Søren T. Heilmann
    6.25 +*)
    6.26 +
    6.27 +
    6.28 +(*Generalize an Isabelle formula, replacing by Vars
    6.29 +  all subterms not intelligible to SVC.*)
    6.30 +fun svc_abstract t =
    6.31 +  let
    6.32 +    (*The oracle's result is given to the subgoal using compose_tac because
    6.33 +      its premises are matched against the assumptions rather than used
    6.34 +      to make subgoals.  Therefore , abstraction must copy the parameters
    6.35 +      precisely and make them available to all generated Vars.*)
    6.36 +    val params = Term.strip_all_vars t
    6.37 +    and body   = Term.strip_all_body t
    6.38 +    val Us = map #2 params
    6.39 +    val nPar = length params
    6.40 +    val vname = ref "V_a"
    6.41 +    val pairs = ref ([] : (term*term) list)
    6.42 +    fun insert t =
    6.43 +        let val T = fastype_of t
    6.44 +            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
    6.45 +        in  vname := Symbol.bump_string (!vname);
    6.46 +            pairs := (t, v) :: !pairs;
    6.47 +            v
    6.48 +        end;
    6.49 +    fun replace t =
    6.50 +        case t of
    6.51 +            Free _  => t  (*but not existing Vars, lest the names clash*)
    6.52 +          | Bound _ => t
    6.53 +          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
    6.54 +                      SOME v => v
    6.55 +                    | NONE   => insert t)
    6.56 +    (*abstraction of a numeric literal*)
    6.57 +    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
    6.58 +      | lit (t as Const(@{const_name HOL.one}, _)) = t
    6.59 +      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
    6.60 +      | lit t = replace t
    6.61 +    (*abstraction of a real/rational expression*)
    6.62 +    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    6.63 +      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    6.64 +      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    6.65 +      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    6.66 +      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
    6.67 +      | rat t = lit t
    6.68 +    (*abstraction of an integer expression: no div, mod*)
    6.69 +    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    6.70 +      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    6.71 +      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    6.72 +      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
    6.73 +      | int t = lit t
    6.74 +    (*abstraction of a natural number expression: no minus*)
    6.75 +    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    6.76 +      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    6.77 +      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
    6.78 +      | nat t = lit t
    6.79 +    (*abstraction of a relation: =, <, <=*)
    6.80 +    fun rel (T, c $ x $ y) =
    6.81 +            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    6.82 +            else if T = HOLogic.intT then c $ (int x) $ (int y)
    6.83 +            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    6.84 +            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    6.85 +            else replace (c $ x $ y)   (*non-numeric comparison*)
    6.86 +    (*abstraction of a formula*)
    6.87 +    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    6.88 +      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    6.89 +      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    6.90 +      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    6.91 +      | fm ((c as Const("True", _))) = c
    6.92 +      | fm ((c as Const("False", _))) = c
    6.93 +      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    6.94 +      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    6.95 +      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    6.96 +      | fm t = replace t
    6.97 +    (*entry point, and abstraction of a meta-formula*)
    6.98 +    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    6.99 +      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
   6.100 +      | mt t = fm t  (*it might be a formula*)
   6.101 +  in (list_all (params, mt body), !pairs) end;
   6.102 +
   6.103 +
   6.104 +(*Present the entire subgoal to the oracle, assumptions and all, but possibly
   6.105 +  abstracted.  Use via compose_tac, which performs no lifting but will
   6.106 +  instantiate variables.*)
   6.107 +
   6.108 +fun svc_tac i st =
   6.109 +  let
   6.110 +    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
   6.111 +    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
   6.112 +   in compose_tac (false, th, 0) i st end
   6.113 +   handle TERM _ => no_tac st;
   6.114 +
   6.115 +
   6.116 +(*check if user has SVC installed*)
   6.117 +fun svc_enabled () = getenv "SVC_HOME" <> "";
   6.118 +fun if_svc_enabled f x = if svc_enabled () then f x else ();
   6.119 +*}
   6.120  
   6.121  end
     7.1 --- a/src/HOL/ex/svc_oracle.ML	Wed Aug 29 10:20:22 2007 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,105 +0,0 @@
     7.4 -(*  Title:      HOL/SVC_Oracle.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson
     7.7 -    Copyright   1999  University of Cambridge
     7.8 -
     7.9 -Installing the oracle for SVC (Stanford Validity Checker)
    7.10 -
    7.11 -The following code merely CALLS the oracle;
    7.12 -  the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    7.13 -
    7.14 -Based upon the work of Soren T. Heilmann
    7.15 -*)
    7.16 -
    7.17 -
    7.18 -(*Generalize an Isabelle formula, replacing by Vars
    7.19 -  all subterms not intelligible to SVC.*)
    7.20 -fun svc_abstract t =
    7.21 -  let
    7.22 -    (*The oracle's result is given to the subgoal using compose_tac because
    7.23 -      its premises are matched against the assumptions rather than used
    7.24 -      to make subgoals.  Therefore , abstraction must copy the parameters
    7.25 -      precisely and make them available to all generated Vars.*)
    7.26 -    val params = Term.strip_all_vars t
    7.27 -    and body   = Term.strip_all_body t
    7.28 -    val Us = map #2 params
    7.29 -    val nPar = length params
    7.30 -    val vname = ref "V_a"
    7.31 -    val pairs = ref ([] : (term*term) list)
    7.32 -    fun insert t =
    7.33 -        let val T = fastype_of t
    7.34 -            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
    7.35 -        in  vname := Symbol.bump_string (!vname);
    7.36 -            pairs := (t, v) :: !pairs;
    7.37 -            v
    7.38 -        end;
    7.39 -    fun replace t =
    7.40 -        case t of
    7.41 -            Free _  => t  (*but not existing Vars, lest the names clash*)
    7.42 -          | Bound _ => t
    7.43 -          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
    7.44 -                      SOME v => v
    7.45 -                    | NONE   => insert t)
    7.46 -    (*abstraction of a numeric literal*)
    7.47 -    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
    7.48 -      | lit (t as Const(@{const_name HOL.one}, _)) = t
    7.49 -      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
    7.50 -      | lit t = replace t
    7.51 -    (*abstraction of a real/rational expression*)
    7.52 -    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.53 -      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.54 -      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.55 -      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    7.56 -      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
    7.57 -      | rat t = lit t
    7.58 -    (*abstraction of an integer expression: no div, mod*)
    7.59 -    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    7.60 -      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    7.61 -      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    7.62 -      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
    7.63 -      | int t = lit t
    7.64 -    (*abstraction of a natural number expression: no minus*)
    7.65 -    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    7.66 -      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    7.67 -      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
    7.68 -      | nat t = lit t
    7.69 -    (*abstraction of a relation: =, <, <=*)
    7.70 -    fun rel (T, c $ x $ y) =
    7.71 -            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    7.72 -            else if T = HOLogic.intT then c $ (int x) $ (int y)
    7.73 -            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    7.74 -            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    7.75 -            else replace (c $ x $ y)   (*non-numeric comparison*)
    7.76 -    (*abstraction of a formula*)
    7.77 -    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.78 -      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.79 -      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    7.80 -      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    7.81 -      | fm ((c as Const("True", _))) = c
    7.82 -      | fm ((c as Const("False", _))) = c
    7.83 -      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.84 -      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.85 -      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    7.86 -      | fm t = replace t
    7.87 -    (*entry point, and abstraction of a meta-formula*)
    7.88 -    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    7.89 -      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    7.90 -      | mt t = fm t  (*it might be a formula*)
    7.91 -  in (list_all (params, mt body), !pairs) end;
    7.92 -
    7.93 -
    7.94 -(*Present the entire subgoal to the oracle, assumptions and all, but possibly
    7.95 -  abstracted.  Use via compose_tac, which performs no lifting but will
    7.96 -  instantiate variables.*)
    7.97 -
    7.98 -fun svc_tac i st =
    7.99 -  let
   7.100 -    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
   7.101 -    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
   7.102 -   in compose_tac (false, th, 0) i st end
   7.103 -   handle TERM _ => no_tac st;
   7.104 -
   7.105 -
   7.106 -(*check if user has SVC installed*)
   7.107 -fun svc_enabled () = getenv "SVC_HOME" <> "";
   7.108 -fun if_svc_enabled f x = if svc_enabled () then f x else ();