src/HOL/Library/old_recdef.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 60774 6c28d8ed2488
child 60825 bacfb7c45d81
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
     1 (*  Title:      HOL/Tools/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:", Display.string_of_thm ctxt th, "split ths:"] @
   379               map (Display.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 (#prop (Thm.crep_thm thm));
   918 fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
   919 
   920 fun dest_thm thm =
   921   let val {prop,hyps,...} = Thm.rep_thm thm
   922   in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
   923   handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
   924 
   925 
   926 (* Inference rules *)
   927 
   928 (*---------------------------------------------------------------------------
   929  *        Equality (one step)
   930  *---------------------------------------------------------------------------*)
   931 
   932 fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
   933   handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
   934 
   935 fun SYM thm = thm RS sym
   936   handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
   937 
   938 fun ALPHA thm ctm1 =
   939   let
   940     val ctm2 = Thm.cprop_of thm;
   941     val ctm2_eq = Thm.reflexive ctm2;
   942     val ctm1_eq = Thm.reflexive ctm1;
   943   in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
   944   handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
   945 
   946 fun rbeta th =
   947   (case Dcterm.strip_comb (cconcl th) of
   948     (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
   949   | _ => raise RULES_ERR "rbeta" "");
   950 
   951 
   952 (*----------------------------------------------------------------------------
   953  *        Implication and the assumption list
   954  *
   955  * Assumptions get stuck on the meta-language assumption list. Implications
   956  * are in the object language, so discharging an assumption "A" from theorem
   957  * "B" results in something that looks like "A --> B".
   958  *---------------------------------------------------------------------------*)
   959 
   960 fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
   961 
   962 
   963 (*---------------------------------------------------------------------------
   964  * Implication in TFL is -->. Meta-language implication (==>) is only used
   965  * in the implementation of some of the inference rules below.
   966  *---------------------------------------------------------------------------*)
   967 fun MP th1 th2 = th2 RS (th1 RS mp)
   968   handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
   969 
   970 (*forces the first argument to be a proposition if necessary*)
   971 fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
   972   handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
   973 
   974 fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
   975 
   976 
   977 fun FILTER_DISCH_ALL P thm =
   978  let fun check tm = P (Thm.term_of tm)
   979  in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
   980  end;
   981 
   982 fun UNDISCH thm =
   983    let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
   984    in Thm.implies_elim (thm RS mp) (ASSUME tm) end
   985    handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
   986      | THM _ => raise RULES_ERR "UNDISCH" "";
   987 
   988 fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
   989 
   990 fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
   991   handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
   992 
   993 
   994 (*----------------------------------------------------------------------------
   995  *        Conjunction
   996  *---------------------------------------------------------------------------*)
   997 
   998 fun CONJUNCT1 thm = thm RS conjunct1
   999   handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
  1000 
  1001 fun CONJUNCT2 thm = thm RS conjunct2
  1002   handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
  1003 
  1004 fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
  1005 
  1006 fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
  1007   | LIST_CONJ [th] = th
  1008   | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
  1009       handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
  1010 
  1011 
  1012 (*----------------------------------------------------------------------------
  1013  *        Disjunction
  1014  *---------------------------------------------------------------------------*)
  1015 local
  1016   val prop = Thm.prop_of disjI1
  1017   val [_,Q] = Misc_Legacy.term_vars prop
  1018   val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
  1019 in
  1020 fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
  1021   handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
  1022 end;
  1023 
  1024 local
  1025   val prop = Thm.prop_of disjI2
  1026   val [P,_] = Misc_Legacy.term_vars prop
  1027   val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
  1028 in
  1029 fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
  1030   handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
  1031 end;
  1032 
  1033 
  1034 (*----------------------------------------------------------------------------
  1035  *
  1036  *                   A1 |- M1, ..., An |- Mn
  1037  *     ---------------------------------------------------
  1038  *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
  1039  *
  1040  *---------------------------------------------------------------------------*)
  1041 
  1042 
  1043 fun EVEN_ORS thms =
  1044   let fun blue ldisjs [] _ = []
  1045         | blue ldisjs (th::rst) rdisjs =
  1046             let val tail = tl rdisjs
  1047                 val rdisj_tl = Dcterm.list_mk_disj tail
  1048             in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
  1049                :: blue (ldisjs @ [cconcl th]) rst tail
  1050             end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
  1051    in blue [] thms (map cconcl thms) end;
  1052 
  1053 
  1054 (*----------------------------------------------------------------------------
  1055  *
  1056  *         A |- P \/ Q   B,P |- R    C,Q |- R
  1057  *     ---------------------------------------------------
  1058  *                     A U B U C |- R
  1059  *
  1060  *---------------------------------------------------------------------------*)
  1061 
  1062 fun DISJ_CASES th1 th2 th3 =
  1063   let
  1064     val c = Dcterm.drop_prop (cconcl th1);
  1065     val (disj1, disj2) = Dcterm.dest_disj c;
  1066     val th2' = DISCH disj1 th2;
  1067     val th3' = DISCH disj2 th3;
  1068   in
  1069     th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
  1070       handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
  1071   end;
  1072 
  1073 
  1074 (*-----------------------------------------------------------------------------
  1075  *
  1076  *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
  1077  *     ---------------------------------------------------
  1078  *                           |- M
  1079  *
  1080  * Note. The list of theorems may be all jumbled up, so we have to
  1081  * first organize it to align with the first argument (the disjunctive
  1082  * theorem).
  1083  *---------------------------------------------------------------------------*)
  1084 
  1085 fun organize eq =    (* a bit slow - analogous to insertion sort *)
  1086  let fun extract a alist =
  1087      let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
  1088            | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
  1089      in ex ([],alist)
  1090      end
  1091      fun place [] [] = []
  1092        | place (a::rst) alist =
  1093            let val (item,next) = extract a alist
  1094            in item::place rst next
  1095            end
  1096        | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
  1097  in place
  1098  end;
  1099 
  1100 fun DISJ_CASESL disjth thl =
  1101    let val c = cconcl disjth
  1102        fun eq th atm =
  1103         exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
  1104        val tml = Dcterm.strip_disj c
  1105        fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases"
  1106          | DL th [th1] = PROVE_HYP th th1
  1107          | DL th [th1,th2] = DISJ_CASES th th1 th2
  1108          | DL th (th1::rst) =
  1109             let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
  1110              in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
  1111    in DL disjth (organize eq tml thl)
  1112    end;
  1113 
  1114 
  1115 (*----------------------------------------------------------------------------
  1116  *        Universals
  1117  *---------------------------------------------------------------------------*)
  1118 local (* this is fragile *)
  1119   val prop = Thm.prop_of spec
  1120   val x = hd (tl (Misc_Legacy.term_vars prop))
  1121   val TV = dest_TVar (type_of x)
  1122   val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
  1123 in
  1124 fun SPEC tm thm =
  1125    let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
  1126    in thm RS (Thm.forall_elim tm gspec') end
  1127 end;
  1128 
  1129 fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
  1130 
  1131 val ISPEC = SPEC
  1132 val ISPECL = fold ISPEC;
  1133 
  1134 (* Not optimized! Too complicated. *)
  1135 local
  1136   val prop = Thm.prop_of allI
  1137   val [P] = Misc_Legacy.add_term_vars (prop, [])
  1138   fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
  1139   fun ctm_theta ctxt =
  1140     map (fn (i, (_, tm2)) =>
  1141       let val ctm2 = Thm.cterm_of ctxt tm2
  1142       in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
  1143   fun certify ctxt (ty_theta,tm_theta) =
  1144     (cty_theta ctxt (Vartab.dest ty_theta),
  1145      ctm_theta ctxt (Vartab.dest tm_theta))
  1146 in
  1147 fun GEN ctxt v th =
  1148    let val gth = Thm.forall_intr v th
  1149        val thy = Proof_Context.theory_of ctxt
  1150        val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
  1151        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
  1152        val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
  1153        val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
  1154        val thm = Thm.implies_elim allI2 gth
  1155        val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
  1156        val prop' = tp $ (A $ Abs(x,ty,M))
  1157    in ALPHA thm (Thm.cterm_of ctxt prop') end
  1158 end;
  1159 
  1160 fun GENL ctxt = fold_rev (GEN ctxt);
  1161 
  1162 fun GEN_ALL ctxt thm =
  1163   let
  1164     val prop = Thm.prop_of thm
  1165     val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
  1166   in GENL ctxt vlist thm end;
  1167 
  1168 
  1169 fun MATCH_MP th1 th2 =
  1170    if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
  1171    then MATCH_MP (th1 RS spec) th2
  1172    else MP th1 th2;
  1173 
  1174 
  1175 (*----------------------------------------------------------------------------
  1176  *        Existentials
  1177  *---------------------------------------------------------------------------*)
  1178 
  1179 
  1180 
  1181 (*---------------------------------------------------------------------------
  1182  * Existential elimination
  1183  *
  1184  *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
  1185  *      ------------------------------------     (variable v occurs nowhere)
  1186  *                A1 u A2 |- t'
  1187  *
  1188  *---------------------------------------------------------------------------*)
  1189 
  1190 fun CHOOSE ctxt (fvar, exth) fact =
  1191   let
  1192     val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
  1193     val redex = Dcterm.capply lam fvar
  1194     val t$u = Thm.term_of redex
  1195     val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
  1196   in
  1197     GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
  1198       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
  1199   end;
  1200 
  1201 fun EXISTS ctxt (template,witness) thm =
  1202   let val abstr = #2 (Dcterm.dest_comb template) in
  1203     thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
  1204       handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
  1205   end;
  1206 
  1207 (*----------------------------------------------------------------------------
  1208  *
  1209  *       A |- M[x_1,...,x_n]
  1210  *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
  1211  *       A |- ?y_1...y_n. M
  1212  *
  1213  *---------------------------------------------------------------------------*)
  1214 (* Could be improved, but needs "subst_free" for certified terms *)
  1215 
  1216 fun IT_EXISTS ctxt blist th =
  1217   let
  1218     val blist' = map (apply2 Thm.term_of) blist
  1219     fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
  1220   in
  1221     fold_rev (fn (b as (r1,r2)) => fn thm =>
  1222         EXISTS ctxt (ex r2 (subst_free [b]
  1223                    (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
  1224               thm)
  1225        blist' th
  1226   end;
  1227 
  1228 (*---------------------------------------------------------------------------
  1229  *  Faster version, that fails for some as yet unknown reason
  1230  * fun IT_EXISTS blist th =
  1231  *    let val {thy,...} = rep_thm th
  1232  *        val tych = cterm_of thy
  1233  *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
  1234  *   in
  1235  *  fold (fn (b as (r1,r2), thm) =>
  1236  *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
  1237  *           r1) thm)  blist th
  1238  *   end;
  1239  *---------------------------------------------------------------------------*)
  1240 
  1241 (*----------------------------------------------------------------------------
  1242  *        Rewriting
  1243  *---------------------------------------------------------------------------*)
  1244 
  1245 fun SUBS ctxt thl =
  1246   rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
  1247 
  1248 val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
  1249 
  1250 fun simpl_conv ctxt thl ctm =
  1251  rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
  1252 
  1253 
  1254 fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
  1255 
  1256 
  1257 
  1258 (*---------------------------------------------------------------------------
  1259  *                  TERMINATION CONDITION EXTRACTION
  1260  *---------------------------------------------------------------------------*)
  1261 
  1262 
  1263 (* Object language quantifier, i.e., "!" *)
  1264 fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
  1265 
  1266 
  1267 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
  1268 fun is_cong thm =
  1269   case (Thm.prop_of thm) of
  1270     (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
  1271       (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) =>
  1272         false
  1273   | _ => true;
  1274 
  1275 
  1276 fun dest_equal(Const (@{const_name Pure.eq},_) $
  1277                (Const (@{const_name Trueprop},_) $ lhs)
  1278                $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
  1279   | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
  1280   | dest_equal tm = USyntax.dest_eq tm;
  1281 
  1282 fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
  1283 
  1284 fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
  1285   | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
  1286 
  1287 val is_all = can (dest_all []);
  1288 
  1289 fun strip_all used fm =
  1290    if (is_all fm)
  1291    then let val ({Bvar, Body}, used') = dest_all used fm
  1292             val (bvs, core, used'') = strip_all used' Body
  1293         in ((Bvar::bvs), core, used'')
  1294         end
  1295    else ([], fm, used);
  1296 
  1297 fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
  1298      let val (L,core) = list_break_all body
  1299      in ((s,ty)::L, core)
  1300      end
  1301   | list_break_all tm = ([],tm);
  1302 
  1303 (*---------------------------------------------------------------------------
  1304  * Rename a term of the form
  1305  *
  1306  *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
  1307  *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
  1308  * to one of
  1309  *
  1310  *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
  1311  *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
  1312  *
  1313  * This prevents name problems in extraction, and helps the result to read
  1314  * better. There is a problem with varstructs, since they can introduce more
  1315  * than n variables, and some extra reasoning needs to be done.
  1316  *---------------------------------------------------------------------------*)
  1317 
  1318 fun get ([],_,L) = rev L
  1319   | get (ant::rst,n,L) =
  1320       case (list_break_all ant)
  1321         of ([],_) => get (rst, n+1,L)
  1322          | (_,body) =>
  1323             let val eq = Logic.strip_imp_concl body
  1324                 val (f,_) = USyntax.strip_comb (get_lhs eq)
  1325                 val (vstrl,_) = USyntax.strip_abs f
  1326                 val names  =
  1327                   Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
  1328             in get (rst, n+1, (names,n)::L) end
  1329             handle TERM _ => get (rst, n+1, L)
  1330               | Utils.ERR _ => get (rst, n+1, L);
  1331 
  1332 (* Note: Thm.rename_params_rule counts from 1, not 0 *)
  1333 fun rename thm =
  1334   let
  1335     val ants = Logic.strip_imp_prems (Thm.prop_of thm)
  1336     val news = get (ants,1,[])
  1337   in fold Thm.rename_params_rule news thm end;
  1338 
  1339 
  1340 (*---------------------------------------------------------------------------
  1341  * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
  1342  *---------------------------------------------------------------------------*)
  1343 
  1344 fun list_beta_conv tm =
  1345   let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
  1346       fun iter [] = Thm.reflexive tm
  1347         | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
  1348   in iter  end;
  1349 
  1350 
  1351 (*---------------------------------------------------------------------------
  1352  * Trace information for the rewriter
  1353  *---------------------------------------------------------------------------*)
  1354 val tracing = Unsynchronized.ref false;
  1355 
  1356 fun say s = if !tracing then writeln s else ();
  1357 
  1358 fun print_thms ctxt s L =
  1359   say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
  1360 
  1361 fun print_term ctxt s t =
  1362   say (cat_lines [s, Syntax.string_of_term ctxt t]);
  1363 
  1364 
  1365 (*---------------------------------------------------------------------------
  1366  * General abstraction handlers, should probably go in USyntax.
  1367  *---------------------------------------------------------------------------*)
  1368 fun mk_aabs (vstr, body) =
  1369   USyntax.mk_abs {Bvar = vstr, Body = body}
  1370   handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
  1371 
  1372 fun list_mk_aabs (vstrl,tm) =
  1373     fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
  1374 
  1375 fun dest_aabs used tm =
  1376    let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
  1377    in (Bvar, Body, used') end
  1378    handle Utils.ERR _ =>
  1379      let val {varstruct, body, used} = USyntax.dest_pabs used tm
  1380      in (varstruct, body, used) end;
  1381 
  1382 fun strip_aabs used tm =
  1383    let val (vstr, body, used') = dest_aabs used tm
  1384        val (bvs, core, used'') = strip_aabs used' body
  1385    in (vstr::bvs, core, used'') end
  1386    handle Utils.ERR _ => ([], tm, used);
  1387 
  1388 fun dest_combn tm 0 = (tm,[])
  1389   | dest_combn tm n =
  1390      let val {Rator,Rand} = USyntax.dest_comb tm
  1391          val (f,rands) = dest_combn Rator (n-1)
  1392      in (f,Rand::rands)
  1393      end;
  1394 
  1395 
  1396 
  1397 
  1398 local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
  1399       fun mk_fst tm =
  1400           let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
  1401           in  Const (@{const_name Product_Type.fst}, ty --> fty) $ tm  end
  1402       fun mk_snd tm =
  1403           let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
  1404           in  Const (@{const_name Product_Type.snd}, ty --> sty) $ tm  end
  1405 in
  1406 fun XFILL tych x vstruct =
  1407   let fun traverse p xocc L =
  1408         if (is_Free p)
  1409         then tych xocc::L
  1410         else let val (p1,p2) = dest_pair p
  1411              in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
  1412              end
  1413   in
  1414   traverse vstruct x []
  1415 end end;
  1416 
  1417 (*---------------------------------------------------------------------------
  1418  * Replace a free tuple (vstr) by a universally quantified variable (a).
  1419  * Note that the notion of "freeness" for a tuple is different than for a
  1420  * variable: if variables in the tuple also occur in any other place than
  1421  * an occurrences of the tuple, they aren't "free" (which is thus probably
  1422  *  the wrong word to use).
  1423  *---------------------------------------------------------------------------*)
  1424 
  1425 fun VSTRUCT_ELIM ctxt tych a vstr th =
  1426   let val L = USyntax.free_vars_lr vstr
  1427       val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
  1428       val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
  1429       val thm2 = forall_intr_list (map tych L) thm1
  1430       val thm3 = forall_elim_list (XFILL tych a vstr) thm2
  1431   in refl RS
  1432      rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
  1433   end;
  1434 
  1435 fun PGEN ctxt tych a vstr th =
  1436   let val a1 = tych a
  1437   in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
  1438 
  1439 
  1440 (*---------------------------------------------------------------------------
  1441  * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
  1442  *
  1443  *     (([x,y],N),vstr)
  1444  *---------------------------------------------------------------------------*)
  1445 fun dest_pbeta_redex used M n =
  1446   let val (f,args) = dest_combn M n
  1447       val _ = dest_aabs used f
  1448   in (strip_aabs used f,args)
  1449   end;
  1450 
  1451 fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
  1452 
  1453 fun dest_impl tm =
  1454   let val ants = Logic.strip_imp_prems tm
  1455       val eq = Logic.strip_imp_concl tm
  1456   in (ants,get_lhs eq)
  1457   end;
  1458 
  1459 fun restricted t = is_some (USyntax.find_term
  1460                             (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
  1461                             t)
  1462 
  1463 fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
  1464  let val globals = func::G
  1465      val ctxt0 = empty_simpset main_ctxt
  1466      val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
  1467      val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
  1468      val cut_lemma' = cut_lemma RS eq_reflection
  1469      fun prover used ctxt thm =
  1470      let fun cong_prover ctxt thm =
  1471          let val _ = say "cong_prover:"
  1472              val cntxt = Simplifier.prems_of ctxt
  1473              val _ = print_thms ctxt "cntxt:" cntxt
  1474              val _ = say "cong rule:"
  1475              val _ = say (Display.string_of_thm ctxt thm)
  1476              (* Unquantified eliminate *)
  1477              fun uq_eliminate (thm,imp) =
  1478                  let val tych = Thm.cterm_of ctxt
  1479                      val _ = print_term ctxt "To eliminate:" imp
  1480                      val ants = map tych (Logic.strip_imp_prems imp)
  1481                      val eq = Logic.strip_imp_concl imp
  1482                      val lhs = tych(get_lhs eq)
  1483                      val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
  1484                      val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
  1485                        handle Utils.ERR _ => Thm.reflexive lhs
  1486                      val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
  1487                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
  1488                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
  1489                   in
  1490                   lhs_eeq_lhs2 COMP thm
  1491                   end
  1492              fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
  1493               let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
  1494                   val _ = forall (op aconv) (ListPair.zip (vlist, args))
  1495                     orelse error "assertion failed in CONTEXT_REWRITE_RULE"
  1496                   val imp_body1 = subst_free (ListPair.zip (args, vstrl))
  1497                                              imp_body
  1498                   val tych = Thm.cterm_of ctxt
  1499                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
  1500                   val eq1 = Logic.strip_imp_concl imp_body1
  1501                   val Q = get_lhs eq1
  1502                   val QeqQ1 = pbeta_reduce (tych Q)
  1503                   val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
  1504                   val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
  1505                   val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
  1506                                 handle Utils.ERR _ => Thm.reflexive Q1
  1507                   val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
  1508                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
  1509                   val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
  1510                   val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
  1511                   val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
  1512                                ((Q2eeqQ3 RS meta_eq_to_obj_eq)
  1513                                 RS ((thA RS meta_eq_to_obj_eq) RS trans))
  1514                                 RS eq_reflection
  1515                   val impth = implies_intr_list ants1 QeeqQ3
  1516                   val impth1 = impth RS meta_eq_to_obj_eq
  1517                   (* Need to abstract *)
  1518                   val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
  1519               in ant_th COMP thm
  1520               end
  1521              fun q_eliminate (thm, imp) =
  1522               let val (vlist, imp_body, used') = strip_all used imp
  1523                   val (ants,Q) = dest_impl imp_body
  1524               in if (pbeta_redex Q) (length vlist)
  1525                  then pq_eliminate (thm, vlist, imp_body, Q)
  1526                  else
  1527                  let val tych = Thm.cterm_of ctxt
  1528                      val ants1 = map tych ants
  1529                      val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
  1530                      val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
  1531                         (false,true,false) (prover used') ctxt' (tych Q)
  1532                       handle Utils.ERR _ => Thm.reflexive (tych Q)
  1533                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
  1534                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
  1535                      val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
  1536                  in
  1537                  ant_th COMP thm
  1538               end end
  1539 
  1540              fun eliminate thm =
  1541                case Thm.prop_of thm of
  1542                  Const(@{const_name Pure.imp},_) $ imp $ _ =>
  1543                    eliminate
  1544                     (if not(is_all imp)
  1545                      then uq_eliminate (thm, imp)
  1546                      else q_eliminate (thm, imp))
  1547                             (* Assume that the leading constant is ==,   *)
  1548                 | _ => thm  (* if it is not a ==>                        *)
  1549          in SOME(eliminate (rename thm)) end
  1550          handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
  1551 
  1552         fun restrict_prover ctxt thm =
  1553           let val _ = say "restrict_prover:"
  1554               val cntxt = rev (Simplifier.prems_of ctxt)
  1555               val _ = print_thms ctxt "cntxt:" cntxt
  1556               val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
  1557                 Thm.prop_of thm
  1558               fun genl tm = let val vlist = subtract (op aconv) globals
  1559                                            (Misc_Legacy.add_term_frees(tm,[]))
  1560                             in fold_rev Forall vlist tm
  1561                             end
  1562               (*--------------------------------------------------------------
  1563                * This actually isn't quite right, since it will think that
  1564                * not-fully applied occs. of "f" in the context mean that the
  1565                * current call is nested. The real solution is to pass in a
  1566                * term "f v1..vn" which is a pattern that any full application
  1567                * of "f" will match.
  1568                *-------------------------------------------------------------*)
  1569               val func_name = #1(dest_Const func)
  1570               fun is_func (Const (name,_)) = (name = func_name)
  1571                 | is_func _                = false
  1572               val rcontext = rev cntxt
  1573               val cncl = HOLogic.dest_Trueprop o Thm.prop_of
  1574               val antl = case rcontext of [] => []
  1575                          | _   => [USyntax.list_mk_conj(map cncl rcontext)]
  1576               val TC = genl(USyntax.list_mk_imp(antl, A))
  1577               val _ = print_term ctxt "func:" func
  1578               val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
  1579               val _ = tc_list := (TC :: !tc_list)
  1580               val nestedp = is_some (USyntax.find_term is_func TC)
  1581               val _ = if nestedp then say "nested" else say "not_nested"
  1582               val th' = if nestedp then raise RULES_ERR "solver" "nested function"
  1583                         else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
  1584                              in case rcontext of
  1585                                 [] => SPEC_ALL(ASSUME cTC)
  1586                                | _ => MP (SPEC_ALL (ASSUME cTC))
  1587                                          (LIST_CONJ rcontext)
  1588                              end
  1589               val th'' = th' RS thm
  1590           in SOME (th'')
  1591           end handle Utils.ERR _ => NONE    (* FIXME handle THM as well?? *)
  1592     in
  1593     (if (is_cong thm) then cong_prover else restrict_prover) ctxt thm
  1594     end
  1595     val ctm = Thm.cprop_of th
  1596     val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
  1597     val th1 =
  1598       Raw_Simplifier.rewrite_cterm (false, true, false)
  1599         (prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
  1600     val th2 = Thm.equal_elim th1 th
  1601  in
  1602  (th2, filter_out restricted (!tc_list))
  1603  end;
  1604 
  1605 
  1606 fun prove ctxt strict (t, tac) =
  1607   let
  1608     val ctxt' = Variable.auto_fixes t ctxt;
  1609   in
  1610     if strict
  1611     then Goal.prove ctxt' [] [] t (K tac)
  1612     else Goal.prove ctxt' [] [] t (K tac)
  1613       handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
  1614   end;
  1615 
  1616 end;
  1617 
  1618 
  1619 
  1620 (*** theory operations ***)
  1621 
  1622 structure Thry: THRY =
  1623 struct
  1624 
  1625 
  1626 fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
  1627 
  1628 
  1629 (*---------------------------------------------------------------------------
  1630  *    Matching
  1631  *---------------------------------------------------------------------------*)
  1632 
  1633 local
  1634 
  1635 fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
  1636 
  1637 in
  1638 
  1639 fun match_term thry pat ob =
  1640   let
  1641     val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
  1642     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
  1643   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
  1644   end;
  1645 
  1646 fun match_type thry pat ob =
  1647   map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
  1648 
  1649 end;
  1650 
  1651 
  1652 (*---------------------------------------------------------------------------
  1653  * Typing
  1654  *---------------------------------------------------------------------------*)
  1655 
  1656 fun typecheck thy t =
  1657   Thm.global_cterm_of thy t
  1658     handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
  1659       | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
  1660 
  1661 
  1662 (*---------------------------------------------------------------------------
  1663  * Get information about datatypes
  1664  *---------------------------------------------------------------------------*)
  1665 
  1666 fun match_info thy dtco =
  1667   case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
  1668          BNF_LFP_Compat.get_constrs thy dtco) of
  1669       (SOME {case_name, ... }, SOME constructors) =>
  1670         SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
  1671     | _ => NONE;
  1672 
  1673 fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
  1674         NONE => NONE
  1675       | SOME {nchotomy, ...} =>
  1676           SOME {nchotomy = nchotomy,
  1677                 constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
  1678 
  1679 fun extract_info thy =
  1680  let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
  1681  in {case_congs = map (mk_meta_eq o #case_cong) infos,
  1682      case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
  1683  end;
  1684 
  1685 
  1686 end;
  1687 
  1688 
  1689 
  1690 (*** first part of main module ***)
  1691 
  1692 structure Prim: PRIM =
  1693 struct
  1694 
  1695 val trace = Unsynchronized.ref false;
  1696 
  1697 
  1698 fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
  1699 
  1700 val concl = #2 o Rules.dest_thm;
  1701 
  1702 val list_mk_type = Utils.end_itlist (curry (op -->));
  1703 
  1704 fun front_last [] = raise TFL_ERR "front_last" "empty list"
  1705   | front_last [x] = ([],x)
  1706   | front_last (h::t) =
  1707      let val (pref,x) = front_last t
  1708      in
  1709         (h::pref,x)
  1710      end;
  1711 
  1712 
  1713 (*---------------------------------------------------------------------------
  1714  * The next function is common to pattern-match translation and
  1715  * proof of completeness of cases for the induction theorem.
  1716  *
  1717  * The curried function "gvvariant" returns a function to generate distinct
  1718  * variables that are guaranteed not to be in names.  The names of
  1719  * the variables go u, v, ..., z, aa, ..., az, ...  The returned
  1720  * function contains embedded refs!
  1721  *---------------------------------------------------------------------------*)
  1722 fun gvvariant names =
  1723   let val slist = Unsynchronized.ref names
  1724       val vname = Unsynchronized.ref "u"
  1725       fun new() =
  1726          if member (op =) (!slist) (!vname)
  1727          then (vname := Symbol.bump_string (!vname);  new())
  1728          else (slist := !vname :: !slist;  !vname)
  1729   in
  1730   fn ty => Free(new(), ty)
  1731   end;
  1732 
  1733 
  1734 (*---------------------------------------------------------------------------
  1735  * Used in induction theorem production. This is the simple case of
  1736  * partitioning up pattern rows by the leading constructor.
  1737  *---------------------------------------------------------------------------*)
  1738 fun ipartition gv (constructors,rows) =
  1739   let fun pfail s = raise TFL_ERR "partition.part" s
  1740       fun part {constrs = [],   rows = [],   A} = rev A
  1741         | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
  1742         | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
  1743         | part {constrs = c::crst, rows,     A} =
  1744           let val (c, T) = dest_Const c
  1745               val L = binder_types T
  1746               val (in_group, not_in_group) =
  1747                fold_rev (fn (row as (p::rst, rhs)) =>
  1748                          fn (in_group,not_in_group) =>
  1749                   let val (pc,args) = USyntax.strip_comb p
  1750                   in if (#1(dest_Const pc) = c)
  1751                      then ((args@rst, rhs)::in_group, not_in_group)
  1752                      else (in_group, row::not_in_group)
  1753                   end)      rows ([],[])
  1754               val col_types = Utils.take type_of (length L, #1(hd in_group))
  1755           in
  1756           part{constrs = crst, rows = not_in_group,
  1757                A = {constructor = c,
  1758                     new_formals = map gv col_types,
  1759                     group = in_group}::A}
  1760           end
  1761   in part{constrs = constructors, rows = rows, A = []}
  1762   end;
  1763 
  1764 
  1765 
  1766 (*---------------------------------------------------------------------------
  1767  * Each pattern carries with it a tag (i,b) where
  1768  * i is the clause it came from and
  1769  * b=true indicates that clause was given by the user
  1770  * (or is an instantiation of a user supplied pattern)
  1771  * b=false --> i = ~1
  1772  *---------------------------------------------------------------------------*)
  1773 
  1774 type pattern = term * (int * bool)
  1775 
  1776 fun pattern_map f (tm,x) = (f tm, x);
  1777 
  1778 fun pattern_subst theta = pattern_map (subst_free theta);
  1779 
  1780 val pat_of = fst;
  1781 fun row_of_pat x = fst (snd x);
  1782 fun given x = snd (snd x);
  1783 
  1784 (*---------------------------------------------------------------------------
  1785  * Produce an instance of a constructor, plus genvars for its arguments.
  1786  *---------------------------------------------------------------------------*)
  1787 fun fresh_constr ty_match colty gv c =
  1788   let val (_,Ty) = dest_Const c
  1789       val L = binder_types Ty
  1790       and ty = body_type Ty
  1791       val ty_theta = ty_match ty colty
  1792       val c' = USyntax.inst ty_theta c
  1793       val gvars = map (USyntax.inst ty_theta o gv) L
  1794   in (c', gvars)
  1795   end;
  1796 
  1797 
  1798 (*---------------------------------------------------------------------------
  1799  * Goes through a list of rows and picks out the ones beginning with a
  1800  * pattern with constructor = name.
  1801  *---------------------------------------------------------------------------*)
  1802 fun mk_group name rows =
  1803   fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
  1804             fn (in_group,not_in_group) =>
  1805                let val (pc,args) = USyntax.strip_comb p
  1806                in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
  1807                   then (((prfx,args@rst), rhs)::in_group, not_in_group)
  1808                   else (in_group, row::not_in_group) end)
  1809       rows ([],[]);
  1810 
  1811 (*---------------------------------------------------------------------------
  1812  * Partition the rows. Not efficient: we should use hashing.
  1813  *---------------------------------------------------------------------------*)
  1814 fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
  1815   | partition gv ty_match
  1816               (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
  1817 let val fresh = fresh_constr ty_match colty gv
  1818      fun part {constrs = [],      rows, A} = rev A
  1819        | part {constrs = c::crst, rows, A} =
  1820          let val (c',gvars) = fresh c
  1821              val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
  1822              val in_group' =
  1823                  if (null in_group)  (* Constructor not given *)
  1824                  then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
  1825                  else in_group
  1826          in
  1827          part{constrs = crst,
  1828               rows = not_in_group,
  1829               A = {constructor = c',
  1830                    new_formals = gvars,
  1831                    group = in_group'}::A}
  1832          end
  1833 in part{constrs=constructors, rows=rows, A=[]}
  1834 end;
  1835 
  1836 (*---------------------------------------------------------------------------
  1837  * Misc. routines used in mk_case
  1838  *---------------------------------------------------------------------------*)
  1839 
  1840 fun mk_pat (c,l) =
  1841   let val L = length (binder_types (type_of c))
  1842       fun build (prfx,tag,plist) =
  1843           let val (args, plist') = chop L plist
  1844           in (prfx,tag,list_comb(c,args)::plist') end
  1845   in map build l end;
  1846 
  1847 fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
  1848   | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
  1849 
  1850 fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
  1851   | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
  1852 
  1853 
  1854 (*----------------------------------------------------------------------------
  1855  * Translation of pattern terms into nested case expressions.
  1856  *
  1857  * This performs the translation and also builds the full set of patterns.
  1858  * Thus it supports the construction of induction theorems even when an
  1859  * incomplete set of patterns is given.
  1860  *---------------------------------------------------------------------------*)
  1861 
  1862 fun mk_case ty_info ty_match usednames range_ty =
  1863  let
  1864  fun mk_case_fail s = raise TFL_ERR "mk_case" s
  1865  val fresh_var = gvvariant usednames
  1866  val divide = partition fresh_var ty_match
  1867  fun expand _ ty ((_,[]), _) = mk_case_fail"expand_var_row"
  1868    | expand constructors ty (row as ((prfx, p::rst), rhs)) =
  1869        if (is_Free p)
  1870        then let val fresh = fresh_constr ty_match ty fresh_var
  1871                 fun expnd (c,gvs) =
  1872                   let val capp = list_comb(c,gvs)
  1873                   in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
  1874                   end
  1875             in map expnd (map fresh constructors)  end
  1876        else [row]
  1877  fun mk{rows=[],...} = mk_case_fail"no rows"
  1878    | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
  1879         ([(prfx,tag,[])], tm)
  1880    | mk{path=[], rows = _::_} = mk_case_fail"blunder"
  1881    | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
  1882         mk{path = path,
  1883            rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
  1884    | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
  1885      let val (pat_rectangle,rights) = ListPair.unzip rows
  1886          val col0 = map(hd o #2) pat_rectangle
  1887      in
  1888      if (forall is_Free col0)
  1889      then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
  1890                                 (ListPair.zip (col0, rights))
  1891               val pat_rectangle' = map v_to_prfx pat_rectangle
  1892               val (pref_patl,tm) = mk{path = rstp,
  1893                                       rows = ListPair.zip (pat_rectangle',
  1894                                                            rights')}
  1895           in (map v_to_pats pref_patl, tm)
  1896           end
  1897      else
  1898      let val pty as Type (ty_name,_) = type_of p
  1899      in
  1900      case (ty_info ty_name)
  1901      of NONE => mk_case_fail("Not a known datatype: "^ty_name)
  1902       | SOME{case_const,constructors} =>
  1903         let
  1904             val case_const_name = #1(dest_Const case_const)
  1905             val nrows = maps (expand constructors pty) rows
  1906             val subproblems = divide(constructors, pty, range_ty, nrows)
  1907             val groups      = map #group subproblems
  1908             and new_formals = map #new_formals subproblems
  1909             and constructors' = map #constructor subproblems
  1910             val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
  1911                            (ListPair.zip (new_formals, groups))
  1912             val rec_calls = map mk news
  1913             val (pat_rect,dtrees) = ListPair.unzip rec_calls
  1914             val case_functions = map USyntax.list_mk_abs
  1915                                   (ListPair.zip (new_formals, dtrees))
  1916             val types = map type_of (case_functions@[u]) @ [range_ty]
  1917             val case_const' = Const(case_const_name, list_mk_type types)
  1918             val tree = list_comb(case_const', case_functions@[u])
  1919             val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
  1920         in (pat_rect1,tree)
  1921         end
  1922      end end
  1923  in mk
  1924  end;
  1925 
  1926 
  1927 (* Repeated variable occurrences in a pattern are not allowed. *)
  1928 fun FV_multiset tm =
  1929    case (USyntax.dest_term tm)
  1930      of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
  1931       | USyntax.CONST _ => []
  1932       | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
  1933       | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
  1934 
  1935 fun no_repeat_vars thy pat =
  1936  let fun check [] = true
  1937        | check (v::rst) =
  1938          if member (op aconv) rst v then
  1939             raise TFL_ERR "no_repeat_vars"
  1940                           (quote (#1 (dest_Free v)) ^
  1941                           " occurs repeatedly in the pattern " ^
  1942                           quote (Syntax.string_of_term_global thy pat))
  1943          else check rst
  1944  in check (FV_multiset pat)
  1945  end;
  1946 
  1947 fun dest_atom (Free p) = p
  1948   | dest_atom (Const p) = p
  1949   | dest_atom  _ = raise TFL_ERR "dest_atom" "function name not an identifier";
  1950 
  1951 fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
  1952 
  1953 local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
  1954       fun single [_$_] =
  1955               mk_functional_err "recdef does not allow currying"
  1956         | single [f] = f
  1957         | single fs  =
  1958               (*multiple function names?*)
  1959               if length (distinct same_name fs) < length fs
  1960               then mk_functional_err
  1961                    "The function being declared appears with multiple types"
  1962               else mk_functional_err
  1963                    (string_of_int (length fs) ^
  1964                     " distinct function names being declared")
  1965 in
  1966 fun mk_functional thy clauses =
  1967  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
  1968                    handle TERM _ => raise TFL_ERR "mk_functional"
  1969                         "recursion equations must use the = relation")
  1970      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
  1971      val atom = single (distinct (op aconv) funcs)
  1972      val (fname,ftype) = dest_atom atom
  1973      val _ = map (no_repeat_vars thy) pats
  1974      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
  1975                               map_index (fn (i, t) => (t,(i,true))) R)
  1976      val names = List.foldr Misc_Legacy.add_term_names [] R
  1977      val atype = type_of(hd pats)
  1978      and aname = singleton (Name.variant_list names) "a"
  1979      val a = Free(aname,atype)
  1980      val ty_info = Thry.match_info thy
  1981      val ty_match = Thry.match_type thy
  1982      val range_ty = type_of (hd R)
  1983      val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
  1984                                     {path=[a], rows=rows}
  1985      val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
  1986           handle Match => mk_functional_err "error in pattern-match translation"
  1987      val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
  1988      val finals = map row_of_pat patts2
  1989      val originals = map (row_of_pat o #2) rows
  1990      val _ = case (subtract (op =) finals originals)
  1991              of [] => ()
  1992           | L => mk_functional_err
  1993  ("The following clauses are redundant (covered by preceding clauses): " ^
  1994                    commas (map (fn i => string_of_int (i + 1)) L))
  1995  in {functional = Abs(Long_Name.base_name fname, ftype,
  1996                       abstract_over (atom, absfree (aname,atype) case_tm)),
  1997      pats = patts2}
  1998 end end;
  1999 
  2000 
  2001 (*----------------------------------------------------------------------------
  2002  *
  2003  *                    PRINCIPLES OF DEFINITION
  2004  *
  2005  *---------------------------------------------------------------------------*)
  2006 
  2007 
  2008 (*For Isabelle, the lhs of a definition must be a constant.*)
  2009 fun const_def sign (c, Ty, rhs) =
  2010   singleton (Syntax.check_terms (Proof_Context.init_global sign))
  2011     (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
  2012 
  2013 (*Make all TVars available for instantiation by adding a ? to the front*)
  2014 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
  2015   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
  2016   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
  2017 
  2018 local
  2019   val f_eq_wfrec_R_M =
  2020     #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec}))))
  2021   val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
  2022   val _ = dest_Free f
  2023   val (wfrec,_) = USyntax.strip_comb rhs
  2024 in
  2025 
  2026 fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
  2027   let
  2028     val def_name = Thm.def_name (Long_Name.base_name fid)
  2029     val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
  2030     val def_term = const_def thy (fid, Ty, wfrec_R_M)
  2031     val ([def], thy') =
  2032       Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
  2033   in (def, thy') end;
  2034 
  2035 end;
  2036 
  2037 
  2038 
  2039 (*---------------------------------------------------------------------------
  2040  * This structure keeps track of congruence rules that aren't derived
  2041  * from a datatype definition.
  2042  *---------------------------------------------------------------------------*)
  2043 fun extraction_thms thy =
  2044  let val {case_rewrites,case_congs} = Thry.extract_info thy
  2045  in (case_rewrites, case_congs)
  2046  end;
  2047 
  2048 
  2049 (*---------------------------------------------------------------------------
  2050  * Pair patterns with termination conditions. The full list of patterns for
  2051  * a definition is merged with the TCs arising from the user-given clauses.
  2052  * There can be fewer clauses than the full list, if the user omitted some
  2053  * cases. This routine is used to prepare input for mk_induction.
  2054  *---------------------------------------------------------------------------*)
  2055 fun merge full_pats TCs =
  2056 let fun insert (p,TCs) =
  2057       let fun insrt ((x as (h,[]))::rst) =
  2058                  if (p aconv h) then (p,TCs)::rst else x::insrt rst
  2059             | insrt (x::rst) = x::insrt rst
  2060             | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
  2061       in insrt end
  2062     fun pass ([],ptcl_final) = ptcl_final
  2063       | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
  2064 in
  2065   pass (TCs, map (fn p => (p,[])) full_pats)
  2066 end;
  2067 
  2068 
  2069 fun givens pats = map pat_of (filter given pats);
  2070 
  2071 fun post_definition ctxt meta_tflCongs (def, pats) =
  2072  let val thy = Proof_Context.theory_of ctxt
  2073      val tych = Thry.typecheck thy
  2074      val f = #lhs(USyntax.dest_eq(concl def))
  2075      val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def
  2076      val pats' = filter given pats
  2077      val given_pats = map pat_of pats'
  2078      val rows = map row_of_pat pats'
  2079      val WFR = #ant(USyntax.dest_imp(concl corollary))
  2080      val R = #Rand(USyntax.dest_comb WFR)
  2081      val corollary' = Rules.UNDISCH corollary  (* put WF R on assums *)
  2082      val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
  2083      val (case_rewrites,context_congs) = extraction_thms thy
  2084      (*case_ss causes minimal simplification: bodies of case expressions are
  2085        not simplified. Otherwise large examples (Red-Black trees) are too
  2086        slow.*)
  2087      val case_simpset =
  2088        put_simpset HOL_basic_ss ctxt
  2089           addsimps case_rewrites
  2090           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
  2091               (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
  2092      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
  2093      val extract =
  2094       Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
  2095      val (rules, TCs) = ListPair.unzip (map extract corollaries')
  2096      val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules
  2097      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
  2098      val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
  2099  in
  2100  {rules = rules1,
  2101   rows = rows,
  2102   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
  2103   TCs = TCs}
  2104  end;
  2105 
  2106 
  2107 (*----------------------------------------------------------------------------
  2108  *
  2109  *                           INDUCTION THEOREM
  2110  *
  2111  *---------------------------------------------------------------------------*)
  2112 
  2113 
  2114 (*------------------------  Miscellaneous function  --------------------------
  2115  *
  2116  *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
  2117  *     -----------------------------------------------------------
  2118  *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
  2119  *                        ...
  2120  *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
  2121  *
  2122  * This function is totally ad hoc. Used in the production of the induction
  2123  * theorem. The nchotomy theorem can have clauses that look like
  2124  *
  2125  *     ?v1..vn. z = C vn..v1
  2126  *
  2127  * in which the order of quantification is not the order of occurrence of the
  2128  * quantified variables as arguments to C. Since we have no control over this
  2129  * aspect of the nchotomy theorem, we make the correspondence explicit by
  2130  * pairing the incoming new variable with the term it gets beta-reduced into.
  2131  *---------------------------------------------------------------------------*)
  2132 
  2133 fun alpha_ex_unroll (xlist, tm) =
  2134   let val (qvars,body) = USyntax.strip_exists tm
  2135       val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
  2136       val plist = ListPair.zip (vlist, xlist)
  2137       val args = map (the o AList.lookup (op aconv) plist) qvars
  2138                    handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
  2139       fun build ex      []   = []
  2140         | build (_$rex) (v::rst) =
  2141            let val ex1 = Term.betapply(rex, v)
  2142            in  ex1 :: build ex1 rst
  2143            end
  2144      val (nex::exl) = rev (tm::build tm args)
  2145   in
  2146   (nex, ListPair.zip (args, rev exl))
  2147   end;
  2148 
  2149 
  2150 
  2151 (*----------------------------------------------------------------------------
  2152  *
  2153  *             PROVING COMPLETENESS OF PATTERNS
  2154  *
  2155  *---------------------------------------------------------------------------*)
  2156 
  2157 fun mk_case ctxt ty_info usednames =
  2158  let
  2159  val thy = Proof_Context.theory_of ctxt
  2160  val divide = ipartition (gvvariant usednames)
  2161  val tych = Thry.typecheck thy
  2162  fun tych_binding(x,y) = (tych x, tych y)
  2163  fun fail s = raise TFL_ERR "mk_case" s
  2164  fun mk{rows=[],...} = fail"no rows"
  2165    | mk{path=[], rows = [([], (thm, bindings))]} =
  2166                          Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
  2167    | mk{path = u::rstp, rows as (p::_, _)::_} =
  2168      let val (pat_rectangle,rights) = ListPair.unzip rows
  2169          val col0 = map hd pat_rectangle
  2170          val pat_rectangle' = map tl pat_rectangle
  2171      in
  2172      if (forall is_Free col0) (* column 0 is all variables *)
  2173      then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
  2174                                 (ListPair.zip (rights, col0))
  2175           in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
  2176           end
  2177      else                     (* column 0 is all constructors *)
  2178      let val Type (ty_name,_) = type_of p
  2179      in
  2180      case (ty_info ty_name)
  2181      of NONE => fail("Not a known datatype: "^ty_name)
  2182       | SOME{constructors,nchotomy} =>
  2183         let val thm' = Rules.ISPEC (tych u) nchotomy
  2184             val disjuncts = USyntax.strip_disj (concl thm')
  2185             val subproblems = divide(constructors, rows)
  2186             val groups      = map #group subproblems
  2187             and new_formals = map #new_formals subproblems
  2188             val existentials = ListPair.map alpha_ex_unroll
  2189                                    (new_formals, disjuncts)
  2190             val constraints = map #1 existentials
  2191             val vexl = map #2 existentials
  2192             fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
  2193             val news = map (fn (nf,rows,c) => {path = nf@rstp,
  2194                                                rows = map (expnd c) rows})
  2195                            (Utils.zip3 new_formals groups constraints)
  2196             val recursive_thms = map mk news
  2197             val build_exists = Library.foldr
  2198                                 (fn((x,t), th) =>
  2199                                  Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
  2200             val thms' = ListPair.map build_exists (vexl, recursive_thms)
  2201             val same_concls = Rules.EVEN_ORS thms'
  2202         in Rules.DISJ_CASESL thm' same_concls
  2203         end
  2204      end end
  2205  in mk
  2206  end;
  2207 
  2208 
  2209 fun complete_cases ctxt =
  2210  let val thy = Proof_Context.theory_of ctxt
  2211      val tych = Thry.typecheck thy
  2212      val ty_info = Thry.induct_info thy
  2213  in fn pats =>
  2214  let val names = List.foldr Misc_Legacy.add_term_names [] pats
  2215      val T = type_of (hd pats)
  2216      val aname = singleton (Name.variant_list names) "a"
  2217      val vname = singleton (Name.variant_list (aname::names)) "v"
  2218      val a = Free (aname, T)
  2219      val v = Free (vname, T)
  2220      val a_eq_v = HOLogic.mk_eq(a,v)
  2221      val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
  2222                            (Rules.REFL (tych a))
  2223      val th0 = Rules.ASSUME (tych a_eq_v)
  2224      val rows = map (fn x => ([x], (th0,[]))) pats
  2225  in
  2226  Rules.GEN ctxt (tych a)
  2227        (Rules.RIGHT_ASSOC ctxt
  2228           (Rules.CHOOSE ctxt (tych v, ex_th0)
  2229                 (mk_case ctxt ty_info (vname::aname::names)
  2230                  {path=[v], rows=rows})))
  2231  end end;
  2232 
  2233 
  2234 (*---------------------------------------------------------------------------
  2235  * Constructing induction hypotheses: one for each recursive call.
  2236  *
  2237  * Note. R will never occur as a variable in the ind_clause, because
  2238  * to do so, it would have to be from a nested definition, and we don't
  2239  * allow nested defns to have R variable.
  2240  *
  2241  * Note. When the context is empty, there can be no local variables.
  2242  *---------------------------------------------------------------------------*)
  2243 
  2244 local infix 5 ==>
  2245       fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
  2246 in
  2247 fun build_ih f (P,SV) (pat,TCs) =
  2248  let val pat_vars = USyntax.free_vars_lr pat
  2249      val globals = pat_vars@SV
  2250      fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
  2251      fun dest_TC tm =
  2252          let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
  2253              val (R,y,_) = USyntax.dest_relation R_y_pat
  2254              val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
  2255          in case cntxt
  2256               of [] => (P_y, (tm,[]))
  2257                | _  => let
  2258                     val imp = USyntax.list_mk_conj cntxt ==> P_y
  2259                     val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
  2260                     val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
  2261                     in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
  2262          end
  2263  in case TCs
  2264     of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
  2265      |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
  2266                  val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
  2267              in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
  2268              end
  2269  end
  2270 end;
  2271 
  2272 (*---------------------------------------------------------------------------
  2273  * This function makes good on the promise made in "build_ih".
  2274  *
  2275  * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",
  2276  *           TCs = TC_1[pat] ... TC_n[pat]
  2277  *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
  2278  *---------------------------------------------------------------------------*)
  2279 fun prove_case ctxt f (tm,TCs_locals,thm) =
  2280  let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
  2281      val antc = tych(#ant(USyntax.dest_imp tm))
  2282      val thm' = Rules.SPEC_ALL thm
  2283      fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
  2284      fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
  2285      fun mk_ih ((TC,locals),th2,nested) =
  2286          Rules.GENL ctxt (map tych locals)
  2287             (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
  2288              else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
  2289              else Rules.MP th2 TC)
  2290  in
  2291  Rules.DISCH antc
  2292  (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
  2293   then let val th1 = Rules.ASSUME antc
  2294            val TCs = map #1 TCs_locals
  2295            val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
  2296                             #2 o USyntax.strip_forall) TCs
  2297            val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
  2298                             TCs_locals
  2299            val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
  2300            val nlist = map nested TCs
  2301            val triples = Utils.zip3 TClist th2list nlist
  2302            val Pylist = map mk_ih triples
  2303        in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
  2304   else thm')
  2305  end;
  2306 
  2307 
  2308 (*---------------------------------------------------------------------------
  2309  *
  2310  *         x = (v1,...,vn)  |- M[x]
  2311  *    ---------------------------------------------
  2312  *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
  2313  *
  2314  *---------------------------------------------------------------------------*)
  2315 fun LEFT_ABS_VSTRUCT ctxt tych thm =
  2316   let fun CHOOSER v (tm,thm) =
  2317         let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
  2318         in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
  2319         end
  2320       val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
  2321       val {lhs,rhs} = USyntax.dest_eq veq
  2322       val L = USyntax.free_vars_lr rhs
  2323   in  #2 (fold_rev CHOOSER L (veq,thm))  end;
  2324 
  2325 
  2326 (*----------------------------------------------------------------------------
  2327  * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
  2328  *
  2329  * Instantiates tfl_wf_induct, getting Sinduct and then tries to prove
  2330  * recursion induction (Rinduct) by proving the antecedent of Sinduct from
  2331  * the antecedent of Rinduct.
  2332  *---------------------------------------------------------------------------*)
  2333 fun mk_induction ctxt {fconst, R, SV, pat_TCs_list} =
  2334 let
  2335     val thy = Proof_Context.theory_of ctxt
  2336     val tych = Thry.typecheck thy
  2337     val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct})
  2338     val (pats,TCsl) = ListPair.unzip pat_TCs_list
  2339     val case_thm = complete_cases ctxt pats
  2340     val domain = (type_of o hd) pats
  2341     val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
  2342                               [] (pats::TCsl))) "P"
  2343     val P = Free(Pname, domain --> HOLogic.boolT)
  2344     val Sinduct = Rules.SPEC (tych P) Sinduction
  2345     val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
  2346     val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
  2347     val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
  2348     val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
  2349     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
  2350     val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
  2351     val proved_cases = map (prove_case ctxt fconst) tasks
  2352     val v =
  2353       Free (singleton
  2354         (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
  2355           domain)
  2356     val vtyped = tych v
  2357     val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
  2358     val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
  2359                           (substs, proved_cases)
  2360     val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
  2361     val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
  2362     val dc = Rules.MP Sinduct dant
  2363     val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
  2364     val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
  2365     val dc' = fold_rev (Rules.GEN ctxt o tych) vars
  2366                        (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
  2367 in
  2368    Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
  2369 end
  2370 handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
  2371 
  2372 
  2373 
  2374 (*---------------------------------------------------------------------------
  2375  *
  2376  *                        POST PROCESSING
  2377  *
  2378  *---------------------------------------------------------------------------*)
  2379 
  2380 
  2381 fun simplify_induction thy hth ind =
  2382   let val tych = Thry.typecheck thy
  2383       val (asl,_) = Rules.dest_thm ind
  2384       val (_,tc_eq_tc') = Rules.dest_thm hth
  2385       val tc = USyntax.lhs tc_eq_tc'
  2386       fun loop [] = ind
  2387         | loop (asm::rst) =
  2388           if (can (Thry.match_term thy asm) tc)
  2389           then Rules.UNDISCH
  2390                  (Rules.MATCH_MP
  2391                      (Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind))
  2392                      hth)
  2393          else loop rst
  2394   in loop asl
  2395 end;
  2396 
  2397 
  2398 (*---------------------------------------------------------------------------
  2399  * The termination condition is an antecedent to the rule, and an
  2400  * assumption to the theorem.
  2401  *---------------------------------------------------------------------------*)
  2402 fun elim_tc tcthm (rule,induction) =
  2403    (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
  2404 
  2405 
  2406 fun trace_thms ctxt s L =
  2407   if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
  2408   else ();
  2409 
  2410 fun trace_cterm ctxt s ct =
  2411   if !trace then
  2412     writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
  2413   else ();
  2414 
  2415 
  2416 fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
  2417   let
  2418     val thy = Proof_Context.theory_of ctxt;
  2419     val tych = Thry.typecheck thy;
  2420 
  2421    (*---------------------------------------------------------------------
  2422     * Attempt to eliminate WF condition. It's the only assumption of rules
  2423     *---------------------------------------------------------------------*)
  2424     val (rules1,induction1)  =
  2425        let val thm =
  2426         Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
  2427        in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
  2428        end handle Utils.ERR _ => (rules,induction);
  2429 
  2430    (*----------------------------------------------------------------------
  2431     * The termination condition (tc) is simplified to |- tc = tc' (there
  2432     * might not be a change!) and then 3 attempts are made:
  2433     *
  2434     *   1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise,
  2435     *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
  2436     *   3. replace tc by tc' in both the rules and the induction theorem.
  2437     *---------------------------------------------------------------------*)
  2438 
  2439    fun simplify_tc tc (r,ind) =
  2440        let val tc1 = tych tc
  2441            val _ = trace_cterm ctxt "TC before simplification: " tc1
  2442            val tc_eq = simplifier tc1
  2443            val _ = trace_thms ctxt "result: " [tc_eq]
  2444        in
  2445        elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
  2446        handle Utils.ERR _ =>
  2447         (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
  2448                   (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
  2449                            terminator)))
  2450                  (r,ind)
  2451          handle Utils.ERR _ =>
  2452           (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
  2453            simplify_induction thy tc_eq ind))
  2454        end
  2455 
  2456    (*----------------------------------------------------------------------
  2457     * Nested termination conditions are harder to get at, since they are
  2458     * left embedded in the body of the function (and in induction
  2459     * theorem hypotheses). Our "solution" is to simplify them, and try to
  2460     * prove termination, but leave the application of the resulting theorem
  2461     * to a higher level. So things go much as in "simplify_tc": the
  2462     * termination condition (tc) is simplified to |- tc = tc' (there might
  2463     * not be a change) and then 2 attempts are made:
  2464     *
  2465     *   1. if |- tc = T, then return |- tc; otherwise,
  2466     *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
  2467     *   3. return |- tc = tc'
  2468     *---------------------------------------------------------------------*)
  2469    fun simplify_nested_tc tc =
  2470       let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
  2471       in
  2472       Rules.GEN_ALL ctxt
  2473        (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
  2474         handle Utils.ERR _ =>
  2475           (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
  2476                       (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
  2477                                terminator))
  2478             handle Utils.ERR _ => tc_eq))
  2479       end
  2480 
  2481    (*-------------------------------------------------------------------
  2482     * Attempt to simplify the termination conditions in each rule and
  2483     * in the induction theorem.
  2484     *-------------------------------------------------------------------*)
  2485    fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
  2486    fun loop ([],extras,R,ind) = (rev R, ind, extras)
  2487      | loop ((r,ftcs)::rst, nthms, R, ind) =
  2488         let val tcs = #1(strip_imp (concl r))
  2489             val extra_tcs = subtract (op aconv) tcs ftcs
  2490             val extra_tc_thms = map simplify_nested_tc extra_tcs
  2491             val (r1,ind1) = fold simplify_tc tcs (r,ind)
  2492             val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
  2493         in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
  2494         end
  2495    val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
  2496    val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
  2497 in
  2498   {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
  2499 end;
  2500 
  2501 end;
  2502 
  2503 
  2504 
  2505 (*** second part of main module (postprocessing of TFL definitions) ***)
  2506 
  2507 structure Tfl: TFL =
  2508 struct
  2509 
  2510 (* misc *)
  2511 
  2512 (*---------------------------------------------------------------------------
  2513  * Extract termination goals so that they can be put it into a goalstack, or
  2514  * have a tactic directly applied to them.
  2515  *--------------------------------------------------------------------------*)
  2516 fun termination_goals rules =
  2517     map (Type.legacy_freeze o HOLogic.dest_Trueprop)
  2518       (fold_rev (union (op aconv) o Thm.prems_of) rules []);
  2519 
  2520 (*---------------------------------------------------------------------------
  2521  * Three postprocessors are applied to the definition.  It
  2522  * attempts to prove wellfoundedness of the given relation, simplifies the
  2523  * non-proved termination conditions, and finally attempts to prove the
  2524  * simplified termination conditions.
  2525  *--------------------------------------------------------------------------*)
  2526 fun std_postprocessor ctxt strict wfs =
  2527   Prim.postprocess ctxt strict
  2528    {wf_tac = REPEAT (ares_tac ctxt wfs 1),
  2529     terminator =
  2530       asm_simp_tac ctxt 1
  2531       THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
  2532         fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
  2533     simplifier = Rules.simpl_conv ctxt []};
  2534 
  2535 
  2536 
  2537 val concl = #2 o Rules.dest_thm;
  2538 
  2539 (*---------------------------------------------------------------------------
  2540  * Postprocess a definition made by "define". This is a separate stage of
  2541  * processing from the definition stage.
  2542  *---------------------------------------------------------------------------*)
  2543 local
  2544 
  2545 (* The rest of these local definitions are for the tricky nested case *)
  2546 val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
  2547 
  2548 fun id_thm th =
  2549    let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
  2550    in lhs aconv rhs end
  2551    handle Utils.ERR _ => false;
  2552 
  2553 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
  2554 fun mk_meta_eq r =
  2555   (case Thm.concl_of r of
  2556      Const(@{const_name Pure.eq},_)$_$_ => r
  2557   |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
  2558   |   _ => r RS P_imp_P_eq_True)
  2559 
  2560 (*Is this the best way to invoke the simplifier??*)
  2561 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
  2562 
  2563 fun join_assums ctxt th =
  2564   let val tych = Thm.cterm_of ctxt
  2565       val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
  2566       val cntxtl = (#1 o USyntax.strip_imp) lhs  (* cntxtl should = cntxtr *)
  2567       val cntxtr = (#1 o USyntax.strip_imp) rhs  (* but union is solider *)
  2568       val cntxt = union (op aconv) cntxtl cntxtr
  2569   in
  2570     Rules.GEN_ALL ctxt
  2571       (Rules.DISCH_ALL
  2572          (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
  2573   end
  2574   val gen_all = USyntax.gen_all
  2575 in
  2576 fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
  2577   let
  2578     val _ = writeln "Proving induction theorem ..."
  2579     val ind =
  2580       Prim.mk_induction ctxt
  2581         {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
  2582     val _ = writeln "Postprocessing ...";
  2583     val {rules, induction, nested_tcs} =
  2584       std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
  2585   in
  2586   case nested_tcs
  2587   of [] => {induction=induction, rules=rules,tcs=[]}
  2588   | L  => let val _ = writeln "Simplifying nested TCs ..."
  2589               val (solved,simplified,stubborn) =
  2590                fold_rev (fn th => fn (So,Si,St) =>
  2591                      if (id_thm th) then (So, Si, th::St) else
  2592                      if (solved th) then (th::So, Si, St)
  2593                      else (So, th::Si, St)) nested_tcs ([],[],[])
  2594               val simplified' = map (join_assums ctxt) simplified
  2595               val dummy = (Prim.trace_thms ctxt "solved =" solved;
  2596                            Prim.trace_thms ctxt "simplified' =" simplified')
  2597               val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
  2598               val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
  2599               val induction' = rewr induction
  2600               val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
  2601               val rules'     = rewr rules
  2602               val _ = writeln "... Postprocessing finished";
  2603           in
  2604           {induction = induction',
  2605                rules = rules',
  2606                  tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
  2607                            (simplified@stubborn)}
  2608           end
  2609   end;
  2610 
  2611 
  2612 (*lcp: curry the predicate of the induction rule*)
  2613 fun curry_rule ctxt rl =
  2614   Split_Rule.split_rule_var ctxt (Term.head_of (HOLogic.dest_Trueprop (Thm.concl_of rl))) rl;
  2615 
  2616 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
  2617 fun meta_outer ctxt =
  2618   curry_rule ctxt o Drule.export_without_context o
  2619   rule_by_tactic ctxt
  2620     (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
  2621 
  2622 (*Strip off the outer !P*)
  2623 val spec'=
  2624   Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
  2625 
  2626 fun simplify_defn ctxt strict congs wfs pats def0 =
  2627   let
  2628     val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
  2629     val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
  2630     val {lhs=f,rhs} = USyntax.dest_eq (concl def)
  2631     val (_,[R,_]) = USyntax.strip_comb rhs
  2632     val _ = Prim.trace_thms ctxt "congs =" congs
  2633     (*the next step has caused simplifier looping in some cases*)
  2634     val {induction, rules, tcs} =
  2635       proof_stage ctxt strict wfs
  2636        {f = f, R = R, rules = rules,
  2637         full_pats_TCs = full_pats_TCs,
  2638         TCs = TCs}
  2639     val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
  2640                       (Rules.CONJUNCTS rules)
  2641   in
  2642     {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
  2643      rules = ListPair.zip(rules', rows),
  2644      tcs = (termination_goals rules') @ tcs}
  2645   end
  2646   handle Utils.ERR {mesg,func,module} =>
  2647     error (mesg ^ "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
  2648 
  2649 
  2650 (* Derive the initial equations from the case-split rules to meet the
  2651 users specification of the recursive function. *)
  2652 local
  2653   fun get_related_thms i =
  2654       map_filter ((fn (r,x) => if x = i then SOME r else NONE));
  2655 
  2656   fun solve_eq _ (_, [], _) =  error "derive_init_eqs: missing rules"
  2657     | solve_eq _ (_, [a], i) = [(a, i)]
  2658     | solve_eq ctxt (th, splitths, i) =
  2659       (writeln "Proving unsplit equation...";
  2660       [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
  2661           (CaseSplit.splitto ctxt splitths th), i)])
  2662       handle ERROR s =>
  2663              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
  2664 in
  2665 fun derive_init_eqs ctxt rules eqs =
  2666   map (Thm.trivial o Thm.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
  2667   |> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
  2668   |> flat;
  2669 end;
  2670 
  2671 
  2672 (*---------------------------------------------------------------------------
  2673  * Defining a function with an associated termination relation.
  2674  *---------------------------------------------------------------------------*)
  2675 fun define_i strict congs wfs fid R eqs ctxt =
  2676   let
  2677     val thy = Proof_Context.theory_of ctxt
  2678     val {functional, pats} = Prim.mk_functional thy eqs
  2679     val (def, thy') = Prim.wfrec_definition0 fid R functional thy
  2680     val ctxt' = Proof_Context.transfer thy' ctxt
  2681     val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
  2682     val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs pats def
  2683     val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
  2684   in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
  2685 
  2686 fun define strict congs wfs fid R seqs ctxt =
  2687   define_i strict congs wfs fid
  2688     (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
  2689       handle Utils.ERR {mesg,...} => error mesg;
  2690 
  2691 end;
  2692 
  2693 end;
  2694 
  2695 
  2696 
  2697 (*** wrappers for Isar ***)
  2698 
  2699 (** recdef hints **)
  2700 
  2701 (* type hints *)
  2702 
  2703 type hints = {simps: thm list, congs: (string * thm) list, wfs: thm list};
  2704 
  2705 fun mk_hints (simps, congs, wfs) = {simps = simps, congs = congs, wfs = wfs}: hints;
  2706 fun map_hints f ({simps, congs, wfs}: hints) = mk_hints (f (simps, congs, wfs));
  2707 
  2708 fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs));
  2709 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
  2710 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
  2711 
  2712 
  2713 (* congruence rules *)
  2714 
  2715 local
  2716 
  2717 val cong_head =
  2718   fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
  2719 
  2720 fun prep_cong raw_thm =
  2721   let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
  2722 
  2723 in
  2724 
  2725 fun add_cong raw_thm congs =
  2726   let
  2727     val (c, thm) = prep_cong raw_thm;
  2728     val _ = if AList.defined (op =) congs c
  2729       then warning ("Overwriting recdef congruence rule for " ^ quote c)
  2730       else ();
  2731   in AList.update (op =) (c, thm) congs end;
  2732 
  2733 fun del_cong raw_thm congs =
  2734   let
  2735     val (c, _) = prep_cong raw_thm;
  2736     val _ = if AList.defined (op =) congs c
  2737       then ()
  2738       else warning ("No recdef congruence rule for " ^ quote c);
  2739   in AList.delete (op =) c congs end;
  2740 
  2741 end;
  2742 
  2743 
  2744 
  2745 (** global and local recdef data **)
  2746 
  2747 (* theory data *)
  2748 
  2749 type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
  2750 
  2751 structure Data = Generic_Data
  2752 (
  2753   type T = recdef_info Symtab.table * hints;
  2754   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
  2755   val extend = I;
  2756   fun merge
  2757    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
  2758     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
  2759       (Symtab.merge (K true) (tab1, tab2),
  2760         mk_hints (Thm.merge_thms (simps1, simps2),
  2761           AList.merge (op =) (K true) (congs1, congs2),
  2762           Thm.merge_thms (wfs1, wfs2)));
  2763 );
  2764 
  2765 val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory;
  2766 
  2767 fun put_recdef name info =
  2768   (Context.theory_map o Data.map o apfst) (fn tab =>
  2769     Symtab.update_new (name, info) tab
  2770       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name));
  2771 
  2772 val get_hints = #2 o Data.get o Context.Proof;
  2773 val map_hints = Data.map o apsnd;
  2774 
  2775 
  2776 (* attributes *)
  2777 
  2778 fun attrib f = Thm.declaration_attribute (map_hints o f);
  2779 
  2780 val simp_add = attrib (map_simps o Thm.add_thm);
  2781 val simp_del = attrib (map_simps o Thm.del_thm);
  2782 val cong_add = attrib (map_congs o add_cong);
  2783 val cong_del = attrib (map_congs o del_cong);
  2784 val wf_add = attrib (map_wfs o Thm.add_thm);
  2785 val wf_del = attrib (map_wfs o Thm.del_thm);
  2786 
  2787 
  2788 (* modifiers *)
  2789 
  2790 val recdef_simpN = "recdef_simp";
  2791 val recdef_congN = "recdef_cong";
  2792 val recdef_wfN = "recdef_wf";
  2793 
  2794 val recdef_modifiers =
  2795  [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
  2796   Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
  2797   Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
  2798   Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
  2799   Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
  2800   Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
  2801   Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
  2802   Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
  2803   Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
  2804   Clasimp.clasimp_modifiers;
  2805 
  2806 
  2807 
  2808 (** prepare hints **)
  2809 
  2810 fun prepare_hints opt_src ctxt =
  2811   let
  2812     val ctxt' =
  2813       (case opt_src of
  2814         NONE => ctxt
  2815       | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt));
  2816     val {simps, congs, wfs} = get_hints ctxt';
  2817     val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong};
  2818   in ((rev (map snd congs), wfs), ctxt'') end;
  2819 
  2820 fun prepare_hints_i () ctxt =
  2821   let
  2822     val {simps, congs, wfs} = get_hints ctxt;
  2823     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
  2824   in ((rev (map snd congs), wfs), ctxt') end;
  2825 
  2826 
  2827 
  2828 (** add_recdef(_i) **)
  2829 
  2830 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
  2831   let
  2832     val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
  2833 
  2834     val name = Sign.intern_const thy raw_name;
  2835     val bname = Long_Name.base_name name;
  2836     val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
  2837 
  2838     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
  2839     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
  2840 
  2841     val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy);
  2842     (*We must remove imp_cong to prevent looping when the induction rule
  2843       is simplified. Many induction rules have nested implications that would
  2844       give rise to looping conditional rewriting.*)
  2845     val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) =
  2846       tfl_fn not_permissive congs wfs name R eqs ctxt;
  2847     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
  2848     val simp_att =
  2849       if null tcs then [Simplifier.simp_add,
  2850         Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
  2851       else [];
  2852     val ((simps' :: rules', [induct']), thy2) =
  2853       Proof_Context.theory_of ctxt1
  2854       |> Sign.add_path bname
  2855       |> Global_Theory.add_thmss
  2856         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
  2857       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
  2858       ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
  2859     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
  2860     val thy3 =
  2861       thy2
  2862       |> put_recdef name result
  2863       |> Sign.parent_path;
  2864   in (thy3, result) end;
  2865 
  2866 val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
  2867 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
  2868 
  2869 
  2870 
  2871 (** package setup **)
  2872 
  2873 (* setup theory *)
  2874 
  2875 val _ =
  2876   Theory.setup
  2877    (Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
  2878       "declaration of recdef simp rule" #>
  2879     Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
  2880       "declaration of recdef cong rule" #>
  2881     Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
  2882       "declaration of recdef wf rule");
  2883 
  2884 
  2885 (* outer syntax *)
  2886 
  2887 val hints =
  2888   @{keyword "("} |--
  2889     Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
  2890   >> uncurry Token.src;
  2891 
  2892 val recdef_decl =
  2893   Scan.optional
  2894     (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
  2895   Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
  2896     -- Scan.option hints
  2897   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
  2898 
  2899 val _ =
  2900   Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
  2901     (recdef_decl >> Toplevel.theory);
  2902 
  2903 end;