src/HOL/Library/old_recdef.ML
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 67710 cc2db3239932
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/old_recdef.ML
     2     Author:     Konrad Slind, Cambridge University Computer Laboratory
     3     Author:     Lucas Dixon, University of Edinburgh
     4 
     5 Old TFL/recdef package.
     6 *)
     7 
     8 signature CASE_SPLIT =
     9 sig
    10   (* try to recursively split conjectured thm to given list of thms *)
    11   val splitto : Proof.context -> thm list -> thm -> thm
    12 end;
    13 
    14 signature UTILS =
    15 sig
    16   exception ERR of {module: string, func: string, mesg: string}
    17   val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
    18   val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    19   val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
    20   val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
    21   val take: ('a -> 'b) -> int * 'a list -> 'b list
    22 end;
    23 
    24 signature USYNTAX =
    25 sig
    26   datatype lambda = VAR   of {Name : string, Ty : typ}
    27                   | CONST of {Name : string, Ty : typ}
    28                   | COMB  of {Rator: term, Rand : term}
    29                   | LAMB  of {Bvar : term, Body : term}
    30 
    31   val alpha : typ
    32 
    33   (* Types *)
    34   val type_vars  : typ -> typ list
    35   val type_varsl : typ list -> typ list
    36   val mk_vartype : string -> typ
    37   val is_vartype : typ -> bool
    38   val strip_prod_type : typ -> typ list
    39 
    40   (* Terms *)
    41   val free_vars_lr : term -> term list
    42   val type_vars_in_term : term -> typ list
    43   val dest_term  : term -> lambda
    44 
    45   (* Prelogic *)
    46   val inst      : (typ*typ) list -> term -> term
    47 
    48   (* Construction routines *)
    49   val mk_abs    :{Bvar  : term, Body : term} -> term
    50 
    51   val mk_imp    :{ant : term, conseq :  term} -> term
    52   val mk_select :{Bvar : term, Body : term} -> term
    53   val mk_forall :{Bvar : term, Body : term} -> term
    54   val mk_exists :{Bvar : term, Body : term} -> term
    55   val mk_conj   :{conj1 : term, conj2 : term} -> term
    56   val mk_disj   :{disj1 : term, disj2 : term} -> term
    57   val mk_pabs   :{varstruct : term, body : term} -> term
    58 
    59   (* Destruction routines *)
    60   val dest_const: term -> {Name : string, Ty : typ}
    61   val dest_comb : term -> {Rator : term, Rand : term}
    62   val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
    63   val dest_eq     : term -> {lhs : term, rhs : term}
    64   val dest_imp    : term -> {ant : term, conseq : term}
    65   val dest_forall : term -> {Bvar : term, Body : term}
    66   val dest_exists : term -> {Bvar : term, Body : term}
    67   val dest_neg    : term -> term
    68   val dest_conj   : term -> {conj1 : term, conj2 : term}
    69   val dest_disj   : term -> {disj1 : term, disj2 : term}
    70   val dest_pair   : term -> {fst : term, snd : term}
    71   val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
    72 
    73   val lhs   : term -> term
    74   val rhs   : term -> term
    75   val rand  : term -> term
    76 
    77   (* Query routines *)
    78   val is_imp    : term -> bool
    79   val is_forall : term -> bool
    80   val is_exists : term -> bool
    81   val is_neg    : term -> bool
    82   val is_conj   : term -> bool
    83   val is_disj   : term -> bool
    84   val is_pair   : term -> bool
    85   val is_pabs   : term -> bool
    86 
    87   (* Construction of a term from a list of Preterms *)
    88   val list_mk_abs    : (term list * term) -> term
    89   val list_mk_imp    : (term list * term) -> term
    90   val list_mk_forall : (term list * term) -> term
    91   val list_mk_conj   : term list -> term
    92 
    93   (* Destructing a term to a list of Preterms *)
    94   val strip_comb     : term -> (term * term list)
    95   val strip_abs      : term -> (term list * term)
    96   val strip_imp      : term -> (term list * term)
    97   val strip_forall   : term -> (term list * term)
    98   val strip_exists   : term -> (term list * term)
    99   val strip_disj     : term -> term list
   100 
   101   (* Miscellaneous *)
   102   val mk_vstruct : typ -> term list -> term
   103   val gen_all    : term -> term
   104   val find_term  : (term -> bool) -> term -> term option
   105   val dest_relation : term -> term * term * term
   106   val is_WFR : term -> bool
   107   val ARB : typ -> term
   108 end;
   109 
   110 signature DCTERM =
   111 sig
   112   val dest_comb: cterm -> cterm * cterm
   113   val dest_abs: string option -> cterm -> cterm * cterm
   114   val capply: cterm -> cterm -> cterm
   115   val cabs: cterm -> cterm -> cterm
   116   val mk_conj: cterm * cterm -> cterm
   117   val mk_disj: cterm * cterm -> cterm
   118   val mk_exists: cterm * cterm -> cterm
   119   val dest_conj: cterm -> cterm * cterm
   120   val dest_const: cterm -> {Name: string, Ty: typ}
   121   val dest_disj: cterm -> cterm * cterm
   122   val dest_eq: cterm -> cterm * cterm
   123   val dest_exists: cterm -> cterm * cterm
   124   val dest_forall: cterm -> cterm * cterm
   125   val dest_imp: cterm -> cterm * cterm
   126   val dest_neg: cterm -> cterm
   127   val dest_pair: cterm -> cterm * cterm
   128   val dest_var: cterm -> {Name:string, Ty:typ}
   129   val is_conj: cterm -> bool
   130   val is_disj: cterm -> bool
   131   val is_eq: cterm -> bool
   132   val is_exists: cterm -> bool
   133   val is_forall: cterm -> bool
   134   val is_imp: cterm -> bool
   135   val is_neg: cterm -> bool
   136   val is_pair: cterm -> bool
   137   val list_mk_disj: cterm list -> cterm
   138   val strip_abs: cterm -> cterm list * cterm
   139   val strip_comb: cterm -> cterm * cterm list
   140   val strip_disj: cterm -> cterm list
   141   val strip_exists: cterm -> cterm list * cterm
   142   val strip_forall: cterm -> cterm list * cterm
   143   val strip_imp: cterm -> cterm list * cterm
   144   val drop_prop: cterm -> cterm
   145   val mk_prop: cterm -> cterm
   146 end;
   147 
   148 signature RULES =
   149 sig
   150   val dest_thm: thm -> term list * term
   151 
   152   (* Inference rules *)
   153   val REFL: cterm -> thm
   154   val ASSUME: cterm -> thm
   155   val MP: thm -> thm -> thm
   156   val MATCH_MP: thm -> thm -> thm
   157   val CONJUNCT1: thm -> thm
   158   val CONJUNCT2: thm -> thm
   159   val CONJUNCTS: thm -> thm list
   160   val DISCH: cterm -> thm -> thm
   161   val UNDISCH: thm  -> thm
   162   val SPEC: cterm -> thm -> thm
   163   val ISPEC: cterm -> thm -> thm
   164   val ISPECL: cterm list -> thm -> thm
   165   val GEN: Proof.context -> cterm -> thm -> thm
   166   val GENL: Proof.context -> cterm list -> thm -> thm
   167   val LIST_CONJ: thm list -> thm
   168 
   169   val SYM: thm -> thm
   170   val DISCH_ALL: thm -> thm
   171   val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
   172   val SPEC_ALL: thm -> thm
   173   val GEN_ALL: Proof.context -> thm -> thm
   174   val IMP_TRANS: thm -> thm -> thm
   175   val PROVE_HYP: thm -> thm -> thm
   176 
   177   val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
   178   val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
   179   val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
   180 
   181   val EVEN_ORS: thm list -> thm list
   182   val DISJ_CASESL: thm -> thm list -> thm
   183 
   184   val list_beta_conv: cterm -> cterm list -> thm
   185   val SUBS: Proof.context -> thm list -> thm -> thm
   186   val simpl_conv: Proof.context -> thm list -> cterm -> thm
   187 
   188   val rbeta: thm -> thm
   189   val tracing: bool Unsynchronized.ref
   190   val CONTEXT_REWRITE_RULE: Proof.context ->
   191     term * term list * thm * thm list -> thm -> thm * term list
   192   val RIGHT_ASSOC: Proof.context -> thm -> thm
   193 
   194   val prove: Proof.context -> bool -> term * tactic -> thm
   195 end;
   196 
   197 signature THRY =
   198 sig
   199   val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
   200   val match_type: theory -> typ -> typ -> (typ * typ) list
   201   val typecheck: theory -> term -> cterm
   202   (*datatype facts of various flavours*)
   203   val match_info: theory -> string -> {constructors: term list, case_const: term} option
   204   val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
   205   val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
   206 end;
   207 
   208 signature PRIM =
   209 sig
   210   val trace: bool Unsynchronized.ref
   211   val trace_thms: Proof.context -> string -> thm list -> unit
   212   val trace_cterm: Proof.context -> string -> cterm -> unit
   213   type pattern
   214   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
   215   val wfrec_definition0: string -> term -> term -> theory -> thm * theory
   216   val post_definition: Proof.context -> thm list -> thm * pattern list ->
   217    {rules: thm,
   218     rows: int list,
   219     TCs: term list list,
   220     full_pats_TCs: (term * term list) list}
   221   val mk_induction: Proof.context ->
   222     {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
   223   val postprocess: Proof.context -> bool ->
   224     {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
   225     {rules: thm, induction: thm, TCs: term list list} ->
   226     {rules: thm, induction: thm, nested_tcs: thm list}
   227 end;
   228 
   229 signature TFL =
   230 sig
   231   val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
   232     {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
   233   val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
   234     {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
   235 end;
   236 
   237 signature OLD_RECDEF =
   238 sig
   239   val get_recdef: theory -> string
   240     -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
   241   val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   242   val simp_add: attribute
   243   val simp_del: attribute
   244   val cong_add: attribute
   245   val cong_del: attribute
   246   val wf_add: attribute
   247   val wf_del: attribute
   248   val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
   249     Token.src option -> theory -> theory
   250       * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   251   val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
   252     theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   253 end;
   254 
   255 structure Old_Recdef: OLD_RECDEF =
   256 struct
   257 
   258 (*** extra case splitting for TFL ***)
   259 
   260 structure CaseSplit: CASE_SPLIT =
   261 struct
   262 
   263 (* make a casethm from an induction thm *)
   264 fun cases_thm_of_induct_thm ctxt =
   265   Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
   266 
   267 (* get the case_thm (my version) from a type *)
   268 fun case_thm_of_ty ctxt ty  =
   269     let
   270       val thy = Proof_Context.theory_of ctxt
   271       val ty_str = case ty of
   272                      Type(ty_str, _) => ty_str
   273                    | TFree(s,_)  => error ("Free type: " ^ s)
   274                    | TVar((s,_),_) => error ("Free variable: " ^ s)
   275       val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
   276     in
   277       cases_thm_of_induct_thm ctxt induct
   278     end;
   279 
   280 
   281 (* for use when there are no prems to the subgoal *)
   282 (* does a case split on the given variable *)
   283 fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
   284     let
   285       val thy = Proof_Context.theory_of ctxt;
   286 
   287       val x = Free(vstr,ty);
   288       val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
   289 
   290       val case_thm = case_thm_of_ty ctxt ty;
   291 
   292       val abs_ct = Thm.cterm_of ctxt abst;
   293       val free_ct = Thm.cterm_of ctxt x;
   294 
   295       val (Pv, Dv, type_insts) =
   296           case (Thm.concl_of case_thm) of
   297             (_ $ (Pv $ (Dv as Var(_, Dty)))) =>
   298             (Pv, Dv,
   299              Sign.typ_match thy (Dty, ty) Vartab.empty)
   300           | _ => error "not a valid case thm";
   301       val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
   302         (Vartab.dest type_insts);
   303       val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
   304       val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
   305     in
   306       Conv.fconv_rule Drule.beta_eta_conversion
   307          (case_thm
   308             |> Thm.instantiate (type_cinsts, [])
   309             |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
   310     end;
   311 
   312 
   313 (* the find_XXX_split functions are simply doing a lightwieght (I
   314 think) term matching equivalent to find where to do the next split *)
   315 
   316 (* assuming two twems are identical except for a free in one at a
   317 subterm, or constant in another, ie assume that one term is a plit of
   318 another, then gives back the free variable that has been split. *)
   319 exception find_split_exp of string
   320 fun find_term_split (Free v, _ $ _) = SOME v
   321   | find_term_split (Free v, Const _) = SOME v
   322   | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
   323   | find_term_split (Free _, Var _) = NONE (* keep searching *)
   324   | find_term_split (a $ b, a2 $ b2) =
   325     (case find_term_split (a, a2) of
   326        NONE => find_term_split (b,b2)
   327      | vopt => vopt)
   328   | find_term_split (Abs(_,_,t1), Abs(_,_,t2)) =
   329     find_term_split (t1, t2)
   330   | find_term_split (Const (x,_), Const(x2,_)) =
   331     if x = x2 then NONE else (* keep searching *)
   332     raise find_split_exp (* stop now *)
   333             "Terms are not identical upto a free varaible! (Consts)"
   334   | find_term_split (Bound i, Bound j) =
   335     if i = j then NONE else (* keep searching *)
   336     raise find_split_exp (* stop now *)
   337             "Terms are not identical upto a free varaible! (Bound)"
   338   | find_term_split _ =
   339     raise find_split_exp (* stop now *)
   340             "Terms are not identical upto a free varaible! (Other)";
   341 
   342 (* assume that "splitth" is a case split form of subgoal i of "genth",
   343 then look for a free variable to split, breaking the subgoal closer to
   344 splitth. *)
   345 fun find_thm_split splitth i genth =
   346     find_term_split (Logic.get_goal (Thm.prop_of genth) i,
   347                      Thm.concl_of splitth) handle find_split_exp _ => NONE;
   348 
   349 (* as above but searches "splitths" for a theorem that suggest a case split *)
   350 fun find_thms_split splitths i genth =
   351     Library.get_first (fn sth => find_thm_split sth i genth) splitths;
   352 
   353 
   354 (* split the subgoal i of "genth" until we get to a member of
   355 splitths. Assumes that genth will be a general form of splitths, that
   356 can be case-split, as needed. Otherwise fails. Note: We assume that
   357 all of "splitths" are split to the same level, and thus it doesn't
   358 matter which one we choose to look for the next split. Simply add
   359 search on splitthms and split variable, to change this.  *)
   360 (* Note: possible efficiency measure: when a case theorem is no longer
   361 useful, drop it? *)
   362 (* Note: This should not be a separate tactic but integrated into the
   363 case split done during recdef's case analysis, this would avoid us
   364 having to (re)search for variables to split. *)
   365 fun splitto ctxt splitths genth =
   366     let
   367       val _ = not (null splitths) orelse error "splitto: no given splitths";
   368 
   369       (* check if we are a member of splitths - FIXME: quicker and
   370       more flexible with discrim net. *)
   371       fun solve_by_splitth th split =
   372         Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
   373 
   374       fun split th =
   375         (case find_thms_split splitths 1 th of
   376           NONE =>
   377            (writeln (cat_lines
   378             (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
   379               map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
   380             error "splitto: cannot find variable to split on")
   381         | SOME v =>
   382             let
   383               val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
   384               val split_thm = mk_casesplit_goal_thm ctxt v gt;
   385               val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
   386             in
   387               expf (map recsplitf subthms)
   388             end)
   389 
   390       and recsplitf th =
   391         (* note: multiple unifiers! we only take the first element,
   392            probably fine -- there is probably only one anyway. *)
   393         (case get_first (Seq.pull o solve_by_splitth th) splitths of
   394           NONE => split th
   395         | SOME (solved_th, _) => solved_th);
   396     in
   397       recsplitf genth
   398     end;
   399 
   400 end;
   401 
   402 
   403 
   404 (*** basic utilities ***)
   405 
   406 structure Utils: UTILS =
   407 struct
   408 
   409 (*standard exception for TFL*)
   410 exception ERR of {module: string, func: string, mesg: string};
   411 
   412 fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
   413 
   414 
   415 fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short")
   416   | end_itlist _ [x] = x
   417   | end_itlist f (x :: xs) = f x (end_itlist f xs);
   418 
   419 fun itlist2 f L1 L2 base_value =
   420  let fun it ([],[]) = base_value
   421        | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
   422        | it _ = raise UTILS_ERR "itlist2" "different length lists"
   423  in  it (L1,L2)
   424  end;
   425 
   426 fun pluck p  =
   427   let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
   428         | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
   429   in fn L => remv(L,[])
   430   end;
   431 
   432 fun take f =
   433   let fun grab(0, _) = []
   434         | grab(n, x::rst) = f x::grab(n-1,rst)
   435   in grab
   436   end;
   437 
   438 fun zip3 [][][] = []
   439   | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
   440   | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
   441 
   442 
   443 end;
   444 
   445 
   446 
   447 (*** emulation of HOL's abstract syntax functions ***)
   448 
   449 structure USyntax: USYNTAX =
   450 struct
   451 
   452 infix 4 ##;
   453 
   454 fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
   455 
   456 
   457 (*---------------------------------------------------------------------------
   458  *
   459  *                            Types
   460  *
   461  *---------------------------------------------------------------------------*)
   462 val mk_prim_vartype = TVar;
   463 fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
   464 
   465 (* But internally, it's useful *)
   466 fun dest_vtype (TVar x) = x
   467   | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
   468 
   469 val is_vartype = can dest_vtype;
   470 
   471 val type_vars  = map mk_prim_vartype o Misc_Legacy.typ_tvars
   472 fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
   473 
   474 val alpha  = mk_vartype "'a"
   475 
   476 val strip_prod_type = HOLogic.flatten_tupleT;
   477 
   478 
   479 
   480 (*---------------------------------------------------------------------------
   481  *
   482  *                              Terms
   483  *
   484  *---------------------------------------------------------------------------*)
   485 
   486 (* Free variables, in order of occurrence, from left to right in the
   487  * syntax tree. *)
   488 fun free_vars_lr tm =
   489   let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
   490       fun add (t, frees) = case t of
   491             Free   _ => if (memb t frees) then frees else t::frees
   492           | Abs (_,_,body) => add(body,frees)
   493           | f$t =>  add(t, add(f, frees))
   494           | _ => frees
   495   in rev(add(tm,[]))
   496   end;
   497 
   498 
   499 
   500 val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
   501 
   502 
   503 
   504 (* Prelogic *)
   505 fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
   506 fun inst theta = subst_vars (map dest_tybinding theta,[])
   507 
   508 
   509 (* Construction routines *)
   510 
   511 fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   512   | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   513   | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
   514 
   515 
   516 fun mk_imp{ant,conseq} =
   517    let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   518    in list_comb(c,[ant,conseq])
   519    end;
   520 
   521 fun mk_select (r as {Bvar,Body}) =
   522   let val ty = type_of Bvar
   523       val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
   524   in list_comb(c,[mk_abs r])
   525   end;
   526 
   527 fun mk_forall (r as {Bvar,Body}) =
   528   let val ty = type_of Bvar
   529       val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   530   in list_comb(c,[mk_abs r])
   531   end;
   532 
   533 fun mk_exists (r as {Bvar,Body}) =
   534   let val ty = type_of Bvar
   535       val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   536   in list_comb(c,[mk_abs r])
   537   end;
   538 
   539 
   540 fun mk_conj{conj1,conj2} =
   541    let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   542    in list_comb(c,[conj1,conj2])
   543    end;
   544 
   545 fun mk_disj{disj1,disj2} =
   546    let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   547    in list_comb(c,[disj1,disj2])
   548    end;
   549 
   550 fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
   551 
   552 local
   553 fun mk_uncurry (xt, yt, zt) =
   554     Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
   555 fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   556   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   557 fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   558 in
   559 fun mk_pabs{varstruct,body} =
   560  let fun mpa (varstruct, body) =
   561        if is_var varstruct
   562        then mk_abs {Bvar = varstruct, Body = body}
   563        else let val {fst, snd} = dest_pair varstruct
   564             in mk_uncurry (type_of fst, type_of snd, type_of body) $
   565                mpa (fst, mpa (snd, body))
   566             end
   567  in mpa (varstruct, body) end
   568  handle TYPE _ => raise USYN_ERR "mk_pabs" "";
   569 end;
   570 
   571 (* Destruction routines *)
   572 
   573 datatype lambda = VAR   of {Name : string, Ty : typ}
   574                 | CONST of {Name : string, Ty : typ}
   575                 | COMB  of {Rator: term, Rand : term}
   576                 | LAMB  of {Bvar : term, Body : term};
   577 
   578 
   579 fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty}
   580   | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
   581   | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
   582   | dest_term(M$N)           = COMB{Rator=M,Rand=N}
   583   | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
   584                                in LAMB{Bvar = v, Body = Term.betapply (M,v)}
   585                                end
   586   | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
   587 
   588 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
   589   | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
   590 
   591 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
   592   | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
   593 
   594 fun dest_abs used (a as Abs(s, ty, _)) =
   595      let
   596        val s' = singleton (Name.variant_list used) s;
   597        val v = Free(s', ty);
   598      in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
   599      end
   600   | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
   601 
   602 fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
   603   | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   604 
   605 fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
   606   | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
   607 
   608 fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
   609   | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
   610 
   611 fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
   612   | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
   613 
   614 fun dest_neg(Const(@{const_name Not},_) $ M) = M
   615   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
   616 
   617 fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
   618   | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
   619 
   620 fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
   621   | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
   622 
   623 fun mk_pair{fst,snd} =
   624    let val ty1 = type_of fst
   625        val ty2 = type_of snd
   626        val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
   627    in list_comb(c,[fst,snd])
   628    end;
   629 
   630 fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   631   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   632 
   633 
   634 local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
   635                        else raise Match)
   636 in
   637 fun dest_pabs used tm =
   638    let val ({Bvar,Body}, used') = dest_abs used tm
   639    in {varstruct = Bvar, body = Body, used = used'}
   640    end handle Utils.ERR _ =>
   641           let val {Rator,Rand} = dest_comb tm
   642               val _ = ucheck Rator
   643               val {varstruct = lv, body, used = used'} = dest_pabs used Rand
   644               val {varstruct = rv, body, used = used''} = dest_pabs used' body
   645           in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
   646           end
   647 end;
   648 
   649 
   650 val lhs   = #lhs o dest_eq
   651 val rhs   = #rhs o dest_eq
   652 val rand  = #Rand o dest_comb
   653 
   654 
   655 (* Query routines *)
   656 val is_imp    = can dest_imp
   657 val is_forall = can dest_forall
   658 val is_exists = can dest_exists
   659 val is_neg    = can dest_neg
   660 val is_conj   = can dest_conj
   661 val is_disj   = can dest_disj
   662 val is_pair   = can dest_pair
   663 val is_pabs   = can (dest_pabs [])
   664 
   665 
   666 (* Construction of a cterm from a list of Terms *)
   667 
   668 fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
   669 
   670 (* These others are almost never used *)
   671 fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   672 fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
   673 val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
   674 
   675 
   676 (* Need to reverse? *)
   677 fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
   678 
   679 (* Destructing a cterm to a list of Terms *)
   680 fun strip_comb tm =
   681    let fun dest(M$N, A) = dest(M, N::A)
   682          | dest x = x
   683    in dest(tm,[])
   684    end;
   685 
   686 fun strip_abs(tm as Abs _) =
   687        let val ({Bvar,Body}, _) = dest_abs [] tm
   688            val (bvs, core) = strip_abs Body
   689        in (Bvar::bvs, core)
   690        end
   691   | strip_abs M = ([],M);
   692 
   693 
   694 fun strip_imp fm =
   695    if (is_imp fm)
   696    then let val {ant,conseq} = dest_imp fm
   697             val (was,wb) = strip_imp conseq
   698         in ((ant::was), wb)
   699         end
   700    else ([],fm);
   701 
   702 fun strip_forall fm =
   703    if (is_forall fm)
   704    then let val {Bvar,Body} = dest_forall fm
   705             val (bvs,core) = strip_forall Body
   706         in ((Bvar::bvs), core)
   707         end
   708    else ([],fm);
   709 
   710 
   711 fun strip_exists fm =
   712    if (is_exists fm)
   713    then let val {Bvar, Body} = dest_exists fm
   714             val (bvs,core) = strip_exists Body
   715         in (Bvar::bvs, core)
   716         end
   717    else ([],fm);
   718 
   719 fun strip_disj w =
   720    if (is_disj w)
   721    then let val {disj1,disj2} = dest_disj w
   722         in (strip_disj disj1@strip_disj disj2)
   723         end
   724    else [w];
   725 
   726 
   727 (* Miscellaneous *)
   728 
   729 fun mk_vstruct ty V =
   730   let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
   731               let val (ltm,vs1) = follow_prod_type ty1 vs
   732                   val (rtm,vs2) = follow_prod_type ty2 vs1
   733               in (mk_pair{fst=ltm, snd=rtm}, vs2) end
   734         | follow_prod_type _ (v::vs) = (v,vs)
   735   in #1 (follow_prod_type ty V)  end;
   736 
   737 
   738 (* Search a term for a sub-term satisfying the predicate p. *)
   739 fun find_term p =
   740    let fun find tm =
   741       if (p tm) then SOME tm
   742       else case tm of
   743           Abs(_,_,body) => find body
   744         | (t$u)         => (case find t of NONE => find u | some => some)
   745         | _             => NONE
   746    in find
   747    end;
   748 
   749 fun dest_relation tm =
   750    if (type_of tm = HOLogic.boolT)
   751    then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
   752         in (R,y,x)
   753         end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
   754    else raise USYN_ERR "dest_relation" "not a boolean term";
   755 
   756 fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
   757   | is_WFR _                 = false;
   758 
   759 fun ARB ty = mk_select{Bvar=Free("v",ty),
   760                        Body=Const(@{const_name True},HOLogic.boolT)};
   761 
   762 end;
   763 
   764 
   765 
   766 (*** derived cterm destructors ***)
   767 
   768 structure Dcterm: DCTERM =
   769 struct
   770 
   771 fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
   772 
   773 
   774 fun dest_comb t = Thm.dest_comb t
   775   handle CTERM (msg, _) => raise ERR "dest_comb" msg;
   776 
   777 fun dest_abs a t = Thm.dest_abs a t
   778   handle CTERM (msg, _) => raise ERR "dest_abs" msg;
   779 
   780 fun capply t u = Thm.apply t u
   781   handle CTERM (msg, _) => raise ERR "capply" msg;
   782 
   783 fun cabs a t = Thm.lambda a t
   784   handle CTERM (msg, _) => raise ERR "cabs" msg;
   785 
   786 
   787 (*---------------------------------------------------------------------------
   788  * Some simple constructor functions.
   789  *---------------------------------------------------------------------------*)
   790 
   791 val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const;
   792 
   793 fun mk_exists (r as (Bvar, Body)) =
   794   let val ty = Thm.typ_of_cterm Bvar
   795       val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
   796   in capply c (uncurry cabs r) end;
   797 
   798 
   799 local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   800 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
   801 end;
   802 
   803 local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   804 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
   805 end;
   806 
   807 
   808 (*---------------------------------------------------------------------------
   809  * The primitives.
   810  *---------------------------------------------------------------------------*)
   811 fun dest_const ctm =
   812    (case Thm.term_of ctm
   813       of Const(s,ty) => {Name = s, Ty = ty}
   814        | _ => raise ERR "dest_const" "not a constant");
   815 
   816 fun dest_var ctm =
   817    (case Thm.term_of ctm
   818       of Var((s,_),ty) => {Name=s, Ty=ty}
   819        | Free(s,ty)    => {Name=s, Ty=ty}
   820        |             _ => raise ERR "dest_var" "not a variable");
   821 
   822 
   823 (*---------------------------------------------------------------------------
   824  * Derived destructor operations.
   825  *---------------------------------------------------------------------------*)
   826 
   827 fun dest_monop expected tm =
   828  let
   829    fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
   830    val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
   831    val name = #Name (dest_const c handle Utils.ERR _ => err ());
   832  in if name = expected then N else err () end;
   833 
   834 fun dest_binop expected tm =
   835  let
   836    fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
   837    val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
   838  in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
   839 
   840 fun dest_binder expected tm =
   841   dest_abs NONE (dest_monop expected tm)
   842   handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
   843 
   844 
   845 val dest_neg    = dest_monop @{const_name Not}
   846 val dest_pair   = dest_binop @{const_name Pair}
   847 val dest_eq     = dest_binop @{const_name HOL.eq}
   848 val dest_imp    = dest_binop @{const_name HOL.implies}
   849 val dest_conj   = dest_binop @{const_name HOL.conj}
   850 val dest_disj   = dest_binop @{const_name HOL.disj}
   851 val dest_exists = dest_binder @{const_name Ex}
   852 val dest_forall = dest_binder @{const_name All}
   853 
   854 (* Query routines *)
   855 
   856 val is_eq     = can dest_eq
   857 val is_imp    = can dest_imp
   858 val is_forall = can dest_forall
   859 val is_exists = can dest_exists
   860 val is_neg    = can dest_neg
   861 val is_conj   = can dest_conj
   862 val is_disj   = can dest_disj
   863 val is_pair   = can dest_pair
   864 
   865 
   866 (*---------------------------------------------------------------------------
   867  * Iterated creation.
   868  *---------------------------------------------------------------------------*)
   869 val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
   870 
   871 (*---------------------------------------------------------------------------
   872  * Iterated destruction. (To the "right" in a term.)
   873  *---------------------------------------------------------------------------*)
   874 fun strip break tm =
   875   let fun dest (p as (ctm,accum)) =
   876         let val (M,N) = break ctm
   877         in dest (N, M::accum)
   878         end handle Utils.ERR _ => p
   879   in dest (tm,[])
   880   end;
   881 
   882 fun rev2swap (x,l) = (rev l, x);
   883 
   884 val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
   885 val strip_imp    = rev2swap o strip dest_imp
   886 val strip_abs    = rev2swap o strip (dest_abs NONE)
   887 val strip_forall = rev2swap o strip dest_forall
   888 val strip_exists = rev2swap o strip dest_exists
   889 
   890 val strip_disj   = rev o (op::) o strip dest_disj
   891 
   892 
   893 (*---------------------------------------------------------------------------
   894  * Going into and out of prop
   895  *---------------------------------------------------------------------------*)
   896 
   897 fun is_Trueprop ct =
   898   (case Thm.term_of ct of
   899     Const (@{const_name Trueprop}, _) $ _ => true
   900   | _ => false);
   901 
   902 fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply @{cterm Trueprop} ct;
   903 fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
   904 
   905 end;
   906 
   907 
   908 
   909 (*** emulation of HOL inference rules for TFL ***)
   910 
   911 structure Rules: RULES =
   912 struct
   913 
   914 fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
   915 
   916 
   917 fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm);
   918 fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
   919 
   920 fun dest_thm thm =
   921   (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm))
   922     handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
   923 
   924 
   925 (* Inference rules *)
   926 
   927 (*---------------------------------------------------------------------------
   928  *        Equality (one step)
   929  *---------------------------------------------------------------------------*)
   930 
   931 fun REFL tm = HOLogic.mk_obj_eq (Thm.reflexive tm)
   932   handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
   933 
   934 fun SYM thm = thm RS sym
   935   handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
   936 
   937 fun ALPHA thm ctm1 =
   938   let
   939     val ctm2 = Thm.cprop_of thm;
   940     val ctm2_eq = Thm.reflexive ctm2;
   941     val ctm1_eq = Thm.reflexive ctm1;
   942   in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
   943   handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
   944 
   945 fun rbeta th =
   946   (case Dcterm.strip_comb (cconcl th) of
   947     (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
   948   | _ => raise RULES_ERR "rbeta" "");
   949 
   950 
   951 (*----------------------------------------------------------------------------
   952  *        Implication and the assumption list
   953  *
   954  * Assumptions get stuck on the meta-language assumption list. Implications
   955  * are in the object language, so discharging an assumption "A" from theorem
   956  * "B" results in something that looks like "A --> B".
   957  *---------------------------------------------------------------------------*)
   958 
   959 fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
   960 
   961 
   962 (*---------------------------------------------------------------------------
   963  * Implication in TFL is -->. Meta-language implication (==>) is only used
   964  * in the implementation of some of the inference rules below.
   965  *---------------------------------------------------------------------------*)
   966 fun MP th1 th2 = th2 RS (th1 RS mp)
   967   handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
   968 
   969 (*forces the first argument to be a proposition if necessary*)
   970 fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
   971   handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
   972 
   973 fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm;
   974 
   975 
   976 fun FILTER_DISCH_ALL P thm =
   977  let fun check tm = P (Thm.term_of tm)
   978  in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
   979  end;
   980 
   981 fun UNDISCH thm =
   982    let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
   983    in Thm.implies_elim (thm RS mp) (ASSUME tm) end
   984    handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
   985      | THM _ => raise RULES_ERR "UNDISCH" "";
   986 
   987 fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
   988 
   989 fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
   990   handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
   991 
   992 
   993 (*----------------------------------------------------------------------------
   994  *        Conjunction
   995  *---------------------------------------------------------------------------*)
   996 
   997 fun CONJUNCT1 thm = thm RS conjunct1
   998   handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
   999 
  1000 fun CONJUNCT2 thm = thm RS conjunct2
  1001   handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
  1002 
  1003 fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
  1004 
  1005 fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
  1006   | LIST_CONJ [th] = th
  1007   | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
  1008       handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
  1009 
  1010 
  1011 (*----------------------------------------------------------------------------
  1012  *        Disjunction
  1013  *---------------------------------------------------------------------------*)
  1014 local
  1015   val prop = Thm.prop_of disjI1
  1016   val [_,Q] = Misc_Legacy.term_vars prop
  1017   val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
  1018 in
  1019 fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
  1020   handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
  1021 end;
  1022 
  1023 local
  1024   val prop = Thm.prop_of disjI2
  1025   val [P,_] = Misc_Legacy.term_vars prop
  1026   val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
  1027 in
  1028 fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
  1029   handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
  1030 end;
  1031 
  1032 
  1033 (*----------------------------------------------------------------------------
  1034  *
  1035  *                   A1 |- M1, ..., An |- Mn
  1036  *     ---------------------------------------------------
  1037  *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
  1038  *
  1039  *---------------------------------------------------------------------------*)
  1040 
  1041 
  1042 fun EVEN_ORS thms =
  1043   let fun blue ldisjs [] _ = []
  1044         | blue ldisjs (th::rst) rdisjs =
  1045             let val tail = tl rdisjs
  1046                 val rdisj_tl = Dcterm.list_mk_disj tail
  1047             in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
  1048                :: blue (ldisjs @ [cconcl th]) rst tail
  1049             end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
  1050    in blue [] thms (map cconcl thms) end;
  1051 
  1052 
  1053 (*----------------------------------------------------------------------------
  1054  *
  1055  *         A |- P \/ Q   B,P |- R    C,Q |- R
  1056  *     ---------------------------------------------------
  1057  *                     A U B U C |- R
  1058  *
  1059  *---------------------------------------------------------------------------*)
  1060 
  1061 fun DISJ_CASES th1 th2 th3 =
  1062   let
  1063     val c = Dcterm.drop_prop (cconcl th1);
  1064     val (disj1, disj2) = Dcterm.dest_disj c;
  1065     val th2' = DISCH disj1 th2;
  1066     val th3' = DISCH disj2 th3;
  1067   in
  1068     th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
  1069       handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
  1070   end;
  1071 
  1072 
  1073 (*-----------------------------------------------------------------------------
  1074  *
  1075  *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
  1076  *     ---------------------------------------------------
  1077  *                           |- M
  1078  *
  1079  * Note. The list of theorems may be all jumbled up, so we have to
  1080  * first organize it to align with the first argument (the disjunctive
  1081  * theorem).
  1082  *---------------------------------------------------------------------------*)
  1083 
  1084 fun organize eq =    (* a bit slow - analogous to insertion sort *)
  1085  let fun extract a alist =
  1086      let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
  1087            | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
  1088      in ex ([],alist)
  1089      end
  1090      fun place [] [] = []
  1091        | place (a::rst) alist =
  1092            let val (item,next) = extract a alist
  1093            in item::place rst next
  1094            end
  1095        | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
  1096  in place
  1097  end;
  1098 
  1099 fun DISJ_CASESL disjth thl =
  1100    let val c = cconcl disjth
  1101        fun eq th atm =
  1102         exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
  1103        val tml = Dcterm.strip_disj c
  1104        fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases"
  1105          | DL th [th1] = PROVE_HYP th th1
  1106          | DL th [th1,th2] = DISJ_CASES th th1 th2
  1107          | DL th (th1::rst) =
  1108             let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
  1109              in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
  1110    in DL disjth (organize eq tml thl)
  1111    end;
  1112 
  1113 
  1114 (*----------------------------------------------------------------------------
  1115  *        Universals
  1116  *---------------------------------------------------------------------------*)
  1117 local (* this is fragile *)
  1118   val prop = Thm.prop_of spec
  1119   val x = hd (tl (Misc_Legacy.term_vars prop))
  1120   val TV = dest_TVar (type_of x)
  1121   val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
  1122 in
  1123 fun SPEC tm thm =
  1124    let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
  1125    in thm RS (Thm.forall_elim tm gspec') end
  1126 end;
  1127 
  1128 fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
  1129 
  1130 val ISPEC = SPEC
  1131 val ISPECL = fold ISPEC;
  1132 
  1133 (* Not optimized! Too complicated. *)
  1134 local
  1135   val prop = Thm.prop_of allI
  1136   val [P] = Misc_Legacy.add_term_vars (prop, [])
  1137   fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
  1138   fun ctm_theta ctxt =
  1139     map (fn (i, (_, tm2)) =>
  1140       let val ctm2 = Thm.cterm_of ctxt tm2
  1141       in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
  1142   fun certify ctxt (ty_theta,tm_theta) =
  1143     (cty_theta ctxt (Vartab.dest ty_theta),
  1144      ctm_theta ctxt (Vartab.dest tm_theta))
  1145 in
  1146 fun GEN ctxt v th =
  1147    let val gth = Thm.forall_intr v th
  1148        val thy = Proof_Context.theory_of ctxt
  1149        val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
  1150        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
  1151        val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
  1152        val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
  1153        val thm = Thm.implies_elim allI2 gth
  1154        val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
  1155        val prop' = tp $ (A $ Abs(x,ty,M))
  1156    in ALPHA thm (Thm.cterm_of ctxt prop') end
  1157 end;
  1158 
  1159 fun GENL ctxt = fold_rev (GEN ctxt);
  1160 
  1161 fun GEN_ALL ctxt thm =
  1162   let
  1163     val prop = Thm.prop_of thm
  1164     val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
  1165   in GENL ctxt vlist thm end;
  1166 
  1167 
  1168 fun MATCH_MP th1 th2 =
  1169    if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
  1170    then MATCH_MP (th1 RS spec) th2
  1171    else MP th1 th2;
  1172 
  1173 
  1174 (*----------------------------------------------------------------------------
  1175  *        Existentials
  1176  *---------------------------------------------------------------------------*)
  1177 
  1178 
  1179 
  1180 (*---------------------------------------------------------------------------
  1181  * Existential elimination
  1182  *
  1183  *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
  1184  *      ------------------------------------     (variable v occurs nowhere)
  1185  *                A1 u A2 |- t'
  1186  *
  1187  *---------------------------------------------------------------------------*)
  1188 
  1189 fun CHOOSE ctxt (fvar, exth) fact =
  1190   let
  1191     val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
  1192     val redex = Dcterm.capply lam fvar
  1193     val t$u = Thm.term_of redex
  1194     val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
  1195   in
  1196     GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
  1197       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
  1198   end;
  1199 
  1200 fun EXISTS ctxt (template,witness) thm =
  1201   let val abstr = #2 (Dcterm.dest_comb template) in
  1202     thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
  1203       handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
  1204   end;
  1205 
  1206 (*----------------------------------------------------------------------------
  1207  *
  1208  *       A |- M[x_1,...,x_n]
  1209  *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
  1210  *       A |- ?y_1...y_n. M
  1211  *
  1212  *---------------------------------------------------------------------------*)
  1213 (* Could be improved, but needs "subst_free" for certified terms *)
  1214 
  1215 fun IT_EXISTS ctxt blist th =
  1216   let
  1217     val blist' = map (apply2 Thm.term_of) blist
  1218     fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
  1219   in
  1220     fold_rev (fn (b as (r1,r2)) => fn thm =>
  1221         EXISTS ctxt (ex r2 (subst_free [b]
  1222                    (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
  1223               thm)
  1224        blist' th
  1225   end;
  1226 
  1227 (*----------------------------------------------------------------------------
  1228  *        Rewriting
  1229  *---------------------------------------------------------------------------*)
  1230 
  1231 fun SUBS ctxt thl =
  1232   rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
  1233 
  1234 val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
  1235 
  1236 fun simpl_conv ctxt thl ctm =
  1237   HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm);
  1238 
  1239 
  1240 fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
  1241 
  1242 
  1243 
  1244 (*---------------------------------------------------------------------------
  1245  *                  TERMINATION CONDITION EXTRACTION
  1246  *---------------------------------------------------------------------------*)
  1247 
  1248 
  1249 (* Object language quantifier, i.e., "!" *)
  1250 fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
  1251 
  1252 
  1253 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
  1254 fun is_cong thm =
  1255   case (Thm.prop_of thm) of
  1256     (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
  1257       (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) =>
  1258         false
  1259   | _ => true;
  1260 
  1261 
  1262 fun dest_equal(Const (@{const_name Pure.eq},_) $
  1263                (Const (@{const_name Trueprop},_) $ lhs)
  1264                $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
  1265   | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
  1266   | dest_equal tm = USyntax.dest_eq tm;
  1267 
  1268 fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
  1269 
  1270 fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
  1271   | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
  1272 
  1273 val is_all = can (dest_all []);
  1274 
  1275 fun strip_all used fm =
  1276    if (is_all fm)
  1277    then let val ({Bvar, Body}, used') = dest_all used fm
  1278             val (bvs, core, used'') = strip_all used' Body
  1279         in ((Bvar::bvs), core, used'')
  1280         end
  1281    else ([], fm, used);
  1282 
  1283 fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
  1284      let val (L,core) = list_break_all body
  1285      in ((s,ty)::L, core)
  1286      end
  1287   | list_break_all tm = ([],tm);
  1288 
  1289 (*---------------------------------------------------------------------------
  1290  * Rename a term of the form
  1291  *
  1292  *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
  1293  *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
  1294  * to one of
  1295  *
  1296  *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
  1297  *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
  1298  *
  1299  * This prevents name problems in extraction, and helps the result to read
  1300  * better. There is a problem with varstructs, since they can introduce more
  1301  * than n variables, and some extra reasoning needs to be done.
  1302  *---------------------------------------------------------------------------*)
  1303 
  1304 fun get ([],_,L) = rev L
  1305   | get (ant::rst,n,L) =
  1306       case (list_break_all ant)
  1307         of ([],_) => get (rst, n+1,L)
  1308          | (_,body) =>
  1309             let val eq = Logic.strip_imp_concl body
  1310                 val (f,_) = USyntax.strip_comb (get_lhs eq)
  1311                 val (vstrl,_) = USyntax.strip_abs f
  1312                 val names  =
  1313                   Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
  1314             in get (rst, n+1, (names,n)::L) end
  1315             handle TERM _ => get (rst, n+1, L)
  1316               | Utils.ERR _ => get (rst, n+1, L);
  1317 
  1318 (* Note: Thm.rename_params_rule counts from 1, not 0 *)
  1319 fun rename thm =
  1320   let
  1321     val ants = Logic.strip_imp_prems (Thm.prop_of thm)
  1322     val news = get (ants,1,[])
  1323   in fold Thm.rename_params_rule news thm end;
  1324 
  1325 
  1326 (*---------------------------------------------------------------------------
  1327  * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
  1328  *---------------------------------------------------------------------------*)
  1329 
  1330 fun list_beta_conv tm =
  1331   let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
  1332       fun iter [] = Thm.reflexive tm
  1333         | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
  1334   in iter  end;
  1335 
  1336 
  1337 (*---------------------------------------------------------------------------
  1338  * Trace information for the rewriter
  1339  *---------------------------------------------------------------------------*)
  1340 val tracing = Unsynchronized.ref false;
  1341 
  1342 fun say s = if !tracing then writeln s else ();
  1343 
  1344 fun print_thms ctxt s L =
  1345   say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
  1346 
  1347 fun print_term ctxt s t =
  1348   say (cat_lines [s, Syntax.string_of_term ctxt t]);
  1349 
  1350 
  1351 (*---------------------------------------------------------------------------
  1352  * General abstraction handlers, should probably go in USyntax.
  1353  *---------------------------------------------------------------------------*)
  1354 fun mk_aabs (vstr, body) =
  1355   USyntax.mk_abs {Bvar = vstr, Body = body}
  1356   handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
  1357 
  1358 fun list_mk_aabs (vstrl,tm) =
  1359     fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
  1360 
  1361 fun dest_aabs used tm =
  1362    let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
  1363    in (Bvar, Body, used') end
  1364    handle Utils.ERR _ =>
  1365      let val {varstruct, body, used} = USyntax.dest_pabs used tm
  1366      in (varstruct, body, used) end;
  1367 
  1368 fun strip_aabs used tm =
  1369    let val (vstr, body, used') = dest_aabs used tm
  1370        val (bvs, core, used'') = strip_aabs used' body
  1371    in (vstr::bvs, core, used'') end
  1372    handle Utils.ERR _ => ([], tm, used);
  1373 
  1374 fun dest_combn tm 0 = (tm,[])
  1375   | dest_combn tm n =
  1376      let val {Rator,Rand} = USyntax.dest_comb tm
  1377          val (f,rands) = dest_combn Rator (n-1)
  1378      in (f,Rand::rands)
  1379      end;
  1380 
  1381 
  1382 
  1383 
  1384 local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
  1385       fun mk_fst tm =
  1386           let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
  1387           in  Const (@{const_name Product_Type.fst}, ty --> fty) $ tm  end
  1388       fun mk_snd tm =
  1389           let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
  1390           in  Const (@{const_name Product_Type.snd}, ty --> sty) $ tm  end
  1391 in
  1392 fun XFILL tych x vstruct =
  1393   let fun traverse p xocc L =
  1394         if (is_Free p)
  1395         then tych xocc::L
  1396         else let val (p1,p2) = dest_pair p
  1397              in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
  1398              end
  1399   in
  1400   traverse vstruct x []
  1401 end end;
  1402 
  1403 (*---------------------------------------------------------------------------
  1404  * Replace a free tuple (vstr) by a universally quantified variable (a).
  1405  * Note that the notion of "freeness" for a tuple is different than for a
  1406  * variable: if variables in the tuple also occur in any other place than
  1407  * an occurrences of the tuple, they aren't "free" (which is thus probably
  1408  *  the wrong word to use).
  1409  *---------------------------------------------------------------------------*)
  1410 
  1411 fun VSTRUCT_ELIM ctxt tych a vstr th =
  1412   let val L = USyntax.free_vars_lr vstr
  1413       val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
  1414       val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
  1415       val thm2 = forall_intr_list (map tych L) thm1
  1416       val thm3 = forall_elim_list (XFILL tych a vstr) thm2
  1417   in refl RS
  1418      rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
  1419   end;
  1420 
  1421 fun PGEN ctxt tych a vstr th =
  1422   let val a1 = tych a
  1423   in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
  1424 
  1425 
  1426 (*---------------------------------------------------------------------------
  1427  * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
  1428  *
  1429  *     (([x,y],N),vstr)
  1430  *---------------------------------------------------------------------------*)
  1431 fun dest_pbeta_redex used M n =
  1432   let val (f,args) = dest_combn M n
  1433       val _ = dest_aabs used f
  1434   in (strip_aabs used f,args)
  1435   end;
  1436 
  1437 fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
  1438 
  1439 fun dest_impl tm =
  1440   let val ants = Logic.strip_imp_prems tm
  1441       val eq = Logic.strip_imp_concl tm
  1442   in (ants,get_lhs eq)
  1443   end;
  1444 
  1445 fun restricted t = is_some (USyntax.find_term
  1446                             (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
  1447                             t)
  1448 
  1449 fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
  1450  let val globals = func::G
  1451      val ctxt0 = empty_simpset main_ctxt
  1452      val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
  1453      val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
  1454      val cut_lemma' = cut_lemma RS eq_reflection
  1455      fun prover used ctxt thm =
  1456      let fun cong_prover ctxt thm =
  1457          let val _ = say "cong_prover:"
  1458              val cntxt = Simplifier.prems_of ctxt
  1459              val _ = print_thms ctxt "cntxt:" cntxt
  1460              val _ = say "cong rule:"
  1461              val _ = say (Thm.string_of_thm ctxt thm)
  1462              (* Unquantified eliminate *)
  1463              fun uq_eliminate (thm,imp) =
  1464                  let val tych = Thm.cterm_of ctxt
  1465                      val _ = print_term ctxt "To eliminate:" imp
  1466                      val ants = map tych (Logic.strip_imp_prems imp)
  1467                      val eq = Logic.strip_imp_concl imp
  1468                      val lhs = tych(get_lhs eq)
  1469                      val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
  1470                      val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
  1471                        handle Utils.ERR _ => Thm.reflexive lhs
  1472                      val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
  1473                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
  1474                      val lhs_eeq_lhs2 = HOLogic.mk_obj_eq lhs_eq_lhs2
  1475                   in
  1476                   lhs_eeq_lhs2 COMP thm
  1477                   end
  1478              fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
  1479               let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
  1480                   val _ = forall (op aconv) (ListPair.zip (vlist, args))
  1481                     orelse error "assertion failed in CONTEXT_REWRITE_RULE"
  1482                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
  1483                                              imp_body
  1484                   val tych = Thm.cterm_of ctxt
  1485                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
  1486                   val eq1 = Logic.strip_imp_concl imp_body1
  1487                   val Q = get_lhs eq1
  1488                   val QeqQ1 = pbeta_reduce (tych Q)
  1489                   val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
  1490                   val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
  1491                   val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
  1492                                 handle Utils.ERR _ => Thm.reflexive Q1
  1493                   val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
  1494                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
  1495                   val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
  1496                   val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
  1497                   val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
  1498                                (HOLogic.mk_obj_eq Q2eeqQ3
  1499                                 RS (HOLogic.mk_obj_eq thA RS trans))
  1500                                 RS eq_reflection
  1501                   val impth = implies_intr_list ants1 QeeqQ3
  1502                   val impth1 = HOLogic.mk_obj_eq impth
  1503                   (* Need to abstract *)
  1504                   val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
  1505               in ant_th COMP thm
  1506               end
  1507              fun q_eliminate (thm, imp) =
  1508               let val (vlist, imp_body, used') = strip_all used imp
  1509                   val (ants,Q) = dest_impl imp_body
  1510               in if (pbeta_redex Q) (length vlist)
  1511                  then pq_eliminate (thm, vlist, imp_body, Q)
  1512                  else
  1513                  let val tych = Thm.cterm_of ctxt
  1514                      val ants1 = map tych ants
  1515                      val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
  1516                      val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
  1517                         (false,true,false) (prover used') ctxt' (tych Q)
  1518                       handle Utils.ERR _ => Thm.reflexive (tych Q)
  1519                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
  1520                      val lhs_eq_lhs2 = HOLogic.mk_obj_eq lhs_eeq_lhs2
  1521                      val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
  1522                  in
  1523                  ant_th COMP thm
  1524               end end
  1525 
  1526              fun eliminate thm =
  1527                case Thm.prop_of thm of
  1528                  Const(@{const_name Pure.imp},_) $ imp $ _ =>
  1529                    eliminate
  1530                     (if not(is_all imp)
  1531                      then uq_eliminate (thm, imp)
  1532                      else q_eliminate (thm, imp))
  1533                             (* Assume that the leading constant is ==,   *)
  1534                 | _ => thm  (* if it is not a ==>                        *)
  1535          in SOME(eliminate (rename thm)) end
  1536          handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
  1537 
  1538         fun restrict_prover ctxt thm =
  1539           let val _ = say "restrict_prover:"
  1540               val cntxt = rev (Simplifier.prems_of ctxt)
  1541               val _ = print_thms ctxt "cntxt:" cntxt
  1542               val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
  1543                 Thm.prop_of thm
  1544               fun genl tm = let val vlist = subtract (op aconv) globals
  1545                                            (Misc_Legacy.add_term_frees(tm,[]))
  1546                             in fold_rev Forall vlist tm
  1547                             end
  1548               (*--------------------------------------------------------------
  1549                * This actually isn't quite right, since it will think that
  1550                * not-fully applied occs. of "f" in the context mean that the
  1551                * current call is nested. The real solution is to pass in a
  1552                * term "f v1..vn" which is a pattern that any full application
  1553                * of "f" will match.
  1554                *-------------------------------------------------------------*)
  1555               val func_name = #1(dest_Const func)
  1556               fun is_func (Const (name,_)) = (name = func_name)
  1557                 | is_func _                = false
  1558               val rcontext = rev cntxt
  1559               val cncl = HOLogic.dest_Trueprop o Thm.prop_of
  1560               val antl = case rcontext of [] => []
  1561                          | _   => [USyntax.list_mk_conj(map cncl rcontext)]
  1562               val TC = genl(USyntax.list_mk_imp(antl, A))
  1563               val _ = print_term ctxt "func:" func
  1564               val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
  1565               val _ = tc_list := (TC :: !tc_list)
  1566               val nestedp = is_some (USyntax.find_term is_func TC)
  1567               val _ = if nestedp then say "nested" else say "not_nested"
  1568               val th' = if nestedp then raise RULES_ERR "solver" "nested function"
  1569                         else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
  1570                              in case rcontext of
  1571                                 [] => SPEC_ALL(ASSUME cTC)
  1572                                | _ => MP (SPEC_ALL (ASSUME cTC))
  1573                                          (LIST_CONJ rcontext)
  1574                              end
  1575               val th'' = th' RS thm
  1576           in SOME (th'')
  1577           end handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
  1578     in
  1579     (if (is_cong thm) then cong_prover else restrict_prover) ctxt thm
  1580     end
  1581     val ctm = Thm.cprop_of th
  1582     val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
  1583     val th1 =
  1584       Raw_Simplifier.rewrite_cterm (false, true, false)
  1585         (prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
  1586     val th2 = Thm.equal_elim th1 th
  1587  in
  1588  (th2, filter_out restricted (!tc_list))
  1589  end;
  1590 
  1591 
  1592 fun prove ctxt strict (t, tac) =
  1593   let
  1594     val ctxt' = Variable.auto_fixes t ctxt;
  1595   in
  1596     if strict
  1597     then Goal.prove ctxt' [] [] t (K tac)
  1598     else Goal.prove ctxt' [] [] t (K tac)
  1599       handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
  1600   end;
  1601 
  1602 end;
  1603 
  1604 
  1605 
  1606 (*** theory operations ***)
  1607 
  1608 structure Thry: THRY =
  1609 struct
  1610 
  1611 
  1612 fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
  1613 
  1614 
  1615 (*---------------------------------------------------------------------------
  1616  *    Matching
  1617  *---------------------------------------------------------------------------*)
  1618 
  1619 local
  1620 
  1621 fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
  1622 
  1623 in
  1624 
  1625 fun match_term thry pat ob =
  1626   let
  1627     val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
  1628     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
  1629   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
  1630   end;
  1631 
  1632 fun match_type thry pat ob =
  1633   map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
  1634 
  1635 end;
  1636 
  1637 
  1638 (*---------------------------------------------------------------------------
  1639  * Typing
  1640  *---------------------------------------------------------------------------*)
  1641 
  1642 fun typecheck thy t =
  1643   Thm.global_cterm_of thy t
  1644     handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
  1645       | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
  1646 
  1647 
  1648 (*---------------------------------------------------------------------------
  1649  * Get information about datatypes
  1650  *---------------------------------------------------------------------------*)
  1651 
  1652 fun match_info thy dtco =
  1653   case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
  1654          BNF_LFP_Compat.get_constrs thy dtco) of
  1655       (SOME {case_name, ... }, SOME constructors) =>
  1656         SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
  1657     | _ => NONE;
  1658 
  1659 fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
  1660         NONE => NONE
  1661       | SOME {nchotomy, ...} =>
  1662           SOME {nchotomy = nchotomy,
  1663                 constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
  1664 
  1665 fun extract_info thy =
  1666  let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
  1667  in {case_congs = map (mk_meta_eq o #case_cong) infos,
  1668      case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
  1669  end;
  1670 
  1671 
  1672 end;
  1673 
  1674 
  1675 
  1676 (*** first part of main module ***)
  1677 
  1678 structure Prim: PRIM =
  1679 struct
  1680 
  1681 val trace = Unsynchronized.ref false;
  1682 
  1683 
  1684 fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
  1685 
  1686 val concl = #2 o Rules.dest_thm;
  1687 
  1688 val list_mk_type = Utils.end_itlist (curry (op -->));
  1689 
  1690 fun front_last [] = raise TFL_ERR "front_last" "empty list"
  1691   | front_last [x] = ([],x)
  1692   | front_last (h::t) =
  1693      let val (pref,x) = front_last t
  1694      in
  1695         (h::pref,x)
  1696      end;
  1697 
  1698 
  1699 (*---------------------------------------------------------------------------
  1700  * The next function is common to pattern-match translation and
  1701  * proof of completeness of cases for the induction theorem.
  1702  *
  1703  * The curried function "gvvariant" returns a function to generate distinct
  1704  * variables that are guaranteed not to be in names.  The names of
  1705  * the variables go u, v, ..., z, aa, ..., az, ...  The returned
  1706  * function contains embedded refs!
  1707  *---------------------------------------------------------------------------*)
  1708 fun gvvariant names =
  1709   let val slist = Unsynchronized.ref names
  1710       val vname = Unsynchronized.ref "u"
  1711       fun new() =
  1712          if member (op =) (!slist) (!vname)
  1713          then (vname := Symbol.bump_string (!vname);  new())
  1714          else (slist := !vname :: !slist;  !vname)
  1715   in
  1716   fn ty => Free(new(), ty)
  1717   end;
  1718 
  1719 
  1720 (*---------------------------------------------------------------------------
  1721  * Used in induction theorem production. This is the simple case of
  1722  * partitioning up pattern rows by the leading constructor.
  1723  *---------------------------------------------------------------------------*)
  1724 fun ipartition gv (constructors,rows) =
  1725   let fun pfail s = raise TFL_ERR "partition.part" s
  1726       fun part {constrs = [],   rows = [],   A} = rev A
  1727         | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
  1728         | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
  1729         | part {constrs = c::crst, rows,     A} =
  1730           let val (c, T) = dest_Const c
  1731               val L = binder_types T
  1732               val (in_group, not_in_group) =
  1733                fold_rev (fn (row as (p::rst, rhs)) =>
  1734                          fn (in_group,not_in_group) =>
  1735                   let val (pc,args) = USyntax.strip_comb p
  1736                   in if (#1(dest_Const pc) = c)
  1737                      then ((args@rst, rhs)::in_group, not_in_group)
  1738                      else (in_group, row::not_in_group)
  1739                   end)      rows ([],[])
  1740               val col_types = Utils.take type_of (length L, #1(hd in_group))
  1741           in
  1742           part{constrs = crst, rows = not_in_group,
  1743                A = {constructor = c,
  1744                     new_formals = map gv col_types,
  1745                     group = in_group}::A}
  1746           end
  1747   in part{constrs = constructors, rows = rows, A = []}
  1748   end;
  1749 
  1750 
  1751 
  1752 (*---------------------------------------------------------------------------
  1753  * Each pattern carries with it a tag (i,b) where
  1754  * i is the clause it came from and
  1755  * b=true indicates that clause was given by the user
  1756  * (or is an instantiation of a user supplied pattern)
  1757  * b=false --> i = ~1
  1758  *---------------------------------------------------------------------------*)
  1759 
  1760 type pattern = term * (int * bool)
  1761 
  1762 fun pattern_map f (tm,x) = (f tm, x);
  1763 
  1764 fun pattern_subst theta = pattern_map (subst_free theta);
  1765 
  1766 val pat_of = fst;
  1767 fun row_of_pat x = fst (snd x);
  1768 fun given x = snd (snd x);
  1769 
  1770 (*---------------------------------------------------------------------------
  1771  * Produce an instance of a constructor, plus genvars for its arguments.
  1772  *---------------------------------------------------------------------------*)
  1773 fun fresh_constr ty_match colty gv c =
  1774   let val (_,Ty) = dest_Const c
  1775       val L = binder_types Ty
  1776       and ty = body_type Ty
  1777       val ty_theta = ty_match ty colty
  1778       val c' = USyntax.inst ty_theta c
  1779       val gvars = map (USyntax.inst ty_theta o gv) L
  1780   in (c', gvars)
  1781   end;
  1782 
  1783 
  1784 (*---------------------------------------------------------------------------
  1785  * Goes through a list of rows and picks out the ones beginning with a
  1786  * pattern with constructor = name.
  1787  *---------------------------------------------------------------------------*)
  1788 fun mk_group name rows =
  1789   fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
  1790             fn (in_group,not_in_group) =>
  1791                let val (pc,args) = USyntax.strip_comb p
  1792                in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
  1793                   then (((prfx,args@rst), rhs)::in_group, not_in_group)
  1794                   else (in_group, row::not_in_group) end)
  1795       rows ([],[]);
  1796 
  1797 (*---------------------------------------------------------------------------
  1798  * Partition the rows. Not efficient: we should use hashing.
  1799  *---------------------------------------------------------------------------*)
  1800 fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
  1801   | partition gv ty_match
  1802               (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
  1803 let val fresh = fresh_constr ty_match colty gv
  1804      fun part {constrs = [],      rows, A} = rev A
  1805        | part {constrs = c::crst, rows, A} =
  1806          let val (c',gvars) = fresh c
  1807              val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
  1808              val in_group' =
  1809                  if (null in_group)  (* Constructor not given *)
  1810                  then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
  1811                  else in_group
  1812          in
  1813          part{constrs = crst,
  1814               rows = not_in_group,
  1815               A = {constructor = c',
  1816                    new_formals = gvars,
  1817                    group = in_group'}::A}
  1818          end
  1819 in part{constrs=constructors, rows=rows, A=[]}
  1820 end;
  1821 
  1822 (*---------------------------------------------------------------------------
  1823  * Misc. routines used in mk_case
  1824  *---------------------------------------------------------------------------*)
  1825 
  1826 fun mk_pat (c,l) =
  1827   let val L = length (binder_types (type_of c))
  1828       fun build (prfx,tag,plist) =
  1829           let val (args, plist') = chop L plist
  1830           in (prfx,tag,list_comb(c,args)::plist') end
  1831   in map build l end;
  1832 
  1833 fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
  1834   | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
  1835 
  1836 fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
  1837   | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
  1838 
  1839 
  1840 (*----------------------------------------------------------------------------
  1841  * Translation of pattern terms into nested case expressions.
  1842  *
  1843  * This performs the translation and also builds the full set of patterns.
  1844  * Thus it supports the construction of induction theorems even when an
  1845  * incomplete set of patterns is given.
  1846  *---------------------------------------------------------------------------*)
  1847 
  1848 fun mk_case ty_info ty_match usednames range_ty =
  1849  let
  1850  fun mk_case_fail s = raise TFL_ERR "mk_case" s
  1851  val fresh_var = gvvariant usednames
  1852  val divide = partition fresh_var ty_match
  1853  fun expand _ ty ((_,[]), _) = mk_case_fail"expand_var_row"
  1854    | expand constructors ty (row as ((prfx, p::rst), rhs)) =
  1855        if (is_Free p)
  1856        then let val fresh = fresh_constr ty_match ty fresh_var
  1857                 fun expnd (c,gvs) =
  1858                   let val capp = list_comb(c,gvs)
  1859                   in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
  1860                   end
  1861             in map expnd (map fresh constructors)  end
  1862        else [row]
  1863  fun mk{rows=[],...} = mk_case_fail"no rows"
  1864    | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
  1865         ([(prfx,tag,[])], tm)
  1866    | mk{path=[], rows = _::_} = mk_case_fail"blunder"
  1867    | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
  1868         mk{path = path,
  1869            rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
  1870    | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
  1871      let val (pat_rectangle,rights) = ListPair.unzip rows
  1872          val col0 = map(hd o #2) pat_rectangle
  1873      in
  1874      if (forall is_Free col0)
  1875      then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
  1876                                 (ListPair.zip (col0, rights))
  1877               val pat_rectangle' = map v_to_prfx pat_rectangle
  1878               val (pref_patl,tm) = mk{path = rstp,
  1879                                       rows = ListPair.zip (pat_rectangle',
  1880                                                            rights')}
  1881           in (map v_to_pats pref_patl, tm)
  1882           end
  1883      else
  1884      let val pty as Type (ty_name,_) = type_of p
  1885      in
  1886      case (ty_info ty_name)
  1887      of NONE => mk_case_fail("Not a known datatype: "^ty_name)
  1888       | SOME{case_const,constructors} =>
  1889         let
  1890             val case_const_name = #1(dest_Const case_const)
  1891             val nrows = maps (expand constructors pty) rows
  1892             val subproblems = divide(constructors, pty, range_ty, nrows)
  1893             val groups      = map #group subproblems
  1894             and new_formals = map #new_formals subproblems
  1895             and constructors' = map #constructor subproblems
  1896             val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
  1897                            (ListPair.zip (new_formals, groups))
  1898             val rec_calls = map mk news
  1899             val (pat_rect,dtrees) = ListPair.unzip rec_calls
  1900             val case_functions = map USyntax.list_mk_abs
  1901                                   (ListPair.zip (new_formals, dtrees))
  1902             val types = map type_of (case_functions@[u]) @ [range_ty]
  1903             val case_const' = Const(case_const_name, list_mk_type types)
  1904             val tree = list_comb(case_const', case_functions@[u])
  1905             val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
  1906         in (pat_rect1,tree)
  1907         end
  1908      end end
  1909  in mk
  1910  end;
  1911 
  1912 
  1913 (* Repeated variable occurrences in a pattern are not allowed. *)
  1914 fun FV_multiset tm =
  1915    case (USyntax.dest_term tm)
  1916      of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
  1917       | USyntax.CONST _ => []
  1918       | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
  1919       | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
  1920 
  1921 fun no_repeat_vars thy pat =
  1922  let fun check [] = true
  1923        | check (v::rst) =
  1924          if member (op aconv) rst v then
  1925             raise TFL_ERR "no_repeat_vars"
  1926                           (quote (#1 (dest_Free v)) ^
  1927                           " occurs repeatedly in the pattern " ^
  1928                           quote (Syntax.string_of_term_global thy pat))
  1929          else check rst
  1930  in check (FV_multiset pat)
  1931  end;
  1932 
  1933 fun dest_atom (Free p) = p
  1934   | dest_atom (Const p) = p
  1935   | dest_atom  _ = raise TFL_ERR "dest_atom" "function name not an identifier";
  1936 
  1937 fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
  1938 
  1939 local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
  1940       fun single [_$_] =
  1941               mk_functional_err "recdef does not allow currying"
  1942         | single [f] = f
  1943         | single fs  =
  1944               (*multiple function names?*)
  1945               if length (distinct same_name fs) < length fs
  1946               then mk_functional_err
  1947                    "The function being declared appears with multiple types"
  1948               else mk_functional_err
  1949                    (string_of_int (length fs) ^
  1950                     " distinct function names being declared")
  1951 in
  1952 fun mk_functional thy clauses =
  1953  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
  1954                    handle TERM _ => raise TFL_ERR "mk_functional"
  1955                         "recursion equations must use the = relation")
  1956      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
  1957      val atom = single (distinct (op aconv) funcs)
  1958      val (fname,ftype) = dest_atom atom
  1959      val _ = map (no_repeat_vars thy) pats
  1960      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
  1961                               map_index (fn (i, t) => (t,(i,true))) R)
  1962      val names = List.foldr Misc_Legacy.add_term_names [] R
  1963      val atype = type_of(hd pats)
  1964      and aname = singleton (Name.variant_list names) "a"
  1965      val a = Free(aname,atype)
  1966      val ty_info = Thry.match_info thy
  1967      val ty_match = Thry.match_type thy
  1968      val range_ty = type_of (hd R)
  1969      val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
  1970                                     {path=[a], rows=rows}
  1971      val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
  1972           handle Match => mk_functional_err "error in pattern-match translation"
  1973      val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
  1974      val finals = map row_of_pat patts2
  1975      val originals = map (row_of_pat o #2) rows
  1976      val _ = case (subtract (op =) finals originals)
  1977              of [] => ()
  1978           | L => mk_functional_err
  1979  ("The following clauses are redundant (covered by preceding clauses): " ^
  1980                    commas (map (fn i => string_of_int (i + 1)) L))
  1981  in {functional = Abs(Long_Name.base_name fname, ftype,
  1982                       abstract_over (atom, absfree (aname,atype) case_tm)),
  1983      pats = patts2}
  1984 end end;
  1985 
  1986 
  1987 (*----------------------------------------------------------------------------
  1988  *
  1989  *                    PRINCIPLES OF DEFINITION
  1990  *
  1991  *---------------------------------------------------------------------------*)
  1992 
  1993 
  1994 (*For Isabelle, the lhs of a definition must be a constant.*)
  1995 fun const_def sign (c, Ty, rhs) =
  1996   singleton (Syntax.check_terms (Proof_Context.init_global sign))
  1997     (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
  1998 
  1999 (*Make all TVars available for instantiation by adding a ? to the front*)
  2000 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
  2001   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
  2002   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
  2003 
  2004 local
  2005   val f_eq_wfrec_R_M =
  2006     #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec}))))
  2007   val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
  2008   val _ = dest_Free f
  2009   val (wfrec,_) = USyntax.strip_comb rhs
  2010 in
  2011 
  2012 fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
  2013   let
  2014     val def_name = Thm.def_name (Long_Name.base_name fid)
  2015     val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
  2016     val def_term = const_def thy (fid, Ty, wfrec_R_M)
  2017     val ([def], thy') =
  2018       Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
  2019   in (def, thy') end;
  2020 
  2021 end;
  2022 
  2023 
  2024 
  2025 (*---------------------------------------------------------------------------
  2026  * This structure keeps track of congruence rules that aren't derived
  2027  * from a datatype definition.
  2028  *---------------------------------------------------------------------------*)
  2029 fun extraction_thms thy =
  2030  let val {case_rewrites,case_congs} = Thry.extract_info thy
  2031  in (case_rewrites, case_congs)
  2032  end;
  2033 
  2034 
  2035 (*---------------------------------------------------------------------------
  2036  * Pair patterns with termination conditions. The full list of patterns for
  2037  * a definition is merged with the TCs arising from the user-given clauses.
  2038  * There can be fewer clauses than the full list, if the user omitted some
  2039  * cases. This routine is used to prepare input for mk_induction.
  2040  *---------------------------------------------------------------------------*)
  2041 fun merge full_pats TCs =
  2042 let fun insert (p,TCs) =
  2043       let fun insrt ((x as (h,[]))::rst) =
  2044                  if (p aconv h) then (p,TCs)::rst else x::insrt rst
  2045             | insrt (x::rst) = x::insrt rst
  2046             | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
  2047       in insrt end
  2048     fun pass ([],ptcl_final) = ptcl_final
  2049       | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
  2050 in
  2051   pass (TCs, map (fn p => (p,[])) full_pats)
  2052 end;
  2053 
  2054 
  2055 fun givens pats = map pat_of (filter given pats);
  2056 
  2057 fun post_definition ctxt meta_tflCongs (def, pats) =
  2058  let val thy = Proof_Context.theory_of ctxt
  2059      val tych = Thry.typecheck thy
  2060      val f = #lhs(USyntax.dest_eq(concl def))
  2061      val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def
  2062      val pats' = filter given pats
  2063      val given_pats = map pat_of pats'
  2064      val rows = map row_of_pat pats'
  2065      val WFR = #ant(USyntax.dest_imp(concl corollary))
  2066      val R = #Rand(USyntax.dest_comb WFR)
  2067      val corollary' = Rules.UNDISCH corollary  (* put WF R on assums *)
  2068      val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
  2069      val (case_rewrites,context_congs) = extraction_thms thy
  2070      (*case_ss causes minimal simplification: bodies of case expressions are
  2071        not simplified. Otherwise large examples (Red-Black trees) are too
  2072        slow.*)
  2073      val case_simpset =
  2074        put_simpset HOL_basic_ss ctxt
  2075           addsimps case_rewrites
  2076           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
  2077               (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
  2078      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
  2079      val extract =
  2080       Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
  2081      val (rules, TCs) = ListPair.unzip (map extract corollaries')
  2082      val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules
  2083      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
  2084      val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
  2085  in
  2086  {rules = rules1,
  2087   rows = rows,
  2088   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
  2089   TCs = TCs}
  2090  end;
  2091 
  2092 
  2093 (*----------------------------------------------------------------------------
  2094  *
  2095  *                           INDUCTION THEOREM
  2096  *
  2097  *---------------------------------------------------------------------------*)
  2098 
  2099 
  2100 (*------------------------  Miscellaneous function  --------------------------
  2101  *
  2102  *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
  2103  *     -----------------------------------------------------------
  2104  *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
  2105  *                        ...
  2106  *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
  2107  *
  2108  * This function is totally ad hoc. Used in the production of the induction
  2109  * theorem. The nchotomy theorem can have clauses that look like
  2110  *
  2111  *     ?v1..vn. z = C vn..v1
  2112  *
  2113  * in which the order of quantification is not the order of occurrence of the
  2114  * quantified variables as arguments to C. Since we have no control over this
  2115  * aspect of the nchotomy theorem, we make the correspondence explicit by
  2116  * pairing the incoming new variable with the term it gets beta-reduced into.
  2117  *---------------------------------------------------------------------------*)
  2118 
  2119 fun alpha_ex_unroll (xlist, tm) =
  2120   let val (qvars,body) = USyntax.strip_exists tm
  2121       val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
  2122       val plist = ListPair.zip (vlist, xlist)
  2123       val args = map (the o AList.lookup (op aconv) plist) qvars
  2124                    handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
  2125       fun build ex      []   = []
  2126         | build (_$rex) (v::rst) =
  2127            let val ex1 = Term.betapply(rex, v)
  2128            in  ex1 :: build ex1 rst
  2129            end
  2130      val (nex::exl) = rev (tm::build tm args)
  2131   in
  2132   (nex, ListPair.zip (args, rev exl))
  2133   end;
  2134 
  2135 
  2136 
  2137 (*----------------------------------------------------------------------------
  2138  *
  2139  *             PROVING COMPLETENESS OF PATTERNS
  2140  *
  2141  *---------------------------------------------------------------------------*)
  2142 
  2143 fun mk_case ctxt ty_info usednames =
  2144  let
  2145  val thy = Proof_Context.theory_of ctxt
  2146  val divide = ipartition (gvvariant usednames)
  2147  val tych = Thry.typecheck thy
  2148  fun tych_binding(x,y) = (tych x, tych y)
  2149  fun fail s = raise TFL_ERR "mk_case" s
  2150  fun mk{rows=[],...} = fail"no rows"
  2151    | mk{path=[], rows = [([], (thm, bindings))]} =
  2152                          Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
  2153    | mk{path = u::rstp, rows as (p::_, _)::_} =
  2154      let val (pat_rectangle,rights) = ListPair.unzip rows
  2155          val col0 = map hd pat_rectangle
  2156          val pat_rectangle' = map tl pat_rectangle
  2157      in
  2158      if (forall is_Free col0) (* column 0 is all variables *)
  2159      then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
  2160                                 (ListPair.zip (rights, col0))
  2161           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
  2162           end
  2163      else                     (* column 0 is all constructors *)
  2164      let val Type (ty_name,_) = type_of p
  2165      in
  2166      case (ty_info ty_name)
  2167      of NONE => fail("Not a known datatype: "^ty_name)
  2168       | SOME{constructors,nchotomy} =>
  2169         let val thm' = Rules.ISPEC (tych u) nchotomy
  2170             val disjuncts = USyntax.strip_disj (concl thm')
  2171             val subproblems = divide(constructors, rows)
  2172             val groups      = map #group subproblems
  2173             and new_formals = map #new_formals subproblems
  2174             val existentials = ListPair.map alpha_ex_unroll
  2175                                    (new_formals, disjuncts)
  2176             val constraints = map #1 existentials
  2177             val vexl = map #2 existentials
  2178             fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
  2179             val news = map (fn (nf,rows,c) => {path = nf@rstp,
  2180                                                rows = map (expnd c) rows})
  2181                            (Utils.zip3 new_formals groups constraints)
  2182             val recursive_thms = map mk news
  2183             val build_exists = Library.foldr
  2184                                 (fn((x,t), th) =>
  2185                                  Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
  2186             val thms' = ListPair.map build_exists (vexl, recursive_thms)
  2187             val same_concls = Rules.EVEN_ORS thms'
  2188         in Rules.DISJ_CASESL thm' same_concls
  2189         end
  2190      end end
  2191  in mk
  2192  end;
  2193 
  2194 
  2195 fun complete_cases ctxt =
  2196  let val thy = Proof_Context.theory_of ctxt
  2197      val tych = Thry.typecheck thy
  2198      val ty_info = Thry.induct_info thy
  2199  in fn pats =>
  2200  let val names = List.foldr Misc_Legacy.add_term_names [] pats
  2201      val T = type_of (hd pats)
  2202      val aname = singleton (Name.variant_list names) "a"
  2203      val vname = singleton (Name.variant_list (aname::names)) "v"
  2204      val a = Free (aname, T)
  2205      val v = Free (vname, T)
  2206      val a_eq_v = HOLogic.mk_eq(a,v)
  2207      val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
  2208                            (Rules.REFL (tych a))
  2209      val th0 = Rules.ASSUME (tych a_eq_v)
  2210      val rows = map (fn x => ([x], (th0,[]))) pats
  2211  in
  2212  Rules.GEN ctxt (tych a)
  2213        (Rules.RIGHT_ASSOC ctxt
  2214           (Rules.CHOOSE ctxt (tych v, ex_th0)
  2215                 (mk_case ctxt ty_info (vname::aname::names)
  2216                  {path=[v], rows=rows})))
  2217  end end;
  2218 
  2219 
  2220 (*---------------------------------------------------------------------------
  2221  * Constructing induction hypotheses: one for each recursive call.
  2222  *
  2223  * Note. R will never occur as a variable in the ind_clause, because
  2224  * to do so, it would have to be from a nested definition, and we don't
  2225  * allow nested defns to have R variable.
  2226  *
  2227  * Note. When the context is empty, there can be no local variables.
  2228  *---------------------------------------------------------------------------*)
  2229 
  2230 local infix 5 ==>
  2231       fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
  2232 in
  2233 fun build_ih f (P,SV) (pat,TCs) =
  2234  let val pat_vars = USyntax.free_vars_lr pat
  2235      val globals = pat_vars@SV
  2236      fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
  2237      fun dest_TC tm =
  2238          let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
  2239              val (R,y,_) = USyntax.dest_relation R_y_pat
  2240              val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
  2241          in case cntxt
  2242               of [] => (P_y, (tm,[]))
  2243                | _  => let
  2244                     val imp = USyntax.list_mk_conj cntxt ==> P_y
  2245                     val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
  2246                     val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
  2247                     in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
  2248          end
  2249  in case TCs
  2250     of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
  2251      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
  2252                  val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
  2253              in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
  2254              end
  2255  end
  2256 end;
  2257 
  2258 (*---------------------------------------------------------------------------
  2259  * This function makes good on the promise made in "build_ih".
  2260  *
  2261  * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",
  2262  *           TCs = TC_1[pat] ... TC_n[pat]
  2263  *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
  2264  *---------------------------------------------------------------------------*)
  2265 fun prove_case ctxt f (tm,TCs_locals,thm) =
  2266  let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
  2267      val antc = tych(#ant(USyntax.dest_imp tm))
  2268      val thm' = Rules.SPEC_ALL thm
  2269      fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
  2270      fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
  2271      fun mk_ih ((TC,locals),th2,nested) =
  2272          Rules.GENL ctxt (map tych locals)
  2273             (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
  2274              else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
  2275              else Rules.MP th2 TC)
  2276  in
  2277  Rules.DISCH antc
  2278  (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
  2279   then let val th1 = Rules.ASSUME antc
  2280            val TCs = map #1 TCs_locals
  2281            val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
  2282                             #2 o USyntax.strip_forall) TCs
  2283            val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
  2284                             TCs_locals
  2285            val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
  2286            val nlist = map nested TCs
  2287            val triples = Utils.zip3 TClist th2list nlist
  2288            val Pylist = map mk_ih triples
  2289        in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
  2290   else thm')
  2291  end;
  2292 
  2293 
  2294 (*---------------------------------------------------------------------------
  2295  *
  2296  *         x = (v1,...,vn)  |- M[x]
  2297  *    ---------------------------------------------
  2298  *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
  2299  *
  2300  *---------------------------------------------------------------------------*)
  2301 fun LEFT_ABS_VSTRUCT ctxt tych thm =
  2302   let fun CHOOSER v (tm,thm) =
  2303         let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
  2304         in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
  2305         end
  2306       val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
  2307       val {lhs,rhs} = USyntax.dest_eq veq
  2308       val L = USyntax.free_vars_lr rhs
  2309   in  #2 (fold_rev CHOOSER L (veq,thm))  end;
  2310 
  2311 
  2312 (*----------------------------------------------------------------------------
  2313  * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
  2314  *
  2315  * Instantiates tfl_wf_induct, getting Sinduct and then tries to prove
  2316  * recursion induction (Rinduct) by proving the antecedent of Sinduct from
  2317  * the antecedent of Rinduct.
  2318  *---------------------------------------------------------------------------*)
  2319 fun mk_induction ctxt {fconst, R, SV, pat_TCs_list} =
  2320 let
  2321     val thy = Proof_Context.theory_of ctxt
  2322     val tych = Thry.typecheck thy
  2323     val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct})
  2324     val (pats,TCsl) = ListPair.unzip pat_TCs_list
  2325     val case_thm = complete_cases ctxt pats
  2326     val domain = (type_of o hd) pats
  2327     val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
  2328                               [] (pats::TCsl))) "P"
  2329     val P = Free(Pname, domain --> HOLogic.boolT)
  2330     val Sinduct = Rules.SPEC (tych P) Sinduction
  2331     val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
  2332     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
  2333     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
  2334     val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
  2335     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
  2336     val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
  2337     val proved_cases = map (prove_case ctxt fconst) tasks
  2338     val v =
  2339       Free (singleton
  2340         (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
  2341           domain)
  2342     val vtyped = tych v
  2343     val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
  2344     val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
  2345                           (substs, proved_cases)
  2346     val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
  2347     val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
  2348     val dc = Rules.MP Sinduct dant
  2349     val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
  2350     val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
  2351     val dc' = fold_rev (Rules.GEN ctxt o tych) vars
  2352                        (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
  2353 in
  2354    Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
  2355 end
  2356 handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
  2357 
  2358 
  2359 
  2360 (*---------------------------------------------------------------------------
  2361  *
  2362  *                        POST PROCESSING
  2363  *
  2364  *---------------------------------------------------------------------------*)
  2365 
  2366 
  2367 fun simplify_induction thy hth ind =
  2368   let val tych = Thry.typecheck thy
  2369       val (asl,_) = Rules.dest_thm ind
  2370       val (_,tc_eq_tc') = Rules.dest_thm hth
  2371       val tc = USyntax.lhs tc_eq_tc'
  2372       fun loop [] = ind
  2373         | loop (asm::rst) =
  2374           if (can (Thry.match_term thy asm) tc)
  2375           then Rules.UNDISCH
  2376                  (Rules.MATCH_MP
  2377                      (Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind))
  2378                      hth)
  2379          else loop rst
  2380   in loop asl
  2381 end;
  2382 
  2383 
  2384 (*---------------------------------------------------------------------------
  2385  * The termination condition is an antecedent to the rule, and an
  2386  * assumption to the theorem.
  2387  *---------------------------------------------------------------------------*)
  2388 fun elim_tc tcthm (rule,induction) =
  2389    (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
  2390 
  2391 
  2392 fun trace_thms ctxt s L =
  2393   if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L))
  2394   else ();
  2395 
  2396 fun trace_cterm ctxt s ct =
  2397   if !trace then
  2398     writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
  2399   else ();
  2400 
  2401 
  2402 fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
  2403   let
  2404     val thy = Proof_Context.theory_of ctxt;
  2405     val tych = Thry.typecheck thy;
  2406 
  2407    (*---------------------------------------------------------------------
  2408     * Attempt to eliminate WF condition. It's the only assumption of rules
  2409     *---------------------------------------------------------------------*)
  2410     val (rules1,induction1)  =
  2411        let val thm =
  2412         Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
  2413        in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
  2414        end handle Utils.ERR _ => (rules,induction);
  2415 
  2416    (*----------------------------------------------------------------------
  2417     * The termination condition (tc) is simplified to |- tc = tc' (there
  2418     * might not be a change!) and then 3 attempts are made:
  2419     *
  2420     *   1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise,
  2421     *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
  2422     *   3. replace tc by tc' in both the rules and the induction theorem.
  2423     *---------------------------------------------------------------------*)
  2424 
  2425    fun simplify_tc tc (r,ind) =
  2426        let val tc1 = tych tc
  2427            val _ = trace_cterm ctxt "TC before simplification: " tc1
  2428            val tc_eq = simplifier tc1
  2429            val _ = trace_thms ctxt "result: " [tc_eq]
  2430        in
  2431        elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
  2432        handle Utils.ERR _ =>
  2433         (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
  2434                   (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
  2435                            terminator)))
  2436                  (r,ind)
  2437          handle Utils.ERR _ =>
  2438           (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
  2439            simplify_induction thy tc_eq ind))
  2440        end
  2441 
  2442    (*----------------------------------------------------------------------
  2443     * Nested termination conditions are harder to get at, since they are
  2444     * left embedded in the body of the function (and in induction
  2445     * theorem hypotheses). Our "solution" is to simplify them, and try to
  2446     * prove termination, but leave the application of the resulting theorem
  2447     * to a higher level. So things go much as in "simplify_tc": the
  2448     * termination condition (tc) is simplified to |- tc = tc' (there might
  2449     * not be a change) and then 2 attempts are made:
  2450     *
  2451     *   1. if |- tc = T, then return |- tc; otherwise,
  2452     *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
  2453     *   3. return |- tc = tc'
  2454     *---------------------------------------------------------------------*)
  2455    fun simplify_nested_tc tc =
  2456       let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
  2457       in
  2458       Rules.GEN_ALL ctxt
  2459        (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
  2460         handle Utils.ERR _ =>
  2461           (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
  2462                       (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
  2463                                terminator))
  2464             handle Utils.ERR _ => tc_eq))
  2465       end
  2466 
  2467    (*-------------------------------------------------------------------
  2468     * Attempt to simplify the termination conditions in each rule and
  2469     * in the induction theorem.
  2470     *-------------------------------------------------------------------*)
  2471    fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
  2472    fun loop ([],extras,R,ind) = (rev R, ind, extras)
  2473      | loop ((r,ftcs)::rst, nthms, R, ind) =
  2474         let val tcs = #1(strip_imp (concl r))
  2475             val extra_tcs = subtract (op aconv) tcs ftcs
  2476             val extra_tc_thms = map simplify_nested_tc extra_tcs
  2477             val (r1,ind1) = fold simplify_tc tcs (r,ind)
  2478             val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
  2479         in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
  2480         end
  2481    val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
  2482    val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
  2483 in
  2484   {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
  2485 end;
  2486 
  2487 end;
  2488 
  2489 
  2490 
  2491 (*** second part of main module (postprocessing of TFL definitions) ***)
  2492 
  2493 structure Tfl: TFL =
  2494 struct
  2495 
  2496 (* misc *)
  2497 
  2498 (*---------------------------------------------------------------------------
  2499  * Extract termination goals so that they can be put it into a goalstack, or
  2500  * have a tactic directly applied to them.
  2501  *--------------------------------------------------------------------------*)
  2502 fun termination_goals rules =
  2503     map (Type.legacy_freeze o HOLogic.dest_Trueprop)
  2504       (fold_rev (union (op aconv) o Thm.prems_of) rules []);
  2505 
  2506 (*---------------------------------------------------------------------------
  2507  * Three postprocessors are applied to the definition.  It
  2508  * attempts to prove wellfoundedness of the given relation, simplifies the
  2509  * non-proved termination conditions, and finally attempts to prove the
  2510  * simplified termination conditions.
  2511  *--------------------------------------------------------------------------*)
  2512 fun std_postprocessor ctxt strict wfs =
  2513   Prim.postprocess ctxt strict
  2514    {wf_tac = REPEAT (ares_tac ctxt wfs 1),
  2515     terminator =
  2516       asm_simp_tac ctxt 1
  2517       THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
  2518         fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
  2519     simplifier = Rules.simpl_conv ctxt []};
  2520 
  2521 
  2522 
  2523 val concl = #2 o Rules.dest_thm;
  2524 
  2525 (*---------------------------------------------------------------------------
  2526  * Postprocess a definition made by "define". This is a separate stage of
  2527  * processing from the definition stage.
  2528  *---------------------------------------------------------------------------*)
  2529 local
  2530 
  2531 (* The rest of these local definitions are for the tricky nested case *)
  2532 val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
  2533 
  2534 fun id_thm th =
  2535    let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
  2536    in lhs aconv rhs end
  2537    handle Utils.ERR _ => false;
  2538 
  2539 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
  2540 fun mk_meta_eq r =
  2541   (case Thm.concl_of r of
  2542      Const(@{const_name Pure.eq},_)$_$_ => r
  2543   |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
  2544   |   _ => r RS P_imp_P_eq_True)
  2545 
  2546 (*Is this the best way to invoke the simplifier??*)
  2547 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
  2548 
  2549 fun join_assums ctxt th =
  2550   let val tych = Thm.cterm_of ctxt
  2551       val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
  2552       val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
  2553       val cntxtr = (#1 o USyntax.strip_imp) rhs  (* but union is solider *)
  2554       val cntxt = union (op aconv) cntxtl cntxtr
  2555   in
  2556     Rules.GEN_ALL ctxt
  2557       (Rules.DISCH_ALL
  2558          (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
  2559   end
  2560   val gen_all = USyntax.gen_all
  2561 in
  2562 fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
  2563   let
  2564     val _ = writeln "Proving induction theorem ..."
  2565     val ind =
  2566       Prim.mk_induction ctxt
  2567         {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
  2568     val _ = writeln "Postprocessing ...";
  2569     val {rules, induction, nested_tcs} =
  2570       std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
  2571   in
  2572   case nested_tcs
  2573   of [] => {induction=induction, rules=rules,tcs=[]}
  2574   | L  => let val _ = writeln "Simplifying nested TCs ..."
  2575               val (solved,simplified,stubborn) =
  2576                fold_rev (fn th => fn (So,Si,St) =>
  2577                      if (id_thm th) then (So, Si, th::St) else
  2578                      if (solved th) then (th::So, Si, St)
  2579                      else (So, th::Si, St)) nested_tcs ([],[],[])
  2580               val simplified' = map (join_assums ctxt) simplified
  2581               val dummy = (Prim.trace_thms ctxt "solved =" solved;
  2582                            Prim.trace_thms ctxt "simplified' =" simplified')
  2583               val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
  2584               val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
  2585               val induction' = rewr induction
  2586               val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
  2587               val rules'     = rewr rules
  2588               val _ = writeln "... Postprocessing finished";
  2589           in
  2590           {induction = induction',
  2591                rules = rules',
  2592                  tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
  2593                            (simplified@stubborn)}
  2594           end
  2595   end;
  2596 
  2597 
  2598 (*lcp: curry the predicate of the induction rule*)
  2599 fun curry_rule ctxt rl =
  2600   Split_Rule.split_rule_var ctxt (Term.head_of (HOLogic.dest_Trueprop (Thm.concl_of rl))) rl;
  2601 
  2602 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
  2603 fun meta_outer ctxt =
  2604   curry_rule ctxt o Drule.export_without_context o
  2605   rule_by_tactic ctxt
  2606     (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
  2607 
  2608 (*Strip off the outer !P*)
  2609 val spec'=
  2610   Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
  2611 
  2612 fun simplify_defn ctxt strict congs wfs pats def0 =
  2613   let
  2614     val thy = Proof_Context.theory_of ctxt;
  2615     val def = HOLogic.mk_obj_eq (Thm.unvarify_global thy def0)
  2616     val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
  2617     val {lhs=f,rhs} = USyntax.dest_eq (concl def)
  2618     val (_,[R,_]) = USyntax.strip_comb rhs
  2619     val _ = Prim.trace_thms ctxt "congs =" congs
  2620     (*the next step has caused simplifier looping in some cases*)
  2621     val {induction, rules, tcs} =
  2622       proof_stage ctxt strict wfs
  2623        {f = f, R = R, rules = rules,
  2624         full_pats_TCs = full_pats_TCs,
  2625         TCs = TCs}
  2626     val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
  2627                       (Rules.CONJUNCTS rules)
  2628   in
  2629     {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
  2630      rules = ListPair.zip(rules', rows),
  2631      tcs = (termination_goals rules') @ tcs}
  2632   end
  2633   handle Utils.ERR {mesg,func,module} =>
  2634     error (mesg ^ "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
  2635 
  2636 
  2637 (* Derive the initial equations from the case-split rules to meet the
  2638 users specification of the recursive function. *)
  2639 local
  2640   fun get_related_thms i =
  2641       map_filter ((fn (r,x) => if x = i then SOME r else NONE));
  2642 
  2643   fun solve_eq _ (_, [], _) =  error "derive_init_eqs: missing rules"
  2644     | solve_eq _ (_, [a], i) = [(a, i)]
  2645     | solve_eq ctxt (th, splitths, i) =
  2646       (writeln "Proving unsplit equation...";
  2647       [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
  2648           (CaseSplit.splitto ctxt splitths th), i)])
  2649       handle ERROR s =>
  2650              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
  2651 in
  2652 fun derive_init_eqs ctxt rules eqs =
  2653   map (Thm.trivial o Thm.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
  2654   |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
  2655   |> flat;
  2656 end;
  2657 
  2658 
  2659 (*---------------------------------------------------------------------------
  2660  * Defining a function with an associated termination relation.
  2661  *---------------------------------------------------------------------------*)
  2662 fun define_i strict congs wfs fid R eqs ctxt =
  2663   let
  2664     val thy = Proof_Context.theory_of ctxt
  2665     val {functional, pats} = Prim.mk_functional thy eqs
  2666     val (def, thy') = Prim.wfrec_definition0 fid R functional thy
  2667     val ctxt' = Proof_Context.transfer thy' ctxt
  2668     val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
  2669     val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs pats def
  2670     val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
  2671   in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
  2672 
  2673 fun define strict congs wfs fid R seqs ctxt =
  2674   define_i strict congs wfs fid
  2675     (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
  2676       handle Utils.ERR {mesg,...} => error mesg;
  2677 
  2678 end;
  2679 
  2680 end;
  2681 
  2682 
  2683 
  2684 (*** wrappers for Isar ***)
  2685 
  2686 (** recdef hints **)
  2687 
  2688 (* type hints *)
  2689 
  2690 type hints = {simps: thm list, congs: (string * thm) list, wfs: thm list};
  2691 
  2692 fun mk_hints (simps, congs, wfs) = {simps = simps, congs = congs, wfs = wfs}: hints;
  2693 fun map_hints f ({simps, congs, wfs}: hints) = mk_hints (f (simps, congs, wfs));
  2694 
  2695 fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs));
  2696 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
  2697 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
  2698 
  2699 
  2700 (* congruence rules *)
  2701 
  2702 local
  2703 
  2704 val cong_head =
  2705   fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
  2706 
  2707 fun prep_cong raw_thm =
  2708   let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
  2709 
  2710 in
  2711 
  2712 fun add_cong raw_thm congs =
  2713   let
  2714     val (c, thm) = prep_cong raw_thm;
  2715     val _ = if AList.defined (op =) congs c
  2716       then warning ("Overwriting recdef congruence rule for " ^ quote c)
  2717       else ();
  2718   in AList.update (op =) (c, thm) congs end;
  2719 
  2720 fun del_cong raw_thm congs =
  2721   let
  2722     val (c, _) = prep_cong raw_thm;
  2723     val _ = if AList.defined (op =) congs c
  2724       then ()
  2725       else warning ("No recdef congruence rule for " ^ quote c);
  2726   in AList.delete (op =) c congs end;
  2727 
  2728 end;
  2729 
  2730 
  2731 
  2732 (** global and local recdef data **)
  2733 
  2734 (* theory data *)
  2735 
  2736 type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
  2737 
  2738 structure Data = Generic_Data
  2739 (
  2740   type T = recdef_info Symtab.table * hints;
  2741   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
  2742   val extend = I;
  2743   fun merge
  2744    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
  2745     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
  2746       (Symtab.merge (K true) (tab1, tab2),
  2747         mk_hints (Thm.merge_thms (simps1, simps2),
  2748           AList.merge (op =) (K true) (congs1, congs2),
  2749           Thm.merge_thms (wfs1, wfs2)));
  2750 );
  2751 
  2752 val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory;
  2753 
  2754 fun put_recdef name info =
  2755   (Context.theory_map o Data.map o apfst) (fn tab =>
  2756     Symtab.update_new (name, info) tab
  2757       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name));
  2758 
  2759 val get_hints = #2 o Data.get o Context.Proof;
  2760 val map_hints = Data.map o apsnd;
  2761 
  2762 
  2763 (* attributes *)
  2764 
  2765 fun attrib f = Thm.declaration_attribute (map_hints o f);
  2766 
  2767 val simp_add = attrib (map_simps o Thm.add_thm);
  2768 val simp_del = attrib (map_simps o Thm.del_thm);
  2769 val cong_add = attrib (map_congs o add_cong);
  2770 val cong_del = attrib (map_congs o del_cong);
  2771 val wf_add = attrib (map_wfs o Thm.add_thm);
  2772 val wf_del = attrib (map_wfs o Thm.del_thm);
  2773 
  2774 
  2775 (* modifiers *)
  2776 
  2777 val recdef_simpN = "recdef_simp";
  2778 val recdef_congN = "recdef_cong";
  2779 val recdef_wfN = "recdef_wf";
  2780 
  2781 val recdef_modifiers =
  2782  [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
  2783   Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
  2784   Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
  2785   Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add \<^here>),
  2786   Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>),
  2787   Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>),
  2788   Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add \<^here>),
  2789   Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add \<^here>),
  2790   Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del \<^here>)] @
  2791   Clasimp.clasimp_modifiers;
  2792 
  2793 
  2794 
  2795 (** prepare hints **)
  2796 
  2797 fun prepare_hints opt_src ctxt =
  2798   let
  2799     val ctxt' =
  2800       (case opt_src of
  2801         NONE => ctxt
  2802       | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt));
  2803     val {simps, congs, wfs} = get_hints ctxt';
  2804     val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong};
  2805   in ((rev (map snd congs), wfs), ctxt'') end;
  2806 
  2807 fun prepare_hints_i () ctxt =
  2808   let
  2809     val {simps, congs, wfs} = get_hints ctxt;
  2810     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
  2811   in ((rev (map snd congs), wfs), ctxt') end;
  2812 
  2813 
  2814 
  2815 (** add_recdef(_i) **)
  2816 
  2817 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
  2818   let
  2819     val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
  2820 
  2821     val name = Sign.intern_const thy raw_name;
  2822     val bname = Long_Name.base_name name;
  2823     val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
  2824 
  2825     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
  2826     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
  2827 
  2828     val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy);
  2829     (*We must remove imp_cong to prevent looping when the induction rule
  2830       is simplified. Many induction rules have nested implications that would
  2831       give rise to looping conditional rewriting.*)
  2832     val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) =
  2833       tfl_fn not_permissive congs wfs name R eqs ctxt;
  2834     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
  2835     val simp_att =
  2836       if null tcs then [Simplifier.simp_add,
  2837         Named_Theorems.add @{named_theorems nitpick_simp}]
  2838       else [];
  2839     val ((simps' :: rules', [induct']), thy2) =
  2840       Proof_Context.theory_of ctxt1
  2841       |> Sign.add_path bname
  2842       |> Global_Theory.add_thmss
  2843         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
  2844       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
  2845       ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules)
  2846       ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
  2847     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
  2848     val thy3 =
  2849       thy2
  2850       |> put_recdef name result
  2851       |> Sign.parent_path;
  2852   in (thy3, result) end;
  2853 
  2854 val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
  2855 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
  2856 
  2857 
  2858 
  2859 (** package setup **)
  2860 
  2861 (* setup theory *)
  2862 
  2863 val _ =
  2864   Theory.setup
  2865    (Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
  2866       "declaration of recdef simp rule" #>
  2867     Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
  2868       "declaration of recdef cong rule" #>
  2869     Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
  2870       "declaration of recdef wf rule");
  2871 
  2872 
  2873 (* outer syntax *)
  2874 
  2875 val hints =
  2876   @{keyword "("} |--
  2877     Parse.!!! ((Parse.token @{keyword "hints"} ::: Parse.args) --| @{keyword ")"});
  2878 
  2879 val recdef_decl =
  2880   Scan.optional
  2881     (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
  2882   Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
  2883     -- Scan.option hints
  2884   >> (fn ((((p, f), R), eqs), src) =>
  2885       #1 o add_recdef p f R (map (fn ((x, y), z) => ((x, z), y)) eqs) src);
  2886 
  2887 val _ =
  2888   Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
  2889     (recdef_decl >> Toplevel.theory);
  2890 
  2891 end;