src/HOL/Tools/Function/function_core.ML
author wenzelm
Thu Nov 19 14:46:33 2009 +0100 (2009-11-19)
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 33855 cd8acf137c9c
permissions -rw-r--r--
adapted Local_Theory.define -- eliminated odd thm kind;
     1 (*  Title:      HOL/Tools/Function/function_core.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 A package for general recursive function definitions:
     5 Main functionality.
     6 *)
     7 
     8 signature FUNCTION_CORE =
     9 sig
    10     val trace: bool Unsynchronized.ref
    11 
    12     val prepare_function : Function_Common.function_config
    13                          -> string (* defname *)
    14                          -> ((bstring * typ) * mixfix) list (* defined symbol *)
    15                          -> ((bstring * typ) list * term list * term * term) list (* specification *)
    16                          -> local_theory
    17 
    18                          -> (term   (* f *)
    19                              * thm  (* goalstate *)
    20                              * (thm -> Function_Common.function_result) (* continuation *)
    21                             ) * local_theory
    22 
    23 end
    24 
    25 structure Function_Core : FUNCTION_CORE =
    26 struct
    27 
    28 val trace = Unsynchronized.ref false;
    29 fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    30 
    31 val boolT = HOLogic.boolT
    32 val mk_eq = HOLogic.mk_eq
    33 
    34 open Function_Lib
    35 open Function_Common
    36 
    37 datatype globals =
    38    Globals of {
    39          fvar: term,
    40          domT: typ,
    41          ranT: typ,
    42          h: term,
    43          y: term,
    44          x: term,
    45          z: term,
    46          a: term,
    47          P: term,
    48          D: term,
    49          Pbool:term
    50 }
    51 
    52 
    53 datatype rec_call_info =
    54   RCInfo of
    55   {
    56    RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    57    CCas: thm list,
    58    rcarg: term,                 (* The recursive argument *)
    59 
    60    llRI: thm,
    61    h_assum: term
    62   }
    63 
    64 
    65 datatype clause_context =
    66   ClauseContext of
    67   {
    68     ctxt : Proof.context,
    69 
    70     qs : term list,
    71     gs : term list,
    72     lhs: term,
    73     rhs: term,
    74 
    75     cqs: cterm list,
    76     ags: thm list,
    77     case_hyp : thm
    78   }
    79 
    80 
    81 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
    82     ClauseContext { ctxt = ProofContext.transfer thy ctxt,
    83                     qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
    84 
    85 
    86 datatype clause_info =
    87   ClauseInfo of
    88      {
    89       no: int,
    90       qglr : ((string * typ) list * term list * term * term),
    91       cdata : clause_context,
    92 
    93       tree: Function_Ctx_Tree.ctx_tree,
    94       lGI: thm,
    95       RCs: rec_call_info list
    96      }
    97 
    98 
    99 (* Theory dependencies. *)
   100 val Pair_inject = @{thm Product_Type.Pair_inject};
   101 
   102 val acc_induct_rule = @{thm accp_induct_rule};
   103 
   104 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
   105 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
   106 val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
   107 
   108 val acc_downward = @{thm accp_downward};
   109 val accI = @{thm accp.accI};
   110 val case_split = @{thm HOL.case_split};
   111 val fundef_default_value = @{thm FunDef.fundef_default_value};
   112 val not_acc_down = @{thm not_accp_down};
   113 
   114 
   115 
   116 fun find_calls tree =
   117     let
   118       fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
   119         | add_Ri _ _ _ _ = raise Match
   120     in
   121       rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
   122     end
   123 
   124 
   125 (** building proof obligations *)
   126 
   127 fun mk_compat_proof_obligations domT ranT fvar f glrs =
   128     let
   129       fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   130           let
   131             val shift = incr_boundvars (length qs')
   132           in
   133             Logic.mk_implies
   134               (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
   135                 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
   136               |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
   137               |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
   138               |> curry abstract_over fvar
   139               |> curry subst_bound f
   140           end
   141     in
   142       map mk_impl (unordered_pairs glrs)
   143     end
   144 
   145 
   146 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
   147     let
   148         fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
   149             HOLogic.mk_Trueprop Pbool
   150                      |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
   151                      |> fold_rev (curry Logic.mk_implies) gs
   152                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   153     in
   154         HOLogic.mk_Trueprop Pbool
   155                  |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
   156                  |> mk_forall_rename ("x", x)
   157                  |> mk_forall_rename ("P", Pbool)
   158     end
   159 
   160 (** making a context with it's own local bindings **)
   161 
   162 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   163     let
   164       val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   165                                            |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   166 
   167       val thy = ProofContext.theory_of ctxt'
   168 
   169       fun inst t = subst_bounds (rev qs, t)
   170       val gs = map inst pre_gs
   171       val lhs = inst pre_lhs
   172       val rhs = inst pre_rhs
   173 
   174       val cqs = map (cterm_of thy) qs
   175       val ags = map (assume o cterm_of thy) gs
   176 
   177       val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   178     in
   179       ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   180                       cqs = cqs, ags = ags, case_hyp = case_hyp }
   181     end
   182 
   183 
   184 (* lowlevel term function. FIXME: remove *)
   185 fun abstract_over_list vs body =
   186   let
   187     fun abs lev v tm =
   188       if v aconv tm then Bound lev
   189       else
   190         (case tm of
   191           Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
   192         | t $ u => abs lev v t $ abs lev v u
   193         | t => t);
   194   in
   195     fold_index (fn (i, v) => fn t => abs i v t) vs body
   196   end
   197 
   198 
   199 
   200 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   201     let
   202         val Globals {h, fvar, x, ...} = globals
   203 
   204         val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   205         val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   206 
   207         (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   208         val lGI = GIntro_thm
   209                     |> forall_elim (cert f)
   210                     |> fold forall_elim cqs
   211                     |> fold Thm.elim_implies ags
   212 
   213         fun mk_call_info (rcfix, rcassm, rcarg) RI =
   214             let
   215                 val llRI = RI
   216                              |> fold forall_elim cqs
   217                              |> fold (forall_elim o cert o Free) rcfix
   218                              |> fold Thm.elim_implies ags
   219                              |> fold Thm.elim_implies rcassm
   220 
   221                 val h_assum =
   222                     HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
   223                               |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   224                               |> fold_rev (Logic.all o Free) rcfix
   225                               |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
   226                               |> abstract_over_list (rev qs)
   227             in
   228                 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   229             end
   230 
   231         val RC_infos = map2 mk_call_info RCs RIntro_thms
   232     in
   233         ClauseInfo
   234             {
   235              no=no,
   236              cdata=cdata,
   237              qglr=qglr,
   238 
   239              lGI=lGI,
   240              RCs=RC_infos,
   241              tree=tree
   242             }
   243     end
   244 
   245 
   246 
   247 
   248 
   249 
   250 
   251 (* replace this by a table later*)
   252 fun store_compat_thms 0 thms = []
   253   | store_compat_thms n thms =
   254     let
   255         val (thms1, thms2) = chop n thms
   256     in
   257         (thms1 :: store_compat_thms (n - 1) thms2)
   258     end
   259 
   260 (* expects i <= j *)
   261 fun lookup_compat_thm i j cts =
   262     nth (nth cts (i - 1)) (j - i)
   263 
   264 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   265 (* if j < i, then turn around *)
   266 fun get_compat_thm thy cts i j ctxi ctxj =
   267     let
   268       val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
   269       val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
   270 
   271       val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   272     in if j < i then
   273          let
   274            val compat = lookup_compat_thm j i cts
   275          in
   276            compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   277                 |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
   278                 |> fold Thm.elim_implies agsj
   279                 |> fold Thm.elim_implies agsi
   280                 |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
   281          end
   282        else
   283          let
   284            val compat = lookup_compat_thm i j cts
   285          in
   286                compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   287                  |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
   288                  |> fold Thm.elim_implies agsi
   289                  |> fold Thm.elim_implies agsj
   290                  |> Thm.elim_implies (assume lhsi_eq_lhsj)
   291                  |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
   292          end
   293     end
   294 
   295 
   296 
   297 
   298 (* Generates the replacement lemma in fully quantified form. *)
   299 fun mk_replacement_lemma thy h ih_elim clause =
   300     let
   301         val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
   302         local open Conv in
   303         val ih_conv = arg1_conv o arg_conv o arg_conv
   304         end
   305 
   306         val ih_elim_case = 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, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   310 
   311         val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
   312 
   313         val replace_lemma = (eql RS meta_eq_to_obj_eq)
   314                                 |> implies_intr (cprop_of case_hyp)
   315                                 |> fold_rev (implies_intr o cprop_of) h_assums
   316                                 |> fold_rev (implies_intr o cprop_of) ags
   317                                 |> fold_rev forall_intr cqs
   318                                 |> Thm.close_derivation
   319     in
   320       replace_lemma
   321     end
   322 
   323 
   324 fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
   325     let
   326         val Globals {h, y, x, fvar, ...} = globals
   327         val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
   328         val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   329 
   330         val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
   331             = mk_clause_context x ctxti cdescj
   332 
   333         val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   334         val compat = get_compat_thm thy compat_store i j cctxi cctxj
   335         val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   336 
   337         val RLj_import =
   338             RLj |> fold forall_elim cqsj'
   339                 |> fold Thm.elim_implies agsj'
   340                 |> fold Thm.elim_implies Ghsj'
   341 
   342         val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   343         val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   344     in
   345         (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   346         |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   347         |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   348         |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   349         |> fold_rev (implies_intr o cprop_of) Ghsj'
   350         |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   351         |> implies_intr (cprop_of y_eq_rhsj'h)
   352         |> implies_intr (cprop_of lhsi_eq_lhsj')
   353         |> fold_rev forall_intr (cterm_of thy h :: cqsj')
   354     end
   355 
   356 
   357 
   358 fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   359     let
   360         val Globals {x, y, ranT, fvar, ...} = globals
   361         val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   362         val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   363 
   364         val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   365 
   366         fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   367                                                             |> fold_rev (implies_intr o cprop_of) CCas
   368                                                             |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   369 
   370         val existence = fold (curry op COMP o prep_RC) RCs lGI
   371 
   372         val P = cterm_of thy (mk_eq (y, rhsC))
   373         val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
   374 
   375         val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
   376 
   377         val uniqueness = G_cases
   378                            |> forall_elim (cterm_of thy lhs)
   379                            |> forall_elim (cterm_of thy y)
   380                            |> forall_elim P
   381                            |> Thm.elim_implies G_lhs_y
   382                            |> fold Thm.elim_implies unique_clauses
   383                            |> implies_intr (cprop_of G_lhs_y)
   384                            |> forall_intr (cterm_of thy y)
   385 
   386         val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   387 
   388         val exactly_one =
   389             ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   390                  |> curry (op COMP) existence
   391                  |> curry (op COMP) uniqueness
   392                  |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   393                  |> implies_intr (cprop_of case_hyp)
   394                  |> fold_rev (implies_intr o cprop_of) ags
   395                  |> fold_rev forall_intr cqs
   396 
   397         val function_value =
   398             existence
   399               |> implies_intr ihyp
   400               |> implies_intr (cprop_of case_hyp)
   401               |> forall_intr (cterm_of thy x)
   402               |> forall_elim (cterm_of thy lhs)
   403               |> curry (op RS) refl
   404     in
   405         (exactly_one, function_value)
   406     end
   407 
   408 
   409 
   410 
   411 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
   412     let
   413         val Globals {h, domT, ranT, x, ...} = globals
   414         val thy = ProofContext.theory_of ctxt
   415 
   416         (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   417         val ihyp = Term.all domT $ Abs ("z", domT,
   418                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   419                                      HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   420                                                              Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   421                        |> cterm_of thy
   422 
   423         val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
   424         val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   425         val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   426                         |> instantiate' [] [NONE, SOME (cterm_of thy h)]
   427 
   428         val _ = trace_msg (K "Proving Replacement lemmas...")
   429         val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   430 
   431         val _ = trace_msg (K "Proving cases for unique existence...")
   432         val (ex1s, values) =
   433             split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   434 
   435         val _ = trace_msg (K "Proving: Graph is a function")
   436         val graph_is_function = complete
   437                                   |> Thm.forall_elim_vars 0
   438                                   |> fold (curry op COMP) ex1s
   439                                   |> implies_intr (ihyp)
   440                                   |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   441                                   |> forall_intr (cterm_of thy x)
   442                                   |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   443                                   |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
   444 
   445         val goalstate =  Conjunction.intr graph_is_function complete
   446                           |> Thm.close_derivation
   447                           |> Goal.protect
   448                           |> fold_rev (implies_intr o cprop_of) compat
   449                           |> implies_intr (cprop_of complete)
   450     in
   451       (goalstate, values)
   452     end
   453 
   454 (* wrapper -- restores quantifiers in rule specifications *)
   455 fun inductive_def (binding as ((R, T), _)) intrs lthy =
   456   let
   457     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
   458       lthy
   459       |> Local_Theory.conceal
   460       |> Inductive.add_inductive_i
   461           {quiet_mode = true,
   462             verbose = ! trace,
   463             alt_name = Binding.empty,
   464             coind = false,
   465             no_elim = false,
   466             no_ind = false,
   467             skip_mono = true,
   468             fork_mono = false}
   469           [binding] (* relation *)
   470           [] (* no parameters *)
   471           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
   472           [] (* no special monos *)
   473       ||> Local_Theory.restore_naming lthy
   474 
   475     val cert = cterm_of (ProofContext.theory_of lthy)
   476     fun requantify orig_intro thm =
   477       let
   478         val (qs, t) = dest_all_all orig_intro
   479         val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
   480         val vars = Term.add_vars (prop_of thm) [] |> rev
   481         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
   482           #> the_default ("",0)
   483       in
   484         fold_rev (fn Free (n, T) =>
   485           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
   486       end
   487   in
   488       ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   489   end
   490 
   491 fun define_graph Gname fvar domT ranT clauses RCss lthy =
   492   let
   493     val GT = domT --> ranT --> boolT
   494     val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
   495 
   496     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   497       let
   498         fun mk_h_assm (rcfix, rcassm, rcarg) =
   499           HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
   500           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   501           |> fold_rev (Logic.all o Free) rcfix
   502       in
   503         HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
   504         |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   505         |> fold_rev (curry Logic.mk_implies) gs
   506         |> fold_rev Logic.all (fvar :: qs)
   507       end
   508 
   509     val G_intros = map2 mk_GIntro clauses RCss
   510   in
   511     inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
   512   end
   513 
   514 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   515   let
   516     val f_def =
   517       Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 
   518         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   519       |> Syntax.check_term lthy
   520   in
   521     Local_Theory.define
   522       ((Binding.name (function_name fname), mixfix),
   523         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   524   end
   525 
   526 fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
   527   let
   528     val RT = domT --> domT --> boolT
   529     val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
   530 
   531     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   532       HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
   533       |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   534       |> fold_rev (curry Logic.mk_implies) gs
   535       |> fold_rev (Logic.all o Free) rcfix
   536       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   537       (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
   538 
   539     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
   540 
   541     val ((R, RIntro_thms, R_elim, _), lthy) =
   542       inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
   543   in
   544     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   545   end
   546 
   547 
   548 fun fix_globals domT ranT fvar ctxt =
   549     let
   550       val ([h, y, x, z, a, D, P, Pbool],ctxt') =
   551           Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   552     in
   553       (Globals {h = Free (h, domT --> ranT),
   554                 y = Free (y, ranT),
   555                 x = Free (x, domT),
   556                 z = Free (z, domT),
   557                 a = Free (a, domT),
   558                 D = Free (D, domT --> boolT),
   559                 P = Free (P, domT --> boolT),
   560                 Pbool = Free (Pbool, boolT),
   561                 fvar = fvar,
   562                 domT = domT,
   563                 ranT = ranT
   564                },
   565        ctxt')
   566     end
   567 
   568 
   569 
   570 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
   571     let
   572       fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   573     in
   574       (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   575     end
   576 
   577 
   578 
   579 (**********************************************************
   580  *                   PROVING THE RULES
   581  **********************************************************)
   582 
   583 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
   584     let
   585       val Globals {domT, z, ...} = globals
   586 
   587       fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   588           let
   589             val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   590             val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   591           in
   592             ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   593               |> (fn it => it COMP graph_is_function)
   594               |> implies_intr z_smaller
   595               |> forall_intr (cterm_of thy z)
   596               |> (fn it => it COMP valthm)
   597               |> implies_intr lhs_acc
   598               |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   599               |> fold_rev (implies_intr o cprop_of) ags
   600               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   601           end
   602     in
   603       map2 mk_psimp clauses valthms
   604     end
   605 
   606 
   607 (** Induction rule **)
   608 
   609 
   610 val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
   611 
   612 
   613 fun mk_partial_induct_rule thy globals R complete_thm clauses =
   614     let
   615       val Globals {domT, x, z, a, P, D, ...} = globals
   616       val acc_R = mk_acc domT R
   617 
   618       val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
   619       val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
   620 
   621       val D_subset = cterm_of thy (Logic.all x
   622         (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
   623 
   624       val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   625                     Logic.all x
   626                     (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   627                                                     Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   628                                                                       HOLogic.mk_Trueprop (D $ z)))))
   629                     |> cterm_of thy
   630 
   631 
   632   (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   633       val ihyp = Term.all domT $ Abs ("z", domT,
   634                Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   635                  HOLogic.mk_Trueprop (P $ Bound 0)))
   636            |> cterm_of thy
   637 
   638       val aihyp = assume ihyp
   639 
   640   fun prove_case clause =
   641       let
   642     val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
   643                     qglr = (oqs, _, _, _), ...} = clause
   644 
   645     val case_hyp_conv = K (case_hyp RS eq_reflection)
   646     local open Conv in
   647     val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
   648     val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
   649     end
   650 
   651     fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   652         sih |> forall_elim (cterm_of thy rcarg)
   653             |> Thm.elim_implies llRI
   654             |> fold_rev (implies_intr o cprop_of) CCas
   655             |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   656 
   657     val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   658 
   659     val step = HOLogic.mk_Trueprop (P $ lhs)
   660             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   661             |> fold_rev (curry Logic.mk_implies) gs
   662             |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   663             |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   664             |> cterm_of thy
   665 
   666     val P_lhs = assume step
   667            |> fold forall_elim cqs
   668            |> Thm.elim_implies lhs_D
   669            |> fold Thm.elim_implies ags
   670            |> fold Thm.elim_implies P_recs
   671 
   672     val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
   673            |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
   674            |> symmetric (* P lhs == P x *)
   675            |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   676            |> implies_intr (cprop_of case_hyp)
   677            |> fold_rev (implies_intr o cprop_of) ags
   678            |> fold_rev forall_intr cqs
   679       in
   680         (res, step)
   681       end
   682 
   683   val (cases, steps) = split_list (map prove_case clauses)
   684 
   685   val istep = complete_thm
   686                 |> Thm.forall_elim_vars 0
   687                 |> fold (curry op COMP) cases (*  P x  *)
   688                 |> implies_intr ihyp
   689                 |> implies_intr (cprop_of x_D)
   690                 |> forall_intr (cterm_of thy x)
   691 
   692   val subset_induct_rule =
   693       acc_subset_induct
   694         |> (curry op COMP) (assume D_subset)
   695         |> (curry op COMP) (assume D_dcl)
   696         |> (curry op COMP) (assume a_D)
   697         |> (curry op COMP) istep
   698         |> fold_rev implies_intr steps
   699         |> implies_intr a_D
   700         |> implies_intr D_dcl
   701         |> implies_intr D_subset
   702 
   703   val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   704 
   705   val simple_induct_rule =
   706       subset_induct_rule
   707         |> forall_intr (cterm_of thy D)
   708         |> forall_elim (cterm_of thy acc_R)
   709         |> assume_tac 1 |> Seq.hd
   710         |> (curry op COMP) (acc_downward
   711                               |> (instantiate' [SOME (ctyp_of thy domT)]
   712                                                (map (SOME o cterm_of thy) [R, x, z]))
   713                               |> forall_intr (cterm_of thy z)
   714                               |> forall_intr (cterm_of thy x))
   715         |> forall_intr (cterm_of thy a)
   716         |> forall_intr (cterm_of thy P)
   717     in
   718       simple_induct_rule
   719     end
   720 
   721 
   722 
   723 (* FIXME: This should probably use fixed goals, to be more reliable and faster *)
   724 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   725     let
   726       val thy = ProofContext.theory_of ctxt
   727       val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
   728                       qglr = (oqs, _, _, _), ...} = clause
   729       val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
   730                           |> fold_rev (curry Logic.mk_implies) gs
   731                           |> cterm_of thy
   732     in
   733       Goal.init goal
   734       |> (SINGLE (resolve_tac [accI] 1)) |> the
   735       |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
   736       |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
   737       |> Goal.conclude
   738       |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   739     end
   740 
   741 
   742 
   743 (** Termination rule **)
   744 
   745 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
   746 val wf_in_rel = @{thm FunDef.wf_in_rel};
   747 val in_rel_def = @{thm FunDef.in_rel_def};
   748 
   749 fun mk_nest_term_case thy globals R' ihyp clause =
   750     let
   751       val Globals {x, z, ...} = globals
   752       val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   753                       qglr=(oqs, _, _, _), ...} = clause
   754 
   755       val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   756 
   757       fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
   758           let
   759             val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
   760 
   761             val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
   762                       |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
   763                       |> Function_Ctx_Tree.export_term (fixes, assumes)
   764                       |> fold_rev (curry Logic.mk_implies o prop_of) ags
   765                       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   766                       |> cterm_of thy
   767 
   768             val thm = assume hyp
   769                       |> fold forall_elim cqs
   770                       |> fold Thm.elim_implies ags
   771                       |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
   772                       |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
   773 
   774             val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
   775 
   776             val acc = thm COMP ih_case
   777             val z_acc_local = acc
   778             |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
   779 
   780             val ethm = z_acc_local
   781                          |> Function_Ctx_Tree.export_thm thy (fixes,
   782                                                           z_eq_arg :: case_hyp :: ags @ assumes)
   783                          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   784 
   785             val sub' = sub @ [(([],[]), acc)]
   786           in
   787             (sub', (hyp :: hyps, ethm :: thms))
   788           end
   789         | step _ _ _ _ = raise Match
   790     in
   791       Function_Ctx_Tree.traverse_tree step tree
   792     end
   793 
   794 
   795 fun mk_nest_term_rule thy globals R R_cases clauses =
   796     let
   797       val Globals { domT, x, z, ... } = globals
   798       val acc_R = mk_acc domT R
   799 
   800       val R' = Free ("R", fastype_of R)
   801 
   802       val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
   803       val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   804 
   805       val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   806 
   807       (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   808       val ihyp = Term.all domT $ Abs ("z", domT,
   809                                  Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
   810                                    HOLogic.mk_Trueprop (acc_R $ Bound 0)))
   811                      |> cterm_of thy
   812 
   813       val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
   814 
   815       val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
   816 
   817       val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   818     in
   819       R_cases
   820         |> forall_elim (cterm_of thy z)
   821         |> forall_elim (cterm_of thy x)
   822         |> forall_elim (cterm_of thy (acc_R $ z))
   823         |> curry op COMP (assume R_z_x)
   824         |> fold_rev (curry op COMP) cases
   825         |> implies_intr R_z_x
   826         |> forall_intr (cterm_of thy z)
   827         |> (fn it => it COMP accI)
   828         |> implies_intr ihyp
   829         |> forall_intr (cterm_of thy x)
   830         |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   831         |> curry op RS (assume wfR')
   832         |> forall_intr_vars
   833         |> (fn it => it COMP allI)
   834         |> fold implies_intr hyps
   835         |> implies_intr wfR'
   836         |> forall_intr (cterm_of thy R')
   837         |> forall_elim (cterm_of thy (inrel_R))
   838         |> curry op RS wf_in_rel
   839         |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   840         |> forall_intr (cterm_of thy Rrel)
   841     end
   842 
   843 
   844 
   845 (* Tail recursion (probably very fragile)
   846  *
   847  * FIXME:
   848  * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
   849  * - Must we really replace the fvar by f here?
   850  * - Splitting is not configured automatically: Problems with case?
   851  *)
   852 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
   853     let
   854       val Globals {domT, ranT, fvar, ...} = globals
   855 
   856       val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
   857 
   858       val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
   859           Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
   860                      (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
   861                      (fn {prems=[a], ...} =>
   862                          ((rtac (G_induct OF [a]))
   863                             THEN_ALL_NEW (rtac accI)
   864                             THEN_ALL_NEW (etac R_cases)
   865                             THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
   866 
   867       val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
   868 
   869       fun mk_trsimp clause psimp =
   870           let
   871             val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
   872             val thy = ProofContext.theory_of ctxt
   873             val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   874 
   875             val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
   876             val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
   877             fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
   878           in
   879             Goal.prove ctxt [] [] trsimp
   880                        (fn _ =>
   881                            rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
   882                                 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
   883                                 THEN (simp_default_tac (simpset_of ctxt) 1)
   884                                 THEN (etac not_acc_down 1)
   885                                 THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
   886               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   887           end
   888     in
   889       map2 mk_trsimp clauses psimps
   890     end
   891 
   892 
   893 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
   894     let
   895       val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
   896 
   897       val fvar = Free (fname, fT)
   898       val domT = domain_type fT
   899       val ranT = range_type fT
   900 
   901       val default = Syntax.parse_term lthy default_str
   902         |> TypeInfer.constrain fT |> Syntax.check_term lthy
   903 
   904       val (globals, ctxt') = fix_globals domT ranT fvar lthy
   905 
   906       val Globals { x, h, ... } = globals
   907 
   908       val clauses = map (mk_clause_context x ctxt') abstract_qglrs
   909 
   910       val n = length abstract_qglrs
   911 
   912       fun build_tree (ClauseContext { ctxt, rhs, ...}) =
   913             Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
   914 
   915       val trees = map build_tree clauses
   916       val RCss = map find_calls trees
   917 
   918       val ((G, GIntro_thms, G_elim, G_induct), lthy) =
   919           PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
   920 
   921       val ((f, (_, f_defthm)), lthy) =
   922           PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
   923 
   924       val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
   925       val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
   926 
   927       val ((R, RIntro_thmss, R_elim), lthy) =
   928           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
   929 
   930       val (_, lthy) =
   931           Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
   932 
   933       val newthy = ProofContext.theory_of lthy
   934       val clauses = map (transfer_clause_ctx newthy) clauses
   935 
   936       val cert = cterm_of (ProofContext.theory_of lthy)
   937 
   938       val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
   939 
   940       val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
   941       val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
   942 
   943       val compat_store = store_compat_thms n compat
   944 
   945       val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
   946 
   947       val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
   948 
   949       fun mk_partial_rules provedgoal =
   950           let
   951             val newthy = theory_of_thm provedgoal (*FIXME*)
   952 
   953             val (graph_is_function, complete_thm) =
   954                 provedgoal
   955                   |> Conjunction.elim
   956                   |> apfst (Thm.forall_elim_vars 0)
   957 
   958             val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
   959 
   960             val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
   961 
   962             val simple_pinduct = PROFILE "Proving partial induction rule"
   963                                                            (mk_partial_induct_rule newthy globals R complete_thm) xclauses
   964 
   965 
   966             val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
   967 
   968             val dom_intros = if domintros
   969                              then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
   970                              else NONE
   971             val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
   972 
   973           in
   974             FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
   975                           psimps=psimps, simple_pinducts=[simple_pinduct],
   976                           termination=total_intro, trsimps=trsimps,
   977                           domintros=dom_intros}
   978           end
   979     in
   980       ((f, goalstate, mk_partial_rules), lthy)
   981     end
   982 
   983 
   984 end