moved TFL files to canonical place;
authorwenzelm
Thu May 31 13:18:52 2007 +0200 (2007-05-31)
changeset 23150073a65f0bc40
parent 23149 ddc5800b699f
child 23151 ed3f6685ff90
moved TFL files to canonical place;
src/HOL/IsaMakefile
src/HOL/Recdef.thy
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/thms.ML
src/HOL/Tools/TFL/thry.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/TFL/utils.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu May 31 13:18:42 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 31 13:18:52 2007 +0200
     1.3 @@ -81,10 +81,10 @@
     1.4    $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML			\
     1.5    $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML				\
     1.6    $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML				\
     1.7 -  $(SRC)/Pure/General/rat.ML $(SRC)/TFL/casesplit.ML				\
     1.8 -  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML			\
     1.9 -  $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML			\
    1.10 -  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML ATP_Linkup.thy			\
    1.11 +  $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML				\
    1.12 +  Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML			\
    1.13 +  Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML				\
    1.14 +  Tools/TFL/usyntax.ML Tools/TFL/utils.ML ATP_Linkup.thy			\
    1.15    Accessible_Part.thy Code_Generator.thy Datatype.thy Divides.thy		\
    1.16    Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy		\
    1.17    Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy			\
     2.1 --- a/src/HOL/Recdef.thy	Thu May 31 13:18:42 2007 +0200
     2.2 +++ b/src/HOL/Recdef.thy	Thu May 31 13:18:52 2007 +0200
     2.3 @@ -8,15 +8,15 @@
     2.4  theory Recdef
     2.5  imports Wellfounded_Relations FunDef
     2.6  uses
     2.7 -  ("../TFL/casesplit.ML")
     2.8 -  ("../TFL/utils.ML")
     2.9 -  ("../TFL/usyntax.ML")
    2.10 -  ("../TFL/dcterm.ML")
    2.11 -  ("../TFL/thms.ML")
    2.12 -  ("../TFL/rules.ML")
    2.13 -  ("../TFL/thry.ML")
    2.14 -  ("../TFL/tfl.ML")
    2.15 -  ("../TFL/post.ML")
    2.16 +  ("Tools/TFL/casesplit.ML")
    2.17 +  ("Tools/TFL/utils.ML")
    2.18 +  ("Tools/TFL/usyntax.ML")
    2.19 +  ("Tools/TFL/dcterm.ML")
    2.20 +  ("Tools/TFL/thms.ML")
    2.21 +  ("Tools/TFL/rules.ML")
    2.22 +  ("Tools/TFL/thry.ML")
    2.23 +  ("Tools/TFL/tfl.ML")
    2.24 +  ("Tools/TFL/post.ML")
    2.25    ("Tools/recdef_package.ML")
    2.26  begin
    2.27  
    2.28 @@ -44,15 +44,15 @@
    2.29  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    2.30    by blast
    2.31  
    2.32 -use "../TFL/casesplit.ML"
    2.33 -use "../TFL/utils.ML"
    2.34 -use "../TFL/usyntax.ML"
    2.35 -use "../TFL/dcterm.ML"
    2.36 -use "../TFL/thms.ML"
    2.37 -use "../TFL/rules.ML"
    2.38 -use "../TFL/thry.ML"
    2.39 -use "../TFL/tfl.ML"
    2.40 -use "../TFL/post.ML"
    2.41 +use "Tools/TFL/casesplit.ML"
    2.42 +use "Tools/TFL/utils.ML"
    2.43 +use "Tools/TFL/usyntax.ML"
    2.44 +use "Tools/TFL/dcterm.ML"
    2.45 +use "Tools/TFL/thms.ML"
    2.46 +use "Tools/TFL/rules.ML"
    2.47 +use "Tools/TFL/thry.ML"
    2.48 +use "Tools/TFL/tfl.ML"
    2.49 +use "Tools/TFL/post.ML"
    2.50  use "Tools/recdef_package.ML"
    2.51  setup RecdefPackage.setup
    2.52  
    2.53 @@ -63,7 +63,7 @@
    2.54    same_fst_def
    2.55    less_Suc_eq [THEN iffD2]
    2.56  
    2.57 -lemmas [recdef_cong] = 
    2.58 +lemmas [recdef_cong] =
    2.59    if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    2.60  
    2.61  lemmas [recdef_wf] =
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Thu May 31 13:18:52 2007 +0200
     3.3 @@ -0,0 +1,331 @@
     3.4 +(*  Title:      HOL/Tools/TFL/casesplit.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lucas Dixon, University of Edinburgh
     3.7 +
     3.8 +A structure that defines a tactic to program case splits.
     3.9 +
    3.10 +    casesplit_free :
    3.11 +      string * typ -> int -> thm -> thm Seq.seq
    3.12 +
    3.13 +    casesplit_name :
    3.14 +      string -> int -> thm -> thm Seq.seq
    3.15 +
    3.16 +These use the induction theorem associated with the recursive data
    3.17 +type to be split.
    3.18 +
    3.19 +The structure includes a function to try and recursively split a
    3.20 +conjecture into a list sub-theorems:
    3.21 +
    3.22 +    splitto : thm list -> thm -> thm
    3.23 +*)
    3.24 +
    3.25 +(* logic-specific *)
    3.26 +signature CASE_SPLIT_DATA =
    3.27 +sig
    3.28 +  val dest_Trueprop : term -> term
    3.29 +  val mk_Trueprop : term -> term
    3.30 +  val atomize : thm list
    3.31 +  val rulify : thm list
    3.32 +end;
    3.33 +
    3.34 +structure CaseSplitData_HOL : CASE_SPLIT_DATA =
    3.35 +struct
    3.36 +val dest_Trueprop = HOLogic.dest_Trueprop;
    3.37 +val mk_Trueprop = HOLogic.mk_Trueprop;
    3.38 +
    3.39 +val atomize = thms "induct_atomize";
    3.40 +val rulify = thms "induct_rulify";
    3.41 +val rulify_fallback = thms "induct_rulify_fallback";
    3.42 +
    3.43 +end;
    3.44 +
    3.45 +
    3.46 +signature CASE_SPLIT =
    3.47 +sig
    3.48 +  (* failure to find a free to split on *)
    3.49 +  exception find_split_exp of string
    3.50 +
    3.51 +  (* getting a case split thm from the induction thm *)
    3.52 +  val case_thm_of_ty : theory -> typ -> thm
    3.53 +  val cases_thm_of_induct_thm : thm -> thm
    3.54 +
    3.55 +  (* case split tactics *)
    3.56 +  val casesplit_free :
    3.57 +      string * typ -> int -> thm -> thm Seq.seq
    3.58 +  val casesplit_name : string -> int -> thm -> thm Seq.seq
    3.59 +
    3.60 +  (* finding a free var to split *)
    3.61 +  val find_term_split :
    3.62 +      term * term -> (string * typ) option
    3.63 +  val find_thm_split :
    3.64 +      thm -> int -> thm -> (string * typ) option
    3.65 +  val find_thms_split :
    3.66 +      thm list -> int -> thm -> (string * typ) option
    3.67 +
    3.68 +  (* try to recursively split conjectured thm to given list of thms *)
    3.69 +  val splitto : thm list -> thm -> thm
    3.70 +
    3.71 +  (* for use with the recdef package *)
    3.72 +  val derive_init_eqs :
    3.73 +      theory ->
    3.74 +      (thm * int) list -> term list -> (thm * int) list
    3.75 +end;
    3.76 +
    3.77 +functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    3.78 +struct
    3.79 +
    3.80 +val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
    3.81 +val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
    3.82 +
    3.83 +(* beta-eta contract the theorem *)
    3.84 +fun beta_eta_contract thm =
    3.85 +    let
    3.86 +      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    3.87 +      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    3.88 +    in thm3 end;
    3.89 +
    3.90 +(* make a casethm from an induction thm *)
    3.91 +val cases_thm_of_induct_thm =
    3.92 +     Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    3.93 +
    3.94 +(* get the case_thm (my version) from a type *)
    3.95 +fun case_thm_of_ty sgn ty  =
    3.96 +    let
    3.97 +      val dtypestab = DatatypePackage.get_datatypes sgn;
    3.98 +      val ty_str = case ty of
    3.99 +                     Type(ty_str, _) => ty_str
   3.100 +                   | TFree(s,_)  => error ("Free type: " ^ s)
   3.101 +                   | TVar((s,i),_) => error ("Free variable: " ^ s)
   3.102 +      val dt = case Symtab.lookup dtypestab ty_str
   3.103 +                of SOME dt => dt
   3.104 +                 | NONE => error ("Not a Datatype: " ^ ty_str)
   3.105 +    in
   3.106 +      cases_thm_of_induct_thm (#induction dt)
   3.107 +    end;
   3.108 +
   3.109 +(*
   3.110 + val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
   3.111 +*)
   3.112 +
   3.113 +
   3.114 +(* for use when there are no prems to the subgoal *)
   3.115 +(* does a case split on the given variable *)
   3.116 +fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
   3.117 +    let
   3.118 +      val x = Free(vstr,ty)
   3.119 +      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
   3.120 +
   3.121 +      val ctermify = Thm.cterm_of sgn;
   3.122 +      val ctypify = Thm.ctyp_of sgn;
   3.123 +      val case_thm = case_thm_of_ty sgn ty;
   3.124 +
   3.125 +      val abs_ct = ctermify abst;
   3.126 +      val free_ct = ctermify x;
   3.127 +
   3.128 +      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
   3.129 +
   3.130 +      val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   3.131 +      val (Pv, Dv, type_insts) =
   3.132 +          case (Thm.concl_of case_thm) of
   3.133 +            (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
   3.134 +            (Pv, Dv,
   3.135 +             Sign.typ_match sgn (Dty, ty) Vartab.empty)
   3.136 +          | _ => error "not a valid case thm";
   3.137 +      val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
   3.138 +        (Vartab.dest type_insts);
   3.139 +      val cPv = ctermify (Envir.subst_TVars type_insts Pv);
   3.140 +      val cDv = ctermify (Envir.subst_TVars type_insts Dv);
   3.141 +    in
   3.142 +      (beta_eta_contract
   3.143 +         (case_thm
   3.144 +            |> Thm.instantiate (type_cinsts, [])
   3.145 +            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
   3.146 +    end;
   3.147 +
   3.148 +
   3.149 +(* for use when there are no prems to the subgoal *)
   3.150 +(* does a case split on the given variable (Free fv) *)
   3.151 +fun casesplit_free fv i th =
   3.152 +    let
   3.153 +      val (subgoalth, exp) = IsaND.fix_alls i th;
   3.154 +      val subgoalth' = atomize_goals subgoalth;
   3.155 +      val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   3.156 +      val sgn = Thm.theory_of_thm th;
   3.157 +
   3.158 +      val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
   3.159 +      val nsplits = Thm.nprems_of splitter_thm;
   3.160 +
   3.161 +      val split_goal_th = splitter_thm RS subgoalth';
   3.162 +      val rulified_split_goal_th = rulify_goals split_goal_th;
   3.163 +    in
   3.164 +      IsaND.export_back exp rulified_split_goal_th
   3.165 +    end;
   3.166 +
   3.167 +
   3.168 +(* for use when there are no prems to the subgoal *)
   3.169 +(* does a case split on the given variable *)
   3.170 +fun casesplit_name vstr i th =
   3.171 +    let
   3.172 +      val (subgoalth, exp) = IsaND.fix_alls i th;
   3.173 +      val subgoalth' = atomize_goals subgoalth;
   3.174 +      val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   3.175 +
   3.176 +      val freets = Term.term_frees gt;
   3.177 +      fun getter x =
   3.178 +          let val (n,ty) = Term.dest_Free x in
   3.179 +            (if vstr = n orelse vstr = Name.dest_skolem n
   3.180 +             then SOME (n,ty) else NONE )
   3.181 +            handle Fail _ => NONE (* dest_skolem *)
   3.182 +          end;
   3.183 +      val (n,ty) = case Library.get_first getter freets
   3.184 +                of SOME (n, ty) => (n, ty)
   3.185 +                 | _ => error ("no such variable " ^ vstr);
   3.186 +      val sgn = Thm.theory_of_thm th;
   3.187 +
   3.188 +      val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
   3.189 +      val nsplits = Thm.nprems_of splitter_thm;
   3.190 +
   3.191 +      val split_goal_th = splitter_thm RS subgoalth';
   3.192 +
   3.193 +      val rulified_split_goal_th = rulify_goals split_goal_th;
   3.194 +    in
   3.195 +      IsaND.export_back exp rulified_split_goal_th
   3.196 +    end;
   3.197 +
   3.198 +
   3.199 +(* small example:
   3.200 +Goal "P (x :: nat) & (C y --> Q (y :: nat))";
   3.201 +by (rtac (thm "conjI") 1);
   3.202 +val th = topthm();
   3.203 +val i = 2;
   3.204 +val vstr = "y";
   3.205 +
   3.206 +by (casesplit_name "y" 2);
   3.207 +
   3.208 +val th = topthm();
   3.209 +val i = 1;
   3.210 +val th' = casesplit_name "x" i th;
   3.211 +*)
   3.212 +
   3.213 +
   3.214 +(* the find_XXX_split functions are simply doing a lightwieght (I
   3.215 +think) term matching equivalent to find where to do the next split *)
   3.216 +
   3.217 +(* assuming two twems are identical except for a free in one at a
   3.218 +subterm, or constant in another, ie assume that one term is a plit of
   3.219 +another, then gives back the free variable that has been split. *)
   3.220 +exception find_split_exp of string
   3.221 +fun find_term_split (Free v, _ $ _) = SOME v
   3.222 +  | find_term_split (Free v, Const _) = SOME v
   3.223 +  | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
   3.224 +  | find_term_split (Free v, Var _) = NONE (* keep searching *)
   3.225 +  | find_term_split (a $ b, a2 $ b2) =
   3.226 +    (case find_term_split (a, a2) of
   3.227 +       NONE => find_term_split (b,b2)
   3.228 +     | vopt => vopt)
   3.229 +  | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
   3.230 +    find_term_split (t1, t2)
   3.231 +  | find_term_split (Const (x,ty), Const(x2,ty2)) =
   3.232 +    if x = x2 then NONE else (* keep searching *)
   3.233 +    raise find_split_exp (* stop now *)
   3.234 +            "Terms are not identical upto a free varaible! (Consts)"
   3.235 +  | find_term_split (Bound i, Bound j) =
   3.236 +    if i = j then NONE else (* keep searching *)
   3.237 +    raise find_split_exp (* stop now *)
   3.238 +            "Terms are not identical upto a free varaible! (Bound)"
   3.239 +  | find_term_split (a, b) =
   3.240 +    raise find_split_exp (* stop now *)
   3.241 +            "Terms are not identical upto a free varaible! (Other)";
   3.242 +
   3.243 +(* assume that "splitth" is a case split form of subgoal i of "genth",
   3.244 +then look for a free variable to split, breaking the subgoal closer to
   3.245 +splitth. *)
   3.246 +fun find_thm_split splitth i genth =
   3.247 +    find_term_split (Logic.get_goal (Thm.prop_of genth) i,
   3.248 +                     Thm.concl_of splitth) handle find_split_exp _ => NONE;
   3.249 +
   3.250 +(* as above but searches "splitths" for a theorem that suggest a case split *)
   3.251 +fun find_thms_split splitths i genth =
   3.252 +    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
   3.253 +
   3.254 +
   3.255 +(* split the subgoal i of "genth" until we get to a member of
   3.256 +splitths. Assumes that genth will be a general form of splitths, that
   3.257 +can be case-split, as needed. Otherwise fails. Note: We assume that
   3.258 +all of "splitths" are split to the same level, and thus it doesn't
   3.259 +matter which one we choose to look for the next split. Simply add
   3.260 +search on splitthms and split variable, to change this.  *)
   3.261 +(* Note: possible efficiency measure: when a case theorem is no longer
   3.262 +useful, drop it? *)
   3.263 +(* Note: This should not be a separate tactic but integrated into the
   3.264 +case split done during recdef's case analysis, this would avoid us
   3.265 +having to (re)search for variables to split. *)
   3.266 +fun splitto splitths genth =
   3.267 +    let
   3.268 +      val _ = not (null splitths) orelse error "splitto: no given splitths";
   3.269 +      val sgn = Thm.theory_of_thm genth;
   3.270 +
   3.271 +      (* check if we are a member of splitths - FIXME: quicker and
   3.272 +      more flexible with discrim net. *)
   3.273 +      fun solve_by_splitth th split =
   3.274 +          Thm.biresolution false [(false,split)] 1 th;
   3.275 +
   3.276 +      fun split th =
   3.277 +          (case find_thms_split splitths 1 th of
   3.278 +             NONE =>
   3.279 +             (writeln "th:";
   3.280 +              Display.print_thm th; writeln "split ths:";
   3.281 +              Display.print_thms splitths; writeln "\n--";
   3.282 +              error "splitto: cannot find variable to split on")
   3.283 +            | SOME v =>
   3.284 +             let
   3.285 +               val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0));
   3.286 +               val split_thm = mk_casesplit_goal_thm sgn v gt;
   3.287 +               val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
   3.288 +             in
   3.289 +               expf (map recsplitf subthms)
   3.290 +             end)
   3.291 +
   3.292 +      and recsplitf th =
   3.293 +          (* note: multiple unifiers! we only take the first element,
   3.294 +             probably fine -- there is probably only one anyway. *)
   3.295 +          (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of
   3.296 +             NONE => split th
   3.297 +           | SOME (solved_th, more) => solved_th)
   3.298 +    in
   3.299 +      recsplitf genth
   3.300 +    end;
   3.301 +
   3.302 +
   3.303 +(* Note: We dont do this if wf conditions fail to be solved, as each
   3.304 +case may have a different wf condition - we could group the conditions
   3.305 +togeather and say that they must be true to solve the general case,
   3.306 +but that would hide from the user which sub-case they were related
   3.307 +to. Probably this is not important, and it would work fine, but I
   3.308 +prefer leaving more fine grain control to the user. *)
   3.309 +
   3.310 +(* derive eqs, assuming strict, ie the rules have no assumptions = all
   3.311 +   the well-foundness conditions have been solved. *)
   3.312 +fun derive_init_eqs sgn rules eqs =
   3.313 +  let
   3.314 +    fun get_related_thms i =
   3.315 +      List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
   3.316 +    fun add_eq (i, e) xs =
   3.317 +      (e, (get_related_thms i rules), i) :: xs
   3.318 +    fun solve_eq (th, [], i) =
   3.319 +          error "derive_init_eqs: missing rules"
   3.320 +      | solve_eq (th, [a], i) = (a, i)
   3.321 +      | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
   3.322 +    val eqths =
   3.323 +      map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
   3.324 +  in
   3.325 +    []
   3.326 +    |> fold_index add_eq eqths
   3.327 +    |> map solve_eq
   3.328 +    |> rev
   3.329 +  end;
   3.330 +
   3.331 +end;
   3.332 +
   3.333 +
   3.334 +structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Thu May 31 13:18:52 2007 +0200
     4.3 @@ -0,0 +1,200 @@
     4.4 +(*  Title:      HOL/Tools/TFL/dcterm.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     4.7 +    Copyright   1997  University of Cambridge
     4.8 +*)
     4.9 +
    4.10 +(*---------------------------------------------------------------------------
    4.11 + * Derived efficient cterm destructors.
    4.12 + *---------------------------------------------------------------------------*)
    4.13 +
    4.14 +signature DCTERM =
    4.15 +sig
    4.16 +  val dest_comb: cterm -> cterm * cterm
    4.17 +  val dest_abs: string option -> cterm -> cterm * cterm
    4.18 +  val capply: cterm -> cterm -> cterm
    4.19 +  val cabs: cterm -> cterm -> cterm
    4.20 +  val mk_conj: cterm * cterm -> cterm
    4.21 +  val mk_disj: cterm * cterm -> cterm
    4.22 +  val mk_exists: cterm * cterm -> cterm
    4.23 +  val dest_conj: cterm -> cterm * cterm
    4.24 +  val dest_const: cterm -> {Name: string, Ty: typ}
    4.25 +  val dest_disj: cterm -> cterm * cterm
    4.26 +  val dest_eq: cterm -> cterm * cterm
    4.27 +  val dest_exists: cterm -> cterm * cterm
    4.28 +  val dest_forall: cterm -> cterm * cterm
    4.29 +  val dest_imp: cterm -> cterm * cterm
    4.30 +  val dest_let: cterm -> cterm * cterm
    4.31 +  val dest_neg: cterm -> cterm
    4.32 +  val dest_pair: cterm -> cterm * cterm
    4.33 +  val dest_var: cterm -> {Name:string, Ty:typ}
    4.34 +  val is_conj: cterm -> bool
    4.35 +  val is_cons: cterm -> bool
    4.36 +  val is_disj: cterm -> bool
    4.37 +  val is_eq: cterm -> bool
    4.38 +  val is_exists: cterm -> bool
    4.39 +  val is_forall: cterm -> bool
    4.40 +  val is_imp: cterm -> bool
    4.41 +  val is_let: cterm -> bool
    4.42 +  val is_neg: cterm -> bool
    4.43 +  val is_pair: cterm -> bool
    4.44 +  val list_mk_disj: cterm list -> cterm
    4.45 +  val strip_abs: cterm -> cterm list * cterm
    4.46 +  val strip_comb: cterm -> cterm * cterm list
    4.47 +  val strip_disj: cterm -> cterm list
    4.48 +  val strip_exists: cterm -> cterm list * cterm
    4.49 +  val strip_forall: cterm -> cterm list * cterm
    4.50 +  val strip_imp: cterm -> cterm list * cterm
    4.51 +  val drop_prop: cterm -> cterm
    4.52 +  val mk_prop: cterm -> cterm
    4.53 +end;
    4.54 +
    4.55 +structure Dcterm: DCTERM =
    4.56 +struct
    4.57 +
    4.58 +structure U = Utils;
    4.59 +
    4.60 +fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
    4.61 +
    4.62 +
    4.63 +fun dest_comb t = Thm.dest_comb t
    4.64 +  handle CTERM (msg, _) => raise ERR "dest_comb" msg;
    4.65 +
    4.66 +fun dest_abs a t = Thm.dest_abs a t
    4.67 +  handle CTERM (msg, _) => raise ERR "dest_abs" msg;
    4.68 +
    4.69 +fun capply t u = Thm.capply t u
    4.70 +  handle CTERM (msg, _) => raise ERR "capply" msg;
    4.71 +
    4.72 +fun cabs a t = Thm.cabs a t
    4.73 +  handle CTERM (msg, _) => raise ERR "cabs" msg;
    4.74 +
    4.75 +
    4.76 +(*---------------------------------------------------------------------------
    4.77 + * Some simple constructor functions.
    4.78 + *---------------------------------------------------------------------------*)
    4.79 +
    4.80 +val mk_hol_const = Thm.cterm_of HOL.thy o Const;
    4.81 +
    4.82 +fun mk_exists (r as (Bvar, Body)) =
    4.83 +  let val ty = #T(rep_cterm Bvar)
    4.84 +      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    4.85 +  in capply c (uncurry cabs r) end;
    4.86 +
    4.87 +
    4.88 +local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    4.89 +in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
    4.90 +end;
    4.91 +
    4.92 +local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    4.93 +in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
    4.94 +end;
    4.95 +
    4.96 +
    4.97 +(*---------------------------------------------------------------------------
    4.98 + * The primitives.
    4.99 + *---------------------------------------------------------------------------*)
   4.100 +fun dest_const ctm =
   4.101 +   (case #t(rep_cterm ctm)
   4.102 +      of Const(s,ty) => {Name = s, Ty = ty}
   4.103 +       | _ => raise ERR "dest_const" "not a constant");
   4.104 +
   4.105 +fun dest_var ctm =
   4.106 +   (case #t(rep_cterm ctm)
   4.107 +      of Var((s,i),ty) => {Name=s, Ty=ty}
   4.108 +       | Free(s,ty)    => {Name=s, Ty=ty}
   4.109 +       |             _ => raise ERR "dest_var" "not a variable");
   4.110 +
   4.111 +
   4.112 +(*---------------------------------------------------------------------------
   4.113 + * Derived destructor operations.
   4.114 + *---------------------------------------------------------------------------*)
   4.115 +
   4.116 +fun dest_monop expected tm =
   4.117 + let
   4.118 +   fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
   4.119 +   val (c, N) = dest_comb tm handle U.ERR _ => err ();
   4.120 +   val name = #Name (dest_const c handle U.ERR _ => err ());
   4.121 + in if name = expected then N else err () end;
   4.122 +
   4.123 +fun dest_binop expected tm =
   4.124 + let
   4.125 +   fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
   4.126 +   val (M, N) = dest_comb tm handle U.ERR _ => err ()
   4.127 + in (dest_monop expected M, N) handle U.ERR _ => err () end;
   4.128 +
   4.129 +fun dest_binder expected tm =
   4.130 +  dest_abs NONE (dest_monop expected tm)
   4.131 +  handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
   4.132 +
   4.133 +
   4.134 +val dest_neg    = dest_monop "not"
   4.135 +val dest_pair   = dest_binop "Pair";
   4.136 +val dest_eq     = dest_binop "op ="
   4.137 +val dest_imp    = dest_binop "op -->"
   4.138 +val dest_conj   = dest_binop "op &"
   4.139 +val dest_disj   = dest_binop "op |"
   4.140 +val dest_cons   = dest_binop "Cons"
   4.141 +val dest_let    = Library.swap o dest_binop "Let";
   4.142 +val dest_select = dest_binder "Hilbert_Choice.Eps"
   4.143 +val dest_exists = dest_binder "Ex"
   4.144 +val dest_forall = dest_binder "All"
   4.145 +
   4.146 +(* Query routines *)
   4.147 +
   4.148 +val is_eq     = can dest_eq
   4.149 +val is_imp    = can dest_imp
   4.150 +val is_select = can dest_select
   4.151 +val is_forall = can dest_forall
   4.152 +val is_exists = can dest_exists
   4.153 +val is_neg    = can dest_neg
   4.154 +val is_conj   = can dest_conj
   4.155 +val is_disj   = can dest_disj
   4.156 +val is_pair   = can dest_pair
   4.157 +val is_let    = can dest_let
   4.158 +val is_cons   = can dest_cons
   4.159 +
   4.160 +
   4.161 +(*---------------------------------------------------------------------------
   4.162 + * Iterated creation.
   4.163 + *---------------------------------------------------------------------------*)
   4.164 +val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
   4.165 +
   4.166 +(*---------------------------------------------------------------------------
   4.167 + * Iterated destruction. (To the "right" in a term.)
   4.168 + *---------------------------------------------------------------------------*)
   4.169 +fun strip break tm =
   4.170 +  let fun dest (p as (ctm,accum)) =
   4.171 +        let val (M,N) = break ctm
   4.172 +        in dest (N, M::accum)
   4.173 +        end handle U.ERR _ => p
   4.174 +  in dest (tm,[])
   4.175 +  end;
   4.176 +
   4.177 +fun rev2swap (x,l) = (rev l, x);
   4.178 +
   4.179 +val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
   4.180 +val strip_imp    = rev2swap o strip dest_imp
   4.181 +val strip_abs    = rev2swap o strip (dest_abs NONE)
   4.182 +val strip_forall = rev2swap o strip dest_forall
   4.183 +val strip_exists = rev2swap o strip dest_exists
   4.184 +
   4.185 +val strip_disj   = rev o (op::) o strip dest_disj
   4.186 +
   4.187 +
   4.188 +(*---------------------------------------------------------------------------
   4.189 + * Going into and out of prop
   4.190 + *---------------------------------------------------------------------------*)
   4.191 +
   4.192 +fun mk_prop ctm =
   4.193 +  let val {t, thy, ...} = Thm.rep_cterm ctm in
   4.194 +    if can HOLogic.dest_Trueprop t then ctm
   4.195 +    else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
   4.196 +  end
   4.197 +  handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
   4.198 +    | TERM (msg, _) => raise ERR "mk_prop" msg;
   4.199 +
   4.200 +fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
   4.201 +
   4.202 +
   4.203 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu May 31 13:18:52 2007 +0200
     5.3 @@ -0,0 +1,279 @@
     5.4 +(*  Title:      HOL/Tools/TFL/post.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     5.7 +    Copyright   1997  University of Cambridge
     5.8 +
     5.9 +Second part of main module (postprocessing of TFL definitions).
    5.10 +*)
    5.11 +
    5.12 +signature TFL =
    5.13 +sig
    5.14 +  val trace: bool ref
    5.15 +  val quiet_mode: bool ref
    5.16 +  val message: string -> unit
    5.17 +  val tgoalw: theory -> thm list -> thm list -> thm list
    5.18 +  val tgoal: theory -> thm list -> thm list
    5.19 +  val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    5.20 +    term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    5.21 +  val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    5.22 +    string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    5.23 +  val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
    5.24 +  val defer: theory -> thm list -> xstring -> string list -> theory * thm
    5.25 +end;
    5.26 +
    5.27 +structure Tfl: TFL =
    5.28 +struct
    5.29 +
    5.30 +structure S = USyntax
    5.31 +
    5.32 +
    5.33 +(* messages *)
    5.34 +
    5.35 +val trace = Prim.trace
    5.36 +
    5.37 +val quiet_mode = ref false;
    5.38 +fun message s = if ! quiet_mode then () else writeln s;
    5.39 +
    5.40 +
    5.41 +(* misc *)
    5.42 +
    5.43 +(*---------------------------------------------------------------------------
    5.44 + * Extract termination goals so that they can be put it into a goalstack, or
    5.45 + * have a tactic directly applied to them.
    5.46 + *--------------------------------------------------------------------------*)
    5.47 +fun termination_goals rules =
    5.48 +    map (Type.freeze o HOLogic.dest_Trueprop)
    5.49 +      (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
    5.50 +
    5.51 +(*---------------------------------------------------------------------------
    5.52 + * Finds the termination conditions in (highly massaged) definition and
    5.53 + * puts them into a goalstack.
    5.54 + *--------------------------------------------------------------------------*)
    5.55 +fun tgoalw thy defs rules =
    5.56 +  case termination_goals rules of
    5.57 +      [] => error "tgoalw: no termination conditions to prove"
    5.58 +    | L  => OldGoals.goalw_cterm defs
    5.59 +              (Thm.cterm_of thy
    5.60 +                        (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
    5.61 +
    5.62 +fun tgoal thy = tgoalw thy [];
    5.63 +
    5.64 +(*---------------------------------------------------------------------------
    5.65 + * Three postprocessors are applied to the definition.  It
    5.66 + * attempts to prove wellfoundedness of the given relation, simplifies the
    5.67 + * non-proved termination conditions, and finally attempts to prove the
    5.68 + * simplified termination conditions.
    5.69 + *--------------------------------------------------------------------------*)
    5.70 +fun std_postprocessor strict cs ss wfs =
    5.71 +  Prim.postprocess strict
    5.72 +   {wf_tac     = REPEAT (ares_tac wfs 1),
    5.73 +    terminator = asm_simp_tac ss 1
    5.74 +                 THEN TRY (silent_arith_tac 1 ORELSE
    5.75 +                           fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    5.76 +    simplifier = Rules.simpl_conv ss []};
    5.77 +
    5.78 +
    5.79 +
    5.80 +val concl = #2 o Rules.dest_thm;
    5.81 +
    5.82 +(*---------------------------------------------------------------------------
    5.83 + * Postprocess a definition made by "define". This is a separate stage of
    5.84 + * processing from the definition stage.
    5.85 + *---------------------------------------------------------------------------*)
    5.86 +local
    5.87 +structure R = Rules
    5.88 +structure U = Utils
    5.89 +
    5.90 +(* The rest of these local definitions are for the tricky nested case *)
    5.91 +val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
    5.92 +
    5.93 +fun id_thm th =
    5.94 +   let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
    5.95 +   in lhs aconv rhs end
    5.96 +   handle U.ERR _ => false;
    5.97 +   
    5.98 +
    5.99 +fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
   5.100 +val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
   5.101 +val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
   5.102 +fun mk_meta_eq r = case concl_of r of
   5.103 +     Const("==",_)$_$_ => r
   5.104 +  |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
   5.105 +  |   _ => r RS P_imp_P_eq_True
   5.106 +
   5.107 +(*Is this the best way to invoke the simplifier??*)
   5.108 +fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
   5.109 +
   5.110 +fun join_assums th =
   5.111 +  let val {thy,...} = rep_thm th
   5.112 +      val tych = cterm_of thy
   5.113 +      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   5.114 +      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   5.115 +      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   5.116 +      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
   5.117 +  in
   5.118 +    R.GEN_ALL
   5.119 +      (R.DISCH_ALL
   5.120 +         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   5.121 +  end
   5.122 +  val gen_all = S.gen_all
   5.123 +in
   5.124 +fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
   5.125 +  let
   5.126 +    val _ = message "Proving induction theorem ..."
   5.127 +    val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
   5.128 +    val _ = message "Postprocessing ...";
   5.129 +    val {rules, induction, nested_tcs} =
   5.130 +      std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
   5.131 +  in
   5.132 +  case nested_tcs
   5.133 +  of [] => {induction=induction, rules=rules,tcs=[]}
   5.134 +  | L  => let val dummy = message "Simplifying nested TCs ..."
   5.135 +              val (solved,simplified,stubborn) =
   5.136 +               fold_rev (fn th => fn (So,Si,St) =>
   5.137 +                     if (id_thm th) then (So, Si, th::St) else
   5.138 +                     if (solved th) then (th::So, Si, St)
   5.139 +                     else (So, th::Si, St)) nested_tcs ([],[],[])
   5.140 +              val simplified' = map join_assums simplified
   5.141 +              val dummy = (Prim.trace_thms "solved =" solved;
   5.142 +                           Prim.trace_thms "simplified' =" simplified')
   5.143 +              val rewr = full_simplify (ss addsimps (solved @ simplified'));
   5.144 +              val dummy = Prim.trace_thms "Simplifying the induction rule..."
   5.145 +                                          [induction]
   5.146 +              val induction' = rewr induction
   5.147 +              val dummy = Prim.trace_thms "Simplifying the recursion rules..."
   5.148 +                                          [rules]
   5.149 +              val rules'     = rewr rules
   5.150 +              val _ = message "... Postprocessing finished";
   5.151 +          in
   5.152 +          {induction = induction',
   5.153 +               rules = rules',
   5.154 +                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   5.155 +                           (simplified@stubborn)}
   5.156 +          end
   5.157 +  end;
   5.158 +
   5.159 +
   5.160 +(*lcp: curry the predicate of the induction rule*)
   5.161 +fun curry_rule rl =
   5.162 +  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
   5.163 +
   5.164 +(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   5.165 +val meta_outer =
   5.166 +  curry_rule o standard o
   5.167 +  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   5.168 +
   5.169 +(*Strip off the outer !P*)
   5.170 +val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   5.171 +
   5.172 +fun tracing true _ = ()
   5.173 +  | tracing false msg = writeln msg;
   5.174 +
   5.175 +fun simplify_defn strict thy cs ss congs wfs id pats def0 =
   5.176 +   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
   5.177 +       val {rules,rows,TCs,full_pats_TCs} =
   5.178 +           Prim.post_definition congs (thy, (def,pats))
   5.179 +       val {lhs=f,rhs} = S.dest_eq (concl def)
   5.180 +       val (_,[R,_]) = S.strip_comb rhs
   5.181 +       val dummy = Prim.trace_thms "congs =" congs
   5.182 +       (*the next step has caused simplifier looping in some cases*)
   5.183 +       val {induction, rules, tcs} =
   5.184 +             proof_stage strict cs ss wfs thy
   5.185 +               {f = f, R = R, rules = rules,
   5.186 +                full_pats_TCs = full_pats_TCs,
   5.187 +                TCs = TCs}
   5.188 +       val rules' = map (standard o ObjectLogic.rulify_no_asm)
   5.189 +                        (R.CONJUNCTS rules)
   5.190 +         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   5.191 +        rules = ListPair.zip(rules', rows),
   5.192 +        tcs = (termination_goals rules') @ tcs}
   5.193 +   end
   5.194 +  handle U.ERR {mesg,func,module} =>
   5.195 +               error (mesg ^
   5.196 +                      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   5.197 +
   5.198 +
   5.199 +(* Derive the initial equations from the case-split rules to meet the
   5.200 +users specification of the recursive function. 
   5.201 + Note: We don't do this if the wf conditions fail to be solved, as each
   5.202 +case may have a different wf condition. We could group the conditions
   5.203 +together and say that they must be true to solve the general case,
   5.204 +but that would hide from the user which sub-case they were related
   5.205 +to. Probably this is not important, and it would work fine, but, for now, I
   5.206 +prefer leaving more fine-grain control to the user. 
   5.207 +-- Lucas Dixon, Aug 2004 *)
   5.208 +local
   5.209 +  fun get_related_thms i = 
   5.210 +      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
   5.211 +
   5.212 +  fun solve_eq (th, [], i) = 
   5.213 +        error "derive_init_eqs: missing rules"
   5.214 +    | solve_eq (th, [a], i) = [(a, i)]
   5.215 +    | solve_eq (th, splitths as (_ :: _), i) = 
   5.216 +      (writeln "Proving unsplit equation...";
   5.217 +      [((standard o ObjectLogic.rulify_no_asm)
   5.218 +          (CaseSplit.splitto splitths th), i)])
   5.219 +      (* if there's an error, pretend nothing happened with this definition 
   5.220 +         We should probably print something out so that the user knows...? *)
   5.221 +      handle ERROR s => 
   5.222 +             (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
   5.223 +in
   5.224 +fun derive_init_eqs sgn rules eqs = 
   5.225 +    let 
   5.226 +      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
   5.227 +                      eqs
   5.228 +      fun countlist l = 
   5.229 +          (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
   5.230 +    in
   5.231 +      List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
   5.232 +                (countlist eqths))
   5.233 +    end;
   5.234 +end;
   5.235 +
   5.236 +
   5.237 +(*---------------------------------------------------------------------------
   5.238 + * Defining a function with an associated termination relation.
   5.239 + *---------------------------------------------------------------------------*)
   5.240 +fun define_i strict thy cs ss congs wfs fid R eqs =
   5.241 +  let val {functional,pats} = Prim.mk_functional thy eqs
   5.242 +      val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
   5.243 +      val {induct, rules, tcs} = 
   5.244 +          simplify_defn strict thy cs ss congs wfs fid pats def
   5.245 +      val rules' = 
   5.246 +          if strict then derive_init_eqs thy rules eqs
   5.247 +          else rules
   5.248 +  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
   5.249 +
   5.250 +fun define strict thy cs ss congs wfs fid R seqs =
   5.251 +  define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
   5.252 +    handle U.ERR {mesg,...} => error mesg;
   5.253 +
   5.254 +
   5.255 +(*---------------------------------------------------------------------------
   5.256 + *
   5.257 + *     Definitions with synthesized termination relation
   5.258 + *
   5.259 + *---------------------------------------------------------------------------*)
   5.260 +
   5.261 +fun func_of_cond_eqn tm =
   5.262 +  #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
   5.263 +
   5.264 +fun defer_i thy congs fid eqs =
   5.265 + let val {rules,R,theory,full_pats_TCs,SV,...} =
   5.266 +             Prim.lazyR_def thy (Sign.base_name fid) congs eqs
   5.267 +     val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
   5.268 +     val dummy = message "Proving induction theorem ...";
   5.269 +     val induction = Prim.mk_induction theory
   5.270 +                        {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
   5.271 + in (theory,
   5.272 +     (*return the conjoined induction rule and recursion equations,
   5.273 +       with assumptions remaining to discharge*)
   5.274 +     standard (induction RS (rules RS conjI)))
   5.275 + end
   5.276 +
   5.277 +fun defer thy congs fid seqs =
   5.278 +  defer_i thy congs fid (map (Sign.read_term thy) seqs)
   5.279 +    handle U.ERR {mesg,...} => error mesg;
   5.280 +end;
   5.281 +
   5.282 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu May 31 13:18:52 2007 +0200
     6.3 @@ -0,0 +1,825 @@
     6.4 +(*  Title:      HOL/Tools/TFL/rules.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     6.7 +    Copyright   1997  University of Cambridge
     6.8 +
     6.9 +Emulation of HOL inference rules for TFL
    6.10 +*)
    6.11 +
    6.12 +signature RULES =
    6.13 +sig
    6.14 +  val dest_thm: thm -> term list * term
    6.15 +
    6.16 +  (* Inference rules *)
    6.17 +  val REFL: cterm -> thm
    6.18 +  val ASSUME: cterm -> thm
    6.19 +  val MP: thm -> thm -> thm
    6.20 +  val MATCH_MP: thm -> thm -> thm
    6.21 +  val CONJUNCT1: thm -> thm
    6.22 +  val CONJUNCT2: thm -> thm
    6.23 +  val CONJUNCTS: thm -> thm list
    6.24 +  val DISCH: cterm -> thm -> thm
    6.25 +  val UNDISCH: thm  -> thm
    6.26 +  val SPEC: cterm -> thm -> thm
    6.27 +  val ISPEC: cterm -> thm -> thm
    6.28 +  val ISPECL: cterm list -> thm -> thm
    6.29 +  val GEN: cterm -> thm -> thm
    6.30 +  val GENL: cterm list -> thm -> thm
    6.31 +  val LIST_CONJ: thm list -> thm
    6.32 +
    6.33 +  val SYM: thm -> thm
    6.34 +  val DISCH_ALL: thm -> thm
    6.35 +  val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
    6.36 +  val SPEC_ALL: thm -> thm
    6.37 +  val GEN_ALL: thm -> thm
    6.38 +  val IMP_TRANS: thm -> thm -> thm
    6.39 +  val PROVE_HYP: thm -> thm -> thm
    6.40 +
    6.41 +  val CHOOSE: cterm * thm -> thm -> thm
    6.42 +  val EXISTS: cterm * cterm -> thm -> thm
    6.43 +  val EXISTL: cterm list -> thm -> thm
    6.44 +  val IT_EXISTS: (cterm*cterm) list -> thm -> thm
    6.45 +
    6.46 +  val EVEN_ORS: thm list -> thm list
    6.47 +  val DISJ_CASESL: thm -> thm list -> thm
    6.48 +
    6.49 +  val list_beta_conv: cterm -> cterm list -> thm
    6.50 +  val SUBS: thm list -> thm -> thm
    6.51 +  val simpl_conv: simpset -> thm list -> cterm -> thm
    6.52 +
    6.53 +  val rbeta: thm -> thm
    6.54 +(* For debugging my isabelle solver in the conditional rewriter *)
    6.55 +  val term_ref: term list ref
    6.56 +  val thm_ref: thm list ref
    6.57 +  val ss_ref: simpset list ref
    6.58 +  val tracing: bool ref
    6.59 +  val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
    6.60 +                             -> thm -> thm * term list
    6.61 +  val RIGHT_ASSOC: thm -> thm
    6.62 +
    6.63 +  val prove: bool -> cterm * tactic -> thm
    6.64 +end;
    6.65 +
    6.66 +structure Rules: RULES =
    6.67 +struct
    6.68 +
    6.69 +structure S = USyntax;
    6.70 +structure U = Utils;
    6.71 +structure D = Dcterm;
    6.72 +
    6.73 +
    6.74 +fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
    6.75 +
    6.76 +
    6.77 +fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
    6.78 +fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
    6.79 +
    6.80 +fun dest_thm thm =
    6.81 +  let val {prop,hyps,...} = Thm.rep_thm thm
    6.82 +  in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
    6.83 +  handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
    6.84 +
    6.85 +
    6.86 +(* Inference rules *)
    6.87 +
    6.88 +(*---------------------------------------------------------------------------
    6.89 + *        Equality (one step)
    6.90 + *---------------------------------------------------------------------------*)
    6.91 +
    6.92 +fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
    6.93 +  handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
    6.94 +
    6.95 +fun SYM thm = thm RS sym
    6.96 +  handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
    6.97 +
    6.98 +fun ALPHA thm ctm1 =
    6.99 +  let
   6.100 +    val ctm2 = Thm.cprop_of thm;
   6.101 +    val ctm2_eq = Thm.reflexive ctm2;
   6.102 +    val ctm1_eq = Thm.reflexive ctm1;
   6.103 +  in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
   6.104 +  handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
   6.105 +
   6.106 +fun rbeta th =
   6.107 +  (case D.strip_comb (cconcl th) of
   6.108 +    (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
   6.109 +  | _ => raise RULES_ERR "rbeta" "");
   6.110 +
   6.111 +
   6.112 +(*----------------------------------------------------------------------------
   6.113 + *        Implication and the assumption list
   6.114 + *
   6.115 + * Assumptions get stuck on the meta-language assumption list. Implications
   6.116 + * are in the object language, so discharging an assumption "A" from theorem
   6.117 + * "B" results in something that looks like "A --> B".
   6.118 + *---------------------------------------------------------------------------*)
   6.119 +
   6.120 +fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
   6.121 +
   6.122 +
   6.123 +(*---------------------------------------------------------------------------
   6.124 + * Implication in TFL is -->. Meta-language implication (==>) is only used
   6.125 + * in the implementation of some of the inference rules below.
   6.126 + *---------------------------------------------------------------------------*)
   6.127 +fun MP th1 th2 = th2 RS (th1 RS mp)
   6.128 +  handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
   6.129 +
   6.130 +(*forces the first argument to be a proposition if necessary*)
   6.131 +fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
   6.132 +  handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
   6.133 +
   6.134 +fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
   6.135 +
   6.136 +
   6.137 +fun FILTER_DISCH_ALL P thm =
   6.138 + let fun check tm = P (#t (Thm.rep_cterm tm))
   6.139 + in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
   6.140 +              thm (chyps thm)
   6.141 + end;
   6.142 +
   6.143 +(* freezeT expensive! *)
   6.144 +fun UNDISCH thm =
   6.145 +   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
   6.146 +   in Thm.implies_elim (thm RS mp) (ASSUME tm) end
   6.147 +   handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
   6.148 +     | THM _ => raise RULES_ERR "UNDISCH" "";
   6.149 +
   6.150 +fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
   6.151 +
   6.152 +fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
   6.153 +  handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
   6.154 +
   6.155 +
   6.156 +(*----------------------------------------------------------------------------
   6.157 + *        Conjunction
   6.158 + *---------------------------------------------------------------------------*)
   6.159 +
   6.160 +fun CONJUNCT1 thm = thm RS conjunct1
   6.161 +  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
   6.162 +
   6.163 +fun CONJUNCT2 thm = thm RS conjunct2
   6.164 +  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
   6.165 +
   6.166 +fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
   6.167 +
   6.168 +fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
   6.169 +  | LIST_CONJ [th] = th
   6.170 +  | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
   6.171 +      handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
   6.172 +
   6.173 +
   6.174 +(*----------------------------------------------------------------------------
   6.175 + *        Disjunction
   6.176 + *---------------------------------------------------------------------------*)
   6.177 +local val {prop,thy,...} = rep_thm disjI1
   6.178 +      val [P,Q] = term_vars prop
   6.179 +      val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
   6.180 +in
   6.181 +fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
   6.182 +  handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
   6.183 +end;
   6.184 +
   6.185 +local val {prop,thy,...} = rep_thm disjI2
   6.186 +      val [P,Q] = term_vars prop
   6.187 +      val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
   6.188 +in
   6.189 +fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   6.190 +  handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
   6.191 +end;
   6.192 +
   6.193 +
   6.194 +(*----------------------------------------------------------------------------
   6.195 + *
   6.196 + *                   A1 |- M1, ..., An |- Mn
   6.197 + *     ---------------------------------------------------
   6.198 + *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
   6.199 + *
   6.200 + *---------------------------------------------------------------------------*)
   6.201 +
   6.202 +
   6.203 +fun EVEN_ORS thms =
   6.204 +  let fun blue ldisjs [] _ = []
   6.205 +        | blue ldisjs (th::rst) rdisjs =
   6.206 +            let val tail = tl rdisjs
   6.207 +                val rdisj_tl = D.list_mk_disj tail
   6.208 +            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
   6.209 +               :: blue (ldisjs @ [cconcl th]) rst tail
   6.210 +            end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
   6.211 +   in blue [] thms (map cconcl thms) end;
   6.212 +
   6.213 +
   6.214 +(*----------------------------------------------------------------------------
   6.215 + *
   6.216 + *         A |- P \/ Q   B,P |- R    C,Q |- R
   6.217 + *     ---------------------------------------------------
   6.218 + *                     A U B U C |- R
   6.219 + *
   6.220 + *---------------------------------------------------------------------------*)
   6.221 +
   6.222 +fun DISJ_CASES th1 th2 th3 =
   6.223 +  let
   6.224 +    val c = D.drop_prop (cconcl th1);
   6.225 +    val (disj1, disj2) = D.dest_disj c;
   6.226 +    val th2' = DISCH disj1 th2;
   6.227 +    val th3' = DISCH disj2 th3;
   6.228 +  in
   6.229 +    th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
   6.230 +      handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
   6.231 +  end;
   6.232 +
   6.233 +
   6.234 +(*-----------------------------------------------------------------------------
   6.235 + *
   6.236 + *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
   6.237 + *     ---------------------------------------------------
   6.238 + *                           |- M
   6.239 + *
   6.240 + * Note. The list of theorems may be all jumbled up, so we have to
   6.241 + * first organize it to align with the first argument (the disjunctive
   6.242 + * theorem).
   6.243 + *---------------------------------------------------------------------------*)
   6.244 +
   6.245 +fun organize eq =    (* a bit slow - analogous to insertion sort *)
   6.246 + let fun extract a alist =
   6.247 +     let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
   6.248 +           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
   6.249 +     in ex ([],alist)
   6.250 +     end
   6.251 +     fun place [] [] = []
   6.252 +       | place (a::rst) alist =
   6.253 +           let val (item,next) = extract a alist
   6.254 +           in item::place rst next
   6.255 +           end
   6.256 +       | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
   6.257 + in place
   6.258 + end;
   6.259 +(* freezeT expensive! *)
   6.260 +fun DISJ_CASESL disjth thl =
   6.261 +   let val c = cconcl disjth
   6.262 +       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
   6.263 +                                       aconv term_of atm)
   6.264 +                              (#hyps(rep_thm th))
   6.265 +       val tml = D.strip_disj c
   6.266 +       fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
   6.267 +         | DL th [th1] = PROVE_HYP th th1
   6.268 +         | DL th [th1,th2] = DISJ_CASES th th1 th2
   6.269 +         | DL th (th1::rst) =
   6.270 +            let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
   6.271 +             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
   6.272 +   in DL (Thm.freezeT disjth) (organize eq tml thl)
   6.273 +   end;
   6.274 +
   6.275 +
   6.276 +(*----------------------------------------------------------------------------
   6.277 + *        Universals
   6.278 + *---------------------------------------------------------------------------*)
   6.279 +local (* this is fragile *)
   6.280 +      val {prop,thy,...} = rep_thm spec
   6.281 +      val x = hd (tl (term_vars prop))
   6.282 +      val cTV = ctyp_of thy (type_of x)
   6.283 +      val gspec = forall_intr (cterm_of thy x) spec
   6.284 +in
   6.285 +fun SPEC tm thm =
   6.286 +   let val {thy,T,...} = rep_cterm tm
   6.287 +       val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec
   6.288 +   in
   6.289 +      thm RS (forall_elim tm gspec')
   6.290 +   end
   6.291 +end;
   6.292 +
   6.293 +fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
   6.294 +
   6.295 +val ISPEC = SPEC
   6.296 +val ISPECL = fold ISPEC;
   6.297 +
   6.298 +(* Not optimized! Too complicated. *)
   6.299 +local val {prop,thy,...} = rep_thm allI
   6.300 +      val [P] = add_term_vars (prop, [])
   6.301 +      fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
   6.302 +      fun ctm_theta s = map (fn (i, (_, tm2)) =>
   6.303 +                             let val ctm2 = cterm_of s tm2
   6.304 +                             in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
   6.305 +                             end)
   6.306 +      fun certify s (ty_theta,tm_theta) =
   6.307 +        (cty_theta s (Vartab.dest ty_theta),
   6.308 +         ctm_theta s (Vartab.dest tm_theta))
   6.309 +in
   6.310 +fun GEN v th =
   6.311 +   let val gth = forall_intr v th
   6.312 +       val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth
   6.313 +       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   6.314 +       val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
   6.315 +       val allI2 = instantiate (certify thy theta) allI
   6.316 +       val thm = Thm.implies_elim allI2 gth
   6.317 +       val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm
   6.318 +       val prop' = tp $ (A $ Abs(x,ty,M))
   6.319 +   in ALPHA thm (cterm_of thy prop')
   6.320 +   end
   6.321 +end;
   6.322 +
   6.323 +val GENL = fold_rev GEN;
   6.324 +
   6.325 +fun GEN_ALL thm =
   6.326 +   let val {prop,thy,...} = rep_thm thm
   6.327 +       val tycheck = cterm_of thy
   6.328 +       val vlist = map tycheck (add_term_vars (prop, []))
   6.329 +  in GENL vlist thm
   6.330 +  end;
   6.331 +
   6.332 +
   6.333 +fun MATCH_MP th1 th2 =
   6.334 +   if (D.is_forall (D.drop_prop(cconcl th1)))
   6.335 +   then MATCH_MP (th1 RS spec) th2
   6.336 +   else MP th1 th2;
   6.337 +
   6.338 +
   6.339 +(*----------------------------------------------------------------------------
   6.340 + *        Existentials
   6.341 + *---------------------------------------------------------------------------*)
   6.342 +
   6.343 +
   6.344 +
   6.345 +(*---------------------------------------------------------------------------
   6.346 + * Existential elimination
   6.347 + *
   6.348 + *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
   6.349 + *      ------------------------------------     (variable v occurs nowhere)
   6.350 + *                A1 u A2 |- t'
   6.351 + *
   6.352 + *---------------------------------------------------------------------------*)
   6.353 +
   6.354 +fun CHOOSE (fvar, exth) fact =
   6.355 +  let
   6.356 +    val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
   6.357 +    val redex = D.capply lam fvar
   6.358 +    val {thy, t = t$u,...} = Thm.rep_cterm redex
   6.359 +    val residue = Thm.cterm_of thy (Term.betapply (t, u))
   6.360 +  in
   6.361 +    GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
   6.362 +      handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   6.363 +  end;
   6.364 +
   6.365 +local val {prop,thy,...} = rep_thm exI
   6.366 +      val [P,x] = term_vars prop
   6.367 +in
   6.368 +fun EXISTS (template,witness) thm =
   6.369 +   let val {prop,thy,...} = rep_thm thm
   6.370 +       val P' = cterm_of thy P
   6.371 +       val x' = cterm_of thy x
   6.372 +       val abstr = #2 (D.dest_comb template)
   6.373 +   in
   6.374 +   thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   6.375 +     handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
   6.376 +   end
   6.377 +end;
   6.378 +
   6.379 +(*----------------------------------------------------------------------------
   6.380 + *
   6.381 + *         A |- M
   6.382 + *   -------------------   [v_1,...,v_n]
   6.383 + *    A |- ?v1...v_n. M
   6.384 + *
   6.385 + *---------------------------------------------------------------------------*)
   6.386 +
   6.387 +fun EXISTL vlist th =
   6.388 +  fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
   6.389 +           vlist th;
   6.390 +
   6.391 +
   6.392 +(*----------------------------------------------------------------------------
   6.393 + *
   6.394 + *       A |- M[x_1,...,x_n]
   6.395 + *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
   6.396 + *       A |- ?y_1...y_n. M
   6.397 + *
   6.398 + *---------------------------------------------------------------------------*)
   6.399 +(* Could be improved, but needs "subst_free" for certified terms *)
   6.400 +
   6.401 +fun IT_EXISTS blist th =
   6.402 +   let val {thy,...} = rep_thm th
   6.403 +       val tych = cterm_of thy
   6.404 +       val detype = #t o rep_cterm
   6.405 +       val blist' = map (fn (x,y) => (detype x, detype y)) blist
   6.406 +       fun ex v M  = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
   6.407 +
   6.408 +  in
   6.409 +  fold_rev (fn (b as (r1,r2)) => fn thm =>
   6.410 +        EXISTS(ex r2 (subst_free [b]
   6.411 +                   (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
   6.412 +              thm)
   6.413 +       blist' th
   6.414 +  end;
   6.415 +
   6.416 +(*---------------------------------------------------------------------------
   6.417 + *  Faster version, that fails for some as yet unknown reason
   6.418 + * fun IT_EXISTS blist th =
   6.419 + *    let val {thy,...} = rep_thm th
   6.420 + *        val tych = cterm_of thy
   6.421 + *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
   6.422 + *   in
   6.423 + *  fold (fn (b as (r1,r2), thm) =>
   6.424 + *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
   6.425 + *           r1) thm)  blist th
   6.426 + *   end;
   6.427 + *---------------------------------------------------------------------------*)
   6.428 +
   6.429 +(*----------------------------------------------------------------------------
   6.430 + *        Rewriting
   6.431 + *---------------------------------------------------------------------------*)
   6.432 +
   6.433 +fun SUBS thl =
   6.434 +  rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
   6.435 +
   6.436 +val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));
   6.437 +
   6.438 +fun simpl_conv ss thl ctm =
   6.439 + rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
   6.440 +
   6.441 +
   6.442 +val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
   6.443 +
   6.444 +
   6.445 +
   6.446 +(*---------------------------------------------------------------------------
   6.447 + *                  TERMINATION CONDITION EXTRACTION
   6.448 + *---------------------------------------------------------------------------*)
   6.449 +
   6.450 +
   6.451 +(* Object language quantifier, i.e., "!" *)
   6.452 +fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   6.453 +
   6.454 +
   6.455 +(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   6.456 +fun is_cong thm =
   6.457 +  let val {prop, ...} = rep_thm thm
   6.458 +  in case prop
   6.459 +     of (Const("==>",_)$(Const("Trueprop",_)$ _) $
   6.460 +         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
   6.461 +      | _ => true
   6.462 +  end;
   6.463 +
   6.464 +
   6.465 +
   6.466 +fun dest_equal(Const ("==",_) $
   6.467 +               (Const ("Trueprop",_) $ lhs)
   6.468 +               $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
   6.469 +  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   6.470 +  | dest_equal tm = S.dest_eq tm;
   6.471 +
   6.472 +fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   6.473 +
   6.474 +fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
   6.475 +  | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
   6.476 +
   6.477 +val is_all = can (dest_all []);
   6.478 +
   6.479 +fun strip_all used fm =
   6.480 +   if (is_all fm)
   6.481 +   then let val ({Bvar, Body}, used') = dest_all used fm
   6.482 +            val (bvs, core, used'') = strip_all used' Body
   6.483 +        in ((Bvar::bvs), core, used'')
   6.484 +        end
   6.485 +   else ([], fm, used);
   6.486 +
   6.487 +fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   6.488 +  | break_all _ = raise RULES_ERR "break_all" "not a !!";
   6.489 +
   6.490 +fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
   6.491 +     let val (L,core) = list_break_all body
   6.492 +     in ((s,ty)::L, core)
   6.493 +     end
   6.494 +  | list_break_all tm = ([],tm);
   6.495 +
   6.496 +(*---------------------------------------------------------------------------
   6.497 + * Rename a term of the form
   6.498 + *
   6.499 + *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
   6.500 + *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
   6.501 + * to one of
   6.502 + *
   6.503 + *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
   6.504 + *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
   6.505 + *
   6.506 + * This prevents name problems in extraction, and helps the result to read
   6.507 + * better. There is a problem with varstructs, since they can introduce more
   6.508 + * than n variables, and some extra reasoning needs to be done.
   6.509 + *---------------------------------------------------------------------------*)
   6.510 +
   6.511 +fun get ([],_,L) = rev L
   6.512 +  | get (ant::rst,n,L) =
   6.513 +      case (list_break_all ant)
   6.514 +        of ([],_) => get (rst, n+1,L)
   6.515 +         | (vlist,body) =>
   6.516 +            let val eq = Logic.strip_imp_concl body
   6.517 +                val (f,args) = S.strip_comb (get_lhs eq)
   6.518 +                val (vstrl,_) = S.strip_abs f
   6.519 +                val names  =
   6.520 +                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
   6.521 +            in get (rst, n+1, (names,n)::L) end
   6.522 +            handle TERM _ => get (rst, n+1, L)
   6.523 +              | U.ERR _ => get (rst, n+1, L);
   6.524 +
   6.525 +(* Note: rename_params_rule counts from 1, not 0 *)
   6.526 +fun rename thm =
   6.527 +  let val {prop,thy,...} = rep_thm thm
   6.528 +      val tych = cterm_of thy
   6.529 +      val ants = Logic.strip_imp_prems prop
   6.530 +      val news = get (ants,1,[])
   6.531 +  in
   6.532 +  fold rename_params_rule news thm
   6.533 +  end;
   6.534 +
   6.535 +
   6.536 +(*---------------------------------------------------------------------------
   6.537 + * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
   6.538 + *---------------------------------------------------------------------------*)
   6.539 +
   6.540 +fun list_beta_conv tm =
   6.541 +  let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
   6.542 +      fun iter [] = Thm.reflexive tm
   6.543 +        | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
   6.544 +  in iter  end;
   6.545 +
   6.546 +
   6.547 +(*---------------------------------------------------------------------------
   6.548 + * Trace information for the rewriter
   6.549 + *---------------------------------------------------------------------------*)
   6.550 +val term_ref = ref[] : term list ref
   6.551 +val ss_ref = ref [] : simpset list ref;
   6.552 +val thm_ref = ref [] : thm list ref;
   6.553 +val tracing = ref false;
   6.554 +
   6.555 +fun say s = if !tracing then writeln s else ();
   6.556 +
   6.557 +fun print_thms s L =
   6.558 +  say (cat_lines (s :: map string_of_thm L));
   6.559 +
   6.560 +fun print_cterms s L =
   6.561 +  say (cat_lines (s :: map string_of_cterm L));
   6.562 +
   6.563 +
   6.564 +(*---------------------------------------------------------------------------
   6.565 + * General abstraction handlers, should probably go in USyntax.
   6.566 + *---------------------------------------------------------------------------*)
   6.567 +fun mk_aabs (vstr, body) =
   6.568 +  S.mk_abs {Bvar = vstr, Body = body}
   6.569 +  handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
   6.570 +
   6.571 +fun list_mk_aabs (vstrl,tm) =
   6.572 +    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
   6.573 +
   6.574 +fun dest_aabs used tm =
   6.575 +   let val ({Bvar,Body}, used') = S.dest_abs used tm
   6.576 +   in (Bvar, Body, used') end
   6.577 +   handle U.ERR _ =>
   6.578 +     let val {varstruct, body, used} = S.dest_pabs used tm
   6.579 +     in (varstruct, body, used) end;
   6.580 +
   6.581 +fun strip_aabs used tm =
   6.582 +   let val (vstr, body, used') = dest_aabs used tm
   6.583 +       val (bvs, core, used'') = strip_aabs used' body
   6.584 +   in (vstr::bvs, core, used'') end
   6.585 +   handle U.ERR _ => ([], tm, used);
   6.586 +
   6.587 +fun dest_combn tm 0 = (tm,[])
   6.588 +  | dest_combn tm n =
   6.589 +     let val {Rator,Rand} = S.dest_comb tm
   6.590 +         val (f,rands) = dest_combn Rator (n-1)
   6.591 +     in (f,Rand::rands)
   6.592 +     end;
   6.593 +
   6.594 +
   6.595 +
   6.596 +
   6.597 +local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   6.598 +      fun mk_fst tm =
   6.599 +          let val ty as Type("*", [fty,sty]) = type_of tm
   6.600 +          in  Const ("fst", ty --> fty) $ tm  end
   6.601 +      fun mk_snd tm =
   6.602 +          let val ty as Type("*", [fty,sty]) = type_of tm
   6.603 +          in  Const ("snd", ty --> sty) $ tm  end
   6.604 +in
   6.605 +fun XFILL tych x vstruct =
   6.606 +  let fun traverse p xocc L =
   6.607 +        if (is_Free p)
   6.608 +        then tych xocc::L
   6.609 +        else let val (p1,p2) = dest_pair p
   6.610 +             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   6.611 +             end
   6.612 +  in
   6.613 +  traverse vstruct x []
   6.614 +end end;
   6.615 +
   6.616 +(*---------------------------------------------------------------------------
   6.617 + * Replace a free tuple (vstr) by a universally quantified variable (a).
   6.618 + * Note that the notion of "freeness" for a tuple is different than for a
   6.619 + * variable: if variables in the tuple also occur in any other place than
   6.620 + * an occurrences of the tuple, they aren't "free" (which is thus probably
   6.621 + *  the wrong word to use).
   6.622 + *---------------------------------------------------------------------------*)
   6.623 +
   6.624 +fun VSTRUCT_ELIM tych a vstr th =
   6.625 +  let val L = S.free_vars_lr vstr
   6.626 +      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   6.627 +      val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   6.628 +      val thm2 = forall_intr_list (map tych L) thm1
   6.629 +      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   6.630 +  in refl RS
   6.631 +     rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
   6.632 +  end;
   6.633 +
   6.634 +fun PGEN tych a vstr th =
   6.635 +  let val a1 = tych a
   6.636 +      val vstr1 = tych vstr
   6.637 +  in
   6.638 +  forall_intr a1
   6.639 +     (if (is_Free vstr)
   6.640 +      then cterm_instantiate [(vstr1,a1)] th
   6.641 +      else VSTRUCT_ELIM tych a vstr th)
   6.642 +  end;
   6.643 +
   6.644 +
   6.645 +(*---------------------------------------------------------------------------
   6.646 + * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
   6.647 + *
   6.648 + *     (([x,y],N),vstr)
   6.649 + *---------------------------------------------------------------------------*)
   6.650 +fun dest_pbeta_redex used M n =
   6.651 +  let val (f,args) = dest_combn M n
   6.652 +      val dummy = dest_aabs used f
   6.653 +  in (strip_aabs used f,args)
   6.654 +  end;
   6.655 +
   6.656 +fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
   6.657 +
   6.658 +fun dest_impl tm =
   6.659 +  let val ants = Logic.strip_imp_prems tm
   6.660 +      val eq = Logic.strip_imp_concl tm
   6.661 +  in (ants,get_lhs eq)
   6.662 +  end;
   6.663 +
   6.664 +fun restricted t = isSome (S.find_term
   6.665 +                            (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
   6.666 +                            t)
   6.667 +
   6.668 +fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
   6.669 + let val globals = func::G
   6.670 +     val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
   6.671 +     val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
   6.672 +     val tc_list = ref[]: term list ref
   6.673 +     val dummy = term_ref := []
   6.674 +     val dummy = thm_ref  := []
   6.675 +     val dummy = ss_ref  := []
   6.676 +     val cut_lemma' = cut_lemma RS eq_reflection
   6.677 +     fun prover used ss thm =
   6.678 +     let fun cong_prover ss thm =
   6.679 +         let val dummy = say "cong_prover:"
   6.680 +             val cntxt = MetaSimplifier.prems_of_ss ss
   6.681 +             val dummy = print_thms "cntxt:" cntxt
   6.682 +             val dummy = say "cong rule:"
   6.683 +             val dummy = say (string_of_thm thm)
   6.684 +             val dummy = thm_ref := (thm :: !thm_ref)
   6.685 +             val dummy = ss_ref := (ss :: !ss_ref)
   6.686 +             (* Unquantified eliminate *)
   6.687 +             fun uq_eliminate (thm,imp,thy) =
   6.688 +                 let val tych = cterm_of thy
   6.689 +                     val dummy = print_cterms "To eliminate:" [tych imp]
   6.690 +                     val ants = map tych (Logic.strip_imp_prems imp)
   6.691 +                     val eq = Logic.strip_imp_concl imp
   6.692 +                     val lhs = tych(get_lhs eq)
   6.693 +                     val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
   6.694 +                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   6.695 +                       handle U.ERR _ => Thm.reflexive lhs
   6.696 +                     val dummy = print_thms "proven:" [lhs_eq_lhs1]
   6.697 +                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   6.698 +                     val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   6.699 +                  in
   6.700 +                  lhs_eeq_lhs2 COMP thm
   6.701 +                  end
   6.702 +             fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
   6.703 +              let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
   6.704 +                  val dummy = forall (op aconv) (ListPair.zip (vlist, args))
   6.705 +                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
   6.706 +                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
   6.707 +                                             imp_body
   6.708 +                  val tych = cterm_of thy
   6.709 +                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   6.710 +                  val eq1 = Logic.strip_imp_concl imp_body1
   6.711 +                  val Q = get_lhs eq1
   6.712 +                  val QeqQ1 = pbeta_reduce (tych Q)
   6.713 +                  val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   6.714 +                  val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
   6.715 +                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   6.716 +                                handle U.ERR _ => Thm.reflexive Q1
   6.717 +                  val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
   6.718 +                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   6.719 +                  val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
   6.720 +                  val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   6.721 +                  val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
   6.722 +                               ((Q2eeqQ3 RS meta_eq_to_obj_eq)
   6.723 +                                RS ((thA RS meta_eq_to_obj_eq) RS trans))
   6.724 +                                RS eq_reflection
   6.725 +                  val impth = implies_intr_list ants1 QeeqQ3
   6.726 +                  val impth1 = impth RS meta_eq_to_obj_eq
   6.727 +                  (* Need to abstract *)
   6.728 +                  val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   6.729 +              in ant_th COMP thm
   6.730 +              end
   6.731 +             fun q_eliminate (thm,imp,thy) =
   6.732 +              let val (vlist, imp_body, used') = strip_all used imp
   6.733 +                  val (ants,Q) = dest_impl imp_body
   6.734 +              in if (pbeta_redex Q) (length vlist)
   6.735 +                 then pq_eliminate (thm,thy,vlist,imp_body,Q)
   6.736 +                 else
   6.737 +                 let val tych = cterm_of thy
   6.738 +                     val ants1 = map tych ants
   6.739 +                     val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
   6.740 +                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   6.741 +                        (false,true,false) (prover used') ss' (tych Q)
   6.742 +                      handle U.ERR _ => Thm.reflexive (tych Q)
   6.743 +                     val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   6.744 +                     val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   6.745 +                     val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   6.746 +                 in
   6.747 +                 ant_th COMP thm
   6.748 +              end end
   6.749 +
   6.750 +             fun eliminate thm =
   6.751 +               case (rep_thm thm)
   6.752 +               of {prop = (Const("==>",_) $ imp $ _), thy, ...} =>
   6.753 +                   eliminate
   6.754 +                    (if not(is_all imp)
   6.755 +                     then uq_eliminate (thm,imp,thy)
   6.756 +                     else q_eliminate (thm,imp,thy))
   6.757 +                            (* Assume that the leading constant is ==,   *)
   6.758 +                | _ => thm  (* if it is not a ==>                        *)
   6.759 +         in SOME(eliminate (rename thm)) end
   6.760 +         handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
   6.761 +
   6.762 +        fun restrict_prover ss thm =
   6.763 +          let val dummy = say "restrict_prover:"
   6.764 +              val cntxt = rev(MetaSimplifier.prems_of_ss ss)
   6.765 +              val dummy = print_thms "cntxt:" cntxt
   6.766 +              val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   6.767 +                   thy,...} = rep_thm thm
   6.768 +              fun genl tm = let val vlist = subtract (op aconv) globals
   6.769 +                                           (add_term_frees(tm,[]))
   6.770 +                            in fold_rev Forall vlist tm
   6.771 +                            end
   6.772 +              (*--------------------------------------------------------------
   6.773 +               * This actually isn't quite right, since it will think that
   6.774 +               * not-fully applied occs. of "f" in the context mean that the
   6.775 +               * current call is nested. The real solution is to pass in a
   6.776 +               * term "f v1..vn" which is a pattern that any full application
   6.777 +               * of "f" will match.
   6.778 +               *-------------------------------------------------------------*)
   6.779 +              val func_name = #1(dest_Const func)
   6.780 +              fun is_func (Const (name,_)) = (name = func_name)
   6.781 +                | is_func _                = false
   6.782 +              val rcontext = rev cntxt
   6.783 +              val cncl = HOLogic.dest_Trueprop o Thm.prop_of
   6.784 +              val antl = case rcontext of [] => []
   6.785 +                         | _   => [S.list_mk_conj(map cncl rcontext)]
   6.786 +              val TC = genl(S.list_mk_imp(antl, A))
   6.787 +              val dummy = print_cterms "func:" [cterm_of thy func]
   6.788 +              val dummy = print_cterms "TC:"
   6.789 +                              [cterm_of thy (HOLogic.mk_Trueprop TC)]
   6.790 +              val dummy = tc_list := (TC :: !tc_list)
   6.791 +              val nestedp = isSome (S.find_term is_func TC)
   6.792 +              val dummy = if nestedp then say "nested" else say "not_nested"
   6.793 +              val dummy = term_ref := ([func,TC]@(!term_ref))
   6.794 +              val th' = if nestedp then raise RULES_ERR "solver" "nested function"
   6.795 +                        else let val cTC = cterm_of thy
   6.796 +                                              (HOLogic.mk_Trueprop TC)
   6.797 +                             in case rcontext of
   6.798 +                                [] => SPEC_ALL(ASSUME cTC)
   6.799 +                               | _ => MP (SPEC_ALL (ASSUME cTC))
   6.800 +                                         (LIST_CONJ rcontext)
   6.801 +                             end
   6.802 +              val th'' = th' RS thm
   6.803 +          in SOME (th'')
   6.804 +          end handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
   6.805 +    in
   6.806 +    (if (is_cong thm) then cong_prover else restrict_prover) ss thm
   6.807 +    end
   6.808 +    val ctm = cprop_of th
   6.809 +    val names = add_term_names (term_of ctm, [])
   6.810 +    val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   6.811 +      (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   6.812 +    val th2 = equal_elim th1 th
   6.813 + in
   6.814 + (th2, List.filter (not o restricted) (!tc_list))
   6.815 + end;
   6.816 +
   6.817 +
   6.818 +fun prove strict (ptm, tac) =
   6.819 +  let
   6.820 +    val {thy, t, ...} = Thm.rep_cterm ptm;
   6.821 +    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
   6.822 +  in
   6.823 +    if strict then Goal.prove ctxt [] [] t (K tac)
   6.824 +    else Goal.prove ctxt [] [] t (K tac)
   6.825 +      handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
   6.826 +  end;
   6.827 +
   6.828 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu May 31 13:18:52 2007 +0200
     7.3 @@ -0,0 +1,1008 @@
     7.4 +(*  Title:      HOL/Tools/TFL/tfl.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     7.7 +    Copyright   1997  University of Cambridge
     7.8 +
     7.9 +First part of main module.
    7.10 +*)
    7.11 +
    7.12 +signature PRIM =
    7.13 +sig
    7.14 +  val trace: bool ref
    7.15 +  val trace_thms: string -> thm list -> unit
    7.16 +  val trace_cterms: string -> cterm list -> unit
    7.17 +  type pattern
    7.18 +  val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    7.19 +  val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    7.20 +  val post_definition: thm list -> theory * (thm * pattern list) ->
    7.21 +   {rules: thm,
    7.22 +    rows: int list,
    7.23 +    TCs: term list list,
    7.24 +    full_pats_TCs: (term * term list) list}
    7.25 +  val wfrec_eqns: theory -> xstring -> thm list -> term list ->
    7.26 +   {WFR: term,
    7.27 +    SV: term list,
    7.28 +    proto_def: term,
    7.29 +    extracta: (thm * term list) list,
    7.30 +    pats: pattern list}
    7.31 +  val lazyR_def: theory -> xstring -> thm list -> term list ->
    7.32 +   {theory: theory,
    7.33 +    rules: thm,
    7.34 +    R: term,
    7.35 +    SV: term list,
    7.36 +    full_pats_TCs: (term * term list) list,
    7.37 +    patterns : pattern list}
    7.38 +  val mk_induction: theory ->
    7.39 +    {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
    7.40 +  val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm}
    7.41 +    -> theory -> {rules: thm, induction: thm, TCs: term list list}
    7.42 +    -> {rules: thm, induction: thm, nested_tcs: thm list}
    7.43 +end;
    7.44 +
    7.45 +structure Prim: PRIM =
    7.46 +struct
    7.47 +
    7.48 +val trace = ref false;
    7.49 +
    7.50 +structure R = Rules;
    7.51 +structure S = USyntax;
    7.52 +structure U = Utils;
    7.53 +
    7.54 +
    7.55 +fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg};
    7.56 +
    7.57 +val concl = #2 o R.dest_thm;
    7.58 +val hyp = #1 o R.dest_thm;
    7.59 +
    7.60 +val list_mk_type = U.end_itlist (curry (op -->));
    7.61 +
    7.62 +fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
    7.63 +
    7.64 +fun front_last [] = raise TFL_ERR "front_last" "empty list"
    7.65 +  | front_last [x] = ([],x)
    7.66 +  | front_last (h::t) =
    7.67 +     let val (pref,x) = front_last t
    7.68 +     in
    7.69 +        (h::pref,x)
    7.70 +     end;
    7.71 +
    7.72 +
    7.73 +(*---------------------------------------------------------------------------
    7.74 + * The next function is common to pattern-match translation and
    7.75 + * proof of completeness of cases for the induction theorem.
    7.76 + *
    7.77 + * The curried function "gvvariant" returns a function to generate distinct
    7.78 + * variables that are guaranteed not to be in names.  The names of
    7.79 + * the variables go u, v, ..., z, aa, ..., az, ...  The returned
    7.80 + * function contains embedded refs!
    7.81 + *---------------------------------------------------------------------------*)
    7.82 +fun gvvariant names =
    7.83 +  let val slist = ref names
    7.84 +      val vname = ref "u"
    7.85 +      fun new() =
    7.86 +         if !vname mem_string (!slist)
    7.87 +         then (vname := Symbol.bump_string (!vname);  new())
    7.88 +         else (slist := !vname :: !slist;  !vname)
    7.89 +  in
    7.90 +  fn ty => Free(new(), ty)
    7.91 +  end;
    7.92 +
    7.93 +
    7.94 +(*---------------------------------------------------------------------------
    7.95 + * Used in induction theorem production. This is the simple case of
    7.96 + * partitioning up pattern rows by the leading constructor.
    7.97 + *---------------------------------------------------------------------------*)
    7.98 +fun ipartition gv (constructors,rows) =
    7.99 +  let fun pfail s = raise TFL_ERR "partition.part" s
   7.100 +      fun part {constrs = [],   rows = [],   A} = rev A
   7.101 +        | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
   7.102 +        | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
   7.103 +        | part {constrs = c::crst, rows,     A} =
   7.104 +          let val (c, T) = dest_Const c
   7.105 +              val L = binder_types T
   7.106 +              val (in_group, not_in_group) =
   7.107 +               fold_rev (fn (row as (p::rst, rhs)) =>
   7.108 +                         fn (in_group,not_in_group) =>
   7.109 +                  let val (pc,args) = S.strip_comb p
   7.110 +                  in if (#1(dest_Const pc) = c)
   7.111 +                     then ((args@rst, rhs)::in_group, not_in_group)
   7.112 +                     else (in_group, row::not_in_group)
   7.113 +                  end)      rows ([],[])
   7.114 +              val col_types = U.take type_of (length L, #1(hd in_group))
   7.115 +          in
   7.116 +          part{constrs = crst, rows = not_in_group,
   7.117 +               A = {constructor = c,
   7.118 +                    new_formals = map gv col_types,
   7.119 +                    group = in_group}::A}
   7.120 +          end
   7.121 +  in part{constrs = constructors, rows = rows, A = []}
   7.122 +  end;
   7.123 +
   7.124 +
   7.125 +
   7.126 +(*---------------------------------------------------------------------------
   7.127 + * Each pattern carries with it a tag (i,b) where
   7.128 + * i is the clause it came from and
   7.129 + * b=true indicates that clause was given by the user
   7.130 + * (or is an instantiation of a user supplied pattern)
   7.131 + * b=false --> i = ~1
   7.132 + *---------------------------------------------------------------------------*)
   7.133 +
   7.134 +type pattern = term * (int * bool)
   7.135 +
   7.136 +fun pattern_map f (tm,x) = (f tm, x);
   7.137 +
   7.138 +fun pattern_subst theta = pattern_map (subst_free theta);
   7.139 +
   7.140 +val pat_of = fst;
   7.141 +fun row_of_pat x = fst (snd x);
   7.142 +fun given x = snd (snd x);
   7.143 +
   7.144 +(*---------------------------------------------------------------------------
   7.145 + * Produce an instance of a constructor, plus genvars for its arguments.
   7.146 + *---------------------------------------------------------------------------*)
   7.147 +fun fresh_constr ty_match colty gv c =
   7.148 +  let val (_,Ty) = dest_Const c
   7.149 +      val L = binder_types Ty
   7.150 +      and ty = body_type Ty
   7.151 +      val ty_theta = ty_match ty colty
   7.152 +      val c' = S.inst ty_theta c
   7.153 +      val gvars = map (S.inst ty_theta o gv) L
   7.154 +  in (c', gvars)
   7.155 +  end;
   7.156 +
   7.157 +
   7.158 +(*---------------------------------------------------------------------------
   7.159 + * Goes through a list of rows and picks out the ones beginning with a
   7.160 + * pattern with constructor = name.
   7.161 + *---------------------------------------------------------------------------*)
   7.162 +fun mk_group name rows =
   7.163 +  fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
   7.164 +            fn (in_group,not_in_group) =>
   7.165 +               let val (pc,args) = S.strip_comb p
   7.166 +               in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
   7.167 +                  then (((prfx,args@rst), rhs)::in_group, not_in_group)
   7.168 +                  else (in_group, row::not_in_group) end)
   7.169 +      rows ([],[]);
   7.170 +
   7.171 +(*---------------------------------------------------------------------------
   7.172 + * Partition the rows. Not efficient: we should use hashing.
   7.173 + *---------------------------------------------------------------------------*)
   7.174 +fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
   7.175 +  | partition gv ty_match
   7.176 +              (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
   7.177 +let val fresh = fresh_constr ty_match colty gv
   7.178 +     fun part {constrs = [],      rows, A} = rev A
   7.179 +       | part {constrs = c::crst, rows, A} =
   7.180 +         let val (c',gvars) = fresh c
   7.181 +             val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
   7.182 +             val in_group' =
   7.183 +                 if (null in_group)  (* Constructor not given *)
   7.184 +                 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
   7.185 +                 else in_group
   7.186 +         in
   7.187 +         part{constrs = crst,
   7.188 +              rows = not_in_group,
   7.189 +              A = {constructor = c',
   7.190 +                   new_formals = gvars,
   7.191 +                   group = in_group'}::A}
   7.192 +         end
   7.193 +in part{constrs=constructors, rows=rows, A=[]}
   7.194 +end;
   7.195 +
   7.196 +(*---------------------------------------------------------------------------
   7.197 + * Misc. routines used in mk_case
   7.198 + *---------------------------------------------------------------------------*)
   7.199 +
   7.200 +fun mk_pat (c,l) =
   7.201 +  let val L = length (binder_types (type_of c))
   7.202 +      fun build (prfx,tag,plist) =
   7.203 +          let val args   = Library.take (L,plist)
   7.204 +              and plist' = Library.drop(L,plist)
   7.205 +          in (prfx,tag,list_comb(c,args)::plist') end
   7.206 +  in map build l end;
   7.207 +
   7.208 +fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
   7.209 +  | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
   7.210 +
   7.211 +fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
   7.212 +  | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
   7.213 +
   7.214 +
   7.215 +(*----------------------------------------------------------------------------
   7.216 + * Translation of pattern terms into nested case expressions.
   7.217 + *
   7.218 + * This performs the translation and also builds the full set of patterns.
   7.219 + * Thus it supports the construction of induction theorems even when an
   7.220 + * incomplete set of patterns is given.
   7.221 + *---------------------------------------------------------------------------*)
   7.222 +
   7.223 +fun mk_case ty_info ty_match usednames range_ty =
   7.224 + let
   7.225 + fun mk_case_fail s = raise TFL_ERR "mk_case" s
   7.226 + val fresh_var = gvvariant usednames
   7.227 + val divide = partition fresh_var ty_match
   7.228 + fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
   7.229 +   | expand constructors ty (row as ((prfx, p::rst), rhs)) =
   7.230 +       if (is_Free p)
   7.231 +       then let val fresh = fresh_constr ty_match ty fresh_var
   7.232 +                fun expnd (c,gvs) =
   7.233 +                  let val capp = list_comb(c,gvs)
   7.234 +                  in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
   7.235 +                  end
   7.236 +            in map expnd (map fresh constructors)  end
   7.237 +       else [row]
   7.238 + fun mk{rows=[],...} = mk_case_fail"no rows"
   7.239 +   | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
   7.240 +        ([(prfx,tag,[])], tm)
   7.241 +   | mk{path=[], rows = _::_} = mk_case_fail"blunder"
   7.242 +   | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
   7.243 +        mk{path = path,
   7.244 +           rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
   7.245 +   | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
   7.246 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   7.247 +         val col0 = map(hd o #2) pat_rectangle
   7.248 +     in
   7.249 +     if (forall is_Free col0)
   7.250 +     then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
   7.251 +                                (ListPair.zip (col0, rights))
   7.252 +              val pat_rectangle' = map v_to_prfx pat_rectangle
   7.253 +              val (pref_patl,tm) = mk{path = rstp,
   7.254 +                                      rows = ListPair.zip (pat_rectangle',
   7.255 +                                                           rights')}
   7.256 +          in (map v_to_pats pref_patl, tm)
   7.257 +          end
   7.258 +     else
   7.259 +     let val pty as Type (ty_name,_) = type_of p
   7.260 +     in
   7.261 +     case (ty_info ty_name)
   7.262 +     of NONE => mk_case_fail("Not a known datatype: "^ty_name)
   7.263 +      | SOME{case_const,constructors} =>
   7.264 +        let
   7.265 +            val case_const_name = #1(dest_Const case_const)
   7.266 +            val nrows = List.concat (map (expand constructors pty) rows)
   7.267 +            val subproblems = divide(constructors, pty, range_ty, nrows)
   7.268 +            val groups      = map #group subproblems
   7.269 +            and new_formals = map #new_formals subproblems
   7.270 +            and constructors' = map #constructor subproblems
   7.271 +            val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
   7.272 +                           (ListPair.zip (new_formals, groups))
   7.273 +            val rec_calls = map mk news
   7.274 +            val (pat_rect,dtrees) = ListPair.unzip rec_calls
   7.275 +            val case_functions = map S.list_mk_abs
   7.276 +                                  (ListPair.zip (new_formals, dtrees))
   7.277 +            val types = map type_of (case_functions@[u]) @ [range_ty]
   7.278 +            val case_const' = Const(case_const_name, list_mk_type types)
   7.279 +            val tree = list_comb(case_const', case_functions@[u])
   7.280 +            val pat_rect1 = List.concat
   7.281 +                              (ListPair.map mk_pat (constructors', pat_rect))
   7.282 +        in (pat_rect1,tree)
   7.283 +        end
   7.284 +     end end
   7.285 + in mk
   7.286 + end;
   7.287 +
   7.288 +
   7.289 +(* Repeated variable occurrences in a pattern are not allowed. *)
   7.290 +fun FV_multiset tm =
   7.291 +   case (S.dest_term tm)
   7.292 +     of S.VAR{Name = c, Ty = T} => [Free(c, T)]
   7.293 +      | S.CONST _ => []
   7.294 +      | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
   7.295 +      | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
   7.296 +
   7.297 +fun no_repeat_vars thy pat =
   7.298 + let fun check [] = true
   7.299 +       | check (v::rst) =
   7.300 +         if member (op aconv) rst v then
   7.301 +            raise TFL_ERR "no_repeat_vars"
   7.302 +                          (quote (#1 (dest_Free v)) ^
   7.303 +                          " occurs repeatedly in the pattern " ^
   7.304 +                          quote (string_of_cterm (Thry.typecheck thy pat)))
   7.305 +         else check rst
   7.306 + in check (FV_multiset pat)
   7.307 + end;
   7.308 +
   7.309 +fun dest_atom (Free p) = p
   7.310 +  | dest_atom (Const p) = p
   7.311 +  | dest_atom  _ = raise TFL_ERR "dest_atom" "function name not an identifier";
   7.312 +
   7.313 +fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
   7.314 +
   7.315 +local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
   7.316 +      fun single [_$_] =
   7.317 +              mk_functional_err "recdef does not allow currying"
   7.318 +        | single [f] = f
   7.319 +        | single fs  =
   7.320 +              (*multiple function names?*)
   7.321 +              if length (distinct same_name fs) < length fs
   7.322 +              then mk_functional_err
   7.323 +                   "The function being declared appears with multiple types"
   7.324 +              else mk_functional_err
   7.325 +                   (Int.toString (length fs) ^
   7.326 +                    " distinct function names being declared")
   7.327 +in
   7.328 +fun mk_functional thy clauses =
   7.329 + let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
   7.330 +                   handle TERM _ => raise TFL_ERR "mk_functional"
   7.331 +                        "recursion equations must use the = relation")
   7.332 +     val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   7.333 +     val atom = single (distinct (op aconv) funcs)
   7.334 +     val (fname,ftype) = dest_atom atom
   7.335 +     val dummy = map (no_repeat_vars thy) pats
   7.336 +     val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
   7.337 +                              map (fn (t,i) => (t,(i,true))) (enumerate R))
   7.338 +     val names = foldr add_term_names [] R
   7.339 +     val atype = type_of(hd pats)
   7.340 +     and aname = Name.variant names "a"
   7.341 +     val a = Free(aname,atype)
   7.342 +     val ty_info = Thry.match_info thy
   7.343 +     val ty_match = Thry.match_type thy
   7.344 +     val range_ty = type_of (hd R)
   7.345 +     val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
   7.346 +                                    {path=[a], rows=rows}
   7.347 +     val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
   7.348 +          handle Match => mk_functional_err "error in pattern-match translation"
   7.349 +     val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
   7.350 +     val finals = map row_of_pat patts2
   7.351 +     val originals = map (row_of_pat o #2) rows
   7.352 +     val dummy = case (originals\\finals)
   7.353 +             of [] => ()
   7.354 +          | L => mk_functional_err
   7.355 + ("The following clauses are redundant (covered by preceding clauses): " ^
   7.356 +                   commas (map (fn i => Int.toString (i + 1)) L))
   7.357 + in {functional = Abs(Sign.base_name fname, ftype,
   7.358 +                      abstract_over (atom,
   7.359 +                                     absfree(aname,atype, case_tm))),
   7.360 +     pats = patts2}
   7.361 +end end;
   7.362 +
   7.363 +
   7.364 +(*----------------------------------------------------------------------------
   7.365 + *
   7.366 + *                    PRINCIPLES OF DEFINITION
   7.367 + *
   7.368 + *---------------------------------------------------------------------------*)
   7.369 +
   7.370 +
   7.371 +(*For Isabelle, the lhs of a definition must be a constant.*)
   7.372 +fun mk_const_def sign (c, Ty, rhs) =
   7.373 +  singleton (ProofContext.infer_types (ProofContext.init sign))
   7.374 +    (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
   7.375 +
   7.376 +(*Make all TVars available for instantiation by adding a ? to the front*)
   7.377 +fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
   7.378 +  | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   7.379 +  | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
   7.380 +
   7.381 +local val f_eq_wfrec_R_M =
   7.382 +           #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
   7.383 +      val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
   7.384 +      val (fname,_) = dest_Free f
   7.385 +      val (wfrec,_) = S.strip_comb rhs
   7.386 +in
   7.387 +fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
   7.388 + let val def_name = if x<>fid then
   7.389 +                        raise TFL_ERR "wfrec_definition0"
   7.390 +                                      ("Expected a definition of " ^
   7.391 +                                             quote fid ^ " but found one of " ^
   7.392 +                                      quote x)
   7.393 +                    else x ^ "_def"
   7.394 +     val wfrec_R_M =  map_types poly_tvars
   7.395 +                          (wfrec $ map_types poly_tvars R)
   7.396 +                      $ functional
   7.397 +     val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
   7.398 +     val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
   7.399 + in (thy', def) end;
   7.400 +end;
   7.401 +
   7.402 +
   7.403 +
   7.404 +(*---------------------------------------------------------------------------
   7.405 + * This structure keeps track of congruence rules that aren't derived
   7.406 + * from a datatype definition.
   7.407 + *---------------------------------------------------------------------------*)
   7.408 +fun extraction_thms thy =
   7.409 + let val {case_rewrites,case_congs} = Thry.extract_info thy
   7.410 + in (case_rewrites, case_congs)
   7.411 + end;
   7.412 +
   7.413 +
   7.414 +(*---------------------------------------------------------------------------
   7.415 + * Pair patterns with termination conditions. The full list of patterns for
   7.416 + * a definition is merged with the TCs arising from the user-given clauses.
   7.417 + * There can be fewer clauses than the full list, if the user omitted some
   7.418 + * cases. This routine is used to prepare input for mk_induction.
   7.419 + *---------------------------------------------------------------------------*)
   7.420 +fun merge full_pats TCs =
   7.421 +let fun insert (p,TCs) =
   7.422 +      let fun insrt ((x as (h,[]))::rst) =
   7.423 +                 if (p aconv h) then (p,TCs)::rst else x::insrt rst
   7.424 +            | insrt (x::rst) = x::insrt rst
   7.425 +            | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
   7.426 +      in insrt end
   7.427 +    fun pass ([],ptcl_final) = ptcl_final
   7.428 +      | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
   7.429 +in
   7.430 +  pass (TCs, map (fn p => (p,[])) full_pats)
   7.431 +end;
   7.432 +
   7.433 +
   7.434 +fun givens pats = map pat_of (List.filter given pats);
   7.435 +
   7.436 +fun post_definition meta_tflCongs (theory, (def, pats)) =
   7.437 + let val tych = Thry.typecheck theory
   7.438 +     val f = #lhs(S.dest_eq(concl def))
   7.439 +     val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   7.440 +     val pats' = List.filter given pats
   7.441 +     val given_pats = map pat_of pats'
   7.442 +     val rows = map row_of_pat pats'
   7.443 +     val WFR = #ant(S.dest_imp(concl corollary))
   7.444 +     val R = #Rand(S.dest_comb WFR)
   7.445 +     val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
   7.446 +     val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
   7.447 +                           given_pats
   7.448 +     val (case_rewrites,context_congs) = extraction_thms theory
   7.449 +     (*case_ss causes minimal simplification: bodies of case expressions are
   7.450 +       not simplified. Otherwise large examples (Red-Black trees) are too
   7.451 +       slow.*)
   7.452 +     val case_ss = Simplifier.theory_context theory
   7.453 +       (HOL_basic_ss addcongs
   7.454 +         (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites)
   7.455 +     val corollaries' = map (Simplifier.simplify case_ss) corollaries
   7.456 +     val extract = R.CONTEXT_REWRITE_RULE
   7.457 +                     (f, [R], cut_apply, meta_tflCongs@context_congs)
   7.458 +     val (rules, TCs) = ListPair.unzip (map extract corollaries')
   7.459 +     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   7.460 +     val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   7.461 +     val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   7.462 + in
   7.463 + {rules = rules1,
   7.464 +  rows = rows,
   7.465 +  full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
   7.466 +  TCs = TCs}
   7.467 + end;
   7.468 +
   7.469 +
   7.470 +(*---------------------------------------------------------------------------
   7.471 + * Perform the extraction without making the definition. Definition and
   7.472 + * extraction commute for the non-nested case.  (Deferred recdefs)
   7.473 + *
   7.474 + * The purpose of wfrec_eqns is merely to instantiate the recursion theorem
   7.475 + * and extract termination conditions: no definition is made.
   7.476 + *---------------------------------------------------------------------------*)
   7.477 +
   7.478 +fun wfrec_eqns thy fid tflCongs eqns =
   7.479 + let val {lhs,rhs} = S.dest_eq (hd eqns)
   7.480 +     val (f,args) = S.strip_comb lhs
   7.481 +     val (fname,fty) = dest_atom f
   7.482 +     val (SV,a) = front_last args    (* SV = schematic variables *)
   7.483 +     val g = list_comb(f,SV)
   7.484 +     val h = Free(fname,type_of g)
   7.485 +     val eqns1 = map (subst_free[(g,h)]) eqns
   7.486 +     val {functional as Abs(x, Ty, _),  pats} = mk_functional thy eqns1
   7.487 +     val given_pats = givens pats
   7.488 +     (* val f = Free(x,Ty) *)
   7.489 +     val Type("fun", [f_dty, f_rty]) = Ty
   7.490 +     val dummy = if x<>fid then
   7.491 +                        raise TFL_ERR "wfrec_eqns"
   7.492 +                                      ("Expected a definition of " ^
   7.493 +                                      quote fid ^ " but found one of " ^
   7.494 +                                      quote x)
   7.495 +                 else ()
   7.496 +     val (case_rewrites,context_congs) = extraction_thms thy
   7.497 +     val tych = Thry.typecheck thy
   7.498 +     val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   7.499 +     val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   7.500 +     val R = Free (Name.variant (foldr add_term_names [] eqns) Rname,
   7.501 +                   Rtype)
   7.502 +     val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
   7.503 +     val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   7.504 +     val dummy =
   7.505 +           if !trace then
   7.506 +               writeln ("ORIGINAL PROTO_DEF: " ^
   7.507 +                          Sign.string_of_term thy proto_def)
   7.508 +           else ()
   7.509 +     val R1 = S.rand WFR
   7.510 +     val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   7.511 +     val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   7.512 +     val corollaries' = map (rewrite_rule case_rewrites) corollaries
   7.513 +     fun extract X = R.CONTEXT_REWRITE_RULE
   7.514 +                       (f, R1::SV, cut_apply, tflCongs@context_congs) X
   7.515 + in {proto_def = proto_def,
   7.516 +     SV=SV,
   7.517 +     WFR=WFR,
   7.518 +     pats=pats,
   7.519 +     extracta = map extract corollaries'}
   7.520 + end;
   7.521 +
   7.522 +
   7.523 +(*---------------------------------------------------------------------------
   7.524 + * Define the constant after extracting the termination conditions. The
   7.525 + * wellfounded relation used in the definition is computed by using the
   7.526 + * choice operator on the extracted conditions (plus the condition that
   7.527 + * such a relation must be wellfounded).
   7.528 + *---------------------------------------------------------------------------*)
   7.529 +
   7.530 +fun lazyR_def thy fid tflCongs eqns =
   7.531 + let val {proto_def,WFR,pats,extracta,SV} =
   7.532 +           wfrec_eqns thy fid tflCongs eqns
   7.533 +     val R1 = S.rand WFR
   7.534 +     val f = #lhs(S.dest_eq proto_def)
   7.535 +     val (extractants,TCl) = ListPair.unzip extracta
   7.536 +     val dummy = if !trace
   7.537 +                 then (writeln "Extractants = ";
   7.538 +                       prths extractants;
   7.539 +                       ())
   7.540 +                 else ()
   7.541 +     val TCs = foldr (gen_union (op aconv)) [] TCl
   7.542 +     val full_rqt = WFR::TCs
   7.543 +     val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   7.544 +     val R'abs = S.rand R'
   7.545 +     val proto_def' = subst_free[(R1,R')] proto_def
   7.546 +     val dummy = if !trace then writeln ("proto_def' = " ^
   7.547 +                                         Sign.string_of_term
   7.548 +                                         thy proto_def')
   7.549 +                           else ()
   7.550 +     val {lhs,rhs} = S.dest_eq proto_def'
   7.551 +     val (c,args) = S.strip_comb lhs
   7.552 +     val (name,Ty) = dest_atom c
   7.553 +     val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
   7.554 +     val ([def0], theory) =
   7.555 +       thy
   7.556 +       |> PureThy.add_defs_i false
   7.557 +            [Thm.no_attributes (fid ^ "_def", defn)]
   7.558 +     val def = Thm.freezeT def0;
   7.559 +     val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
   7.560 +                           else ()
   7.561 +     (* val fconst = #lhs(S.dest_eq(concl def))  *)
   7.562 +     val tych = Thry.typecheck theory
   7.563 +     val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   7.564 +         (*lcp: a lot of object-logic inference to remove*)
   7.565 +     val baz = R.DISCH_ALL
   7.566 +                 (fold_rev R.DISCH full_rqt_prop
   7.567 +                  (R.LIST_CONJ extractants))
   7.568 +     val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
   7.569 +                           else ()
   7.570 +     val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   7.571 +     val SV' = map tych SV;
   7.572 +     val SVrefls = map reflexive SV'
   7.573 +     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
   7.574 +                   SVrefls def)
   7.575 +                RS meta_eq_to_obj_eq
   7.576 +     val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
   7.577 +     val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
   7.578 +     val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
   7.579 +                       theory Hilbert_Choice*)
   7.580 +         thm "Hilbert_Choice.tfl_some"
   7.581 +         handle ERROR msg => cat_error msg
   7.582 +    "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
   7.583 +     val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
   7.584 + in {theory = theory, R=R1, SV=SV,
   7.585 +     rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
   7.586 +     full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   7.587 +     patterns = pats}
   7.588 + end;
   7.589 +
   7.590 +
   7.591 +
   7.592 +(*----------------------------------------------------------------------------
   7.593 + *
   7.594 + *                           INDUCTION THEOREM
   7.595 + *
   7.596 + *---------------------------------------------------------------------------*)
   7.597 +
   7.598 +
   7.599 +(*------------------------  Miscellaneous function  --------------------------
   7.600 + *
   7.601 + *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
   7.602 + *     -----------------------------------------------------------
   7.603 + *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
   7.604 + *                        ...
   7.605 + *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
   7.606 + *
   7.607 + * This function is totally ad hoc. Used in the production of the induction
   7.608 + * theorem. The nchotomy theorem can have clauses that look like
   7.609 + *
   7.610 + *     ?v1..vn. z = C vn..v1
   7.611 + *
   7.612 + * in which the order of quantification is not the order of occurrence of the
   7.613 + * quantified variables as arguments to C. Since we have no control over this
   7.614 + * aspect of the nchotomy theorem, we make the correspondence explicit by
   7.615 + * pairing the incoming new variable with the term it gets beta-reduced into.
   7.616 + *---------------------------------------------------------------------------*)
   7.617 +
   7.618 +fun alpha_ex_unroll (xlist, tm) =
   7.619 +  let val (qvars,body) = S.strip_exists tm
   7.620 +      val vlist = #2(S.strip_comb (S.rhs body))
   7.621 +      val plist = ListPair.zip (vlist, xlist)
   7.622 +      val args = map (the o AList.lookup (op aconv) plist) qvars
   7.623 +                   handle Option => sys_error
   7.624 +                       "TFL fault [alpha_ex_unroll]: no correspondence"
   7.625 +      fun build ex      []   = []
   7.626 +        | build (_$rex) (v::rst) =
   7.627 +           let val ex1 = Term.betapply(rex, v)
   7.628 +           in  ex1 :: build ex1 rst
   7.629 +           end
   7.630 +     val (nex::exl) = rev (tm::build tm args)
   7.631 +  in
   7.632 +  (nex, ListPair.zip (args, rev exl))
   7.633 +  end;
   7.634 +
   7.635 +
   7.636 +
   7.637 +(*----------------------------------------------------------------------------
   7.638 + *
   7.639 + *             PROVING COMPLETENESS OF PATTERNS
   7.640 + *
   7.641 + *---------------------------------------------------------------------------*)
   7.642 +
   7.643 +fun mk_case ty_info usednames thy =
   7.644 + let
   7.645 + val divide = ipartition (gvvariant usednames)
   7.646 + val tych = Thry.typecheck thy
   7.647 + fun tych_binding(x,y) = (tych x, tych y)
   7.648 + fun fail s = raise TFL_ERR "mk_case" s
   7.649 + fun mk{rows=[],...} = fail"no rows"
   7.650 +   | mk{path=[], rows = [([], (thm, bindings))]} =
   7.651 +                         R.IT_EXISTS (map tych_binding bindings) thm
   7.652 +   | mk{path = u::rstp, rows as (p::_, _)::_} =
   7.653 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   7.654 +         val col0 = map hd pat_rectangle
   7.655 +         val pat_rectangle' = map tl pat_rectangle
   7.656 +     in
   7.657 +     if (forall is_Free col0) (* column 0 is all variables *)
   7.658 +     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
   7.659 +                                (ListPair.zip (rights, col0))
   7.660 +          in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
   7.661 +          end
   7.662 +     else                     (* column 0 is all constructors *)
   7.663 +     let val Type (ty_name,_) = type_of p
   7.664 +     in
   7.665 +     case (ty_info ty_name)
   7.666 +     of NONE => fail("Not a known datatype: "^ty_name)
   7.667 +      | SOME{constructors,nchotomy} =>
   7.668 +        let val thm' = R.ISPEC (tych u) nchotomy
   7.669 +            val disjuncts = S.strip_disj (concl thm')
   7.670 +            val subproblems = divide(constructors, rows)
   7.671 +            val groups      = map #group subproblems
   7.672 +            and new_formals = map #new_formals subproblems
   7.673 +            val existentials = ListPair.map alpha_ex_unroll
   7.674 +                                   (new_formals, disjuncts)
   7.675 +            val constraints = map #1 existentials
   7.676 +            val vexl = map #2 existentials
   7.677 +            fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
   7.678 +            val news = map (fn (nf,rows,c) => {path = nf@rstp,
   7.679 +                                               rows = map (expnd c) rows})
   7.680 +                           (U.zip3 new_formals groups constraints)
   7.681 +            val recursive_thms = map mk news
   7.682 +            val build_exists = Library.foldr
   7.683 +                                (fn((x,t), th) =>
   7.684 +                                 R.CHOOSE (tych x, R.ASSUME (tych t)) th)
   7.685 +            val thms' = ListPair.map build_exists (vexl, recursive_thms)
   7.686 +            val same_concls = R.EVEN_ORS thms'
   7.687 +        in R.DISJ_CASESL thm' same_concls
   7.688 +        end
   7.689 +     end end
   7.690 + in mk
   7.691 + end;
   7.692 +
   7.693 +
   7.694 +fun complete_cases thy =
   7.695 + let val tych = Thry.typecheck thy
   7.696 +     val ty_info = Thry.induct_info thy
   7.697 + in fn pats =>
   7.698 + let val names = foldr add_term_names [] pats
   7.699 +     val T = type_of (hd pats)
   7.700 +     val aname = Name.variant names "a"
   7.701 +     val vname = Name.variant (aname::names) "v"
   7.702 +     val a = Free (aname, T)
   7.703 +     val v = Free (vname, T)
   7.704 +     val a_eq_v = HOLogic.mk_eq(a,v)
   7.705 +     val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   7.706 +                           (R.REFL (tych a))
   7.707 +     val th0 = R.ASSUME (tych a_eq_v)
   7.708 +     val rows = map (fn x => ([x], (th0,[]))) pats
   7.709 + in
   7.710 + R.GEN (tych a)
   7.711 +       (R.RIGHT_ASSOC
   7.712 +          (R.CHOOSE(tych v, ex_th0)
   7.713 +                (mk_case ty_info (vname::aname::names)
   7.714 +                 thy {path=[v], rows=rows})))
   7.715 + end end;
   7.716 +
   7.717 +
   7.718 +(*---------------------------------------------------------------------------
   7.719 + * Constructing induction hypotheses: one for each recursive call.
   7.720 + *
   7.721 + * Note. R will never occur as a variable in the ind_clause, because
   7.722 + * to do so, it would have to be from a nested definition, and we don't
   7.723 + * allow nested defns to have R variable.
   7.724 + *
   7.725 + * Note. When the context is empty, there can be no local variables.
   7.726 + *---------------------------------------------------------------------------*)
   7.727 +(*
   7.728 +local infix 5 ==>
   7.729 +      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   7.730 +in
   7.731 +fun build_ih f P (pat,TCs) =
   7.732 + let val globals = S.free_vars_lr pat
   7.733 +     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
   7.734 +     fun dest_TC tm =
   7.735 +         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   7.736 +             val (R,y,_) = S.dest_relation R_y_pat
   7.737 +             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   7.738 +         in case cntxt
   7.739 +              of [] => (P_y, (tm,[]))
   7.740 +               | _  => let
   7.741 +                    val imp = S.list_mk_conj cntxt ==> P_y
   7.742 +                    val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
   7.743 +                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   7.744 +                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   7.745 +         end
   7.746 + in case TCs
   7.747 +    of [] => (S.list_mk_forall(globals, P$pat), [])
   7.748 +     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   7.749 +                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   7.750 +             in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   7.751 +             end
   7.752 + end
   7.753 +end;
   7.754 +*)
   7.755 +
   7.756 +local infix 5 ==>
   7.757 +      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   7.758 +in
   7.759 +fun build_ih f (P,SV) (pat,TCs) =
   7.760 + let val pat_vars = S.free_vars_lr pat
   7.761 +     val globals = pat_vars@SV
   7.762 +     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
   7.763 +     fun dest_TC tm =
   7.764 +         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   7.765 +             val (R,y,_) = S.dest_relation R_y_pat
   7.766 +             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   7.767 +         in case cntxt
   7.768 +              of [] => (P_y, (tm,[]))
   7.769 +               | _  => let
   7.770 +                    val imp = S.list_mk_conj cntxt ==> P_y
   7.771 +                    val lvs = subtract (op aconv) globals (S.free_vars_lr imp)
   7.772 +                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   7.773 +                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   7.774 +         end
   7.775 + in case TCs
   7.776 +    of [] => (S.list_mk_forall(pat_vars, P$pat), [])
   7.777 +     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   7.778 +                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   7.779 +             in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
   7.780 +             end
   7.781 + end
   7.782 +end;
   7.783 +
   7.784 +(*---------------------------------------------------------------------------
   7.785 + * This function makes good on the promise made in "build_ih".
   7.786 + *
   7.787 + * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",
   7.788 + *           TCs = TC_1[pat] ... TC_n[pat]
   7.789 + *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
   7.790 + *---------------------------------------------------------------------------*)
   7.791 +fun prove_case f thy (tm,TCs_locals,thm) =
   7.792 + let val tych = Thry.typecheck thy
   7.793 +     val antc = tych(#ant(S.dest_imp tm))
   7.794 +     val thm' = R.SPEC_ALL thm
   7.795 +     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
   7.796 +     fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
   7.797 +     fun mk_ih ((TC,locals),th2,nested) =
   7.798 +         R.GENL (map tych locals)
   7.799 +            (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
   7.800 +             else if S.is_imp (concl TC) then R.IMP_TRANS TC th2
   7.801 +             else R.MP th2 TC)
   7.802 + in
   7.803 + R.DISCH antc
   7.804 + (if S.is_imp(concl thm') (* recursive calls in this clause *)
   7.805 +  then let val th1 = R.ASSUME antc
   7.806 +           val TCs = map #1 TCs_locals
   7.807 +           val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
   7.808 +                            #2 o S.strip_forall) TCs
   7.809 +           val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
   7.810 +                            TCs_locals
   7.811 +           val th2list = map (U.C R.SPEC th1 o tych) ylist
   7.812 +           val nlist = map nested TCs
   7.813 +           val triples = U.zip3 TClist th2list nlist
   7.814 +           val Pylist = map mk_ih triples
   7.815 +       in R.MP thm' (R.LIST_CONJ Pylist) end
   7.816 +  else thm')
   7.817 + end;
   7.818 +
   7.819 +
   7.820 +(*---------------------------------------------------------------------------
   7.821 + *
   7.822 + *         x = (v1,...,vn)  |- M[x]
   7.823 + *    ---------------------------------------------
   7.824 + *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
   7.825 + *
   7.826 + *---------------------------------------------------------------------------*)
   7.827 +fun LEFT_ABS_VSTRUCT tych thm =
   7.828 +  let fun CHOOSER v (tm,thm) =
   7.829 +        let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
   7.830 +        in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
   7.831 +        end
   7.832 +      val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
   7.833 +      val {lhs,rhs} = S.dest_eq veq
   7.834 +      val L = S.free_vars_lr rhs
   7.835 +  in  #2 (fold_rev CHOOSER L (veq,thm))  end;
   7.836 +
   7.837 +
   7.838 +(*----------------------------------------------------------------------------
   7.839 + * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
   7.840 + *
   7.841 + * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
   7.842 + * recursion induction (Rinduct) by proving the antecedent of Sinduct from
   7.843 + * the antecedent of Rinduct.
   7.844 + *---------------------------------------------------------------------------*)
   7.845 +fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
   7.846 +let val tych = Thry.typecheck thy
   7.847 +    val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   7.848 +    val (pats,TCsl) = ListPair.unzip pat_TCs_list
   7.849 +    val case_thm = complete_cases thy pats
   7.850 +    val domain = (type_of o hd) pats
   7.851 +    val Pname = Name.variant (foldr (Library.foldr add_term_names)
   7.852 +                              [] (pats::TCsl)) "P"
   7.853 +    val P = Free(Pname, domain --> HOLogic.boolT)
   7.854 +    val Sinduct = R.SPEC (tych P) Sinduction
   7.855 +    val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   7.856 +    val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
   7.857 +    val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   7.858 +    val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   7.859 +    val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
   7.860 +    val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   7.861 +    val proved_cases = map (prove_case fconst thy) tasks
   7.862 +    val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases))
   7.863 +                    "v",
   7.864 +                  domain)
   7.865 +    val vtyped = tych v
   7.866 +    val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   7.867 +    val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
   7.868 +                          (substs, proved_cases)
   7.869 +    val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
   7.870 +    val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
   7.871 +    val dc = R.MP Sinduct dant
   7.872 +    val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
   7.873 +    val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
   7.874 +    val dc' = fold_rev (R.GEN o tych) vars
   7.875 +                       (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
   7.876 +in
   7.877 +   R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
   7.878 +end
   7.879 +handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
   7.880 +
   7.881 +
   7.882 +
   7.883 +
   7.884 +(*---------------------------------------------------------------------------
   7.885 + *
   7.886 + *                        POST PROCESSING
   7.887 + *
   7.888 + *---------------------------------------------------------------------------*)
   7.889 +
   7.890 +
   7.891 +fun simplify_induction thy hth ind =
   7.892 +  let val tych = Thry.typecheck thy
   7.893 +      val (asl,_) = R.dest_thm ind
   7.894 +      val (_,tc_eq_tc') = R.dest_thm hth
   7.895 +      val tc = S.lhs tc_eq_tc'
   7.896 +      fun loop [] = ind
   7.897 +        | loop (asm::rst) =
   7.898 +          if (can (Thry.match_term thy asm) tc)
   7.899 +          then R.UNDISCH
   7.900 +                 (R.MATCH_MP
   7.901 +                     (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
   7.902 +                     hth)
   7.903 +         else loop rst
   7.904 +  in loop asl
   7.905 +end;
   7.906 +
   7.907 +
   7.908 +(*---------------------------------------------------------------------------
   7.909 + * The termination condition is an antecedent to the rule, and an
   7.910 + * assumption to the theorem.
   7.911 + *---------------------------------------------------------------------------*)
   7.912 +fun elim_tc tcthm (rule,induction) =
   7.913 +   (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
   7.914 +
   7.915 +
   7.916 +fun trace_thms s L =
   7.917 +  if !trace then writeln (cat_lines (s :: map string_of_thm L))
   7.918 +  else ();
   7.919 +
   7.920 +fun trace_cterms s L =
   7.921 +  if !trace then writeln (cat_lines (s :: map string_of_cterm L))
   7.922 +  else ();;
   7.923 +
   7.924 +
   7.925 +fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
   7.926 +let val tych = Thry.typecheck theory
   7.927 +    val prove = R.prove strict;
   7.928 +
   7.929 +   (*---------------------------------------------------------------------
   7.930 +    * Attempt to eliminate WF condition. It's the only assumption of rules
   7.931 +    *---------------------------------------------------------------------*)
   7.932 +   val (rules1,induction1)  =
   7.933 +       let val thm = prove(tych(HOLogic.mk_Trueprop
   7.934 +                                  (hd(#1(R.dest_thm rules)))),
   7.935 +                             wf_tac)
   7.936 +       in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
   7.937 +       end handle U.ERR _ => (rules,induction);
   7.938 +
   7.939 +   (*----------------------------------------------------------------------
   7.940 +    * The termination condition (tc) is simplified to |- tc = tc' (there
   7.941 +    * might not be a change!) and then 3 attempts are made:
   7.942 +    *
   7.943 +    *   1. if |- tc = T, then eliminate it with eqT; otherwise,
   7.944 +    *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
   7.945 +    *   3. replace tc by tc' in both the rules and the induction theorem.
   7.946 +    *---------------------------------------------------------------------*)
   7.947 +
   7.948 +   fun simplify_tc tc (r,ind) =
   7.949 +       let val tc1 = tych tc
   7.950 +           val _ = trace_cterms "TC before simplification: " [tc1]
   7.951 +           val tc_eq = simplifier tc1
   7.952 +           val _ = trace_thms "result: " [tc_eq]
   7.953 +       in
   7.954 +       elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   7.955 +       handle U.ERR _ =>
   7.956 +        (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   7.957 +                  (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
   7.958 +                           terminator)))
   7.959 +                 (r,ind)
   7.960 +         handle U.ERR _ =>
   7.961 +          (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
   7.962 +           simplify_induction theory tc_eq ind))
   7.963 +       end
   7.964 +
   7.965 +   (*----------------------------------------------------------------------
   7.966 +    * Nested termination conditions are harder to get at, since they are
   7.967 +    * left embedded in the body of the function (and in induction
   7.968 +    * theorem hypotheses). Our "solution" is to simplify them, and try to
   7.969 +    * prove termination, but leave the application of the resulting theorem
   7.970 +    * to a higher level. So things go much as in "simplify_tc": the
   7.971 +    * termination condition (tc) is simplified to |- tc = tc' (there might
   7.972 +    * not be a change) and then 2 attempts are made:
   7.973 +    *
   7.974 +    *   1. if |- tc = T, then return |- tc; otherwise,
   7.975 +    *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
   7.976 +    *   3. return |- tc = tc'
   7.977 +    *---------------------------------------------------------------------*)
   7.978 +   fun simplify_nested_tc tc =
   7.979 +      let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
   7.980 +      in
   7.981 +      R.GEN_ALL
   7.982 +       (R.MATCH_MP Thms.eqT tc_eq
   7.983 +        handle U.ERR _ =>
   7.984 +          (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   7.985 +                      (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
   7.986 +                               terminator))
   7.987 +            handle U.ERR _ => tc_eq))
   7.988 +      end
   7.989 +
   7.990 +   (*-------------------------------------------------------------------
   7.991 +    * Attempt to simplify the termination conditions in each rule and
   7.992 +    * in the induction theorem.
   7.993 +    *-------------------------------------------------------------------*)
   7.994 +   fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
   7.995 +   fun loop ([],extras,R,ind) = (rev R, ind, extras)
   7.996 +     | loop ((r,ftcs)::rst, nthms, R, ind) =
   7.997 +        let val tcs = #1(strip_imp (concl r))
   7.998 +            val extra_tcs = subtract (op aconv) tcs ftcs
   7.999 +            val extra_tc_thms = map simplify_nested_tc extra_tcs
  7.1000 +            val (r1,ind1) = fold simplify_tc tcs (r,ind)
  7.1001 +            val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
  7.1002 +        in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
  7.1003 +        end
  7.1004 +   val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
  7.1005 +   val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
  7.1006 +in
  7.1007 +  {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
  7.1008 +end;
  7.1009 +
  7.1010 +
  7.1011 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/TFL/thms.ML	Thu May 31 13:18:52 2007 +0200
     8.3 @@ -0,0 +1,20 @@
     8.4 +(*  Title:      HOL/Tools/TFL/thms.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     8.7 +    Copyright   1997  University of Cambridge
     8.8 +*)
     8.9 +
    8.10 +structure Thms =
    8.11 +struct
    8.12 +  val WFREC_COROLLARY = thm "tfl_wfrec";
    8.13 +  val WF_INDUCTION_THM = thm "tfl_wf_induct";
    8.14 +  val CUT_DEF = thm "cut_def";
    8.15 +  val eqT = thm "tfl_eq_True";
    8.16 +  val rev_eq_mp = thm "tfl_rev_eq_mp";
    8.17 +  val simp_thm = thm "tfl_simp_thm";
    8.18 +  val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
    8.19 +  val imp_trans = thm "tfl_imp_trans";
    8.20 +  val disj_assoc = thm "tfl_disj_assoc";
    8.21 +  val tfl_disjE = thm "tfl_disjE";
    8.22 +  val choose_thm = thm "tfl_exE";
    8.23 +end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/TFL/thry.ML	Thu May 31 13:18:52 2007 +0200
     9.3 @@ -0,0 +1,82 @@
     9.4 +(*  Title:      HOL/Tools/TFL/thry.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     9.7 +    Copyright   1997  University of Cambridge
     9.8 +*)
     9.9 +
    9.10 +signature THRY =
    9.11 +sig
    9.12 +  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
    9.13 +  val match_type: theory -> typ -> typ -> (typ * typ) list
    9.14 +  val typecheck: theory -> term -> cterm
    9.15 +  (*datatype facts of various flavours*)
    9.16 +  val match_info: theory -> string -> {constructors: term list, case_const: term} option
    9.17 +  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
    9.18 +  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
    9.19 +end;
    9.20 +
    9.21 +structure Thry: THRY =
    9.22 +struct
    9.23 +
    9.24 +
    9.25 +fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
    9.26 +
    9.27 +
    9.28 +(*---------------------------------------------------------------------------
    9.29 + *    Matching
    9.30 + *---------------------------------------------------------------------------*)
    9.31 +
    9.32 +local
    9.33 +
    9.34 +fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
    9.35 +
    9.36 +in
    9.37 +
    9.38 +fun match_term thry pat ob =
    9.39 +  let
    9.40 +    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
    9.41 +    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
    9.42 +  in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    9.43 +  end;
    9.44 +
    9.45 +fun match_type thry pat ob =
    9.46 +  map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
    9.47 +
    9.48 +end;
    9.49 +
    9.50 +
    9.51 +(*---------------------------------------------------------------------------
    9.52 + * Typing
    9.53 + *---------------------------------------------------------------------------*)
    9.54 +
    9.55 +fun typecheck thry t =
    9.56 +  Thm.cterm_of thry t
    9.57 +    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
    9.58 +      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
    9.59 +
    9.60 +
    9.61 +(*---------------------------------------------------------------------------
    9.62 + * Get information about datatypes
    9.63 + *---------------------------------------------------------------------------*)
    9.64 +
    9.65 +fun match_info thy dtco =
    9.66 +  case (DatatypePackage.get_datatype thy dtco,
    9.67 +         DatatypePackage.get_datatype_constrs thy dtco) of
    9.68 +      (SOME { case_name, ... }, SOME constructors) =>
    9.69 +        SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
    9.70 +    | _ => NONE;
    9.71 +
    9.72 +fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of
    9.73 +        NONE => NONE
    9.74 +      | SOME {nchotomy, ...} =>
    9.75 +          SOME {nchotomy = nchotomy,
    9.76 +                constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco};
    9.77 +
    9.78 +fun extract_info thy =
    9.79 + let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy
    9.80 + in {case_congs = map (mk_meta_eq o #case_cong) infos,
    9.81 +     case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
    9.82 + end;
    9.83 +
    9.84 +
    9.85 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu May 31 13:18:52 2007 +0200
    10.3 @@ -0,0 +1,409 @@
    10.4 +(*  Title:      HOL/Tools/TFL/usyntax.ML
    10.5 +    ID:         $Id$
    10.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    10.7 +    Copyright   1997  University of Cambridge
    10.8 +
    10.9 +Emulation of HOL's abstract syntax functions.
   10.10 +*)
   10.11 +
   10.12 +signature USYNTAX =
   10.13 +sig
   10.14 +  datatype lambda = VAR   of {Name : string, Ty : typ}
   10.15 +                  | CONST of {Name : string, Ty : typ}
   10.16 +                  | COMB  of {Rator: term, Rand : term}
   10.17 +                  | LAMB  of {Bvar : term, Body : term}
   10.18 +
   10.19 +  val alpha : typ
   10.20 +
   10.21 +  (* Types *)
   10.22 +  val type_vars  : typ -> typ list
   10.23 +  val type_varsl : typ list -> typ list
   10.24 +  val mk_vartype : string -> typ
   10.25 +  val is_vartype : typ -> bool
   10.26 +  val strip_prod_type : typ -> typ list
   10.27 +
   10.28 +  (* Terms *)
   10.29 +  val free_vars_lr : term -> term list
   10.30 +  val type_vars_in_term : term -> typ list
   10.31 +  val dest_term  : term -> lambda
   10.32 +
   10.33 +  (* Prelogic *)
   10.34 +  val inst      : (typ*typ) list -> term -> term
   10.35 +
   10.36 +  (* Construction routines *)
   10.37 +  val mk_abs    :{Bvar  : term, Body : term} -> term
   10.38 +
   10.39 +  val mk_imp    :{ant : term, conseq :  term} -> term
   10.40 +  val mk_select :{Bvar : term, Body : term} -> term
   10.41 +  val mk_forall :{Bvar : term, Body : term} -> term
   10.42 +  val mk_exists :{Bvar : term, Body : term} -> term
   10.43 +  val mk_conj   :{conj1 : term, conj2 : term} -> term
   10.44 +  val mk_disj   :{disj1 : term, disj2 : term} -> term
   10.45 +  val mk_pabs   :{varstruct : term, body : term} -> term
   10.46 +
   10.47 +  (* Destruction routines *)
   10.48 +  val dest_const: term -> {Name : string, Ty : typ}
   10.49 +  val dest_comb : term -> {Rator : term, Rand : term}
   10.50 +  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
   10.51 +  val dest_eq     : term -> {lhs : term, rhs : term}
   10.52 +  val dest_imp    : term -> {ant : term, conseq : term}
   10.53 +  val dest_forall : term -> {Bvar : term, Body : term}
   10.54 +  val dest_exists : term -> {Bvar : term, Body : term}
   10.55 +  val dest_neg    : term -> term
   10.56 +  val dest_conj   : term -> {conj1 : term, conj2 : term}
   10.57 +  val dest_disj   : term -> {disj1 : term, disj2 : term}
   10.58 +  val dest_pair   : term -> {fst : term, snd : term}
   10.59 +  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
   10.60 +
   10.61 +  val lhs   : term -> term
   10.62 +  val rhs   : term -> term
   10.63 +  val rand  : term -> term
   10.64 +
   10.65 +  (* Query routines *)
   10.66 +  val is_imp    : term -> bool
   10.67 +  val is_forall : term -> bool
   10.68 +  val is_exists : term -> bool
   10.69 +  val is_neg    : term -> bool
   10.70 +  val is_conj   : term -> bool
   10.71 +  val is_disj   : term -> bool
   10.72 +  val is_pair   : term -> bool
   10.73 +  val is_pabs   : term -> bool
   10.74 +
   10.75 +  (* Construction of a term from a list of Preterms *)
   10.76 +  val list_mk_abs    : (term list * term) -> term
   10.77 +  val list_mk_imp    : (term list * term) -> term
   10.78 +  val list_mk_forall : (term list * term) -> term
   10.79 +  val list_mk_conj   : term list -> term
   10.80 +
   10.81 +  (* Destructing a term to a list of Preterms *)
   10.82 +  val strip_comb     : term -> (term * term list)
   10.83 +  val strip_abs      : term -> (term list * term)
   10.84 +  val strip_imp      : term -> (term list * term)
   10.85 +  val strip_forall   : term -> (term list * term)
   10.86 +  val strip_exists   : term -> (term list * term)
   10.87 +  val strip_disj     : term -> term list
   10.88 +
   10.89 +  (* Miscellaneous *)
   10.90 +  val mk_vstruct : typ -> term list -> term
   10.91 +  val gen_all    : term -> term
   10.92 +  val find_term  : (term -> bool) -> term -> term option
   10.93 +  val dest_relation : term -> term * term * term
   10.94 +  val is_WFR : term -> bool
   10.95 +  val ARB : typ -> term
   10.96 +end;
   10.97 +
   10.98 +structure USyntax: USYNTAX =
   10.99 +struct
  10.100 +
  10.101 +infix 4 ##;
  10.102 +
  10.103 +fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
  10.104 +
  10.105 +
  10.106 +(*---------------------------------------------------------------------------
  10.107 + *
  10.108 + *                            Types
  10.109 + *
  10.110 + *---------------------------------------------------------------------------*)
  10.111 +val mk_prim_vartype = TVar;
  10.112 +fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
  10.113 +
  10.114 +(* But internally, it's useful *)
  10.115 +fun dest_vtype (TVar x) = x
  10.116 +  | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
  10.117 +
  10.118 +val is_vartype = can dest_vtype;
  10.119 +
  10.120 +val type_vars  = map mk_prim_vartype o typ_tvars
  10.121 +fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
  10.122 +
  10.123 +val alpha  = mk_vartype "'a"
  10.124 +val beta   = mk_vartype "'b"
  10.125 +
  10.126 +val strip_prod_type = HOLogic.prodT_factors;
  10.127 +
  10.128 +
  10.129 +
  10.130 +(*---------------------------------------------------------------------------
  10.131 + *
  10.132 + *                              Terms
  10.133 + *
  10.134 + *---------------------------------------------------------------------------*)
  10.135 +
  10.136 +(* Free variables, in order of occurrence, from left to right in the
  10.137 + * syntax tree. *)
  10.138 +fun free_vars_lr tm =
  10.139 +  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
  10.140 +      fun add (t, frees) = case t of
  10.141 +            Free   _ => if (memb t frees) then frees else t::frees
  10.142 +          | Abs (_,_,body) => add(body,frees)
  10.143 +          | f$t =>  add(t, add(f, frees))
  10.144 +          | _ => frees
  10.145 +  in rev(add(tm,[]))
  10.146 +  end;
  10.147 +
  10.148 +
  10.149 +
  10.150 +val type_vars_in_term = map mk_prim_vartype o term_tvars;
  10.151 +
  10.152 +
  10.153 +
  10.154 +(* Prelogic *)
  10.155 +fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
  10.156 +fun inst theta = subst_vars (map dest_tybinding theta,[])
  10.157 +
  10.158 +
  10.159 +(* Construction routines *)
  10.160 +
  10.161 +fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
  10.162 +  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
  10.163 +  | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
  10.164 +
  10.165 +
  10.166 +fun mk_imp{ant,conseq} =
  10.167 +   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
  10.168 +   in list_comb(c,[ant,conseq])
  10.169 +   end;
  10.170 +
  10.171 +fun mk_select (r as {Bvar,Body}) =
  10.172 +  let val ty = type_of Bvar
  10.173 +      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
  10.174 +  in list_comb(c,[mk_abs r])
  10.175 +  end;
  10.176 +
  10.177 +fun mk_forall (r as {Bvar,Body}) =
  10.178 +  let val ty = type_of Bvar
  10.179 +      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
  10.180 +  in list_comb(c,[mk_abs r])
  10.181 +  end;
  10.182 +
  10.183 +fun mk_exists (r as {Bvar,Body}) =
  10.184 +  let val ty = type_of Bvar
  10.185 +      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
  10.186 +  in list_comb(c,[mk_abs r])
  10.187 +  end;
  10.188 +
  10.189 +
  10.190 +fun mk_conj{conj1,conj2} =
  10.191 +   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
  10.192 +   in list_comb(c,[conj1,conj2])
  10.193 +   end;
  10.194 +
  10.195 +fun mk_disj{disj1,disj2} =
  10.196 +   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
  10.197 +   in list_comb(c,[disj1,disj2])
  10.198 +   end;
  10.199 +
  10.200 +fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
  10.201 +
  10.202 +local
  10.203 +fun mk_uncurry(xt,yt,zt) =
  10.204 +    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
  10.205 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  10.206 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
  10.207 +fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
  10.208 +in
  10.209 +fun mk_pabs{varstruct,body} =
  10.210 + let fun mpa (varstruct, body) =
  10.211 +       if is_var varstruct
  10.212 +       then mk_abs {Bvar = varstruct, Body = body}
  10.213 +       else let val {fst, snd} = dest_pair varstruct
  10.214 +            in mk_uncurry (type_of fst, type_of snd, type_of body) $
  10.215 +               mpa (fst, mpa (snd, body))
  10.216 +            end
  10.217 + in mpa (varstruct, body) end
  10.218 + handle TYPE _ => raise USYN_ERR "mk_pabs" "";
  10.219 +end;
  10.220 +
  10.221 +(* Destruction routines *)
  10.222 +
  10.223 +datatype lambda = VAR   of {Name : string, Ty : typ}
  10.224 +                | CONST of {Name : string, Ty : typ}
  10.225 +                | COMB  of {Rator: term, Rand : term}
  10.226 +                | LAMB  of {Bvar : term, Body : term};
  10.227 +
  10.228 +
  10.229 +fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
  10.230 +  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
  10.231 +  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
  10.232 +  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
  10.233 +  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
  10.234 +                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
  10.235 +                               end
  10.236 +  | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
  10.237 +
  10.238 +fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
  10.239 +  | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
  10.240 +
  10.241 +fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
  10.242 +  | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
  10.243 +
  10.244 +fun dest_abs used (a as Abs(s, ty, M)) =
  10.245 +     let
  10.246 +       val s' = Name.variant used s;
  10.247 +       val v = Free(s', ty);
  10.248 +     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
  10.249 +     end
  10.250 +  | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
  10.251 +
  10.252 +fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
  10.253 +  | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
  10.254 +
  10.255 +fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
  10.256 +  | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
  10.257 +
  10.258 +fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
  10.259 +  | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
  10.260 +
  10.261 +fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
  10.262 +  | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
  10.263 +
  10.264 +fun dest_neg(Const("not",_) $ M) = M
  10.265 +  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
  10.266 +
  10.267 +fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
  10.268 +  | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
  10.269 +
  10.270 +fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
  10.271 +  | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
  10.272 +
  10.273 +fun mk_pair{fst,snd} =
  10.274 +   let val ty1 = type_of fst
  10.275 +       val ty2 = type_of snd
  10.276 +       val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
  10.277 +   in list_comb(c,[fst,snd])
  10.278 +   end;
  10.279 +
  10.280 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  10.281 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
  10.282 +
  10.283 +
  10.284 +local  fun ucheck t = (if #Name(dest_const t) = "split" then t
  10.285 +                       else raise Match)
  10.286 +in
  10.287 +fun dest_pabs used tm =
  10.288 +   let val ({Bvar,Body}, used') = dest_abs used tm
  10.289 +   in {varstruct = Bvar, body = Body, used = used'}
  10.290 +   end handle Utils.ERR _ =>
  10.291 +          let val {Rator,Rand} = dest_comb tm
  10.292 +              val _ = ucheck Rator
  10.293 +              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
  10.294 +              val {varstruct = rv, body, used = used''} = dest_pabs used' body
  10.295 +          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
  10.296 +          end
  10.297 +end;
  10.298 +
  10.299 +
  10.300 +val lhs   = #lhs o dest_eq
  10.301 +val rhs   = #rhs o dest_eq
  10.302 +val rand  = #Rand o dest_comb
  10.303 +
  10.304 +
  10.305 +(* Query routines *)
  10.306 +val is_imp    = can dest_imp
  10.307 +val is_forall = can dest_forall
  10.308 +val is_exists = can dest_exists
  10.309 +val is_neg    = can dest_neg
  10.310 +val is_conj   = can dest_conj
  10.311 +val is_disj   = can dest_disj
  10.312 +val is_pair   = can dest_pair
  10.313 +val is_pabs   = can (dest_pabs [])
  10.314 +
  10.315 +
  10.316 +(* Construction of a cterm from a list of Terms *)
  10.317 +
  10.318 +fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
  10.319 +
  10.320 +(* These others are almost never used *)
  10.321 +fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
  10.322 +fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
  10.323 +val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
  10.324 +
  10.325 +
  10.326 +(* Need to reverse? *)
  10.327 +fun gen_all tm = list_mk_forall(term_frees tm, tm);
  10.328 +
  10.329 +(* Destructing a cterm to a list of Terms *)
  10.330 +fun strip_comb tm =
  10.331 +   let fun dest(M$N, A) = dest(M, N::A)
  10.332 +         | dest x = x
  10.333 +   in dest(tm,[])
  10.334 +   end;
  10.335 +
  10.336 +fun strip_abs(tm as Abs _) =
  10.337 +       let val ({Bvar,Body}, _) = dest_abs [] tm
  10.338 +           val (bvs, core) = strip_abs Body
  10.339 +       in (Bvar::bvs, core)
  10.340 +       end
  10.341 +  | strip_abs M = ([],M);
  10.342 +
  10.343 +
  10.344 +fun strip_imp fm =
  10.345 +   if (is_imp fm)
  10.346 +   then let val {ant,conseq} = dest_imp fm
  10.347 +            val (was,wb) = strip_imp conseq
  10.348 +        in ((ant::was), wb)
  10.349 +        end
  10.350 +   else ([],fm);
  10.351 +
  10.352 +fun strip_forall fm =
  10.353 +   if (is_forall fm)
  10.354 +   then let val {Bvar,Body} = dest_forall fm
  10.355 +            val (bvs,core) = strip_forall Body
  10.356 +        in ((Bvar::bvs), core)
  10.357 +        end
  10.358 +   else ([],fm);
  10.359 +
  10.360 +
  10.361 +fun strip_exists fm =
  10.362 +   if (is_exists fm)
  10.363 +   then let val {Bvar, Body} = dest_exists fm
  10.364 +            val (bvs,core) = strip_exists Body
  10.365 +        in (Bvar::bvs, core)
  10.366 +        end
  10.367 +   else ([],fm);
  10.368 +
  10.369 +fun strip_disj w =
  10.370 +   if (is_disj w)
  10.371 +   then let val {disj1,disj2} = dest_disj w
  10.372 +        in (strip_disj disj1@strip_disj disj2)
  10.373 +        end
  10.374 +   else [w];
  10.375 +
  10.376 +
  10.377 +(* Miscellaneous *)
  10.378 +
  10.379 +fun mk_vstruct ty V =
  10.380 +  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
  10.381 +              let val (ltm,vs1) = follow_prod_type ty1 vs
  10.382 +                  val (rtm,vs2) = follow_prod_type ty2 vs1
  10.383 +              in (mk_pair{fst=ltm, snd=rtm}, vs2) end
  10.384 +        | follow_prod_type _ (v::vs) = (v,vs)
  10.385 +  in #1 (follow_prod_type ty V)  end;
  10.386 +
  10.387 +
  10.388 +(* Search a term for a sub-term satisfying the predicate p. *)
  10.389 +fun find_term p =
  10.390 +   let fun find tm =
  10.391 +      if (p tm) then SOME tm
  10.392 +      else case tm of
  10.393 +          Abs(_,_,body) => find body
  10.394 +        | (t$u)         => (case find t of NONE => find u | some => some)
  10.395 +        | _             => NONE
  10.396 +   in find
  10.397 +   end;
  10.398 +
  10.399 +fun dest_relation tm =
  10.400 +   if (type_of tm = HOLogic.boolT)
  10.401 +   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
  10.402 +        in (R,y,x)
  10.403 +        end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
  10.404 +   else raise USYN_ERR "dest_relation" "not a boolean term";
  10.405 +
  10.406 +fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
  10.407 +  | is_WFR _                 = false;
  10.408 +
  10.409 +fun ARB ty = mk_select{Bvar=Free("v",ty),
  10.410 +                       Body=Const("True",HOLogic.boolT)};
  10.411 +
  10.412 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/TFL/utils.ML	Thu May 31 13:18:52 2007 +0200
    11.3 @@ -0,0 +1,59 @@
    11.4 +(*  Title:      HOL/Tools/TFL/utils.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    11.7 +    Copyright   1997  University of Cambridge
    11.8 +
    11.9 +Basic utilities.
   11.10 +*)
   11.11 +
   11.12 +signature UTILS =
   11.13 +sig
   11.14 +  exception ERR of {module: string, func: string, mesg: string}
   11.15 +  val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   11.16 +  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
   11.17 +  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   11.18 +  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
   11.19 +  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
   11.20 +  val take: ('a -> 'b) -> int * 'a list -> 'b list
   11.21 +end;
   11.22 +
   11.23 +structure Utils: UTILS =
   11.24 +struct
   11.25 +
   11.26 +(*standard exception for TFL*)
   11.27 +exception ERR of {module: string, func: string, mesg: string};
   11.28 +
   11.29 +fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
   11.30 +
   11.31 +
   11.32 +fun C f x y = f y x
   11.33 +
   11.34 +fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short")
   11.35 +  | end_itlist f [x] = x 
   11.36 +  | end_itlist f (x :: xs) = f x (end_itlist f xs);
   11.37 +
   11.38 +fun itlist2 f L1 L2 base_value =
   11.39 + let fun it ([],[]) = base_value
   11.40 +       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
   11.41 +       | it _ = raise UTILS_ERR "itlist2" "different length lists"
   11.42 + in  it (L1,L2)
   11.43 + end;
   11.44 +
   11.45 +fun pluck p  =
   11.46 +  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
   11.47 +        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
   11.48 +  in fn L => remv(L,[])
   11.49 +  end;
   11.50 +
   11.51 +fun take f =
   11.52 +  let fun grab(0,L) = []
   11.53 +        | grab(n, x::rst) = f x::grab(n-1,rst)
   11.54 +  in grab
   11.55 +  end;
   11.56 +
   11.57 +fun zip3 [][][] = []
   11.58 +  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
   11.59 +  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
   11.60 +
   11.61 +
   11.62 +end;