renamed .sml files to .ML;
authorwenzelm
Wed Jan 03 21:20:40 2001 +0100 (2001-01-03)
changeset 1076970b9b0cfe05f
parent 10768 a7282df327c6
child 10770 4858ad0b8f38
renamed .sml files to .ML;
proper handling of Isabelle exceptions;
tuned;
TFL/dcterm.ML
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
TFL/thms.ML
TFL/thry.ML
TFL/usyntax.ML
TFL/utils.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/dcterm.ML	Wed Jan 03 21:20:40 2001 +0100
     1.3 @@ -0,0 +1,200 @@
     1.4 +(*  Title:      TFL/dcterm.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +(*---------------------------------------------------------------------------
    1.11 + * Derived efficient cterm destructors.
    1.12 + *---------------------------------------------------------------------------*)
    1.13 +
    1.14 +signature DCTERM =
    1.15 +sig
    1.16 +  val dest_comb: cterm -> cterm * cterm
    1.17 +  val dest_abs: string option -> cterm -> cterm * cterm
    1.18 +  val capply: cterm -> cterm -> cterm
    1.19 +  val cabs: cterm -> cterm -> cterm
    1.20 +  val mk_conj: cterm * cterm -> cterm
    1.21 +  val mk_disj: cterm * cterm -> cterm
    1.22 +  val mk_exists: cterm * cterm -> cterm
    1.23 +  val dest_conj: cterm -> cterm * cterm
    1.24 +  val dest_const: cterm -> {Name: string, Ty: typ}
    1.25 +  val dest_disj: cterm -> cterm * cterm
    1.26 +  val dest_eq: cterm -> cterm * cterm
    1.27 +  val dest_exists: cterm -> cterm * cterm
    1.28 +  val dest_forall: cterm -> cterm * cterm
    1.29 +  val dest_imp: cterm -> cterm * cterm
    1.30 +  val dest_let: cterm -> cterm * cterm
    1.31 +  val dest_neg: cterm -> cterm
    1.32 +  val dest_pair: cterm -> cterm * cterm
    1.33 +  val dest_var: cterm -> {Name:string, Ty:typ}
    1.34 +  val is_conj: cterm -> bool
    1.35 +  val is_cons: cterm -> bool
    1.36 +  val is_disj: cterm -> bool
    1.37 +  val is_eq: cterm -> bool
    1.38 +  val is_exists: cterm -> bool
    1.39 +  val is_forall: cterm -> bool
    1.40 +  val is_imp: cterm -> bool
    1.41 +  val is_let: cterm -> bool
    1.42 +  val is_neg: cterm -> bool
    1.43 +  val is_pair: cterm -> bool
    1.44 +  val list_mk_disj: cterm list -> cterm
    1.45 +  val strip_abs: cterm -> cterm list * cterm
    1.46 +  val strip_comb: cterm -> cterm * cterm list
    1.47 +  val strip_disj: cterm -> cterm list
    1.48 +  val strip_exists: cterm -> cterm list * cterm
    1.49 +  val strip_forall: cterm -> cterm list * cterm
    1.50 +  val strip_imp: cterm -> cterm list * cterm
    1.51 +  val drop_prop: cterm -> cterm
    1.52 +  val mk_prop: cterm -> cterm
    1.53 +end;
    1.54 +
    1.55 +structure Dcterm: DCTERM =
    1.56 +struct
    1.57 +
    1.58 +structure U = Utils;
    1.59 +
    1.60 +fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
    1.61 +
    1.62 +
    1.63 +fun dest_comb t = Thm.dest_comb t
    1.64 +  handle CTERM msg => raise ERR "dest_comb" msg;
    1.65 +
    1.66 +fun dest_abs a t = Thm.dest_abs a t
    1.67 +  handle CTERM msg => raise ERR "dest_abs" msg;
    1.68 +
    1.69 +fun capply t u = Thm.capply t u
    1.70 +  handle CTERM msg => raise ERR "capply" msg;
    1.71 +
    1.72 +fun cabs a t = Thm.cabs a t
    1.73 +  handle CTERM msg => raise ERR "cabs" msg;
    1.74 +
    1.75 +
    1.76 +(*---------------------------------------------------------------------------
    1.77 + * Some simple constructor functions.
    1.78 + *---------------------------------------------------------------------------*)
    1.79 +
    1.80 +val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;
    1.81 +
    1.82 +fun mk_exists (r as (Bvar, Body)) =
    1.83 +  let val ty = #T(rep_cterm Bvar)
    1.84 +      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    1.85 +  in capply c (uncurry cabs r) end;
    1.86 +
    1.87 +
    1.88 +local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    1.89 +in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
    1.90 +end;
    1.91 +
    1.92 +local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    1.93 +in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
    1.94 +end;
    1.95 +
    1.96 +
    1.97 +(*---------------------------------------------------------------------------
    1.98 + * The primitives.
    1.99 + *---------------------------------------------------------------------------*)
   1.100 +fun dest_const ctm =
   1.101 +   (case #t(rep_cterm ctm)
   1.102 +      of Const(s,ty) => {Name = s, Ty = ty}
   1.103 +       | _ => raise ERR "dest_const" "not a constant");
   1.104 +
   1.105 +fun dest_var ctm =
   1.106 +   (case #t(rep_cterm ctm)
   1.107 +      of Var((s,i),ty) => {Name=s, Ty=ty}
   1.108 +       | Free(s,ty)    => {Name=s, Ty=ty}
   1.109 +       |             _ => raise ERR "dest_var" "not a variable");
   1.110 +
   1.111 +
   1.112 +(*---------------------------------------------------------------------------
   1.113 + * Derived destructor operations.
   1.114 + *---------------------------------------------------------------------------*)
   1.115 +
   1.116 +fun dest_monop expected tm =
   1.117 + let
   1.118 +   fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
   1.119 +   val (c, N) = dest_comb tm handle U.ERR _ => err ();
   1.120 +   val name = #Name (dest_const c handle U.ERR _ => err ());
   1.121 + in if name = expected then N else err () end;
   1.122 +
   1.123 +fun dest_binop expected tm =
   1.124 + let
   1.125 +   fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
   1.126 +   val (M, N) = dest_comb tm handle U.ERR _ => err ()
   1.127 + in (dest_monop expected M, N) handle U.ERR _ => err () end;
   1.128 +
   1.129 +fun dest_binder expected tm =
   1.130 +  dest_abs None (dest_monop expected tm)
   1.131 +  handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
   1.132 +
   1.133 +
   1.134 +val dest_neg    = dest_monop "not"
   1.135 +val dest_pair   = dest_binop "Pair";
   1.136 +val dest_eq     = dest_binop "op ="
   1.137 +val dest_imp    = dest_binop "op -->"
   1.138 +val dest_conj   = dest_binop "op &"
   1.139 +val dest_disj   = dest_binop "op |"
   1.140 +val dest_cons   = dest_binop "Cons"
   1.141 +val dest_let    = Library.swap o dest_binop "Let";
   1.142 +val dest_select = dest_binder "Eps"
   1.143 +val dest_exists = dest_binder "Ex"
   1.144 +val dest_forall = dest_binder "All"
   1.145 +
   1.146 +(* Query routines *)
   1.147 +
   1.148 +val is_eq     = can dest_eq
   1.149 +val is_imp    = can dest_imp
   1.150 +val is_select = can dest_select
   1.151 +val is_forall = can dest_forall
   1.152 +val is_exists = can dest_exists
   1.153 +val is_neg    = can dest_neg
   1.154 +val is_conj   = can dest_conj
   1.155 +val is_disj   = can dest_disj
   1.156 +val is_pair   = can dest_pair
   1.157 +val is_let    = can dest_let
   1.158 +val is_cons   = can dest_cons
   1.159 +
   1.160 +
   1.161 +(*---------------------------------------------------------------------------
   1.162 + * Iterated creation.
   1.163 + *---------------------------------------------------------------------------*)
   1.164 +val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
   1.165 +
   1.166 +(*---------------------------------------------------------------------------
   1.167 + * Iterated destruction. (To the "right" in a term.)
   1.168 + *---------------------------------------------------------------------------*)
   1.169 +fun strip break tm =
   1.170 +  let fun dest (p as (ctm,accum)) =
   1.171 +        let val (M,N) = break ctm
   1.172 +        in dest (N, M::accum)
   1.173 +        end handle U.ERR _ => p
   1.174 +  in dest (tm,[])
   1.175 +  end;
   1.176 +
   1.177 +fun rev2swap (x,l) = (rev l, x);
   1.178 +
   1.179 +val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
   1.180 +val strip_imp    = rev2swap o strip dest_imp
   1.181 +val strip_abs    = rev2swap o strip (dest_abs None)
   1.182 +val strip_forall = rev2swap o strip dest_forall
   1.183 +val strip_exists = rev2swap o strip dest_exists
   1.184 +
   1.185 +val strip_disj   = rev o (op::) o strip dest_disj
   1.186 +
   1.187 +
   1.188 +(*---------------------------------------------------------------------------
   1.189 + * Going into and out of prop
   1.190 + *---------------------------------------------------------------------------*)
   1.191 +
   1.192 +fun mk_prop ctm =
   1.193 +  let val {t, sign, ...} = Thm.rep_cterm ctm in
   1.194 +    if can HOLogic.dest_Trueprop t then ctm
   1.195 +    else Thm.cterm_of sign (HOLogic.mk_Trueprop t)
   1.196 +  end
   1.197 +  handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
   1.198 +    | TERM (msg, _) => raise ERR "mk_prop" msg;
   1.199 +
   1.200 +fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
   1.201 +
   1.202 +
   1.203 +end;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/TFL/post.ML	Wed Jan 03 21:20:40 2001 +0100
     2.3 @@ -0,0 +1,229 @@
     2.4 +(*  Title:      TFL/post.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     2.7 +    Copyright   1997  University of Cambridge
     2.8 +
     2.9 +Second part of main module (postprocessing of TFL definitions).
    2.10 +*)
    2.11 +
    2.12 +signature TFL =
    2.13 +sig
    2.14 +  val trace: bool ref
    2.15 +  val quiet_mode: bool ref
    2.16 +  val message: string -> unit
    2.17 +  val tgoalw: theory -> thm list -> thm list -> thm list
    2.18 +  val tgoal: theory -> thm list -> thm list
    2.19 +  val std_postprocessor: claset -> simpset -> thm list -> theory ->
    2.20 +    {induction: thm, rules: thm, TCs: term list list} ->
    2.21 +    {induction: thm, rules: thm, nested_tcs: thm list}
    2.22 +  val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    2.23 +    term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    2.24 +  val define: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    2.25 +    string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    2.26 +  val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
    2.27 +  val defer: theory -> thm list -> xstring -> string list -> theory * thm
    2.28 +end;
    2.29 +
    2.30 +structure Tfl: TFL =
    2.31 +struct
    2.32 +
    2.33 +structure S = USyntax
    2.34 +
    2.35 +
    2.36 +(* messages *)
    2.37 +
    2.38 +val trace = Prim.trace
    2.39 +
    2.40 +val quiet_mode = ref false;
    2.41 +fun message s = if ! quiet_mode then () else writeln s;
    2.42 +
    2.43 +
    2.44 +(* misc *)
    2.45 +
    2.46 +fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT;
    2.47 +
    2.48 +
    2.49 +(*---------------------------------------------------------------------------
    2.50 + * Extract termination goals so that they can be put it into a goalstack, or
    2.51 + * have a tactic directly applied to them.
    2.52 + *--------------------------------------------------------------------------*)
    2.53 +fun termination_goals rules =
    2.54 +    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
    2.55 +      (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
    2.56 +
    2.57 +(*---------------------------------------------------------------------------
    2.58 + * Finds the termination conditions in (highly massaged) definition and
    2.59 + * puts them into a goalstack.
    2.60 + *--------------------------------------------------------------------------*)
    2.61 +fun tgoalw thy defs rules =
    2.62 +  case termination_goals rules of
    2.63 +      [] => error "tgoalw: no termination conditions to prove"
    2.64 +    | L  => goalw_cterm defs
    2.65 +              (Thm.cterm_of (Theory.sign_of thy)
    2.66 +                        (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
    2.67 +
    2.68 +fun tgoal thy = tgoalw thy [];
    2.69 +
    2.70 +(*---------------------------------------------------------------------------
    2.71 + * Three postprocessors are applied to the definition.  It
    2.72 + * attempts to prove wellfoundedness of the given relation, simplifies the
    2.73 + * non-proved termination conditions, and finally attempts to prove the
    2.74 + * simplified termination conditions.
    2.75 + *--------------------------------------------------------------------------*)
    2.76 +fun std_postprocessor cs ss wfs =
    2.77 +  Prim.postprocess
    2.78 +   {wf_tac     = REPEAT (ares_tac wfs 1),
    2.79 +    terminator = asm_simp_tac ss 1
    2.80 +                 THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    2.81 +    simplifier = Rules.simpl_conv ss []};
    2.82 +
    2.83 +
    2.84 +
    2.85 +val concl = #2 o Rules.dest_thm;
    2.86 +
    2.87 +(*---------------------------------------------------------------------------
    2.88 + * Postprocess a definition made by "define". This is a separate stage of
    2.89 + * processing from the definition stage.
    2.90 + *---------------------------------------------------------------------------*)
    2.91 +local
    2.92 +structure R = Rules
    2.93 +structure U = Utils
    2.94 +
    2.95 +(* The rest of these local definitions are for the tricky nested case *)
    2.96 +val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
    2.97 +
    2.98 +fun id_thm th =
    2.99 +   let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
   2.100 +   in lhs aconv rhs end
   2.101 +   handle U.ERR _ => false;
   2.102 +   
   2.103 +
   2.104 +fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
   2.105 +val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
   2.106 +val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
   2.107 +fun mk_meta_eq r = case concl_of r of
   2.108 +     Const("==",_)$_$_ => r
   2.109 +  |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
   2.110 +  |   _ => r RS P_imp_P_eq_True
   2.111 +
   2.112 +(*Is this the best way to invoke the simplifier??*)
   2.113 +fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
   2.114 +
   2.115 +fun join_assums th =
   2.116 +  let val {sign,...} = rep_thm th
   2.117 +      val tych = cterm_of sign
   2.118 +      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   2.119 +      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   2.120 +      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   2.121 +      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
   2.122 +  in
   2.123 +    R.GEN_ALL
   2.124 +      (R.DISCH_ALL
   2.125 +         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   2.126 +  end
   2.127 +  val gen_all = S.gen_all
   2.128 +in
   2.129 +fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
   2.130 +  let
   2.131 +    val _ = message "Proving induction theorem ..."
   2.132 +    val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
   2.133 +    val _ = message "Postprocessing ...";
   2.134 +    val {rules, induction, nested_tcs} =
   2.135 +      std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
   2.136 +  in
   2.137 +  case nested_tcs
   2.138 +  of [] => {induction=induction, rules=rules,tcs=[]}
   2.139 +  | L  => let val dummy = message "Simplifying nested TCs ..."
   2.140 +              val (solved,simplified,stubborn) =
   2.141 +               U.itlist (fn th => fn (So,Si,St) =>
   2.142 +                     if (id_thm th) then (So, Si, th::St) else
   2.143 +                     if (solved th) then (th::So, Si, St)
   2.144 +                     else (So, th::Si, St)) nested_tcs ([],[],[])
   2.145 +              val simplified' = map join_assums simplified
   2.146 +              val rewr = full_simplify (ss addsimps (solved @ simplified'));
   2.147 +              val induction' = rewr induction
   2.148 +              and rules'     = rewr rules
   2.149 +          in
   2.150 +          {induction = induction',
   2.151 +               rules = rules',
   2.152 +                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   2.153 +                           (simplified@stubborn)}
   2.154 +          end
   2.155 +  end;
   2.156 +
   2.157 +
   2.158 +(*lcp: curry the predicate of the induction rule*)
   2.159 +fun curry_rule rl = split_rule_var
   2.160 +                        (head_of (HOLogic.dest_Trueprop (concl_of rl)),
   2.161 +                         rl);
   2.162 +
   2.163 +(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   2.164 +val meta_outer =
   2.165 +    curry_rule o standard o
   2.166 +    rule_by_tactic (REPEAT
   2.167 +                    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
   2.168 +                                ORELSE' etac conjE)));
   2.169 +
   2.170 +(*Strip off the outer !P*)
   2.171 +val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   2.172 +
   2.173 +fun simplify_defn thy cs ss congs wfs id pats def0 =
   2.174 +   let val def = freezeT def0 RS meta_eq_to_obj_eq
   2.175 +       val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
   2.176 +       val {lhs=f,rhs} = S.dest_eq (concl def)
   2.177 +       val (_,[R,_]) = S.strip_comb rhs
   2.178 +       val {induction, rules, tcs} =
   2.179 +             proof_stage cs ss wfs theory
   2.180 +               {f = f, R = R, rules = rules,
   2.181 +                full_pats_TCs = full_pats_TCs,
   2.182 +                TCs = TCs}
   2.183 +       val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
   2.184 +   in  {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
   2.185 +        rules = ListPair.zip(rules', rows),
   2.186 +        tcs = (termination_goals rules') @ tcs}
   2.187 +   end
   2.188 +  handle U.ERR {mesg,func,module} =>
   2.189 +               error (mesg ^
   2.190 +                      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   2.191 +
   2.192 +(*---------------------------------------------------------------------------
   2.193 + * Defining a function with an associated termination relation.
   2.194 + *---------------------------------------------------------------------------*)
   2.195 +fun define_i thy cs ss congs wfs fid R eqs =
   2.196 +  let val {functional,pats} = Prim.mk_functional thy eqs
   2.197 +      val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
   2.198 +  in (thy, simplify_defn thy cs ss congs wfs fid pats def) end;
   2.199 +
   2.200 +fun define thy cs ss congs wfs fid R seqs =
   2.201 +  define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
   2.202 +    handle U.ERR {mesg,...} => error mesg;
   2.203 +
   2.204 +
   2.205 +(*---------------------------------------------------------------------------
   2.206 + *
   2.207 + *     Definitions with synthesized termination relation
   2.208 + *
   2.209 + *---------------------------------------------------------------------------*)
   2.210 +
   2.211 +fun func_of_cond_eqn tm =
   2.212 +  #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
   2.213 +
   2.214 +fun defer_i thy congs fid eqs =
   2.215 + let val {rules,R,theory,full_pats_TCs,SV,...} =
   2.216 +             Prim.lazyR_def thy (Sign.base_name fid) congs eqs
   2.217 +     val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
   2.218 +     val dummy = message "Proving induction theorem ...";
   2.219 +     val induction = Prim.mk_induction theory
   2.220 +                        {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
   2.221 + in (theory,
   2.222 +     (*return the conjoined induction rule and recursion equations,
   2.223 +       with assumptions remaining to discharge*)
   2.224 +     standard (induction RS (rules RS conjI)))
   2.225 + end
   2.226 +
   2.227 +fun defer thy congs fid seqs =
   2.228 +  defer_i thy congs fid (map (read_term thy) seqs)
   2.229 +    handle U.ERR {mesg,...} => error mesg;
   2.230 +end;
   2.231 +
   2.232 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/TFL/rules.ML	Wed Jan 03 21:20:40 2001 +0100
     3.3 @@ -0,0 +1,824 @@
     3.4 +(*  Title:      TFL/rules.sml
     3.5 +    ID:         $Id$
     3.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     3.7 +    Copyright   1997  University of Cambridge
     3.8 +
     3.9 +Emulation of HOL inference rules for TFL
    3.10 +*)
    3.11 +
    3.12 +signature RULES =
    3.13 +sig
    3.14 +  val dest_thm : thm -> term list * term
    3.15 +
    3.16 +  (* Inference rules *)
    3.17 +  val REFL      :cterm -> thm
    3.18 +  val ASSUME    :cterm -> thm
    3.19 +  val MP        :thm -> thm -> thm
    3.20 +  val MATCH_MP  :thm -> thm -> thm
    3.21 +  val CONJUNCT1 :thm -> thm
    3.22 +  val CONJUNCT2 :thm -> thm
    3.23 +  val CONJUNCTS :thm -> thm list
    3.24 +  val DISCH     :cterm -> thm -> thm
    3.25 +  val UNDISCH   :thm  -> thm
    3.26 +  val SPEC      :cterm -> thm -> thm
    3.27 +  val ISPEC     :cterm -> thm -> thm
    3.28 +  val ISPECL    :cterm list -> thm -> thm
    3.29 +  val GEN       :cterm -> thm -> thm
    3.30 +  val GENL      :cterm list -> thm -> thm
    3.31 +  val LIST_CONJ :thm list -> thm
    3.32 +
    3.33 +  val SYM : thm -> thm
    3.34 +  val DISCH_ALL : thm -> thm
    3.35 +  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
    3.36 +  val SPEC_ALL  : thm -> thm
    3.37 +  val GEN_ALL   : thm -> thm
    3.38 +  val IMP_TRANS : thm -> thm -> thm
    3.39 +  val PROVE_HYP : thm -> thm -> thm
    3.40 +
    3.41 +  val CHOOSE : cterm * thm -> thm -> thm
    3.42 +  val EXISTS : cterm * cterm -> thm -> thm
    3.43 +  val EXISTL : cterm list -> thm -> thm
    3.44 +  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
    3.45 +
    3.46 +  val EVEN_ORS : thm list -> thm list
    3.47 +  val DISJ_CASESL : thm -> thm list -> thm
    3.48 +
    3.49 +  val list_beta_conv : cterm -> cterm list -> thm
    3.50 +  val SUBS : thm list -> thm -> thm
    3.51 +  val simpl_conv : simpset -> thm list -> cterm -> thm
    3.52 +
    3.53 +  val rbeta : thm -> thm
    3.54 +(* For debugging my isabelle solver in the conditional rewriter *)
    3.55 +  val term_ref : term list ref
    3.56 +  val thm_ref : thm list ref
    3.57 +  val mss_ref : meta_simpset list ref
    3.58 +  val tracing : bool ref
    3.59 +  val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
    3.60 +                             -> thm -> thm * term list
    3.61 +  val RIGHT_ASSOC : thm -> thm
    3.62 +
    3.63 +  val prove : cterm * tactic -> thm
    3.64 +end;
    3.65 +
    3.66 +structure Rules: RULES =
    3.67 +struct
    3.68 +
    3.69 +structure S = USyntax;
    3.70 +structure U = Utils;
    3.71 +structure D = Dcterm;
    3.72 +
    3.73 +
    3.74 +fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
    3.75 +
    3.76 +
    3.77 +fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
    3.78 +fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
    3.79 +
    3.80 +fun dest_thm thm =
    3.81 +  let val {prop,hyps,...} = Thm.rep_thm thm
    3.82 +  in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
    3.83 +  handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
    3.84 +
    3.85 +
    3.86 +(* Inference rules *)
    3.87 +
    3.88 +(*---------------------------------------------------------------------------
    3.89 + *        Equality (one step)
    3.90 + *---------------------------------------------------------------------------*)
    3.91 +
    3.92 +fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
    3.93 +  handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
    3.94 +
    3.95 +fun SYM thm = thm RS sym
    3.96 +  handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
    3.97 +
    3.98 +fun ALPHA thm ctm1 =
    3.99 +  let
   3.100 +    val ctm2 = Thm.cprop_of thm;
   3.101 +    val ctm2_eq = Thm.reflexive ctm2;
   3.102 +    val ctm1_eq = Thm.reflexive ctm1;
   3.103 +  in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
   3.104 +  handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
   3.105 +
   3.106 +fun rbeta th =
   3.107 +  (case D.strip_comb (cconcl th) of
   3.108 +    (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
   3.109 +  | _ => raise RULES_ERR "rbeta" "");
   3.110 +
   3.111 +
   3.112 +(*----------------------------------------------------------------------------
   3.113 + *        Implication and the assumption list
   3.114 + *
   3.115 + * Assumptions get stuck on the meta-language assumption list. Implications
   3.116 + * are in the object language, so discharging an assumption "A" from theorem
   3.117 + * "B" results in something that looks like "A --> B".
   3.118 + *---------------------------------------------------------------------------*)
   3.119 +
   3.120 +fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
   3.121 +
   3.122 +
   3.123 +(*---------------------------------------------------------------------------
   3.124 + * Implication in TFL is -->. Meta-language implication (==>) is only used
   3.125 + * in the implementation of some of the inference rules below.
   3.126 + *---------------------------------------------------------------------------*)
   3.127 +fun MP th1 th2 = th2 RS (th1 RS mp)
   3.128 +  handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
   3.129 +
   3.130 +(*forces the first argument to be a proposition if necessary*)
   3.131 +fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
   3.132 +  handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
   3.133 +
   3.134 +fun DISCH_ALL thm = U.itlist DISCH (#hyps (Thm.crep_thm thm)) thm;
   3.135 +
   3.136 +
   3.137 +fun FILTER_DISCH_ALL P thm =
   3.138 + let fun check tm = P (#t (Thm.rep_cterm tm))
   3.139 + in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
   3.140 +              (chyps thm, thm)
   3.141 + end;
   3.142 +
   3.143 +(* freezeT expensive! *)
   3.144 +fun UNDISCH thm =
   3.145 +   let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
   3.146 +   in Thm.implies_elim (thm RS mp) (ASSUME tm) end
   3.147 +   handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
   3.148 +     | THM _ => raise RULES_ERR "UNDISCH" "";
   3.149 +
   3.150 +fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
   3.151 +
   3.152 +fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
   3.153 +  handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
   3.154 +
   3.155 +
   3.156 +(*----------------------------------------------------------------------------
   3.157 + *        Conjunction
   3.158 + *---------------------------------------------------------------------------*)
   3.159 +
   3.160 +fun CONJUNCT1 thm = thm RS conjunct1
   3.161 +  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
   3.162 +
   3.163 +fun CONJUNCT2 thm = thm RS conjunct2
   3.164 +  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
   3.165 +
   3.166 +fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
   3.167 +
   3.168 +fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
   3.169 +  | LIST_CONJ [th] = th
   3.170 +  | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
   3.171 +      handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
   3.172 +
   3.173 +
   3.174 +(*----------------------------------------------------------------------------
   3.175 + *        Disjunction
   3.176 + *---------------------------------------------------------------------------*)
   3.177 +local val {prop,sign,...} = rep_thm disjI1
   3.178 +      val [P,Q] = term_vars prop
   3.179 +      val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1
   3.180 +in
   3.181 +fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
   3.182 +  handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
   3.183 +end;
   3.184 +
   3.185 +local val {prop,sign,...} = rep_thm disjI2
   3.186 +      val [P,Q] = term_vars prop
   3.187 +      val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2
   3.188 +in
   3.189 +fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   3.190 +  handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
   3.191 +end;
   3.192 +
   3.193 +
   3.194 +(*----------------------------------------------------------------------------
   3.195 + *
   3.196 + *                   A1 |- M1, ..., An |- Mn
   3.197 + *     ---------------------------------------------------
   3.198 + *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
   3.199 + *
   3.200 + *---------------------------------------------------------------------------*)
   3.201 +
   3.202 +
   3.203 +fun EVEN_ORS thms =
   3.204 +  let fun blue ldisjs [] _ = []
   3.205 +        | blue ldisjs (th::rst) rdisjs =
   3.206 +            let val tail = tl rdisjs
   3.207 +                val rdisj_tl = D.list_mk_disj tail
   3.208 +            in U.itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
   3.209 +               :: blue (ldisjs @ [cconcl th]) rst tail
   3.210 +            end handle U.ERR _ => [U.itlist DISJ2 ldisjs th]
   3.211 +   in blue [] thms (map cconcl thms) end;
   3.212 +
   3.213 +
   3.214 +(*----------------------------------------------------------------------------
   3.215 + *
   3.216 + *         A |- P \/ Q   B,P |- R    C,Q |- R
   3.217 + *     ---------------------------------------------------
   3.218 + *                     A U B U C |- R
   3.219 + *
   3.220 + *---------------------------------------------------------------------------*)
   3.221 +
   3.222 +fun DISJ_CASES th1 th2 th3 =
   3.223 +  let
   3.224 +    val c = D.drop_prop (cconcl th1);
   3.225 +    val (disj1, disj2) = D.dest_disj c;
   3.226 +    val th2' = DISCH disj1 th2;
   3.227 +    val th3' = DISCH disj2 th3;
   3.228 +  in
   3.229 +    th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
   3.230 +      handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
   3.231 +  end;
   3.232 +
   3.233 +
   3.234 +(*-----------------------------------------------------------------------------
   3.235 + *
   3.236 + *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
   3.237 + *     ---------------------------------------------------
   3.238 + *                           |- M
   3.239 + *
   3.240 + * Note. The list of theorems may be all jumbled up, so we have to
   3.241 + * first organize it to align with the first argument (the disjunctive
   3.242 + * theorem).
   3.243 + *---------------------------------------------------------------------------*)
   3.244 +
   3.245 +fun organize eq =    (* a bit slow - analogous to insertion sort *)
   3.246 + let fun extract a alist =
   3.247 +     let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
   3.248 +           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
   3.249 +     in ex ([],alist)
   3.250 +     end
   3.251 +     fun place [] [] = []
   3.252 +       | place (a::rst) alist =
   3.253 +           let val (item,next) = extract a alist
   3.254 +           in item::place rst next
   3.255 +           end
   3.256 +       | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
   3.257 + in place
   3.258 + end;
   3.259 +(* freezeT expensive! *)
   3.260 +fun DISJ_CASESL disjth thl =
   3.261 +   let val c = cconcl disjth
   3.262 +       fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
   3.263 +                                       aconv term_of atm)
   3.264 +                              (#hyps(rep_thm th))
   3.265 +       val tml = D.strip_disj c
   3.266 +       fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
   3.267 +         | DL th [th1] = PROVE_HYP th th1
   3.268 +         | DL th [th1,th2] = DISJ_CASES th th1 th2
   3.269 +         | DL th (th1::rst) =
   3.270 +            let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
   3.271 +             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
   3.272 +   in DL (freezeT disjth) (organize eq tml thl)
   3.273 +   end;
   3.274 +
   3.275 +
   3.276 +(*----------------------------------------------------------------------------
   3.277 + *        Universals
   3.278 + *---------------------------------------------------------------------------*)
   3.279 +local (* this is fragile *)
   3.280 +      val {prop,sign,...} = rep_thm spec
   3.281 +      val x = hd (tl (term_vars prop))
   3.282 +      val (TVar (indx,_)) = type_of x
   3.283 +      val gspec = forall_intr (cterm_of sign x) spec
   3.284 +in
   3.285 +fun SPEC tm thm =
   3.286 +   let val {sign,T,...} = rep_cterm tm
   3.287 +       val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
   3.288 +   in
   3.289 +      thm RS (forall_elim tm gspec')
   3.290 +   end
   3.291 +end;
   3.292 +
   3.293 +fun SPEC_ALL thm = U.rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
   3.294 +
   3.295 +val ISPEC = SPEC
   3.296 +val ISPECL = U.rev_itlist ISPEC;
   3.297 +
   3.298 +(* Not optimized! Too complicated. *)
   3.299 +local val {prop,sign,...} = rep_thm allI
   3.300 +      val [P] = add_term_vars (prop, [])
   3.301 +      fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
   3.302 +      fun ctm_theta s = map (fn (i,tm2) =>
   3.303 +                             let val ctm2 = cterm_of s tm2
   3.304 +                             in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
   3.305 +                             end)
   3.306 +      fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,
   3.307 +                                           ctm_theta s tm_theta)
   3.308 +in
   3.309 +fun GEN v th =
   3.310 +   let val gth = forall_intr v th
   3.311 +       val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
   3.312 +       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   3.313 +       val tsig = #tsig(Sign.rep_sg sign)
   3.314 +       val theta = Pattern.match tsig (P,P')
   3.315 +       val allI2 = instantiate (certify sign theta) allI
   3.316 +       val thm = Thm.implies_elim allI2 gth
   3.317 +       val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
   3.318 +       val prop' = tp $ (A $ Abs(x,ty,M))
   3.319 +   in ALPHA thm (cterm_of sign prop')
   3.320 +   end
   3.321 +end;
   3.322 +
   3.323 +val GENL = U.itlist GEN;
   3.324 +
   3.325 +fun GEN_ALL thm =
   3.326 +   let val {prop,sign,...} = rep_thm thm
   3.327 +       val tycheck = cterm_of sign
   3.328 +       val vlist = map tycheck (add_term_vars (prop, []))
   3.329 +  in GENL vlist thm
   3.330 +  end;
   3.331 +
   3.332 +
   3.333 +fun MATCH_MP th1 th2 =
   3.334 +   if (D.is_forall (D.drop_prop(cconcl th1)))
   3.335 +   then MATCH_MP (th1 RS spec) th2
   3.336 +   else MP th1 th2;
   3.337 +
   3.338 +
   3.339 +(*----------------------------------------------------------------------------
   3.340 + *        Existentials
   3.341 + *---------------------------------------------------------------------------*)
   3.342 +
   3.343 +
   3.344 +
   3.345 +(*---------------------------------------------------------------------------
   3.346 + * Existential elimination
   3.347 + *
   3.348 + *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
   3.349 + *      ------------------------------------     (variable v occurs nowhere)
   3.350 + *                A1 u A2 |- t'
   3.351 + *
   3.352 + *---------------------------------------------------------------------------*)
   3.353 +
   3.354 +fun CHOOSE (fvar, exth) fact =
   3.355 +  let
   3.356 +    val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
   3.357 +    val redex = D.capply lam fvar
   3.358 +    val {sign, t = t$u,...} = Thm.rep_cterm redex
   3.359 +    val residue = Thm.cterm_of sign (betapply (t, u))
   3.360 +  in
   3.361 +    GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
   3.362 +      handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   3.363 +  end;
   3.364 +
   3.365 +local val {prop,sign,...} = rep_thm exI
   3.366 +      val [P,x] = term_vars prop
   3.367 +in
   3.368 +fun EXISTS (template,witness) thm =
   3.369 +   let val {prop,sign,...} = rep_thm thm
   3.370 +       val P' = cterm_of sign P
   3.371 +       val x' = cterm_of sign x
   3.372 +       val abstr = #2 (D.dest_comb template)
   3.373 +   in
   3.374 +   thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   3.375 +     handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
   3.376 +   end
   3.377 +end;
   3.378 +
   3.379 +(*----------------------------------------------------------------------------
   3.380 + *
   3.381 + *         A |- M
   3.382 + *   -------------------   [v_1,...,v_n]
   3.383 + *    A |- ?v1...v_n. M
   3.384 + *
   3.385 + *---------------------------------------------------------------------------*)
   3.386 +
   3.387 +fun EXISTL vlist th =
   3.388 +  U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
   3.389 +           vlist th;
   3.390 +
   3.391 +
   3.392 +(*----------------------------------------------------------------------------
   3.393 + *
   3.394 + *       A |- M[x_1,...,x_n]
   3.395 + *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
   3.396 + *       A |- ?y_1...y_n. M
   3.397 + *
   3.398 + *---------------------------------------------------------------------------*)
   3.399 +(* Could be improved, but needs "subst_free" for certified terms *)
   3.400 +
   3.401 +fun IT_EXISTS blist th =
   3.402 +   let val {sign,...} = rep_thm th
   3.403 +       val tych = cterm_of sign
   3.404 +       val detype = #t o rep_cterm
   3.405 +       val blist' = map (fn (x,y) => (detype x, detype y)) blist
   3.406 +       fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
   3.407 +
   3.408 +  in
   3.409 +  U.itlist (fn (b as (r1,r2)) => fn thm =>
   3.410 +        EXISTS(?r2(subst_free[b]
   3.411 +                   (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
   3.412 +              thm)
   3.413 +       blist' th
   3.414 +  end;
   3.415 +
   3.416 +(*---------------------------------------------------------------------------
   3.417 + *  Faster version, that fails for some as yet unknown reason
   3.418 + * fun IT_EXISTS blist th =
   3.419 + *    let val {sign,...} = rep_thm th
   3.420 + *        val tych = cterm_of sign
   3.421 + *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
   3.422 + *   in
   3.423 + *  fold (fn (b as (r1,r2), thm) =>
   3.424 + *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
   3.425 + *           r1) thm)  blist th
   3.426 + *   end;
   3.427 + *---------------------------------------------------------------------------*)
   3.428 +
   3.429 +(*----------------------------------------------------------------------------
   3.430 + *        Rewriting
   3.431 + *---------------------------------------------------------------------------*)
   3.432 +
   3.433 +fun SUBS thl =
   3.434 +  rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
   3.435 +
   3.436 +local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss
   3.437 +in
   3.438 +fun simpl_conv ss thl ctm =
   3.439 + rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
   3.440 + RS meta_eq_to_obj_eq
   3.441 +end;
   3.442 +
   3.443 +val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
   3.444 +
   3.445 +
   3.446 +
   3.447 +(*---------------------------------------------------------------------------
   3.448 + *                  TERMINATION CONDITION EXTRACTION
   3.449 + *---------------------------------------------------------------------------*)
   3.450 +
   3.451 +
   3.452 +(* Object language quantifier, i.e., "!" *)
   3.453 +fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   3.454 +
   3.455 +
   3.456 +(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   3.457 +fun is_cong thm =
   3.458 +  let val {prop, ...} = rep_thm thm
   3.459 +  in case prop
   3.460 +     of (Const("==>",_)$(Const("Trueprop",_)$ _) $
   3.461 +         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
   3.462 +      | _ => true
   3.463 +  end;
   3.464 +
   3.465 +
   3.466 +
   3.467 +fun dest_equal(Const ("==",_) $
   3.468 +               (Const ("Trueprop",_) $ lhs)
   3.469 +               $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
   3.470 +  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   3.471 +  | dest_equal tm = S.dest_eq tm;
   3.472 +
   3.473 +fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
   3.474 +
   3.475 +fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
   3.476 +  | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
   3.477 +
   3.478 +val is_all = can (dest_all []);
   3.479 +
   3.480 +fun strip_all used fm =
   3.481 +   if (is_all fm)
   3.482 +   then let val ({Bvar, Body}, used') = dest_all used fm
   3.483 +            val (bvs, core, used'') = strip_all used' Body
   3.484 +        in ((Bvar::bvs), core, used'')
   3.485 +        end
   3.486 +   else ([], fm, used);
   3.487 +
   3.488 +fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   3.489 +  | break_all _ = raise RULES_ERR "break_all" "not a !!";
   3.490 +
   3.491 +fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
   3.492 +     let val (L,core) = list_break_all body
   3.493 +     in ((s,ty)::L, core)
   3.494 +     end
   3.495 +  | list_break_all tm = ([],tm);
   3.496 +
   3.497 +(*---------------------------------------------------------------------------
   3.498 + * Rename a term of the form
   3.499 + *
   3.500 + *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
   3.501 + *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
   3.502 + * to one of
   3.503 + *
   3.504 + *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
   3.505 + *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
   3.506 + *
   3.507 + * This prevents name problems in extraction, and helps the result to read
   3.508 + * better. There is a problem with varstructs, since they can introduce more
   3.509 + * than n variables, and some extra reasoning needs to be done.
   3.510 + *---------------------------------------------------------------------------*)
   3.511 +
   3.512 +fun get ([],_,L) = rev L
   3.513 +  | get (ant::rst,n,L) =
   3.514 +      case (list_break_all ant)
   3.515 +        of ([],_) => get (rst, n+1,L)
   3.516 +         | (vlist,body) =>
   3.517 +            let val eq = Logic.strip_imp_concl body
   3.518 +                val (f,args) = S.strip_comb (get_lhs eq)
   3.519 +                val (vstrl,_) = S.strip_abs f
   3.520 +                val names  = variantlist (map (#1 o dest_Free) vstrl,
   3.521 +                                          add_term_names(body, []))
   3.522 +            in get (rst, n+1, (names,n)::L) end
   3.523 +            handle TERM _ => get (rst, n+1, L)
   3.524 +              | U.ERR _ => get (rst, n+1, L);
   3.525 +
   3.526 +(* Note: rename_params_rule counts from 1, not 0 *)
   3.527 +fun rename thm =
   3.528 +  let val {prop,sign,...} = rep_thm thm
   3.529 +      val tych = cterm_of sign
   3.530 +      val ants = Logic.strip_imp_prems prop
   3.531 +      val news = get (ants,1,[])
   3.532 +  in
   3.533 +  U.rev_itlist rename_params_rule news thm
   3.534 +  end;
   3.535 +
   3.536 +
   3.537 +(*---------------------------------------------------------------------------
   3.538 + * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
   3.539 + *---------------------------------------------------------------------------*)
   3.540 +
   3.541 +fun list_beta_conv tm =
   3.542 +  let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
   3.543 +      fun iter [] = Thm.reflexive tm
   3.544 +        | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
   3.545 +  in iter  end;
   3.546 +
   3.547 +
   3.548 +(*---------------------------------------------------------------------------
   3.549 + * Trace information for the rewriter
   3.550 + *---------------------------------------------------------------------------*)
   3.551 +val term_ref = ref[] : term list ref
   3.552 +val mss_ref = ref [] : meta_simpset list ref;
   3.553 +val thm_ref = ref [] : thm list ref;
   3.554 +val tracing = ref false;
   3.555 +
   3.556 +fun say s = if !tracing then writeln s else ();
   3.557 +
   3.558 +fun print_thms s L =
   3.559 +  say (cat_lines (s :: map string_of_thm L));
   3.560 +
   3.561 +fun print_cterms s L =
   3.562 +  say (cat_lines (s :: map string_of_cterm L));
   3.563 +
   3.564 +
   3.565 +(*---------------------------------------------------------------------------
   3.566 + * General abstraction handlers, should probably go in USyntax.
   3.567 + *---------------------------------------------------------------------------*)
   3.568 +fun mk_aabs (vstr, body) =
   3.569 +  S.mk_abs {Bvar = vstr, Body = body}
   3.570 +  handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
   3.571 +
   3.572 +fun list_mk_aabs (vstrl,tm) =
   3.573 +    U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
   3.574 +
   3.575 +fun dest_aabs used tm =
   3.576 +   let val ({Bvar,Body}, used') = S.dest_abs used tm
   3.577 +   in (Bvar, Body, used') end
   3.578 +   handle U.ERR _ =>
   3.579 +     let val {varstruct, body, used} = S.dest_pabs used tm
   3.580 +     in (varstruct, body, used) end;
   3.581 +
   3.582 +fun strip_aabs used tm =
   3.583 +   let val (vstr, body, used') = dest_aabs used tm
   3.584 +       val (bvs, core, used'') = strip_aabs used' body
   3.585 +   in (vstr::bvs, core, used'') end
   3.586 +   handle U.ERR _ => ([], tm, used);
   3.587 +
   3.588 +fun dest_combn tm 0 = (tm,[])
   3.589 +  | dest_combn tm n =
   3.590 +     let val {Rator,Rand} = S.dest_comb tm
   3.591 +         val (f,rands) = dest_combn Rator (n-1)
   3.592 +     in (f,Rand::rands)
   3.593 +     end;
   3.594 +
   3.595 +
   3.596 +
   3.597 +
   3.598 +local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   3.599 +      fun mk_fst tm =
   3.600 +          let val ty as Type("*", [fty,sty]) = type_of tm
   3.601 +          in  Const ("fst", ty --> fty) $ tm  end
   3.602 +      fun mk_snd tm =
   3.603 +          let val ty as Type("*", [fty,sty]) = type_of tm
   3.604 +          in  Const ("snd", ty --> sty) $ tm  end
   3.605 +in
   3.606 +fun XFILL tych x vstruct =
   3.607 +  let fun traverse p xocc L =
   3.608 +        if (is_Free p)
   3.609 +        then tych xocc::L
   3.610 +        else let val (p1,p2) = dest_pair p
   3.611 +             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   3.612 +             end
   3.613 +  in
   3.614 +  traverse vstruct x []
   3.615 +end end;
   3.616 +
   3.617 +(*---------------------------------------------------------------------------
   3.618 + * Replace a free tuple (vstr) by a universally quantified variable (a).
   3.619 + * Note that the notion of "freeness" for a tuple is different than for a
   3.620 + * variable: if variables in the tuple also occur in any other place than
   3.621 + * an occurrences of the tuple, they aren't "free" (which is thus probably
   3.622 + *  the wrong word to use).
   3.623 + *---------------------------------------------------------------------------*)
   3.624 +
   3.625 +fun VSTRUCT_ELIM tych a vstr th =
   3.626 +  let val L = S.free_vars_lr vstr
   3.627 +      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
   3.628 +      val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   3.629 +      val thm2 = forall_intr_list (map tych L) thm1
   3.630 +      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   3.631 +  in refl RS
   3.632 +     rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
   3.633 +  end;
   3.634 +
   3.635 +fun PGEN tych a vstr th =
   3.636 +  let val a1 = tych a
   3.637 +      val vstr1 = tych vstr
   3.638 +  in
   3.639 +  forall_intr a1
   3.640 +     (if (is_Free vstr)
   3.641 +      then cterm_instantiate [(vstr1,a1)] th
   3.642 +      else VSTRUCT_ELIM tych a vstr th)
   3.643 +  end;
   3.644 +
   3.645 +
   3.646 +(*---------------------------------------------------------------------------
   3.647 + * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
   3.648 + *
   3.649 + *     (([x,y],N),vstr)
   3.650 + *---------------------------------------------------------------------------*)
   3.651 +fun dest_pbeta_redex used M n =
   3.652 +  let val (f,args) = dest_combn M n
   3.653 +      val dummy = dest_aabs used f
   3.654 +  in (strip_aabs used f,args)
   3.655 +  end;
   3.656 +
   3.657 +fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
   3.658 +
   3.659 +fun dest_impl tm =
   3.660 +  let val ants = Logic.strip_imp_prems tm
   3.661 +      val eq = Logic.strip_imp_concl tm
   3.662 +  in (ants,get_lhs eq)
   3.663 +  end;
   3.664 +
   3.665 +fun restricted t = is_some (S.find_term
   3.666 +                            (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
   3.667 +                            t)
   3.668 +
   3.669 +fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
   3.670 + let val globals = func::G
   3.671 +     val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];
   3.672 +     val tc_list = ref[]: term list ref
   3.673 +     val dummy = term_ref := []
   3.674 +     val dummy = thm_ref  := []
   3.675 +     val dummy = mss_ref  := []
   3.676 +     val cut_lemma' = cut_lemma RS eq_reflection
   3.677 +     fun prover used mss thm =
   3.678 +     let fun cong_prover mss thm =
   3.679 +         let val dummy = say "cong_prover:"
   3.680 +             val cntxt = prems_of_mss mss
   3.681 +             val dummy = print_thms "cntxt:" cntxt
   3.682 +             val dummy = say "cong rule:"
   3.683 +             val dummy = say (string_of_thm thm)
   3.684 +             val dummy = thm_ref := (thm :: !thm_ref)
   3.685 +             val dummy = mss_ref := (mss :: !mss_ref)
   3.686 +             (* Unquantified eliminate *)
   3.687 +             fun uq_eliminate (thm,imp,sign) =
   3.688 +                 let val tych = cterm_of sign
   3.689 +                     val dummy = print_cterms "To eliminate:" [tych imp]
   3.690 +                     val ants = map tych (Logic.strip_imp_prems imp)
   3.691 +                     val eq = Logic.strip_imp_concl imp
   3.692 +                     val lhs = tych(get_lhs eq)
   3.693 +                     val mss' = add_prems(mss, map ASSUME ants)
   3.694 +                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
   3.695 +                       handle U.ERR _ => Thm.reflexive lhs
   3.696 +                     val dummy = print_thms "proven:" [lhs_eq_lhs1]
   3.697 +                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   3.698 +                     val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   3.699 +                  in
   3.700 +                  lhs_eeq_lhs2 COMP thm
   3.701 +                  end
   3.702 +             fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
   3.703 +              let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
   3.704 +                  val dummy = assert (forall (op aconv)
   3.705 +                                      (ListPair.zip (vlist, args)))
   3.706 +                               "assertion failed in CONTEXT_REWRITE_RULE"
   3.707 +                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
   3.708 +                                             imp_body
   3.709 +                  val tych = cterm_of sign
   3.710 +                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   3.711 +                  val eq1 = Logic.strip_imp_concl imp_body1
   3.712 +                  val Q = get_lhs eq1
   3.713 +                  val QeqQ1 = pbeta_reduce (tych Q)
   3.714 +                  val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   3.715 +                  val mss' = add_prems(mss, map ASSUME ants1)
   3.716 +                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
   3.717 +                                handle U.ERR _ => Thm.reflexive Q1
   3.718 +                  val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
   3.719 +                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   3.720 +                  val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
   3.721 +                  val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   3.722 +                  val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
   3.723 +                               ((Q2eeqQ3 RS meta_eq_to_obj_eq)
   3.724 +                                RS ((thA RS meta_eq_to_obj_eq) RS trans))
   3.725 +                                RS eq_reflection
   3.726 +                  val impth = implies_intr_list ants1 QeeqQ3
   3.727 +                  val impth1 = impth RS meta_eq_to_obj_eq
   3.728 +                  (* Need to abstract *)
   3.729 +                  val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   3.730 +              in ant_th COMP thm
   3.731 +              end
   3.732 +             fun q_eliminate (thm,imp,sign) =
   3.733 +              let val (vlist, imp_body, used') = strip_all used imp
   3.734 +                  val (ants,Q) = dest_impl imp_body
   3.735 +              in if (pbeta_redex Q) (length vlist)
   3.736 +                 then pq_eliminate (thm,sign,vlist,imp_body,Q)
   3.737 +                 else
   3.738 +                 let val tych = cterm_of sign
   3.739 +                     val ants1 = map tych ants
   3.740 +                     val mss' = add_prems(mss, map ASSUME ants1)
   3.741 +                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   3.742 +                        (false,true,false) (prover used') mss' (tych Q)
   3.743 +                      handle U.ERR _ => Thm.reflexive (tych Q)
   3.744 +                     val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   3.745 +                     val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   3.746 +                     val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   3.747 +                 in
   3.748 +                 ant_th COMP thm
   3.749 +              end end
   3.750 +
   3.751 +             fun eliminate thm =
   3.752 +               case (rep_thm thm)
   3.753 +               of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
   3.754 +                   eliminate
   3.755 +                    (if not(is_all imp)
   3.756 +                     then uq_eliminate (thm,imp,sign)
   3.757 +                     else q_eliminate (thm,imp,sign))
   3.758 +                            (* Assume that the leading constant is ==,   *)
   3.759 +                | _ => thm  (* if it is not a ==>                        *)
   3.760 +         in Some(eliminate (rename thm)) end
   3.761 +         handle U.ERR _ => None    (* FIXME handle THM as well?? *)
   3.762 +
   3.763 +        fun restrict_prover mss thm =
   3.764 +          let val dummy = say "restrict_prover:"
   3.765 +              val cntxt = rev(prems_of_mss mss)
   3.766 +              val dummy = print_thms "cntxt:" cntxt
   3.767 +              val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   3.768 +                   sign,...} = rep_thm thm
   3.769 +              fun genl tm = let val vlist = gen_rems (op aconv)
   3.770 +                                           (add_term_frees(tm,[]), globals)
   3.771 +                            in U.itlist Forall vlist tm
   3.772 +                            end
   3.773 +              (*--------------------------------------------------------------
   3.774 +               * This actually isn't quite right, since it will think that
   3.775 +               * not-fully applied occs. of "f" in the context mean that the
   3.776 +               * current call is nested. The real solution is to pass in a
   3.777 +               * term "f v1..vn" which is a pattern that any full application
   3.778 +               * of "f" will match.
   3.779 +               *-------------------------------------------------------------*)
   3.780 +              val func_name = #1(dest_Const func)
   3.781 +              fun is_func (Const (name,_)) = (name = func_name)
   3.782 +                | is_func _                = false
   3.783 +              val rcontext = rev cntxt
   3.784 +              val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   3.785 +              val antl = case rcontext of [] => []
   3.786 +                         | _   => [S.list_mk_conj(map cncl rcontext)]
   3.787 +              val TC = genl(S.list_mk_imp(antl, A))
   3.788 +              val dummy = print_cterms "func:" [cterm_of sign func]
   3.789 +              val dummy = print_cterms "TC:"
   3.790 +                              [cterm_of sign (HOLogic.mk_Trueprop TC)]
   3.791 +              val dummy = tc_list := (TC :: !tc_list)
   3.792 +              val nestedp = is_some (S.find_term is_func TC)
   3.793 +              val dummy = if nestedp then say "nested" else say "not_nested"
   3.794 +              val dummy = term_ref := ([func,TC]@(!term_ref))
   3.795 +              val th' = if nestedp then raise RULES_ERR "solver" "nested function"
   3.796 +                        else let val cTC = cterm_of sign
   3.797 +                                              (HOLogic.mk_Trueprop TC)
   3.798 +                             in case rcontext of
   3.799 +                                [] => SPEC_ALL(ASSUME cTC)
   3.800 +                               | _ => MP (SPEC_ALL (ASSUME cTC))
   3.801 +                                         (LIST_CONJ rcontext)
   3.802 +                             end
   3.803 +              val th'' = th' RS thm
   3.804 +          in Some (th'')
   3.805 +          end handle U.ERR _ => None    (* FIXME handle THM as well?? *)
   3.806 +    in
   3.807 +    (if (is_cong thm) then cong_prover else restrict_prover) mss thm
   3.808 +    end
   3.809 +    val ctm = cprop_of th
   3.810 +    val names = add_term_names (term_of ctm, [])
   3.811 +    val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   3.812 +      (prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm
   3.813 +    val th2 = equal_elim th1 th
   3.814 + in
   3.815 + (th2, filter (not o restricted) (!tc_list))
   3.816 + end;
   3.817 +
   3.818 +
   3.819 +fun prove (ptm, tac) =
   3.820 +  let val result =
   3.821 +    Library.transform_error (fn () =>
   3.822 +      Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
   3.823 +    handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg)
   3.824 +  in #1 (freeze_thaw result) end;
   3.825 +
   3.826 +
   3.827 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/TFL/tfl.ML	Wed Jan 03 21:20:40 2001 +0100
     4.3 @@ -0,0 +1,1001 @@
     4.4 +(*  Title:      TFL/tfl.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 +First part of main module.
    4.10 +*)
    4.11 +
    4.12 +signature PRIM =
    4.13 +sig
    4.14 +  val trace: bool ref
    4.15 +  type pattern
    4.16 +  val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    4.17 +  val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    4.18 +  val post_definition: thm list -> theory * (thm * pattern list) ->
    4.19 +   {theory: theory,
    4.20 +    rules: thm,
    4.21 +    rows: int list,
    4.22 +    TCs: term list list,
    4.23 +    full_pats_TCs: (term * term list) list}
    4.24 +  val wfrec_eqns: theory -> xstring -> thm list -> term list ->
    4.25 +   {WFR: term,
    4.26 +    SV: term list,
    4.27 +    proto_def: term,
    4.28 +    extracta: (thm * term list) list,
    4.29 +    pats: pattern list}
    4.30 +  val lazyR_def: theory -> xstring -> thm list -> term list ->
    4.31 +   {theory: theory,
    4.32 +    rules: thm,
    4.33 +    R: term,
    4.34 +    SV: term list,
    4.35 +    full_pats_TCs: (term * term list) list,
    4.36 +    patterns : pattern list}
    4.37 +  val mk_induction: theory ->
    4.38 +    {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
    4.39 +  val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory ->
    4.40 +    {rules: thm, induction: thm, TCs: term list list} ->
    4.41 +    {rules: thm, induction: thm, nested_tcs: thm list}
    4.42 +end;
    4.43 +
    4.44 +structure Prim: PRIM =
    4.45 +struct
    4.46 +
    4.47 +val trace = ref false;
    4.48 +
    4.49 +open BasisLibrary;
    4.50 +
    4.51 +structure R = Rules;
    4.52 +structure S = USyntax;
    4.53 +structure U = Utils;
    4.54 +
    4.55 +
    4.56 +fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg};
    4.57 +
    4.58 +val concl = #2 o R.dest_thm;
    4.59 +val hyp = #1 o R.dest_thm;
    4.60 +
    4.61 +val list_mk_type = U.end_itlist (curry (op -->));
    4.62 +
    4.63 +fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
    4.64 +
    4.65 +fun front_last [] = raise TFL_ERR "front_last" "empty list"
    4.66 +  | front_last [x] = ([],x)
    4.67 +  | front_last (h::t) =
    4.68 +     let val (pref,x) = front_last t
    4.69 +     in
    4.70 +        (h::pref,x)
    4.71 +     end;
    4.72 +
    4.73 +
    4.74 +(*---------------------------------------------------------------------------
    4.75 + * The next function is common to pattern-match translation and
    4.76 + * proof of completeness of cases for the induction theorem.
    4.77 + *
    4.78 + * The curried function "gvvariant" returns a function to generate distinct
    4.79 + * variables that are guaranteed not to be in names.  The names of
    4.80 + * the variables go u, v, ..., z, aa, ..., az, ...  The returned
    4.81 + * function contains embedded refs!
    4.82 + *---------------------------------------------------------------------------*)
    4.83 +fun gvvariant names =
    4.84 +  let val slist = ref names
    4.85 +      val vname = ref "u"
    4.86 +      fun new() =
    4.87 +         if !vname mem_string (!slist)
    4.88 +         then (vname := bump_string (!vname);  new())
    4.89 +         else (slist := !vname :: !slist;  !vname)
    4.90 +  in
    4.91 +  fn ty => Free(new(), ty)
    4.92 +  end;
    4.93 +
    4.94 +
    4.95 +(*---------------------------------------------------------------------------
    4.96 + * Used in induction theorem production. This is the simple case of
    4.97 + * partitioning up pattern rows by the leading constructor.
    4.98 + *---------------------------------------------------------------------------*)
    4.99 +fun ipartition gv (constructors,rows) =
   4.100 +  let fun pfail s = raise TFL_ERR "partition.part" s
   4.101 +      fun part {constrs = [],   rows = [],   A} = rev A
   4.102 +        | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
   4.103 +        | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
   4.104 +        | part {constrs = c::crst, rows,     A} =
   4.105 +          let val (Name,Ty) = dest_Const c
   4.106 +              val L = binder_types Ty
   4.107 +              val (in_group, not_in_group) =
   4.108 +               U.itlist (fn (row as (p::rst, rhs)) =>
   4.109 +                         fn (in_group,not_in_group) =>
   4.110 +                  let val (pc,args) = S.strip_comb p
   4.111 +                  in if (#1(dest_Const pc) = Name)
   4.112 +                     then ((args@rst, rhs)::in_group, not_in_group)
   4.113 +                     else (in_group, row::not_in_group)
   4.114 +                  end)      rows ([],[])
   4.115 +              val col_types = U.take type_of (length L, #1(hd in_group))
   4.116 +          in
   4.117 +          part{constrs = crst, rows = not_in_group,
   4.118 +               A = {constructor = c,
   4.119 +                    new_formals = map gv col_types,
   4.120 +                    group = in_group}::A}
   4.121 +          end
   4.122 +  in part{constrs = constructors, rows = rows, A = []}
   4.123 +  end;
   4.124 +
   4.125 +
   4.126 +
   4.127 +(*---------------------------------------------------------------------------
   4.128 + * Each pattern carries with it a tag (i,b) where
   4.129 + * i is the clause it came from and
   4.130 + * b=true indicates that clause was given by the user
   4.131 + * (or is an instantiation of a user supplied pattern)
   4.132 + * b=false --> i = ~1
   4.133 + *---------------------------------------------------------------------------*)
   4.134 +
   4.135 +type pattern = term * (int * bool)
   4.136 +
   4.137 +fun pattern_map f (tm,x) = (f tm, x);
   4.138 +
   4.139 +fun pattern_subst theta = pattern_map (subst_free theta);
   4.140 +
   4.141 +val pat_of = fst;
   4.142 +fun row_of_pat x = fst (snd x);
   4.143 +fun given x = snd (snd x);
   4.144 +
   4.145 +(*---------------------------------------------------------------------------
   4.146 + * Produce an instance of a constructor, plus genvars for its arguments.
   4.147 + *---------------------------------------------------------------------------*)
   4.148 +fun fresh_constr ty_match colty gv c =
   4.149 +  let val (_,Ty) = dest_Const c
   4.150 +      val L = binder_types Ty
   4.151 +      and ty = body_type Ty
   4.152 +      val ty_theta = ty_match ty colty
   4.153 +      val c' = S.inst ty_theta c
   4.154 +      val gvars = map (S.inst ty_theta o gv) L
   4.155 +  in (c', gvars)
   4.156 +  end;
   4.157 +
   4.158 +
   4.159 +(*---------------------------------------------------------------------------
   4.160 + * Goes through a list of rows and picks out the ones beginning with a
   4.161 + * pattern with constructor = Name.
   4.162 + *---------------------------------------------------------------------------*)
   4.163 +fun mk_group Name rows =
   4.164 +  U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
   4.165 +            fn (in_group,not_in_group) =>
   4.166 +               let val (pc,args) = S.strip_comb p
   4.167 +               in if ((#1 (Term.dest_Const pc) = Name) handle TERM _ => false)
   4.168 +                  then (((prfx,args@rst), rhs)::in_group, not_in_group)
   4.169 +                  else (in_group, row::not_in_group) end)
   4.170 +      rows ([],[]);
   4.171 +
   4.172 +(*---------------------------------------------------------------------------
   4.173 + * Partition the rows. Not efficient: we should use hashing.
   4.174 + *---------------------------------------------------------------------------*)
   4.175 +fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
   4.176 +  | partition gv ty_match
   4.177 +              (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
   4.178 +let val fresh = fresh_constr ty_match colty gv
   4.179 +     fun part {constrs = [],      rows, A} = rev A
   4.180 +       | part {constrs = c::crst, rows, A} =
   4.181 +         let val (c',gvars) = fresh c
   4.182 +             val (Name,Ty) = dest_Const c'
   4.183 +             val (in_group, not_in_group) = mk_group Name rows
   4.184 +             val in_group' =
   4.185 +                 if (null in_group)  (* Constructor not given *)
   4.186 +                 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
   4.187 +                 else in_group
   4.188 +         in
   4.189 +         part{constrs = crst,
   4.190 +              rows = not_in_group,
   4.191 +              A = {constructor = c',
   4.192 +                   new_formals = gvars,
   4.193 +                   group = in_group'}::A}
   4.194 +         end
   4.195 +in part{constrs=constructors, rows=rows, A=[]}
   4.196 +end;
   4.197 +
   4.198 +(*---------------------------------------------------------------------------
   4.199 + * Misc. routines used in mk_case
   4.200 + *---------------------------------------------------------------------------*)
   4.201 +
   4.202 +fun mk_pat (c,l) =
   4.203 +  let val L = length (binder_types (type_of c))
   4.204 +      fun build (prfx,tag,plist) =
   4.205 +          let val args   = take (L,plist)
   4.206 +              and plist' = drop(L,plist)
   4.207 +          in (prfx,tag,list_comb(c,args)::plist') end
   4.208 +  in map build l end;
   4.209 +
   4.210 +fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
   4.211 +  | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
   4.212 +
   4.213 +fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
   4.214 +  | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
   4.215 +
   4.216 +
   4.217 +(*----------------------------------------------------------------------------
   4.218 + * Translation of pattern terms into nested case expressions.
   4.219 + *
   4.220 + * This performs the translation and also builds the full set of patterns.
   4.221 + * Thus it supports the construction of induction theorems even when an
   4.222 + * incomplete set of patterns is given.
   4.223 + *---------------------------------------------------------------------------*)
   4.224 +
   4.225 +fun mk_case ty_info ty_match usednames range_ty =
   4.226 + let
   4.227 + fun mk_case_fail s = raise TFL_ERR "mk_case" s
   4.228 + val fresh_var = gvvariant usednames
   4.229 + val divide = partition fresh_var ty_match
   4.230 + fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
   4.231 +   | expand constructors ty (row as ((prfx, p::rst), rhs)) =
   4.232 +       if (is_Free p)
   4.233 +       then let val fresh = fresh_constr ty_match ty fresh_var
   4.234 +                fun expnd (c,gvs) =
   4.235 +                  let val capp = list_comb(c,gvs)
   4.236 +                  in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
   4.237 +                  end
   4.238 +            in map expnd (map fresh constructors)  end
   4.239 +       else [row]
   4.240 + fun mk{rows=[],...} = mk_case_fail"no rows"
   4.241 +   | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
   4.242 +        ([(prfx,tag,[])], tm)
   4.243 +   | mk{path=[], rows = _::_} = mk_case_fail"blunder"
   4.244 +   | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
   4.245 +        mk{path = path,
   4.246 +           rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
   4.247 +   | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
   4.248 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   4.249 +         val col0 = map(hd o #2) pat_rectangle
   4.250 +     in
   4.251 +     if (forall is_Free col0)
   4.252 +     then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
   4.253 +                                (ListPair.zip (col0, rights))
   4.254 +              val pat_rectangle' = map v_to_prfx pat_rectangle
   4.255 +              val (pref_patl,tm) = mk{path = rstp,
   4.256 +                                      rows = ListPair.zip (pat_rectangle',
   4.257 +                                                           rights')}
   4.258 +          in (map v_to_pats pref_patl, tm)
   4.259 +          end
   4.260 +     else
   4.261 +     let val pty as Type (ty_name,_) = type_of p
   4.262 +     in
   4.263 +     case (ty_info ty_name)
   4.264 +     of None => mk_case_fail("Not a known datatype: "^ty_name)
   4.265 +      | Some{case_const,constructors} =>
   4.266 +        let
   4.267 +            val case_const_name = #1(dest_Const case_const)
   4.268 +            val nrows = List.concat (map (expand constructors pty) rows)
   4.269 +            val subproblems = divide(constructors, pty, range_ty, nrows)
   4.270 +            val groups      = map #group subproblems
   4.271 +            and new_formals = map #new_formals subproblems
   4.272 +            and constructors' = map #constructor subproblems
   4.273 +            val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
   4.274 +                           (ListPair.zip (new_formals, groups))
   4.275 +            val rec_calls = map mk news
   4.276 +            val (pat_rect,dtrees) = ListPair.unzip rec_calls
   4.277 +            val case_functions = map S.list_mk_abs
   4.278 +                                  (ListPair.zip (new_formals, dtrees))
   4.279 +            val types = map type_of (case_functions@[u]) @ [range_ty]
   4.280 +            val case_const' = Const(case_const_name, list_mk_type types)
   4.281 +            val tree = list_comb(case_const', case_functions@[u])
   4.282 +            val pat_rect1 = List.concat
   4.283 +                              (ListPair.map mk_pat (constructors', pat_rect))
   4.284 +        in (pat_rect1,tree)
   4.285 +        end
   4.286 +     end end
   4.287 + in mk
   4.288 + end;
   4.289 +
   4.290 +
   4.291 +(* Repeated variable occurrences in a pattern are not allowed. *)
   4.292 +fun FV_multiset tm =
   4.293 +   case (S.dest_term tm)
   4.294 +     of S.VAR{Name,Ty} => [Free(Name,Ty)]
   4.295 +      | S.CONST _ => []
   4.296 +      | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
   4.297 +      | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
   4.298 +
   4.299 +fun no_repeat_vars thy pat =
   4.300 + let fun check [] = true
   4.301 +       | check (v::rst) =
   4.302 +         if mem_term (v,rst) then
   4.303 +            raise TFL_ERR "no_repeat_vars"
   4.304 +                          (quote (#1 (dest_Free v)) ^
   4.305 +                          " occurs repeatedly in the pattern " ^
   4.306 +                          quote (string_of_cterm (Thry.typecheck thy pat)))
   4.307 +         else check rst
   4.308 + in check (FV_multiset pat)
   4.309 + end;
   4.310 +
   4.311 +fun dest_atom (Free p) = p
   4.312 +  | dest_atom (Const p) = p
   4.313 +  | dest_atom  _ = raise TFL_ERR "dest_atom" "function name not an identifier";
   4.314 +
   4.315 +fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
   4.316 +
   4.317 +local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
   4.318 +      fun single [_$_] =
   4.319 +              mk_functional_err "recdef does not allow currying"
   4.320 +        | single [f] = f
   4.321 +        | single fs  =
   4.322 +              (*multiple function names?*)
   4.323 +              if length (gen_distinct same_name fs) < length fs
   4.324 +              then mk_functional_err
   4.325 +                   "The function being declared appears with multiple types"
   4.326 +              else mk_functional_err
   4.327 +                   (Int.toString (length fs) ^
   4.328 +                    " distinct function names being declared")
   4.329 +in
   4.330 +fun mk_functional thy clauses =
   4.331 + let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
   4.332 +                   handle TERM _ => raise TFL_ERR "mk_functional"
   4.333 +                        "recursion equations must use the = relation")
   4.334 +     val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   4.335 +     val atom = single (gen_distinct (op aconv) funcs)
   4.336 +     val (fname,ftype) = dest_atom atom
   4.337 +     val dummy = map (no_repeat_vars thy) pats
   4.338 +     val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
   4.339 +                              map (fn (t,i) => (t,(i,true))) (enumerate R))
   4.340 +     val names = foldr add_term_names (R,[])
   4.341 +     val atype = type_of(hd pats)
   4.342 +     and aname = variant names "a"
   4.343 +     val a = Free(aname,atype)
   4.344 +     val ty_info = Thry.match_info thy
   4.345 +     val ty_match = Thry.match_type thy
   4.346 +     val range_ty = type_of (hd R)
   4.347 +     val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
   4.348 +                                    {path=[a], rows=rows}
   4.349 +     val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
   4.350 +          handle Match => mk_functional_err "error in pattern-match translation"
   4.351 +     val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
   4.352 +     val finals = map row_of_pat patts2
   4.353 +     val originals = map (row_of_pat o #2) rows
   4.354 +     val dummy = case (originals\\finals)
   4.355 +             of [] => ()
   4.356 +          | L => mk_functional_err
   4.357 + ("The following clauses are redundant (covered by preceding clauses): " ^
   4.358 +                   commas (map (fn i => Int.toString (i + 1)) L))
   4.359 + in {functional = Abs(Sign.base_name fname, ftype,
   4.360 +                      abstract_over (atom,
   4.361 +                                     absfree(aname,atype, case_tm))),
   4.362 +     pats = patts2}
   4.363 +end end;
   4.364 +
   4.365 +
   4.366 +(*----------------------------------------------------------------------------
   4.367 + *
   4.368 + *                    PRINCIPLES OF DEFINITION
   4.369 + *
   4.370 + *---------------------------------------------------------------------------*)
   4.371 +
   4.372 +
   4.373 +(*For Isabelle, the lhs of a definition must be a constant.*)
   4.374 +fun mk_const_def sign (Name, Ty, rhs) =
   4.375 +    Sign.infer_types sign (K None) (K None) [] false
   4.376 +               ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
   4.377 +    |> #1;
   4.378 +
   4.379 +(*Make all TVars available for instantiation by adding a ? to the front*)
   4.380 +fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
   4.381 +  | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   4.382 +  | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
   4.383 +
   4.384 +local val f_eq_wfrec_R_M =
   4.385 +           #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
   4.386 +      val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
   4.387 +      val (fname,_) = dest_Free f
   4.388 +      val (wfrec,_) = S.strip_comb rhs
   4.389 +in
   4.390 +fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) =
   4.391 + let val def_name = if Name<>fid then
   4.392 +                        raise TFL_ERR "wfrec_definition0"
   4.393 +                                      ("Expected a definition of " ^
   4.394 +                                             quote fid ^ " but found one of " ^
   4.395 +                                      quote Name)
   4.396 +                    else Name ^ "_def"
   4.397 +     val wfrec_R_M =  map_term_types poly_tvars
   4.398 +                          (wfrec $ map_term_types poly_tvars R)
   4.399 +                      $ functional
   4.400 +     val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
   4.401 +     val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
   4.402 + in (thy', def) end;
   4.403 +end;
   4.404 +
   4.405 +
   4.406 +
   4.407 +(*---------------------------------------------------------------------------
   4.408 + * This structure keeps track of congruence rules that aren't derived
   4.409 + * from a datatype definition.
   4.410 + *---------------------------------------------------------------------------*)
   4.411 +fun extraction_thms thy =
   4.412 + let val {case_rewrites,case_congs} = Thry.extract_info thy
   4.413 + in (case_rewrites, case_congs)
   4.414 + end;
   4.415 +
   4.416 +
   4.417 +(*---------------------------------------------------------------------------
   4.418 + * Pair patterns with termination conditions. The full list of patterns for
   4.419 + * a definition is merged with the TCs arising from the user-given clauses.
   4.420 + * There can be fewer clauses than the full list, if the user omitted some
   4.421 + * cases. This routine is used to prepare input for mk_induction.
   4.422 + *---------------------------------------------------------------------------*)
   4.423 +fun merge full_pats TCs =
   4.424 +let fun insert (p,TCs) =
   4.425 +      let fun insrt ((x as (h,[]))::rst) =
   4.426 +                 if (p aconv h) then (p,TCs)::rst else x::insrt rst
   4.427 +            | insrt (x::rst) = x::insrt rst
   4.428 +            | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
   4.429 +      in insrt end
   4.430 +    fun pass ([],ptcl_final) = ptcl_final
   4.431 +      | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
   4.432 +in
   4.433 +  pass (TCs, map (fn p => (p,[])) full_pats)
   4.434 +end;
   4.435 +
   4.436 +
   4.437 +fun givens pats = map pat_of (filter given pats);
   4.438 +
   4.439 +fun post_definition meta_tflCongs (theory, (def, pats)) =
   4.440 + let val tych = Thry.typecheck theory
   4.441 +     val f = #lhs(S.dest_eq(concl def))
   4.442 +     val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   4.443 +     val pats' = filter given pats
   4.444 +     val given_pats = map pat_of pats'
   4.445 +     val rows = map row_of_pat pats'
   4.446 +     val WFR = #ant(S.dest_imp(concl corollary))
   4.447 +     val R = #Rand(S.dest_comb WFR)
   4.448 +     val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
   4.449 +     val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
   4.450 +                           given_pats
   4.451 +     val (case_rewrites,context_congs) = extraction_thms theory
   4.452 +     val corollaries' = map(rewrite_rule case_rewrites) corollaries
   4.453 +     val extract = R.CONTEXT_REWRITE_RULE
   4.454 +                     (f, [R], cut_apply, meta_tflCongs@context_congs)
   4.455 +     val (rules, TCs) = ListPair.unzip (map extract corollaries')
   4.456 +     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   4.457 +     val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   4.458 +     val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   4.459 + in
   4.460 + {theory = theory,
   4.461 +  rules = rules1,
   4.462 +  rows = rows,
   4.463 +  full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
   4.464 +  TCs = TCs}
   4.465 + end;
   4.466 +
   4.467 +
   4.468 +(*---------------------------------------------------------------------------
   4.469 + * Perform the extraction without making the definition. Definition and
   4.470 + * extraction commute for the non-nested case.  (Deferred recdefs)
   4.471 + *
   4.472 + * The purpose of wfrec_eqns is merely to instantiate the recursion theorem
   4.473 + * and extract termination conditions: no definition is made.
   4.474 + *---------------------------------------------------------------------------*)
   4.475 +
   4.476 +fun wfrec_eqns thy fid tflCongs eqns =
   4.477 + let val {lhs,rhs} = S.dest_eq (hd eqns)
   4.478 +     val (f,args) = S.strip_comb lhs
   4.479 +     val (fname,fty) = dest_atom f
   4.480 +     val (SV,a) = front_last args    (* SV = schematic variables *)
   4.481 +     val g = list_comb(f,SV)
   4.482 +     val h = Free(fname,type_of g)
   4.483 +     val eqns1 = map (subst_free[(g,h)]) eqns
   4.484 +     val {functional as Abs(Name, Ty, _),  pats} = mk_functional thy eqns1
   4.485 +     val given_pats = givens pats
   4.486 +     (* val f = Free(Name,Ty) *)
   4.487 +     val Type("fun", [f_dty, f_rty]) = Ty
   4.488 +     val dummy = if Name<>fid then
   4.489 +                        raise TFL_ERR "wfrec_eqns"
   4.490 +                                      ("Expected a definition of " ^
   4.491 +                                      quote fid ^ " but found one of " ^
   4.492 +                                      quote Name)
   4.493 +                 else ()
   4.494 +     val (case_rewrites,context_congs) = extraction_thms thy
   4.495 +     val tych = Thry.typecheck thy
   4.496 +     val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   4.497 +     val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   4.498 +     val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
   4.499 +                   Rtype)
   4.500 +     val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
   4.501 +     val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   4.502 +     val dummy =
   4.503 +           if !trace then
   4.504 +               writeln ("ORIGINAL PROTO_DEF: " ^
   4.505 +                          Sign.string_of_term (Theory.sign_of thy) proto_def)
   4.506 +           else ()
   4.507 +     val R1 = S.rand WFR
   4.508 +     val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   4.509 +     val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   4.510 +     val corollaries' = map (rewrite_rule case_rewrites) corollaries
   4.511 +     fun extract X = R.CONTEXT_REWRITE_RULE
   4.512 +                       (f, R1::SV, cut_apply, tflCongs@context_congs) X
   4.513 + in {proto_def = proto_def,
   4.514 +     SV=SV,
   4.515 +     WFR=WFR,
   4.516 +     pats=pats,
   4.517 +     extracta = map extract corollaries'}
   4.518 + end;
   4.519 +
   4.520 +
   4.521 +(*---------------------------------------------------------------------------
   4.522 + * Define the constant after extracting the termination conditions. The
   4.523 + * wellfounded relation used in the definition is computed by using the
   4.524 + * choice operator on the extracted conditions (plus the condition that
   4.525 + * such a relation must be wellfounded).
   4.526 + *---------------------------------------------------------------------------*)
   4.527 +
   4.528 +fun lazyR_def thy fid tflCongs eqns =
   4.529 + let val {proto_def,WFR,pats,extracta,SV} =
   4.530 +           wfrec_eqns thy fid tflCongs eqns
   4.531 +     val R1 = S.rand WFR
   4.532 +     val f = #lhs(S.dest_eq proto_def)
   4.533 +     val (extractants,TCl) = ListPair.unzip extracta
   4.534 +     val dummy = if !trace
   4.535 +                 then (writeln "Extractants = ";
   4.536 +                       prths extractants;
   4.537 +                       ())
   4.538 +                 else ()
   4.539 +     val TCs = foldr (gen_union (op aconv)) (TCl, [])
   4.540 +     val full_rqt = WFR::TCs
   4.541 +     val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   4.542 +     val R'abs = S.rand R'
   4.543 +     val proto_def' = subst_free[(R1,R')] proto_def
   4.544 +     val dummy = if !trace then writeln ("proto_def' = " ^
   4.545 +                                         Sign.string_of_term
   4.546 +                                         (Theory.sign_of thy) proto_def')
   4.547 +                           else ()
   4.548 +     val {lhs,rhs} = S.dest_eq proto_def'
   4.549 +     val (c,args) = S.strip_comb lhs
   4.550 +     val (Name,Ty) = dest_atom c
   4.551 +     val defn = mk_const_def (Theory.sign_of thy)
   4.552 +                 (Name, Ty, S.list_mk_abs (args,rhs))
   4.553 +     val (theory, [def0]) =
   4.554 +       thy
   4.555 +       |> PureThy.add_defs_i false
   4.556 +            [Thm.no_attributes (fid ^ "_def", defn)]
   4.557 +     val def = freezeT def0;
   4.558 +     val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
   4.559 +                           else ()
   4.560 +     (* val fconst = #lhs(S.dest_eq(concl def))  *)
   4.561 +     val tych = Thry.typecheck theory
   4.562 +     val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   4.563 +         (*lcp: a lot of object-logic inference to remove*)
   4.564 +     val baz = R.DISCH_ALL
   4.565 +                 (U.itlist R.DISCH full_rqt_prop
   4.566 +                  (R.LIST_CONJ extractants))
   4.567 +     val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
   4.568 +                           else ()
   4.569 +     val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   4.570 +     val SV' = map tych SV;
   4.571 +     val SVrefls = map reflexive SV'
   4.572 +     val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
   4.573 +                   SVrefls def)
   4.574 +                RS meta_eq_to_obj_eq
   4.575 +     val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
   4.576 +     val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
   4.577 +     val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
   4.578 +                    body_th
   4.579 + in {theory = theory, R=R1, SV=SV,
   4.580 +     rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
   4.581 +     full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   4.582 +     patterns = pats}
   4.583 + end;
   4.584 +
   4.585 +
   4.586 +
   4.587 +(*----------------------------------------------------------------------------
   4.588 + *
   4.589 + *                           INDUCTION THEOREM
   4.590 + *
   4.591 + *---------------------------------------------------------------------------*)
   4.592 +
   4.593 +
   4.594 +(*------------------------  Miscellaneous function  --------------------------
   4.595 + *
   4.596 + *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
   4.597 + *     -----------------------------------------------------------
   4.598 + *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
   4.599 + *                        ...
   4.600 + *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
   4.601 + *
   4.602 + * This function is totally ad hoc. Used in the production of the induction
   4.603 + * theorem. The nchotomy theorem can have clauses that look like
   4.604 + *
   4.605 + *     ?v1..vn. z = C vn..v1
   4.606 + *
   4.607 + * in which the order of quantification is not the order of occurrence of the
   4.608 + * quantified variables as arguments to C. Since we have no control over this
   4.609 + * aspect of the nchotomy theorem, we make the correspondence explicit by
   4.610 + * pairing the incoming new variable with the term it gets beta-reduced into.
   4.611 + *---------------------------------------------------------------------------*)
   4.612 +
   4.613 +fun alpha_ex_unroll (xlist, tm) =
   4.614 +  let val (qvars,body) = S.strip_exists tm
   4.615 +      val vlist = #2(S.strip_comb (S.rhs body))
   4.616 +      val plist = ListPair.zip (vlist, xlist)
   4.617 +      val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
   4.618 +                   handle Library.OPTION => sys_error
   4.619 +                       "TFL fault [alpha_ex_unroll]: no correspondence"
   4.620 +      fun build ex      []   = []
   4.621 +        | build (_$rex) (v::rst) =
   4.622 +           let val ex1 = betapply(rex, v)
   4.623 +           in  ex1 :: build ex1 rst
   4.624 +           end
   4.625 +     val (nex::exl) = rev (tm::build tm args)
   4.626 +  in
   4.627 +  (nex, ListPair.zip (args, rev exl))
   4.628 +  end;
   4.629 +
   4.630 +
   4.631 +
   4.632 +(*----------------------------------------------------------------------------
   4.633 + *
   4.634 + *             PROVING COMPLETENESS OF PATTERNS
   4.635 + *
   4.636 + *---------------------------------------------------------------------------*)
   4.637 +
   4.638 +fun mk_case ty_info usednames thy =
   4.639 + let
   4.640 + val divide = ipartition (gvvariant usednames)
   4.641 + val tych = Thry.typecheck thy
   4.642 + fun tych_binding(x,y) = (tych x, tych y)
   4.643 + fun fail s = raise TFL_ERR "mk_case" s
   4.644 + fun mk{rows=[],...} = fail"no rows"
   4.645 +   | mk{path=[], rows = [([], (thm, bindings))]} =
   4.646 +                         R.IT_EXISTS (map tych_binding bindings) thm
   4.647 +   | mk{path = u::rstp, rows as (p::_, _)::_} =
   4.648 +     let val (pat_rectangle,rights) = ListPair.unzip rows
   4.649 +         val col0 = map hd pat_rectangle
   4.650 +         val pat_rectangle' = map tl pat_rectangle
   4.651 +     in
   4.652 +     if (forall is_Free col0) (* column 0 is all variables *)
   4.653 +     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
   4.654 +                                (ListPair.zip (rights, col0))
   4.655 +          in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
   4.656 +          end
   4.657 +     else                     (* column 0 is all constructors *)
   4.658 +     let val Type (ty_name,_) = type_of p
   4.659 +     in
   4.660 +     case (ty_info ty_name)
   4.661 +     of None => fail("Not a known datatype: "^ty_name)
   4.662 +      | Some{constructors,nchotomy} =>
   4.663 +        let val thm' = R.ISPEC (tych u) nchotomy
   4.664 +            val disjuncts = S.strip_disj (concl thm')
   4.665 +            val subproblems = divide(constructors, rows)
   4.666 +            val groups      = map #group subproblems
   4.667 +            and new_formals = map #new_formals subproblems
   4.668 +            val existentials = ListPair.map alpha_ex_unroll
   4.669 +                                   (new_formals, disjuncts)
   4.670 +            val constraints = map #1 existentials
   4.671 +            val vexl = map #2 existentials
   4.672 +            fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
   4.673 +            val news = map (fn (nf,rows,c) => {path = nf@rstp,
   4.674 +                                               rows = map (expnd c) rows})
   4.675 +                           (U.zip3 new_formals groups constraints)
   4.676 +            val recursive_thms = map mk news
   4.677 +            val build_exists = foldr
   4.678 +                                (fn((x,t), th) =>
   4.679 +                                 R.CHOOSE (tych x, R.ASSUME (tych t)) th)
   4.680 +            val thms' = ListPair.map build_exists (vexl, recursive_thms)
   4.681 +            val same_concls = R.EVEN_ORS thms'
   4.682 +        in R.DISJ_CASESL thm' same_concls
   4.683 +        end
   4.684 +     end end
   4.685 + in mk
   4.686 + end;
   4.687 +
   4.688 +
   4.689 +fun complete_cases thy =
   4.690 + let val tych = Thry.typecheck thy
   4.691 +     val ty_info = Thry.induct_info thy
   4.692 + in fn pats =>
   4.693 + let val names = foldr add_term_names (pats,[])
   4.694 +     val T = type_of (hd pats)
   4.695 +     val aname = Term.variant names "a"
   4.696 +     val vname = Term.variant (aname::names) "v"
   4.697 +     val a = Free (aname, T)
   4.698 +     val v = Free (vname, T)
   4.699 +     val a_eq_v = HOLogic.mk_eq(a,v)
   4.700 +     val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   4.701 +                           (R.REFL (tych a))
   4.702 +     val th0 = R.ASSUME (tych a_eq_v)
   4.703 +     val rows = map (fn x => ([x], (th0,[]))) pats
   4.704 + in
   4.705 + R.GEN (tych a)
   4.706 +       (R.RIGHT_ASSOC
   4.707 +          (R.CHOOSE(tych v, ex_th0)
   4.708 +                (mk_case ty_info (vname::aname::names)
   4.709 +                 thy {path=[v], rows=rows})))
   4.710 + end end;
   4.711 +
   4.712 +
   4.713 +(*---------------------------------------------------------------------------
   4.714 + * Constructing induction hypotheses: one for each recursive call.
   4.715 + *
   4.716 + * Note. R will never occur as a variable in the ind_clause, because
   4.717 + * to do so, it would have to be from a nested definition, and we don't
   4.718 + * allow nested defns to have R variable.
   4.719 + *
   4.720 + * Note. When the context is empty, there can be no local variables.
   4.721 + *---------------------------------------------------------------------------*)
   4.722 +(*
   4.723 +local infix 5 ==>
   4.724 +      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   4.725 +in
   4.726 +fun build_ih f P (pat,TCs) =
   4.727 + let val globals = S.free_vars_lr pat
   4.728 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   4.729 +     fun dest_TC tm =
   4.730 +         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   4.731 +             val (R,y,_) = S.dest_relation R_y_pat
   4.732 +             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   4.733 +         in case cntxt
   4.734 +              of [] => (P_y, (tm,[]))
   4.735 +               | _  => let
   4.736 +                    val imp = S.list_mk_conj cntxt ==> P_y
   4.737 +                    val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
   4.738 +                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   4.739 +                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   4.740 +         end
   4.741 + in case TCs
   4.742 +    of [] => (S.list_mk_forall(globals, P$pat), [])
   4.743 +     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   4.744 +                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   4.745 +             in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   4.746 +             end
   4.747 + end
   4.748 +end;
   4.749 +*)
   4.750 +
   4.751 +local infix 5 ==>
   4.752 +      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   4.753 +in
   4.754 +fun build_ih f (P,SV) (pat,TCs) =
   4.755 + let val pat_vars = S.free_vars_lr pat
   4.756 +     val globals = pat_vars@SV
   4.757 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   4.758 +     fun dest_TC tm =
   4.759 +         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   4.760 +             val (R,y,_) = S.dest_relation R_y_pat
   4.761 +             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   4.762 +         in case cntxt
   4.763 +              of [] => (P_y, (tm,[]))
   4.764 +               | _  => let
   4.765 +                    val imp = S.list_mk_conj cntxt ==> P_y
   4.766 +                    val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
   4.767 +                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
   4.768 +                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
   4.769 +         end
   4.770 + in case TCs
   4.771 +    of [] => (S.list_mk_forall(pat_vars, P$pat), [])
   4.772 +     |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   4.773 +                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   4.774 +             in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
   4.775 +             end
   4.776 + end
   4.777 +end;
   4.778 +
   4.779 +(*---------------------------------------------------------------------------
   4.780 + * This function makes good on the promise made in "build_ih".
   4.781 + *
   4.782 + * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",
   4.783 + *           TCs = TC_1[pat] ... TC_n[pat]
   4.784 + *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
   4.785 + *---------------------------------------------------------------------------*)
   4.786 +fun prove_case f thy (tm,TCs_locals,thm) =
   4.787 + let val tych = Thry.typecheck thy
   4.788 +     val antc = tych(#ant(S.dest_imp tm))
   4.789 +     val thm' = R.SPEC_ALL thm
   4.790 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   4.791 +     fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
   4.792 +     fun mk_ih ((TC,locals),th2,nested) =
   4.793 +         R.GENL (map tych locals)
   4.794 +            (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
   4.795 +             else if S.is_imp (concl TC) then R.IMP_TRANS TC th2
   4.796 +             else R.MP th2 TC)
   4.797 + in
   4.798 + R.DISCH antc
   4.799 + (if S.is_imp(concl thm') (* recursive calls in this clause *)
   4.800 +  then let val th1 = R.ASSUME antc
   4.801 +           val TCs = map #1 TCs_locals
   4.802 +           val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
   4.803 +                            #2 o S.strip_forall) TCs
   4.804 +           val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
   4.805 +                            TCs_locals
   4.806 +           val th2list = map (U.C R.SPEC th1 o tych) ylist
   4.807 +           val nlist = map nested TCs
   4.808 +           val triples = U.zip3 TClist th2list nlist
   4.809 +           val Pylist = map mk_ih triples
   4.810 +       in R.MP thm' (R.LIST_CONJ Pylist) end
   4.811 +  else thm')
   4.812 + end;
   4.813 +
   4.814 +
   4.815 +(*---------------------------------------------------------------------------
   4.816 + *
   4.817 + *         x = (v1,...,vn)  |- M[x]
   4.818 + *    ---------------------------------------------
   4.819 + *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
   4.820 + *
   4.821 + *---------------------------------------------------------------------------*)
   4.822 +fun LEFT_ABS_VSTRUCT tych thm =
   4.823 +  let fun CHOOSER v (tm,thm) =
   4.824 +        let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
   4.825 +        in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
   4.826 +        end
   4.827 +      val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
   4.828 +      val {lhs,rhs} = S.dest_eq veq
   4.829 +      val L = S.free_vars_lr rhs
   4.830 +  in  #2 (U.itlist CHOOSER L (veq,thm))  end;
   4.831 +
   4.832 +
   4.833 +(*----------------------------------------------------------------------------
   4.834 + * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
   4.835 + *
   4.836 + * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
   4.837 + * recursion induction (Rinduct) by proving the antecedent of Sinduct from
   4.838 + * the antecedent of Rinduct.
   4.839 + *---------------------------------------------------------------------------*)
   4.840 +fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
   4.841 +let val tych = Thry.typecheck thy
   4.842 +    val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
   4.843 +    val (pats,TCsl) = ListPair.unzip pat_TCs_list
   4.844 +    val case_thm = complete_cases thy pats
   4.845 +    val domain = (type_of o hd) pats
   4.846 +    val Pname = Term.variant (foldr (foldr add_term_names)
   4.847 +                              (pats::TCsl, [])) "P"
   4.848 +    val P = Free(Pname, domain --> HOLogic.boolT)
   4.849 +    val Sinduct = R.SPEC (tych P) Sinduction
   4.850 +    val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   4.851 +    val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
   4.852 +    val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   4.853 +    val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   4.854 +    val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
   4.855 +    val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   4.856 +    val proved_cases = map (prove_case fconst thy) tasks
   4.857 +    val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
   4.858 +                    "v",
   4.859 +                  domain)
   4.860 +    val vtyped = tych v
   4.861 +    val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   4.862 +    val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
   4.863 +                          (substs, proved_cases)
   4.864 +    val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
   4.865 +    val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
   4.866 +    val dc = R.MP Sinduct dant
   4.867 +    val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
   4.868 +    val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
   4.869 +    val dc' = U.itlist (R.GEN o tych) vars
   4.870 +                       (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
   4.871 +in
   4.872 +   R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
   4.873 +end
   4.874 +handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
   4.875 +
   4.876 +
   4.877 +
   4.878 +
   4.879 +(*---------------------------------------------------------------------------
   4.880 + *
   4.881 + *                        POST PROCESSING
   4.882 + *
   4.883 + *---------------------------------------------------------------------------*)
   4.884 +
   4.885 +
   4.886 +fun simplify_induction thy hth ind =
   4.887 +  let val tych = Thry.typecheck thy
   4.888 +      val (asl,_) = R.dest_thm ind
   4.889 +      val (_,tc_eq_tc') = R.dest_thm hth
   4.890 +      val tc = S.lhs tc_eq_tc'
   4.891 +      fun loop [] = ind
   4.892 +        | loop (asm::rst) =
   4.893 +          if (can (Thry.match_term thy asm) tc)
   4.894 +          then R.UNDISCH
   4.895 +                 (R.MATCH_MP
   4.896 +                     (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
   4.897 +                     hth)
   4.898 +         else loop rst
   4.899 +  in loop asl
   4.900 +end;
   4.901 +
   4.902 +
   4.903 +(*---------------------------------------------------------------------------
   4.904 + * The termination condition is an antecedent to the rule, and an
   4.905 + * assumption to the theorem.
   4.906 + *---------------------------------------------------------------------------*)
   4.907 +fun elim_tc tcthm (rule,induction) =
   4.908 +   (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
   4.909 +
   4.910 +
   4.911 +fun postprocess{wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
   4.912 +let val tych = Thry.typecheck theory
   4.913 +
   4.914 +   (*---------------------------------------------------------------------
   4.915 +    * Attempt to eliminate WF condition. It's the only assumption of rules
   4.916 +    *---------------------------------------------------------------------*)
   4.917 +   val (rules1,induction1)  =
   4.918 +       let val thm = R.prove(tych(HOLogic.mk_Trueprop
   4.919 +                                  (hd(#1(R.dest_thm rules)))),
   4.920 +                             wf_tac)
   4.921 +       in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
   4.922 +       end handle U.ERR _ => (rules,induction);
   4.923 +
   4.924 +   (*----------------------------------------------------------------------
   4.925 +    * The termination condition (tc) is simplified to |- tc = tc' (there
   4.926 +    * might not be a change!) and then 3 attempts are made:
   4.927 +    *
   4.928 +    *   1. if |- tc = T, then eliminate it with eqT; otherwise,
   4.929 +    *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
   4.930 +    *   3. replace tc by tc' in both the rules and the induction theorem.
   4.931 +    *---------------------------------------------------------------------*)
   4.932 +
   4.933 +   fun print_thms s L =
   4.934 +     if !trace then writeln (cat_lines (s :: map string_of_thm L))
   4.935 +     else ();
   4.936 +
   4.937 +   fun print_cterms s L =
   4.938 +     if !trace then writeln (cat_lines (s :: map string_of_cterm L))
   4.939 +     else ();;
   4.940 +
   4.941 +   fun simplify_tc tc (r,ind) =
   4.942 +       let val tc1 = tych tc
   4.943 +           val _ = print_cterms "TC before simplification: " [tc1]
   4.944 +           val tc_eq = simplifier tc1
   4.945 +           val _ = print_thms "result: " [tc_eq]
   4.946 +       in
   4.947 +       elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   4.948 +       handle U.ERR _ =>
   4.949 +        (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   4.950 +                  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
   4.951 +                           terminator)))
   4.952 +                 (r,ind)
   4.953 +         handle U.ERR _ =>
   4.954 +          (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
   4.955 +           simplify_induction theory tc_eq ind))
   4.956 +       end
   4.957 +
   4.958 +   (*----------------------------------------------------------------------
   4.959 +    * Nested termination conditions are harder to get at, since they are
   4.960 +    * left embedded in the body of the function (and in induction
   4.961 +    * theorem hypotheses). Our "solution" is to simplify them, and try to
   4.962 +    * prove termination, but leave the application of the resulting theorem
   4.963 +    * to a higher level. So things go much as in "simplify_tc": the
   4.964 +    * termination condition (tc) is simplified to |- tc = tc' (there might
   4.965 +    * not be a change) and then 2 attempts are made:
   4.966 +    *
   4.967 +    *   1. if |- tc = T, then return |- tc; otherwise,
   4.968 +    *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
   4.969 +    *   3. return |- tc = tc'
   4.970 +    *---------------------------------------------------------------------*)
   4.971 +   fun simplify_nested_tc tc =
   4.972 +      let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
   4.973 +      in
   4.974 +      R.GEN_ALL
   4.975 +       (R.MATCH_MP Thms.eqT tc_eq
   4.976 +        handle U.ERR _ =>
   4.977 +          (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   4.978 +                      (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
   4.979 +                               terminator))
   4.980 +            handle U.ERR _ => tc_eq))
   4.981 +      end
   4.982 +
   4.983 +   (*-------------------------------------------------------------------
   4.984 +    * Attempt to simplify the termination conditions in each rule and
   4.985 +    * in the induction theorem.
   4.986 +    *-------------------------------------------------------------------*)
   4.987 +   fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
   4.988 +   fun loop ([],extras,R,ind) = (rev R, ind, extras)
   4.989 +     | loop ((r,ftcs)::rst, nthms, R, ind) =
   4.990 +        let val tcs = #1(strip_imp (concl r))
   4.991 +            val extra_tcs = gen_rems (op aconv) (ftcs, tcs)
   4.992 +            val extra_tc_thms = map simplify_nested_tc extra_tcs
   4.993 +            val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind)
   4.994 +            val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
   4.995 +        in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
   4.996 +        end
   4.997 +   val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
   4.998 +   val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
   4.999 +in
  4.1000 +  {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
  4.1001 +end;
  4.1002 +
  4.1003 +
  4.1004 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/TFL/thms.ML	Wed Jan 03 21:20:40 2001 +0100
     5.3 @@ -0,0 +1,21 @@
     5.4 +(*  Title:      TFL/thms.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 +
    5.10 +structure Thms =
    5.11 +struct
    5.12 +  val WFREC_COROLLARY = thm "tfl_wfrec";
    5.13 +  val WF_INDUCTION_THM = thm "tfl_wf_induct";
    5.14 +  val CUT_DEF = thm "cut_def";
    5.15 +  val SELECT_AX = thm "tfl_some";
    5.16 +  val eqT = thm "tfl_eq_True";
    5.17 +  val rev_eq_mp = thm "tfl_rev_eq_mp";
    5.18 +  val simp_thm = thm "tfl_simp_thm";
    5.19 +  val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
    5.20 +  val imp_trans = thm "tfl_imp_trans";
    5.21 +  val disj_assoc = thm "tfl_disj_assoc";
    5.22 +  val tfl_disjE = thm "tfl_disjE";
    5.23 +  val choose_thm = thm "tfl_exE";
    5.24 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/TFL/thry.ML	Wed Jan 03 21:20:40 2001 +0100
     6.3 @@ -0,0 +1,78 @@
     6.4 +(*  Title:      TFL/thry.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 +
    6.10 +signature THRY =
    6.11 +sig
    6.12 +  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
    6.13 +  val match_type: theory -> typ -> typ -> (typ * typ) list
    6.14 +  val typecheck: theory -> term -> cterm
    6.15 +  (*datatype facts of various flavours*)
    6.16 +  val match_info: theory -> string -> {constructors: term list, case_const: term} option
    6.17 +  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
    6.18 +  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
    6.19 +end;
    6.20 +
    6.21 +structure Thry: THRY =
    6.22 +struct
    6.23 +
    6.24 +
    6.25 +fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
    6.26 +
    6.27 +
    6.28 +(*---------------------------------------------------------------------------
    6.29 + *    Matching
    6.30 + *---------------------------------------------------------------------------*)
    6.31 +
    6.32 +local fun tybind (x,y) = (TVar (x, HOLogic.termS) , y)
    6.33 +      fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
    6.34 +in
    6.35 + fun match_term thry pat ob =
    6.36 +    let val tsig = Sign.tsig_of (Theory.sign_of thry)
    6.37 +        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    6.38 +    in (map tmbind tm_theta, map tybind ty_theta)
    6.39 +    end
    6.40 +
    6.41 + fun match_type thry pat ob = map tybind (Vartab.dest
    6.42 +   (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
    6.43 +end;
    6.44 +
    6.45 +
    6.46 +(*---------------------------------------------------------------------------
    6.47 + * Typing
    6.48 + *---------------------------------------------------------------------------*)
    6.49 +
    6.50 +fun typecheck thry t =
    6.51 +  Thm.cterm_of (Theory.sign_of thry) t
    6.52 +    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
    6.53 +      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
    6.54 +
    6.55 +
    6.56 +(*---------------------------------------------------------------------------
    6.57 + * Get information about datatypes
    6.58 + *---------------------------------------------------------------------------*)
    6.59 +
    6.60 +fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
    6.61 +
    6.62 +fun match_info thy tname =
    6.63 +  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
    6.64 +      (Some case_const, Some constructors) =>
    6.65 +        Some {case_const = case_const, constructors = constructors}
    6.66 +    | _ => None;
    6.67 +
    6.68 +fun induct_info thy tname = case get_info thy tname of
    6.69 +        None => None
    6.70 +      | Some {nchotomy, ...} =>
    6.71 +          Some {nchotomy = nchotomy,
    6.72 +                constructors = the (DatatypePackage.constrs_of thy tname)};
    6.73 +
    6.74 +fun extract_info thy =
    6.75 + let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
    6.76 + in {case_congs = map (mk_meta_eq o #case_cong) infos,
    6.77 +     case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
    6.78 + end;
    6.79 +
    6.80 +
    6.81 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/TFL/usyntax.ML	Wed Jan 03 21:20:40 2001 +0100
     7.3 @@ -0,0 +1,409 @@
     7.4 +(*  Title:      TFL/usyntax.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 +Emulation of HOL's abstract syntax functions.
    7.10 +*)
    7.11 +
    7.12 +signature USYNTAX =
    7.13 +sig
    7.14 +  datatype lambda = VAR   of {Name : string, Ty : typ}
    7.15 +                  | CONST of {Name : string, Ty : typ}
    7.16 +                  | COMB  of {Rator: term, Rand : term}
    7.17 +                  | LAMB  of {Bvar : term, Body : term}
    7.18 +
    7.19 +  val alpha : typ
    7.20 +
    7.21 +  (* Types *)
    7.22 +  val type_vars  : typ -> typ list
    7.23 +  val type_varsl : typ list -> typ list
    7.24 +  val mk_vartype : string -> typ
    7.25 +  val is_vartype : typ -> bool
    7.26 +  val strip_prod_type : typ -> typ list
    7.27 +
    7.28 +  (* Terms *)
    7.29 +  val free_vars_lr : term -> term list
    7.30 +  val type_vars_in_term : term -> typ list
    7.31 +  val dest_term  : term -> lambda
    7.32 +
    7.33 +  (* Prelogic *)
    7.34 +  val inst      : (typ*typ) list -> term -> term
    7.35 +
    7.36 +  (* Construction routines *)
    7.37 +  val mk_abs    :{Bvar  : term, Body : term} -> term
    7.38 +
    7.39 +  val mk_imp    :{ant : term, conseq :  term} -> term
    7.40 +  val mk_select :{Bvar : term, Body : term} -> term
    7.41 +  val mk_forall :{Bvar : term, Body : term} -> term
    7.42 +  val mk_exists :{Bvar : term, Body : term} -> term
    7.43 +  val mk_conj   :{conj1 : term, conj2 : term} -> term
    7.44 +  val mk_disj   :{disj1 : term, disj2 : term} -> term
    7.45 +  val mk_pabs   :{varstruct : term, body : term} -> term
    7.46 +
    7.47 +  (* Destruction routines *)
    7.48 +  val dest_const: term -> {Name : string, Ty : typ}
    7.49 +  val dest_comb : term -> {Rator : term, Rand : term}
    7.50 +  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
    7.51 +  val dest_eq     : term -> {lhs : term, rhs : term}
    7.52 +  val dest_imp    : term -> {ant : term, conseq : term}
    7.53 +  val dest_forall : term -> {Bvar : term, Body : term}
    7.54 +  val dest_exists : term -> {Bvar : term, Body : term}
    7.55 +  val dest_neg    : term -> term
    7.56 +  val dest_conj   : term -> {conj1 : term, conj2 : term}
    7.57 +  val dest_disj   : term -> {disj1 : term, disj2 : term}
    7.58 +  val dest_pair   : term -> {fst : term, snd : term}
    7.59 +  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
    7.60 +
    7.61 +  val lhs   : term -> term
    7.62 +  val rhs   : term -> term
    7.63 +  val rand  : term -> term
    7.64 +
    7.65 +  (* Query routines *)
    7.66 +  val is_imp    : term -> bool
    7.67 +  val is_forall : term -> bool
    7.68 +  val is_exists : term -> bool
    7.69 +  val is_neg    : term -> bool
    7.70 +  val is_conj   : term -> bool
    7.71 +  val is_disj   : term -> bool
    7.72 +  val is_pair   : term -> bool
    7.73 +  val is_pabs   : term -> bool
    7.74 +
    7.75 +  (* Construction of a term from a list of Preterms *)
    7.76 +  val list_mk_abs    : (term list * term) -> term
    7.77 +  val list_mk_imp    : (term list * term) -> term
    7.78 +  val list_mk_forall : (term list * term) -> term
    7.79 +  val list_mk_conj   : term list -> term
    7.80 +
    7.81 +  (* Destructing a term to a list of Preterms *)
    7.82 +  val strip_comb     : term -> (term * term list)
    7.83 +  val strip_abs      : term -> (term list * term)
    7.84 +  val strip_imp      : term -> (term list * term)
    7.85 +  val strip_forall   : term -> (term list * term)
    7.86 +  val strip_exists   : term -> (term list * term)
    7.87 +  val strip_disj     : term -> term list
    7.88 +
    7.89 +  (* Miscellaneous *)
    7.90 +  val mk_vstruct : typ -> term list -> term
    7.91 +  val gen_all    : term -> term
    7.92 +  val find_term  : (term -> bool) -> term -> term option
    7.93 +  val dest_relation : term -> term * term * term
    7.94 +  val is_WFR : term -> bool
    7.95 +  val ARB : typ -> term
    7.96 +end;
    7.97 +
    7.98 +structure USyntax: USYNTAX =
    7.99 +struct
   7.100 +
   7.101 +infix 4 ##;
   7.102 +
   7.103 +fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
   7.104 +
   7.105 +
   7.106 +(*---------------------------------------------------------------------------
   7.107 + *
   7.108 + *                            Types
   7.109 + *
   7.110 + *---------------------------------------------------------------------------*)
   7.111 +val mk_prim_vartype = TVar;
   7.112 +fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.termS);
   7.113 +
   7.114 +(* But internally, it's useful *)
   7.115 +fun dest_vtype (TVar x) = x
   7.116 +  | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
   7.117 +
   7.118 +val is_vartype = can dest_vtype;
   7.119 +
   7.120 +val type_vars  = map mk_prim_vartype o typ_tvars
   7.121 +fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
   7.122 +
   7.123 +val alpha  = mk_vartype "'a"
   7.124 +val beta   = mk_vartype "'b"
   7.125 +
   7.126 +val strip_prod_type = HOLogic.prodT_factors;
   7.127 +
   7.128 +
   7.129 +
   7.130 +(*---------------------------------------------------------------------------
   7.131 + *
   7.132 + *                              Terms
   7.133 + *
   7.134 + *---------------------------------------------------------------------------*)
   7.135 +
   7.136 +(* Free variables, in order of occurrence, from left to right in the
   7.137 + * syntax tree. *)
   7.138 +fun free_vars_lr tm =
   7.139 +  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
   7.140 +      fun add (t, frees) = case t of
   7.141 +            Free   _ => if (memb t frees) then frees else t::frees
   7.142 +          | Abs (_,_,body) => add(body,frees)
   7.143 +          | f$t =>  add(t, add(f, frees))
   7.144 +          | _ => frees
   7.145 +  in rev(add(tm,[]))
   7.146 +  end;
   7.147 +
   7.148 +
   7.149 +
   7.150 +val type_vars_in_term = map mk_prim_vartype o term_tvars;
   7.151 +
   7.152 +
   7.153 +
   7.154 +(* Prelogic *)
   7.155 +fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
   7.156 +fun inst theta = subst_vars (map dest_tybinding theta,[])
   7.157 +
   7.158 +
   7.159 +(* Construction routines *)
   7.160 +
   7.161 +fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   7.162 +  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   7.163 +  | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
   7.164 +
   7.165 +
   7.166 +fun mk_imp{ant,conseq} =
   7.167 +   let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   7.168 +   in list_comb(c,[ant,conseq])
   7.169 +   end;
   7.170 +
   7.171 +fun mk_select (r as {Bvar,Body}) =
   7.172 +  let val ty = type_of Bvar
   7.173 +      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
   7.174 +  in list_comb(c,[mk_abs r])
   7.175 +  end;
   7.176 +
   7.177 +fun mk_forall (r as {Bvar,Body}) =
   7.178 +  let val ty = type_of Bvar
   7.179 +      val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   7.180 +  in list_comb(c,[mk_abs r])
   7.181 +  end;
   7.182 +
   7.183 +fun mk_exists (r as {Bvar,Body}) =
   7.184 +  let val ty = type_of Bvar
   7.185 +      val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
   7.186 +  in list_comb(c,[mk_abs r])
   7.187 +  end;
   7.188 +
   7.189 +
   7.190 +fun mk_conj{conj1,conj2} =
   7.191 +   let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   7.192 +   in list_comb(c,[conj1,conj2])
   7.193 +   end;
   7.194 +
   7.195 +fun mk_disj{disj1,disj2} =
   7.196 +   let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   7.197 +   in list_comb(c,[disj1,disj2])
   7.198 +   end;
   7.199 +
   7.200 +fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
   7.201 +
   7.202 +local
   7.203 +fun mk_uncurry(xt,yt,zt) =
   7.204 +    Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
   7.205 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   7.206 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   7.207 +fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   7.208 +in
   7.209 +fun mk_pabs{varstruct,body} =
   7.210 + let fun mpa (varstruct, body) =
   7.211 +       if is_var varstruct
   7.212 +       then mk_abs {Bvar = varstruct, Body = body}
   7.213 +       else let val {fst, snd} = dest_pair varstruct
   7.214 +            in mk_uncurry (type_of fst, type_of snd, type_of body) $
   7.215 +               mpa (fst, mpa (snd, body))
   7.216 +            end
   7.217 + in mpa (varstruct, body) end
   7.218 + handle TYPE _ => raise USYN_ERR "mk_pabs" "";
   7.219 +end;
   7.220 +
   7.221 +(* Destruction routines *)
   7.222 +
   7.223 +datatype lambda = VAR   of {Name : string, Ty : typ}
   7.224 +                | CONST of {Name : string, Ty : typ}
   7.225 +                | COMB  of {Rator: term, Rand : term}
   7.226 +                | LAMB  of {Bvar : term, Body : term};
   7.227 +
   7.228 +
   7.229 +fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
   7.230 +  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
   7.231 +  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
   7.232 +  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
   7.233 +  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
   7.234 +                               in LAMB{Bvar = v, Body = betapply (M,v)}
   7.235 +                               end
   7.236 +  | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
   7.237 +
   7.238 +fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
   7.239 +  | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
   7.240 +
   7.241 +fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
   7.242 +  | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
   7.243 +
   7.244 +fun dest_abs used (a as Abs(s, ty, M)) =
   7.245 +     let
   7.246 +       val s' = variant used s;
   7.247 +       val v = Free(s', ty);
   7.248 +     in ({Bvar = v, Body = betapply (a,v)}, s'::used)
   7.249 +     end
   7.250 +  | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
   7.251 +
   7.252 +fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
   7.253 +  | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   7.254 +
   7.255 +fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
   7.256 +  | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
   7.257 +
   7.258 +fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
   7.259 +  | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
   7.260 +
   7.261 +fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
   7.262 +  | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
   7.263 +
   7.264 +fun dest_neg(Const("not",_) $ M) = M
   7.265 +  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
   7.266 +
   7.267 +fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
   7.268 +  | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
   7.269 +
   7.270 +fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
   7.271 +  | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
   7.272 +
   7.273 +fun mk_pair{fst,snd} =
   7.274 +   let val ty1 = type_of fst
   7.275 +       val ty2 = type_of snd
   7.276 +       val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
   7.277 +   in list_comb(c,[fst,snd])
   7.278 +   end;
   7.279 +
   7.280 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   7.281 +  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   7.282 +
   7.283 +
   7.284 +local  fun ucheck t = (if #Name(dest_const t) = "split" then t
   7.285 +                       else raise Match)
   7.286 +in
   7.287 +fun dest_pabs used tm =
   7.288 +   let val ({Bvar,Body}, used') = dest_abs used tm
   7.289 +   in {varstruct = Bvar, body = Body, used = used'}
   7.290 +   end handle Utils.ERR _ =>
   7.291 +          let val {Rator,Rand} = dest_comb tm
   7.292 +              val _ = ucheck Rator
   7.293 +              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
   7.294 +              val {varstruct = rv, body, used = used''} = dest_pabs used' body
   7.295 +          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
   7.296 +          end
   7.297 +end;
   7.298 +
   7.299 +
   7.300 +val lhs   = #lhs o dest_eq
   7.301 +val rhs   = #rhs o dest_eq
   7.302 +val rand  = #Rand o dest_comb
   7.303 +
   7.304 +
   7.305 +(* Query routines *)
   7.306 +val is_imp    = can dest_imp
   7.307 +val is_forall = can dest_forall
   7.308 +val is_exists = can dest_exists
   7.309 +val is_neg    = can dest_neg
   7.310 +val is_conj   = can dest_conj
   7.311 +val is_disj   = can dest_disj
   7.312 +val is_pair   = can dest_pair
   7.313 +val is_pabs   = can (dest_pabs [])
   7.314 +
   7.315 +
   7.316 +(* Construction of a cterm from a list of Terms *)
   7.317 +
   7.318 +fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
   7.319 +
   7.320 +(* These others are almost never used *)
   7.321 +fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   7.322 +fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
   7.323 +val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
   7.324 +
   7.325 +
   7.326 +(* Need to reverse? *)
   7.327 +fun gen_all tm = list_mk_forall(term_frees tm, tm);
   7.328 +
   7.329 +(* Destructing a cterm to a list of Terms *)
   7.330 +fun strip_comb tm =
   7.331 +   let fun dest(M$N, A) = dest(M, N::A)
   7.332 +         | dest x = x
   7.333 +   in dest(tm,[])
   7.334 +   end;
   7.335 +
   7.336 +fun strip_abs(tm as Abs _) =
   7.337 +       let val ({Bvar,Body}, _) = dest_abs [] tm
   7.338 +           val (bvs, core) = strip_abs Body
   7.339 +       in (Bvar::bvs, core)
   7.340 +       end
   7.341 +  | strip_abs M = ([],M);
   7.342 +
   7.343 +
   7.344 +fun strip_imp fm =
   7.345 +   if (is_imp fm)
   7.346 +   then let val {ant,conseq} = dest_imp fm
   7.347 +            val (was,wb) = strip_imp conseq
   7.348 +        in ((ant::was), wb)
   7.349 +        end
   7.350 +   else ([],fm);
   7.351 +
   7.352 +fun strip_forall fm =
   7.353 +   if (is_forall fm)
   7.354 +   then let val {Bvar,Body} = dest_forall fm
   7.355 +            val (bvs,core) = strip_forall Body
   7.356 +        in ((Bvar::bvs), core)
   7.357 +        end
   7.358 +   else ([],fm);
   7.359 +
   7.360 +
   7.361 +fun strip_exists fm =
   7.362 +   if (is_exists fm)
   7.363 +   then let val {Bvar, Body} = dest_exists fm
   7.364 +            val (bvs,core) = strip_exists Body
   7.365 +        in (Bvar::bvs, core)
   7.366 +        end
   7.367 +   else ([],fm);
   7.368 +
   7.369 +fun strip_disj w =
   7.370 +   if (is_disj w)
   7.371 +   then let val {disj1,disj2} = dest_disj w
   7.372 +        in (strip_disj disj1@strip_disj disj2)
   7.373 +        end
   7.374 +   else [w];
   7.375 +
   7.376 +
   7.377 +(* Miscellaneous *)
   7.378 +
   7.379 +fun mk_vstruct ty V =
   7.380 +  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
   7.381 +              let val (ltm,vs1) = follow_prod_type ty1 vs
   7.382 +                  val (rtm,vs2) = follow_prod_type ty2 vs1
   7.383 +              in (mk_pair{fst=ltm, snd=rtm}, vs2) end
   7.384 +        | follow_prod_type _ (v::vs) = (v,vs)
   7.385 +  in #1 (follow_prod_type ty V)  end;
   7.386 +
   7.387 +
   7.388 +(* Search a term for a sub-term satisfying the predicate p. *)
   7.389 +fun find_term p =
   7.390 +   let fun find tm =
   7.391 +      if (p tm) then Some tm
   7.392 +      else case tm of
   7.393 +          Abs(_,_,body) => find body
   7.394 +        | (t$u)         => (case find t of None => find u | some => some)
   7.395 +        | _             => None
   7.396 +   in find
   7.397 +   end;
   7.398 +
   7.399 +fun dest_relation tm =
   7.400 +   if (type_of tm = HOLogic.boolT)
   7.401 +   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
   7.402 +        in (R,y,x)
   7.403 +        end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
   7.404 +   else raise USYN_ERR "dest_relation" "not a boolean term";
   7.405 +
   7.406 +fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
   7.407 +  | is_WFR _                 = false;
   7.408 +
   7.409 +fun ARB ty = mk_select{Bvar=Free("v",ty),
   7.410 +                       Body=Const("True",HOLogic.boolT)};
   7.411 +
   7.412 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/TFL/utils.ML	Wed Jan 03 21:20:40 2001 +0100
     8.3 @@ -0,0 +1,78 @@
     8.4 +(*  Title:      TFL/utils.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 +Basic utilities.
    8.10 +*)
    8.11 +
    8.12 +signature UTILS =
    8.13 +sig
    8.14 +  exception ERR of {module: string, func: string, mesg: string}
    8.15 +  val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
    8.16 +  val itlist: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    8.17 +  val rev_itlist: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    8.18 +  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
    8.19 +  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    8.20 +  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
    8.21 +  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
    8.22 +  val take: ('a -> 'b) -> int * 'a list -> 'b list
    8.23 +end;
    8.24 +
    8.25 +structure Utils: UTILS =
    8.26 +struct
    8.27 +
    8.28 +(*standard exception for TFL*)
    8.29 +exception ERR of {module: string, func: string, mesg: string};
    8.30 +
    8.31 +fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
    8.32 +
    8.33 +
    8.34 +fun C f x y = f y x
    8.35 +
    8.36 +fun itlist f L base_value =
    8.37 +   let fun it [] = base_value
    8.38 +         | it (a::rst) = f a (it rst)
    8.39 +   in it L
    8.40 +   end;
    8.41 +
    8.42 +fun rev_itlist f =
    8.43 +   let fun rev_it [] base = base
    8.44 +         | rev_it (a::rst) base = rev_it rst (f a base)
    8.45 +   in rev_it
    8.46 +   end;
    8.47 +
    8.48 +fun end_itlist f =
    8.49 +   let fun endit [] = raise UTILS_ERR "end_itlist" "list too short"
    8.50 +         | endit alist =
    8.51 +            let val (base::ralist) = rev alist
    8.52 +            in itlist f (rev ralist) base
    8.53 +            end
    8.54 +   in endit
    8.55 +   end;
    8.56 +
    8.57 +fun itlist2 f L1 L2 base_value =
    8.58 + let fun it ([],[]) = base_value
    8.59 +       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
    8.60 +       | it _ = raise UTILS_ERR "itlist2" "different length lists"
    8.61 + in  it (L1,L2)
    8.62 + end;
    8.63 +
    8.64 +fun pluck p  =
    8.65 +  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
    8.66 +        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
    8.67 +  in fn L => remv(L,[])
    8.68 +  end;
    8.69 +
    8.70 +fun take f =
    8.71 +  let fun grab(0,L) = []
    8.72 +        | grab(n, x::rst) = f x::grab(n-1,rst)
    8.73 +  in grab
    8.74 +  end;
    8.75 +
    8.76 +fun zip3 [][][] = []
    8.77 +  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
    8.78 +  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
    8.79 +
    8.80 +
    8.81 +end;