1 theory LamTest

     2 imports "../Nominal2" 

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype lam =

     8   Var "name"

     9 | App "lam" "lam"

    10 | Lam x::"name" l::"lam"  bind x in l

    11 

    12 

    13 ML {*

    14 

    15 val trace = Unsynchronized.ref false

    16 fun trace_msg msg = if ! trace then tracing (msg ()) else ()

    17 

    18 val boolT = HOLogic.boolT

    19 val mk_eq = HOLogic.mk_eq

    20 

    21 open Function_Lib

    22 open Function_Common

    23 

    24 datatype globals = Globals of

    25  {fvar: term,

    26   domT: typ,

    27   ranT: typ,

    28   h: term,

    29   y: term,

    30   x: term,

    31   z: term,

    32   a: term,

    33   P: term,

    34   D: term,

    35   Pbool:term}

    36 

    37 datatype rec_call_info = RCInfo of

    38  {RIvs: (string * typ) list,  (* Call context: fixes and assumes *)

    39   CCas: thm list,

    40   rcarg: term,                 (* The recursive argument *)

    41   llRI: thm,

    42   h_assum: term}

    43 

    44 

    45 datatype clause_context = ClauseContext of

    46  {ctxt : Proof.context,

    47   qs : term list,

    48   gs : term list,

    49   lhs: term,

    50   rhs: term,

    51   cqs: cterm list,

    52   ags: thm list,

    53   case_hyp : thm}

    54 

    55 

    56 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =

    57   ClauseContext { ctxt = ProofContext.transfer thy ctxt,

    58     qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }

    59 

    60 

    61 datatype clause_info = ClauseInfo of

    62  {no: int,

    63   qglr : ((string * typ) list * term list * term * term),

    64   cdata : clause_context,

    65   tree: Function_Ctx_Tree.ctx_tree,

    66   lGI: thm,

    67   RCs: rec_call_info list}

    68 *}

    69 

    70 thm accp_induct_rule

    71 

    72 ML {*

    73 (* Theory dependencies. *)

    74 val acc_induct_rule = @{thm accp_induct_rule}

    75 

    76 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}

    77 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}

    78 val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}

    79 

    80 val acc_downward = @{thm accp_downward}

    81 val accI = @{thm accp.accI}

    82 val case_split = @{thm HOL.case_split}

    83 val fundef_default_value = @{thm FunDef.fundef_default_value}

    84 val not_acc_down = @{thm not_accp_down}

    85 *}

    86 

    87 

    88 ML {*

    89 fun find_calls tree =

    90   let

    91     fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =

    92       ([], (fixes, assumes, arg) :: xs)

    93       | add_Ri _ _ _ _ = raise Match

    94   in

    95     rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])

    96   end

    97 *}

    98 

    99 ML {*

   100 fun mk_eqvt_at (f_trm, arg_trm) =

   101   let

   102     val f_ty = fastype_of f_trm

   103     val arg_ty = domain_type f_ty

   104   in

   105     Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm

   106     |> HOLogic.mk_Trueprop

   107   end

   108 *}

   109 

   110 ML {*

   111 fun find_calls2 f t = 

   112   let

   113     fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)

   114       | aux (Abs (_, _, t)) = aux t 

   115       | aux _ = I

   116   in

   117     aux t []

   118   end 

   119 *}

   120 

   121 

   122 ML {*

   123 (** building proof obligations *)

   124 

   125 fun mk_compat_proof_obligations domT ranT fvar f glrs =

   126   let

   127     fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =

   128       let

   129         val shift = incr_boundvars (length qs')

   130 

   131         val RCs_rhs  = find_calls2 fvar rhs

   132         val RCs_rhs' = find_calls2 fvar rhs'

   133       in

   134         Logic.mk_implies

   135           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),

   136             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))

   137         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')

   138         |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* HERE *) 

   139         (*|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')*) (* HERE *) 

   140         |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')

   141         |> curry abstract_over fvar

   142         |> curry subst_bound f

   143       end

   144   in

   145     map mk_impl (unordered_pairs glrs)

   146   end

   147 *}

   148 

   149 ML {*

   150 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =

   151   let

   152     fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =

   153       HOLogic.mk_Trueprop Pbool

   154       |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))

   155       |> fold_rev (curry Logic.mk_implies) gs

   156       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)

   157   in

   158     HOLogic.mk_Trueprop Pbool

   159     |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)

   160     |> mk_forall_rename ("x", x)

   161     |> mk_forall_rename ("P", Pbool)

   162   end

   163 *}

   164 

   165 (** making a context with it's own local bindings **)

   166 ML {*

   167 

   168 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =

   169   let

   170     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt

   171       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs

   172 

   173     val thy = ProofContext.theory_of ctxt'

   174 

   175     fun inst t = subst_bounds (rev qs, t)

   176     val gs = map inst pre_gs

   177     val lhs = inst pre_lhs

   178     val rhs = inst pre_rhs

   179 

   180     val cqs = map (cterm_of thy) qs

   181     val ags = map (Thm.assume o cterm_of thy) gs

   182 

   183     val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))

   184   in

   185     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,

   186       cqs = cqs, ags = ags, case_hyp = case_hyp }

   187   end

   188 *}

   189 

   190 ML {*

   191 (* lowlevel term function. FIXME: remove *)

   192 fun abstract_over_list vs body =

   193   let

   194     fun abs lev v tm =

   195       if v aconv tm then Bound lev

   196       else

   197         (case tm of

   198           Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)

   199         | t $ u => abs lev v t $ abs lev v u

   200         | t => t)

   201   in

   202     fold_index (fn (i, v) => fn t => abs i v t) vs body

   203   end

   204 

   205 

   206 

   207 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =

   208   let

   209     val Globals {h, ...} = globals

   210 

   211     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata

   212     val cert = Thm.cterm_of (ProofContext.theory_of ctxt)

   213 

   214     (* Instantiate the GIntro thm with "f" and import into the clause context. *)

   215     val lGI = GIntro_thm

   216       |> Thm.forall_elim (cert f)

   217       |> fold Thm.forall_elim cqs

   218       |> fold Thm.elim_implies ags

   219 

   220     fun mk_call_info (rcfix, rcassm, rcarg) RI =

   221       let

   222         val llRI = RI

   223           |> fold Thm.forall_elim cqs

   224           |> fold (Thm.forall_elim o cert o Free) rcfix

   225           |> fold Thm.elim_implies ags

   226           |> fold Thm.elim_implies rcassm

   227 

   228         val h_assum =

   229           HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))

   230           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm

   231           |> fold_rev (Logic.all o Free) rcfix

   232           |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []

   233           |> abstract_over_list (rev qs)

   234       in

   235         RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}

   236       end

   237 

   238     val RC_infos = map2 mk_call_info RCs RIntro_thms

   239   in

   240     ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,

   241       tree=tree}

   242   end

   243 *}

   244 

   245 ML {*

   246 fun store_compat_thms 0 thms = []

   247   | store_compat_thms n thms =

   248   let

   249     val (thms1, thms2) = chop n thms

   250   in

   251     (thms1 :: store_compat_thms (n - 1) thms2)

   252   end

   253 *}

   254 

   255 ML {*

   256 (* expects i <= j *)

   257 fun lookup_compat_thm i j cts =

   258   nth (nth cts (i - 1)) (j - i)

   259 

   260 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)

   261 (* if j < i, then turn around *)

   262 fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =

   263   let

   264     val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi

   265     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj

   266 

   267     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))

   268   in if j < i then

   269     let

   270       val compat = lookup_compat_thm j i cts

   271     in

   272       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)

   273       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)

   274       |> fold Thm.elim_implies (rev eqvtsj) (* HERE *)

   275       |> fold Thm.elim_implies agsj

   276       |> fold Thm.elim_implies agsi

   277       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)

   278     end

   279     else

   280     let

   281       val compat = lookup_compat_thm i j cts

   282     in

   283       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)

   284       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)

   285       |> fold Thm.elim_implies (rev eqvtsi)  (* HERE *)

   286       |> fold Thm.elim_implies agsi

   287       |> fold Thm.elim_implies agsj

   288       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)

   289       |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)

   290     end

   291   end

   292 *}

   293 

   294 

   295 ML {*

   296 (* Generates the replacement lemma in fully quantified form. *)

   297 fun mk_replacement_lemma thy h ih_elim clause =

   298   let

   299     val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...},

   300       RCs, tree, ...} = clause

   301     local open Conv in

   302       val ih_conv = arg1_conv o arg_conv o arg_conv

   303     end

   304 

   305     val ih_elim_case =

   306       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim

   307 

   308     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs

   309     val h_assums = map (fn RCInfo {h_assum, ...} =>

   310       Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs

   311 

   312     val (eql, _) =

   313       Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree

   314 

   315     val replace_lemma = (eql RS meta_eq_to_obj_eq)

   316       |> Thm.implies_intr (cprop_of case_hyp)

   317       |> fold_rev (Thm.implies_intr o cprop_of) h_assums

   318       |> fold_rev (Thm.implies_intr o cprop_of) ags

   319       |> fold_rev Thm.forall_intr cqs

   320       |> Thm.close_derivation

   321   in

   322     replace_lemma

   323   end

   324 *}

   325 

   326 ML {*

   327 fun mk_eqvt_lemma thy ih_eqvt clause =

   328   let

   329     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause

   330 

   331     local open Conv in

   332       val ih_conv = arg1_conv o arg_conv o arg_conv

   333     end

   334 

   335     val ih_eqvt_case =

   336       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt

   337 

   338     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 

   339         (llRI RS ih_eqvt_case)

   340         |> fold_rev (Thm.implies_intr o cprop_of) CCas

   341         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs

   342   in

   343     map prep_eqvt RCs

   344     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)

   345     |> map (Thm.implies_intr (cprop_of case_hyp))

   346     |> map (fold_rev Thm.forall_intr cqs)

   347     |> map (Thm.close_derivation) 

   348   end

   349 *}

   350 

   351 ML {*

   352 fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =

   353   let

   354     val Globals {h, y, x, fvar, ...} = globals

   355     val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 

   356       ags = agsi, ...}, ...} = clausei

   357     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej

   358 

   359     val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =

   360       mk_clause_context x ctxti cdescj 

   361 

   362     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'

   363 

   364     val Ghsj' = map 

   365       (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj

   366 

   367     val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))

   368     val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))

   369        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 

   370 

   371     val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']

   372 

   373     val RLj_import = RLj

   374       |> fold Thm.forall_elim cqsj'

   375       |> fold Thm.elim_implies agsj'

   376       |> fold Thm.elim_implies Ghsj'

   377 

   378     val eqvtsi = nth eqvts (i - 1)

   379       |> map (fold Thm.forall_elim cqsi)

   380       |> map (fold Thm.elim_implies [case_hyp])

   381       |> map (fold Thm.elim_implies agsi)

   382 

   383     val eqvtsj = nth eqvts (j - 1)

   384       |> map (fold Thm.forall_elim cqsj')

   385       |> map (fold Thm.elim_implies [case_hypj'])

   386       |> map (fold Thm.elim_implies agsj')

   387 

   388     val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj

   389 

   390   in

   391     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)

   392     |> Thm.implies_elim RLj_import

   393       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)

   394     |> (fn it => trans OF [it, compat])

   395       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)

   396     |> (fn it => trans OF [y_eq_rhsj'h, it])

   397       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)

   398     |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'

   399     |> fold_rev (Thm.implies_intr o cprop_of) agsj'

   400       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)

   401     |> Thm.implies_intr (cprop_of y_eq_rhsj'h)

   402     |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')

   403     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')

   404   end

   405 *}

   406 

   407 

   408 ML {*

   409 fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =

   410   let

   411     val Globals {x, y, ranT, fvar, ...} = globals

   412     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei

   413     val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs

   414 

   415     val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro

   416 

   417     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 

   418         (llRI RS ih_intro_case)

   419         |> fold_rev (Thm.implies_intr o cprop_of) CCas

   420         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs

   421 

   422     val existence = fold (curry op COMP o prep_RC) RCs lGI

   423 

   424     val P = cterm_of thy (mk_eq (y, rhsC))

   425     val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))

   426 

   427     val unique_clauses =

   428       map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems

   429 

   430     fun elim_implies_eta A AB =

   431       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single

   432 

   433     val uniqueness = G_cases

   434       |> Thm.forall_elim (cterm_of thy lhs)

   435       |> Thm.forall_elim (cterm_of thy y)

   436       |> Thm.forall_elim P

   437       |> Thm.elim_implies G_lhs_y

   438       |> fold elim_implies_eta unique_clauses

   439       |> Thm.implies_intr (cprop_of G_lhs_y)

   440       |> Thm.forall_intr (cterm_of thy y)

   441 

   442     val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)

   443 

   444     val exactly_one =

   445       ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]

   446       |> curry (op COMP) existence

   447       |> curry (op COMP) uniqueness

   448       |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])

   449       |> Thm.implies_intr (cprop_of case_hyp)

   450       |> fold_rev (Thm.implies_intr o cprop_of) ags

   451       |> fold_rev Thm.forall_intr cqs

   452 

   453     val function_value =

   454       existence

   455       |> Thm.implies_intr ihyp

   456       |> Thm.implies_intr (cprop_of case_hyp)

   457       |> Thm.forall_intr (cterm_of thy x)

   458       |> Thm.forall_elim (cterm_of thy lhs)

   459       |> curry (op RS) refl

   460   in

   461     (exactly_one, function_value)

   462   end

   463 *}

   464 

   465 

   466 ML {*

   467 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =

   468   let

   469     val Globals {h, domT, ranT, x, ...} = globals

   470     val thy = ProofContext.theory_of ctxt

   471 

   472     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)

   473     val ihyp = Term.all domT $ Abs ("z", domT,

   474       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),

   475         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $

   476           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))

   477       |> cterm_of thy

   478 

   479     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0

   480     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)

   481     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)

   482       |> instantiate' [] [NONE, SOME (cterm_of thy h)]

   483     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))

   484 

   485     val _ = trace_msg (K "Proving Replacement lemmas...")

   486     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses

   487 

   488     val _ = trace_msg (K "Proving Equivariance lemmas...")

   489     val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses

   490 

   491     val _ = trace_msg (K "Proving cases for unique existence...")

   492     val (ex1s, values) =

   493       split_list (map (mk_uniqueness_case thy globals G f 

   494         ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)

   495      

   496     val _ = trace_msg (K "Proving: Graph is a function")

   497     val graph_is_function = complete

   498       |> Thm.forall_elim_vars 0

   499       |> fold (curry op COMP) ex1s

   500       |> Thm.implies_intr (ihyp)

   501       |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))

   502       |> Thm.forall_intr (cterm_of thy x)

   503       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)

   504       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)

   505 

   506     val goalstate =  Conjunction.intr graph_is_function complete

   507       |> Thm.close_derivation

   508       |> Goal.protect

   509       |> fold_rev (Thm.implies_intr o cprop_of) compat

   510       |> Thm.implies_intr (cprop_of complete)

   511   in

   512     (goalstate, values)

   513   end

   514 *}

   515 

   516 

   517 ML {*

   518 (* wrapper -- restores quantifiers in rule specifications *)

   519 fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy =

   520   let

   521     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =

   522       lthy

   523       |> Local_Theory.conceal 

   524       |> Inductive.add_inductive_i

   525           {quiet_mode = true,

   526             verbose = ! trace,

   527             alt_name = Binding.empty,

   528             coind = false,

   529             no_elim = false,

   530             no_ind = false,

   531             skip_mono = true,

   532             fork_mono = false}

   533           [binding] (* relation *)

   534           [] (* no parameters *)

   535           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)

   536           [] (* no special monos *)

   537       ||> Local_Theory.restore_naming lthy

   538 

   539     val eqvt_thm' = 

   540       if eqvt_flag = false then NONE

   541       else 

   542         let

   543           val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy

   544         in

   545           SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})

   546         end

   547 

   548     val cert = cterm_of (ProofContext.theory_of lthy)

   549     fun requantify orig_intro thm =

   550       let

   551         val (qs, t) = dest_all_all orig_intro

   552         val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)

   553         val vars = Term.add_vars (prop_of thm) [] |> rev

   554         val varmap = AList.lookup (op =) (frees ~~ map fst vars)

   555           #> the_default ("",0)

   556       in

   557         fold_rev (fn Free (n, T) =>

   558           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm

   559       end

   560   in

   561     ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy)

   562   end

   563 *}

   564 

   565 ML {*

   566 fun define_graph Gname fvar domT ranT clauses RCss lthy =

   567   let

   568     val GT = domT --> ranT --> boolT

   569     val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)

   570 

   571     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =

   572       let

   573         fun mk_h_assm (rcfix, rcassm, rcarg) =

   574           HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))

   575           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm

   576           |> fold_rev (Logic.all o Free) rcfix

   577       in

   578         HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)

   579         |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs

   580         |> fold_rev (curry Logic.mk_implies) gs

   581         |> fold_rev Logic.all (fvar :: qs)

   582       end

   583 

   584     val G_intros = map2 mk_GIntro clauses RCss

   585   in

   586     inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy

   587   end

   588 *}

   589 

   590 ML {*

   591 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =

   592   let

   593     val f_def =

   594       Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 

   595         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))

   596       |> Syntax.check_term lthy

   597   in

   598     Local_Theory.define

   599       ((Binding.name (function_name fname), mixfix),

   600         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy

   601   end

   602 

   603 fun define_recursion_relation Rname domT qglrs clauses RCss lthy =

   604   let

   605     val RT = domT --> domT --> boolT

   606     val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)

   607 

   608     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =

   609       HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)

   610       |> fold_rev (curry Logic.mk_implies o prop_of) rcassm

   611       |> fold_rev (curry Logic.mk_implies) gs

   612       |> fold_rev (Logic.all o Free) rcfix

   613       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)

   614       (* "!!qs xs. CS ==> G => (r, lhs) : R" *)

   615 

   616     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss

   617 

   618     val ((R, RIntro_thms, R_elim, _, _), lthy) =

   619       inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy

   620   in

   621     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)

   622   end

   623 

   624 

   625 fun fix_globals domT ranT fvar ctxt =

   626   let

   627     val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes

   628       ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt

   629   in

   630     (Globals {h = Free (h, domT --> ranT),

   631       y = Free (y, ranT),

   632       x = Free (x, domT),

   633       z = Free (z, domT),

   634       a = Free (a, domT),

   635       D = Free (D, domT --> boolT),

   636       P = Free (P, domT --> boolT),

   637       Pbool = Free (Pbool, boolT),

   638       fvar = fvar,

   639       domT = domT,

   640       ranT = ranT},

   641     ctxt')

   642   end

   643 

   644 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =

   645   let

   646     fun inst_term t = subst_bound(f, abstract_over (fvar, t))

   647   in

   648     (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)

   649   end

   650 

   651 

   652 

   653 (**********************************************************

   654  *                   PROVING THE RULES

   655  **********************************************************)

   656 

   657 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =

   658   let

   659     val Globals {domT, z, ...} = globals

   660 

   661     fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =

   662       let

   663         val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)

   664         val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)

   665       in

   666         ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))

   667         |> (fn it => it COMP graph_is_function)

   668         |> Thm.implies_intr z_smaller

   669         |> Thm.forall_intr (cterm_of thy z)

   670         |> (fn it => it COMP valthm)

   671         |> Thm.implies_intr lhs_acc

   672         |> asm_simplify (HOL_basic_ss addsimps [f_iff])

   673         |> fold_rev (Thm.implies_intr o cprop_of) ags

   674         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

   675       end

   676   in

   677     map2 mk_psimp clauses valthms

   678   end

   679 

   680 

   681 (** Induction rule **)

   682 

   683 

   684 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}

   685 

   686 

   687 fun mk_partial_induct_rule thy globals R complete_thm clauses =

   688   let

   689     val Globals {domT, x, z, a, P, D, ...} = globals

   690     val acc_R = mk_acc domT R

   691 

   692     val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))

   693     val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))

   694 

   695     val D_subset = cterm_of thy (Logic.all x

   696       (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))

   697 

   698     val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)

   699       Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),

   700         Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),

   701           HOLogic.mk_Trueprop (D $ z)))))

   702       |> cterm_of thy

   703 

   704     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)

   705     val ihyp = Term.all domT $ Abs ("z", domT,

   706       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),

   707         HOLogic.mk_Trueprop (P $ Bound 0)))

   708       |> cterm_of thy

   709 

   710     val aihyp = Thm.assume ihyp

   711 

   712     fun prove_case clause =

   713       let

   714         val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},

   715           RCs, qglr = (oqs, _, _, _), ...} = clause

   716 

   717         val case_hyp_conv = K (case_hyp RS eq_reflection)

   718         local open Conv in

   719           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D

   720           val sih =

   721             fconv_rule (Conv.binder_conv

   722               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp

   723         end

   724 

   725         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih

   726           |> Thm.forall_elim (cterm_of thy rcarg)

   727           |> Thm.elim_implies llRI

   728           |> fold_rev (Thm.implies_intr o cprop_of) CCas

   729           |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs

   730 

   731         val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)

   732 

   733         val step = HOLogic.mk_Trueprop (P $ lhs)

   734           |> fold_rev (curry Logic.mk_implies o prop_of) P_recs

   735           |> fold_rev (curry Logic.mk_implies) gs

   736           |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))

   737           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)

   738           |> cterm_of thy

   739 

   740         val P_lhs = Thm.assume step

   741           |> fold Thm.forall_elim cqs

   742           |> Thm.elim_implies lhs_D

   743           |> fold Thm.elim_implies ags

   744           |> fold Thm.elim_implies P_recs

   745 

   746         val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))

   747           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)

   748           |> Thm.symmetric (* P lhs == P x *)

   749           |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)

   750           |> Thm.implies_intr (cprop_of case_hyp)

   751           |> fold_rev (Thm.implies_intr o cprop_of) ags

   752           |> fold_rev Thm.forall_intr cqs

   753       in

   754         (res, step)

   755       end

   756 

   757     val (cases, steps) = split_list (map prove_case clauses)

   758 

   759     val istep = complete_thm

   760       |> Thm.forall_elim_vars 0

   761       |> fold (curry op COMP) cases (*  P x  *)

   762       |> Thm.implies_intr ihyp

   763       |> Thm.implies_intr (cprop_of x_D)

   764       |> Thm.forall_intr (cterm_of thy x)

   765 

   766     val subset_induct_rule =

   767       acc_subset_induct

   768       |> (curry op COMP) (Thm.assume D_subset)

   769       |> (curry op COMP) (Thm.assume D_dcl)

   770       |> (curry op COMP) (Thm.assume a_D)

   771       |> (curry op COMP) istep

   772       |> fold_rev Thm.implies_intr steps

   773       |> Thm.implies_intr a_D

   774       |> Thm.implies_intr D_dcl

   775       |> Thm.implies_intr D_subset

   776 

   777     val simple_induct_rule =

   778       subset_induct_rule

   779       |> Thm.forall_intr (cterm_of thy D)

   780       |> Thm.forall_elim (cterm_of thy acc_R)

   781       |> assume_tac 1 |> Seq.hd

   782       |> (curry op COMP) (acc_downward

   783         |> (instantiate' [SOME (ctyp_of thy domT)]

   784              (map (SOME o cterm_of thy) [R, x, z]))

   785         |> Thm.forall_intr (cterm_of thy z)

   786         |> Thm.forall_intr (cterm_of thy x))

   787       |> Thm.forall_intr (cterm_of thy a)

   788       |> Thm.forall_intr (cterm_of thy P)

   789   in

   790     simple_induct_rule

   791   end

   792 

   793 

   794 (* FIXME: broken by design *)

   795 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =

   796   let

   797     val thy = ProofContext.theory_of ctxt

   798     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},

   799       qglr = (oqs, _, _, _), ...} = clause

   800     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)

   801       |> fold_rev (curry Logic.mk_implies) gs

   802       |> cterm_of thy

   803   in

   804     Goal.init goal

   805     |> (SINGLE (resolve_tac [accI] 1)) |> the

   806     |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the

   807     |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the

   808     |> Goal.conclude

   809     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

   810   end

   811 

   812 

   813 

   814 (** Termination rule **)

   815 

   816 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}

   817 val wf_in_rel = @{thm FunDef.wf_in_rel}

   818 val in_rel_def = @{thm FunDef.in_rel_def}

   819 

   820 fun mk_nest_term_case thy globals R' ihyp clause =

   821   let

   822     val Globals {z, ...} = globals

   823     val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,

   824       qglr=(oqs, _, _, _), ...} = clause

   825 

   826     val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp

   827 

   828     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =

   829       let

   830         val used = (u @ sub)

   831           |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)

   832 

   833         val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)

   834           |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)

   835           |> Function_Ctx_Tree.export_term (fixes, assumes)

   836           |> fold_rev (curry Logic.mk_implies o prop_of) ags

   837           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)

   838           |> cterm_of thy

   839 

   840         val thm = Thm.assume hyp

   841           |> fold Thm.forall_elim cqs

   842           |> fold Thm.elim_implies ags

   843           |> Function_Ctx_Tree.import_thm thy (fixes, assumes)

   844           |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)

   845 

   846         val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))

   847           |> cterm_of thy |> Thm.assume

   848 

   849         val acc = thm COMP ih_case

   850         val z_acc_local = acc

   851           |> Conv.fconv_rule

   852               (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))

   853 

   854         val ethm = z_acc_local

   855           |> Function_Ctx_Tree.export_thm thy (fixes,

   856                z_eq_arg :: case_hyp :: ags @ assumes)

   857           |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

   858 

   859         val sub' = sub @ [(([],[]), acc)]

   860       in

   861         (sub', (hyp :: hyps, ethm :: thms))

   862       end

   863       | step _ _ _ _ = raise Match

   864   in

   865     Function_Ctx_Tree.traverse_tree step tree

   866   end

   867 

   868 

   869 fun mk_nest_term_rule thy globals R R_cases clauses =

   870   let

   871     val Globals { domT, x, z, ... } = globals

   872     val acc_R = mk_acc domT R

   873 

   874     val R' = Free ("R", fastype_of R)

   875 

   876     val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))

   877     val inrel_R = Const (@{const_name FunDef.in_rel},

   878       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel

   879 

   880     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},

   881       (domT --> domT --> boolT) --> boolT) $ R')

   882       |> cterm_of thy (* "wf R'" *)

   883 

   884     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)

   885     val ihyp = Term.all domT $ Abs ("z", domT,

   886       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),

   887         HOLogic.mk_Trueprop (acc_R $ Bound 0)))

   888       |> cterm_of thy

   889 

   890     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0

   891 

   892     val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))

   893 

   894     val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])

   895   in

   896     R_cases

   897     |> Thm.forall_elim (cterm_of thy z)

   898     |> Thm.forall_elim (cterm_of thy x)

   899     |> Thm.forall_elim (cterm_of thy (acc_R $ z))

   900     |> curry op COMP (Thm.assume R_z_x)

   901     |> fold_rev (curry op COMP) cases

   902     |> Thm.implies_intr R_z_x

   903     |> Thm.forall_intr (cterm_of thy z)

   904     |> (fn it => it COMP accI)

   905     |> Thm.implies_intr ihyp

   906     |> Thm.forall_intr (cterm_of thy x)

   907     |> (fn it => Drule.compose_single(it,2,wf_induct_rule))

   908     |> curry op RS (Thm.assume wfR')

   909     |> forall_intr_vars

   910     |> (fn it => it COMP allI)

   911     |> fold Thm.implies_intr hyps

   912     |> Thm.implies_intr wfR'

   913     |> Thm.forall_intr (cterm_of thy R')

   914     |> Thm.forall_elim (cterm_of thy (inrel_R))

   915     |> curry op RS wf_in_rel

   916     |> full_simplify (HOL_basic_ss addsimps [in_rel_def])

   917     |> Thm.forall_intr (cterm_of thy Rrel)

   918   end

   919 

   920 

   921 

   922 (* Tail recursion (probably very fragile)

   923  *

   924  * FIXME:

   925  * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.

   926  * - Must we really replace the fvar by f here?

   927  * - Splitting is not configured automatically: Problems with case?

   928  *)

   929 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =

   930   let

   931     val Globals {domT, ranT, fvar, ...} = globals

   932 

   933     val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)

   934 

   935     val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)

   936       Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]

   937         (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))

   938         (fn {prems=[a], ...} =>

   939           ((rtac (G_induct OF [a]))

   940           THEN_ALL_NEW rtac accI

   941           THEN_ALL_NEW etac R_cases

   942           THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)

   943 

   944     val default_thm =

   945       forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)

   946 

   947     fun mk_trsimp clause psimp =

   948       let

   949         val ClauseInfo {qglr = (oqs, _, _, _), cdata =

   950           ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause

   951         val thy = ProofContext.theory_of ctxt

   952         val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs

   953 

   954         val trsimp = Logic.list_implies(gs,

   955           HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)

   956         val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)

   957         fun simp_default_tac ss =

   958           asm_full_simp_tac (ss addsimps [default_thm, Let_def])

   959       in

   960         Goal.prove ctxt [] [] trsimp (fn _ =>

   961           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1

   962           THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1

   963           THEN (simp_default_tac (simpset_of ctxt) 1)

   964           THEN TRY ((etac not_acc_down 1)

   965             THEN ((etac R_cases)

   966               THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))

   967         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

   968       end

   969   in

   970     map2 mk_trsimp clauses psimps

   971   end

   972 *}

   973 

   974 ML {*

   975 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =

   976   let

   977     val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config

   978 

   979     val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)

   980     val fvar = Free (fname, fT)

   981     val domT = domain_type fT

   982     val ranT = range_type fT

   983 

   984     val default = Syntax.parse_term lthy default_str

   985       |> Type.constraint fT |> Syntax.check_term lthy

   986 

   987     val (globals, ctxt') = fix_globals domT ranT fvar lthy

   988 

   989     val Globals { x, h, ... } = globals

   990 

   991     val clauses = map (mk_clause_context x ctxt') abstract_qglrs

   992 

   993     val n = length abstract_qglrs

   994 

   995     fun build_tree (ClauseContext { ctxt, rhs, ...}) =

   996        Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs

   997 

   998     val trees = map build_tree clauses

   999     val RCss = map find_calls trees

  1000 

  1001     val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) =

  1002       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy

  1003 

  1004     val ((f, (_, f_defthm)), lthy) =

  1005       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy

  1006 

  1007     val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss

  1008     val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees

  1009 

  1010     val ((R, RIntro_thmss, R_elim), lthy) =

  1011       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy

  1012 

  1013     val (_, lthy) =

  1014       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy

  1015 

  1016     val newthy = ProofContext.theory_of lthy

  1017     val clauses = map (transfer_clause_ctx newthy) clauses

  1018 

  1019     val cert = cterm_of (ProofContext.theory_of lthy)

  1020 

  1021     val xclauses = PROFILE "xclauses"

  1022       (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees

  1023         RCss GIntro_thms) RIntro_thmss

  1024 

  1025     val complete =

  1026       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume

  1027 

  1028     val compat =

  1029       mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 

  1030       |> map (cert #> Thm.assume)

  1031 

  1032     val compat_store = store_compat_thms n compat

  1033 

  1034     val (goalstate, values) = PROFILE "prove_stuff"

  1035       (prove_stuff lthy globals G f R xclauses complete compat

  1036          compat_store G_elim G_eqvt) f_defthm

  1037      

  1038     val mk_trsimps =

  1039       mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses

  1040 

  1041     fun mk_partial_rules provedgoal =

  1042       let

  1043         val newthy = theory_of_thm provedgoal (*FIXME*)

  1044 

  1045         val (graph_is_function, complete_thm) =

  1046           provedgoal

  1047           |> Conjunction.elim

  1048           |> apfst (Thm.forall_elim_vars 0)

  1049 

  1050         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)

  1051 

  1052         val psimps = PROFILE "Proving simplification rules"

  1053           (mk_psimps newthy globals R xclauses values f_iff) graph_is_function

  1054 

  1055         val simple_pinduct = PROFILE "Proving partial induction rule"

  1056           (mk_partial_induct_rule newthy globals R complete_thm) xclauses

  1057 

  1058         val total_intro = PROFILE "Proving nested termination rule"

  1059           (mk_nest_term_rule newthy globals R R_elim) xclauses

  1060 

  1061         val dom_intros =

  1062           if domintros then SOME (PROFILE "Proving domain introduction rules"

  1063              (map (mk_domain_intro lthy globals R R_elim)) xclauses)

  1064            else NONE

  1065         val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE

  1066 

  1067       in

  1068         FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,

  1069           psimps=psimps, simple_pinducts=[simple_pinduct],

  1070           termination=total_intro, trsimps=trsimps,

  1071           domintros=dom_intros}

  1072       end

  1073   in

  1074     ((f, goalstate, mk_partial_rules), lthy)

  1075   end

  1076 *}

  1077 

  1078 ML {*

  1079 open Function_Lib

  1080 open Function_Common

  1081 

  1082 type qgar = string * (string * typ) list * term list * term list * term

  1083 

  1084 datatype mutual_part = MutualPart of

  1085  {i : int,

  1086   i' : int,

  1087   fvar : string * typ,

  1088   cargTs: typ list,

  1089   f_def: term,

  1090 

  1091   f: term option,

  1092   f_defthm : thm option}

  1093 

  1094 datatype mutual_info = Mutual of

  1095  {n : int,

  1096   n' : int,

  1097   fsum_var : string * typ,

  1098 

  1099   ST: typ,

  1100   RST: typ,

  1101 

  1102   parts: mutual_part list,

  1103   fqgars: qgar list,

  1104   qglrs: ((string * typ) list * term list * term * term) list,

  1105 

  1106   fsum : term option}

  1107 

  1108 fun mutual_induct_Pnames n =

  1109   if n < 5 then fst (chop n ["P","Q","R","S"])

  1110   else map (fn i => "P" ^ string_of_int i) (1 upto n)

  1111 

  1112 fun get_part fname =

  1113   the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)

  1114 

  1115 (* FIXME *)

  1116 fun mk_prod_abs e (t1, t2) =

  1117   let

  1118     val bTs = rev (map snd e)

  1119     val T1 = fastype_of1 (bTs, t1)

  1120     val T2 = fastype_of1 (bTs, t2)

  1121   in

  1122     HOLogic.pair_const T1 T2 $ t1 $ t2

  1123   end

  1124 

  1125 fun analyze_eqs ctxt defname fs eqs =

  1126   let

  1127     val num = length fs

  1128     val fqgars = map (split_def ctxt (K true)) eqs

  1129     val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars

  1130       |> AList.lookup (op =) #> the

  1131 

  1132     fun curried_types (fname, fT) =

  1133       let

  1134         val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)