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