Nominal/nominal_function_core.ML
changeset 3239 67370521c09c
parent 3229 b52e8651591f
child 3243 c4f31f1564b7
equal deleted inserted replaced
3238:b2e1a7b83e05 3239:67370521c09c
    81 
    81 
    82 datatype clause_info = ClauseInfo of
    82 datatype clause_info = ClauseInfo of
    83  {no: int,
    83  {no: int,
    84   qglr : ((string * typ) list * term list * term * term),
    84   qglr : ((string * typ) list * term list * term * term),
    85   cdata : clause_context,
    85   cdata : clause_context,
    86   tree: Function_Ctx_Tree.ctx_tree,
    86   tree: Function_Context_Tree.ctx_tree,
    87   lGI: thm,
    87   lGI: thm,
    88   RCs: rec_call_info list}
    88   RCs: rec_call_info list}
    89 
    89 
    90 
    90 
    91 (* Theory dependencies. *)
    91 (* Theory dependencies. *)
   107   let
   107   let
   108     fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
   108     fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
   109       ([], (fixes, assumes, arg) :: xs)
   109       ([], (fixes, assumes, arg) :: xs)
   110       | add_Ri _ _ _ _ = raise Match
   110       | add_Ri _ _ _ _ = raise Match
   111   in
   111   in
   112     rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
   112     rev (Function_Context_Tree.traverse_tree add_Ri tree [])
   113   end
   113   end
   114 
   114 
   115 (* nominal *)
   115 (* nominal *)
   116 fun mk_eqvt_at (f_trm, arg_trm) =
   116 fun mk_eqvt_at (f_trm, arg_trm) =
   117   let
   117   let
   145   end  
   145   end  
   146 
   146 
   147 (** building proof obligations *)
   147 (** building proof obligations *)
   148 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   148 fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   149   mk_eqvt_at (fvar, arg)
   149   mk_eqvt_at (fvar, arg)
   150   |> curry Logic.list_implies (map prop_of assms)
   150   |> curry Logic.list_implies (map Thm.prop_of assms)
   151   |> fold_rev (Logic.all o Free) vs
   151   |> fold_rev (Logic.all o Free) vs
   152   |> fold_rev absfree qs
   152   |> fold_rev absfree qs
   153   |> strip_abs_body
   153   |> strip_abs_body
   154 
   154 
   155 fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = 
   155 fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = 
   156   mk_inv inv (fvar, arg)
   156   mk_inv inv (fvar, arg)
   157   |> curry Logic.list_implies (map prop_of assms)
   157   |> curry Logic.list_implies (map Thm.prop_of assms)
   158   |> fold_rev (Logic.all o Free) vs
   158   |> fold_rev (Logic.all o Free) vs
   159   |> fold_rev absfree qs
   159   |> fold_rev absfree qs
   160   |> strip_abs_body
   160   |> strip_abs_body
   161 
   161 
   162 (** building proof obligations *)
   162 (** building proof obligations *)
   205 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   205 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   206   let
   206   let
   207     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   207     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
   208       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   208       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   209 
   209 
   210     val thy = Proof_Context.theory_of ctxt'
       
   211 
       
   212     fun inst t = subst_bounds (rev qs, t)
   210     fun inst t = subst_bounds (rev qs, t)
   213     val gs = map inst pre_gs
   211     val gs = map inst pre_gs
   214     val lhs = inst pre_lhs
   212     val lhs = inst pre_lhs
   215     val rhs = inst pre_rhs
   213     val rhs = inst pre_rhs
   216 
   214 
   217     val cqs = map (cterm_of thy) qs
   215     val cqs = map (Thm.cterm_of ctxt') qs
   218     val ags = map (Thm.assume o cterm_of thy) gs
   216     val ags = map (Thm.assume o Thm.cterm_of ctxt') gs
   219 
   217 
   220     val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   218     val case_hyp = Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
   221   in
   219   in
   222     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   220     ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
   223       cqs = cqs, ags = ags, case_hyp = case_hyp }
   221       cqs = cqs, ags = ags, case_hyp = case_hyp }
   224   end
   222   end
   225 
   223 
   243 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   241 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   244   let
   242   let
   245     val Globals {h, ...} = globals
   243     val Globals {h, ...} = globals
   246 
   244 
   247     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   245     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
   248     val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
   246     val cert = Thm.cterm_of ctxt
   249 
   247 
   250     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   248     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
   251     val lGI = GIntro_thm
   249     val lGI = GIntro_thm
   252       |> Thm.forall_elim (cert f)
   250       |> Thm.forall_elim (cert f)
   253       |> fold Thm.forall_elim cqs
   251       |> fold Thm.forall_elim cqs
   261           |> fold Thm.elim_implies ags
   259           |> fold Thm.elim_implies ags
   262           |> fold Thm.elim_implies rcassm
   260           |> fold Thm.elim_implies rcassm
   263 
   261 
   264         val h_assum =
   262         val h_assum =
   265           HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
   263           HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
   266           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   264           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
   267           |> fold_rev (Logic.all o Free) rcfix
   265           |> fold_rev (Logic.all o Free) rcfix
   268           |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
   266           |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
   269           |> abstract_over_list (rev qs)
   267           |> abstract_over_list (rev qs)
   270       in
   268       in
   271         RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   269         RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
   291   nth (nth cts (i - 1)) (j - i)
   289   nth (nth cts (i - 1)) (j - i)
   292 
   290 
   293 (* nominal *)
   291 (* nominal *)
   294 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   292 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
   295 (* if j < i, then turn around *)
   293 (* if j < i, then turn around *)
   296 fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
   294 fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
   297   let
   295   let
   298     val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
   296     val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
   299     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
   297     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
   300 
   298 
   301     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   299     val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   302 
   300 
   303   in if j < i then
   301   in if j < i then
   304     let
   302     let
   305       val compat = lookup_compat_thm j i cts
   303       val compat = lookup_compat_thm j i cts
   306     in
   304     in
   331     end
   329     end
   332   end
   330   end
   333 
   331 
   334 
   332 
   335 (* Generates the replacement lemma in fully quantified form. *)
   333 (* Generates the replacement lemma in fully quantified form. *)
   336 fun mk_replacement_lemma thy h ih_elim clause =
   334 fun mk_replacement_lemma ctxt h ih_elim clause =
   337   let
   335   let
   338     val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
   336     val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
   339       RCs, tree, ...} = clause
   337       RCs, tree, ...} = clause
   340     local open Conv in
   338     local open Conv in
   341       val ih_conv = arg1_conv o arg_conv o arg_conv
   339       val ih_conv = arg1_conv o arg_conv o arg_conv
   344     val ih_elim_case =
   342     val ih_elim_case =
   345       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
   343       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
   346 
   344 
   347     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   345     val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   348     val h_assums = map (fn RCInfo {h_assum, ...} =>
   346     val h_assums = map (fn RCInfo {h_assum, ...} =>
   349       Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
   347       Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs
   350 
   348 
   351     val (eql, _) =
   349     val (eql, _) =
   352       Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy)
   350       Function_Context_Tree.rewrite_by_tree ctxt
   353         h ih_elim_case (Ris ~~ h_assums) tree
   351         h ih_elim_case (Ris ~~ h_assums) tree
   354 
   352 
   355     val replace_lemma = (eql RS meta_eq_to_obj_eq)
   353     val replace_lemma = (eql RS meta_eq_to_obj_eq)
   356       |> Thm.implies_intr (cprop_of case_hyp)
   354       |> Thm.implies_intr (Thm.cprop_of case_hyp)
   357       |> fold_rev (Thm.implies_intr o cprop_of) h_assums
   355       |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
   358       |> fold_rev (Thm.implies_intr o cprop_of) ags
   356       |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
   359       |> fold_rev Thm.forall_intr cqs
   357       |> fold_rev Thm.forall_intr cqs
   360       |> Thm.close_derivation
   358       |> Thm.close_derivation
   361   in
   359   in
   362     replace_lemma
   360     replace_lemma
   363   end
   361   end
   364 
   362 
   365 (* nominal *)
   363 (* nominal *)
   366 (* Generates the eqvt lemmas for each clause *) 
   364 (* Generates the eqvt lemmas for each clause *) 
   367 fun mk_eqvt_lemma thy ih_eqvt clause =
   365 fun mk_eqvt_lemma ctxt ih_eqvt clause =
   368   let
   366   let
   369     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
   367     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
   370      
   368      
   371     local open Conv in
   369     local open Conv in
   372       val ih_conv = arg1_conv o arg_conv o arg_conv
   370       val ih_conv = arg1_conv o arg_conv o arg_conv
   375     val ih_eqvt_case =
   373     val ih_eqvt_case =
   376       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
   374       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
   377 
   375 
   378     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
   376     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
   379         (llRI RS ih_eqvt_case)
   377         (llRI RS ih_eqvt_case)
   380         |> fold_rev (Thm.implies_intr o cprop_of) CCas
   378         |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
   381         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs 
   379         |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs 
   382   in
   380   in
   383     map prep_eqvt RCs
   381     map prep_eqvt RCs
   384     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
   382     |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
   385     |> map (Thm.implies_intr (cprop_of case_hyp))
   383     |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
   386     |> map (fold_rev Thm.forall_intr cqs)
   384     |> map (fold_rev Thm.forall_intr cqs)
   387     |> map (Thm.close_derivation) 
   385     |> map (Thm.close_derivation) 
   388   end
   386   end
   389 
   387 
   390 (* nominal *)
   388 (* nominal *)
   391 fun mk_invariant_lemma thy ih_inv clause =
   389 fun mk_invariant_lemma ctxt ih_inv clause =
   392   let
   390   let
   393     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
   391     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
   394      
   392      
   395     local open Conv in
   393     local open Conv in
   396       val ih_conv = arg1_conv o arg_conv o arg_conv
   394       val ih_conv = arg1_conv o arg_conv o arg_conv
   399     val ih_inv_case =
   397     val ih_inv_case =
   400       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv
   398       Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv
   401 
   399 
   402     fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) = 
   400     fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) = 
   403         (llRI RS ih_inv_case)
   401         (llRI RS ih_inv_case)
   404         |> fold_rev (Thm.implies_intr o cprop_of) CCas
   402         |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
   405         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs 
   403         |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs 
   406   in
   404   in
   407     map prep_inv RCs
   405     map prep_inv RCs
   408     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
   406     |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
   409     |> map (Thm.implies_intr (cprop_of case_hyp))
   407     |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
   410     |> map (fold_rev Thm.forall_intr cqs)
   408     |> map (fold_rev Thm.forall_intr cqs)
   411     |> map (Thm.close_derivation) 
   409     |> map (Thm.close_derivation) 
   412   end
   410   end
   413 
   411 
   414 (* nominal *)
   412 (* nominal *)
   415 fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj =
   413 fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj =
   416   let
   414   let
       
   415     val thy = Proof_Context.theory_of ctxt
       
   416 
   417     val Globals {h, y, x, fvar, ...} = globals
   417     val Globals {h, y, x, fvar, ...} = globals
   418     val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 
   418     val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 
   419       ags = agsi, ...}, ...} = clausei
   419       ags = agsi, ...}, ...} = clausei
   420     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   420     val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
   421 
   421 
   423       mk_clause_context x ctxti cdescj 
   423       mk_clause_context x ctxti cdescj 
   424 
   424 
   425     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   425     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
   426 
   426 
   427     val Ghsj' = map 
   427     val Ghsj' = map 
   428       (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
   428       (fn RCInfo {h_assum, ...} =>
   429 
   429         Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj
   430     val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
   430 
   431     val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
   431     val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
       
   432     val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
   432        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 
   433        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 
   433 
   434 
   434     val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
   435     val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
   435 
   436 
   436     val RLj_import = RLj
   437     val RLj_import = RLj
   456     val invsj = nth invs (j - 1)
   457     val invsj = nth invs (j - 1)
   457       |> map (fold Thm.forall_elim cqsj')
   458       |> map (fold Thm.forall_elim cqsj')
   458       |> map (fold Thm.elim_implies [case_hypj'])
   459       |> map (fold Thm.elim_implies [case_hypj'])
   459       |> map (fold Thm.elim_implies agsj')
   460       |> map (fold Thm.elim_implies agsj')
   460 
   461 
   461     val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
   462     val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
   462 
   463 
   463   in
   464   in
   464     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   465     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   465     |> Thm.implies_elim RLj_import
   466     |> Thm.implies_elim RLj_import
   466       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   467       (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   467     |> (fn it => trans OF [it, compat])
   468     |> (fn it => trans OF [it, compat])
   468       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   469       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   469     |> (fn it => trans OF [y_eq_rhsj'h, it])
   470     |> (fn it => trans OF [y_eq_rhsj'h, it])
   470       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   471       (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   471     |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
   472     |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj'
   472     |> fold_rev (Thm.implies_intr o cprop_of) agsj'
   473     |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj'
   473       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   474       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
   474     |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
   475     |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h)
   475     |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
   476     |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj')
   476     |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
   477     |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj')
   477   end
   478   end
   478 
   479 
   479 (* nominal *)
   480 (* nominal *)
   480 fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems 
   481 fun mk_uniqueness_case ctxt
   481   clausei =
   482     globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei =
   482   let
   483   let
       
   484     val thy = Proof_Context.theory_of ctxt
       
   485 
   483     val Globals {x, y, ranT, fvar, ...} = globals
   486     val Globals {x, y, ranT, fvar, ...} = globals
   484     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   487     val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
   485     val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   488     val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
   486 
   489 
   487     val ih_intro_case =
   490     val ih_intro_case =
   488       full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
   491       full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
   489         ih_intro
   492         ih_intro
   490 
   493 
   491     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 
   494     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 
   492         (llRI RS ih_intro_case)
   495         (llRI RS ih_intro_case)
   493         |> fold_rev (Thm.implies_intr o cprop_of) CCas
   496         |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
   494         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
   497         |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
   495  
   498  
   496     val existence = fold (curry op COMP o prep_RC) RCs lGI
   499     val existence = fold (curry op COMP o prep_RC) RCs lGI
   497 
   500 
   498     val P = cterm_of thy (mk_eq (y, rhsC))
   501     val P = Thm.cterm_of ctxt (mk_eq (y, rhsC))
   499     val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
   502     val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
   500 
   503 
   501     val unique_clauses =
   504     val unique_clauses =
   502       map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
   505       map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems
   503 
   506 
   504     fun elim_implies_eta A AB =
   507     fun elim_implies_eta A AB =
   505       Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
   508       Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
   506       |> Seq.list_of |> the_single
   509       |> Seq.list_of |> the_single
   507 
   510 
   508     val uniqueness = G_cases
   511     val uniqueness = G_cases
   509       |> Thm.forall_elim (cterm_of thy lhs)
   512       |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
   510       |> Thm.forall_elim (cterm_of thy y)
   513       |> Thm.forall_elim (Thm.cterm_of ctxt y)
   511       |> Thm.forall_elim P
   514       |> Thm.forall_elim P
   512       |> Thm.elim_implies G_lhs_y
   515       |> Thm.elim_implies G_lhs_y
   513       |> fold elim_implies_eta unique_clauses
   516       |> fold elim_implies_eta unique_clauses
   514       |> Thm.implies_intr (cprop_of G_lhs_y)
   517       |> Thm.implies_intr (Thm.cprop_of G_lhs_y)
   515       |> Thm.forall_intr (cterm_of thy y)
   518       |> Thm.forall_intr (Thm.cterm_of ctxt y)
   516 
   519 
   517     val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   520     val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
   518 
   521 
   519     val exactly_one =
   522     val exactly_one =
   520       ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
   523       ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
   521       |> curry (op COMP) existence
   524       |> curry (op COMP) existence
   522       |> curry (op COMP) uniqueness
   525       |> curry (op COMP) uniqueness
   523       |> simplify
   526       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
   524           (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym])
   527       |> Thm.implies_intr (Thm.cprop_of case_hyp)
   525       |> Thm.implies_intr (cprop_of case_hyp)
   528       |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
   526       |> fold_rev (Thm.implies_intr o cprop_of) ags
       
   527       |> fold_rev Thm.forall_intr cqs
   529       |> fold_rev Thm.forall_intr cqs
   528 
   530 
   529     val function_value =
   531     val function_value =
   530       existence
   532       existence
   531       |> Thm.implies_intr ihyp
   533       |> Thm.implies_intr ihyp
   532       |> Thm.implies_intr (cprop_of case_hyp)
   534       |> Thm.implies_intr (Thm.cprop_of case_hyp)
   533       |> Thm.forall_intr (cterm_of thy x)
   535       |> Thm.forall_intr (Thm.cterm_of ctxt x)
   534       |> Thm.forall_elim (cterm_of thy lhs)
   536       |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
   535       |> curry (op RS) refl
   537       |> curry (op RS) refl
   536   in
   538   in
   537     (exactly_one, function_value)
   539     (exactly_one, function_value)
   538   end
   540   end
   539 
   541 
   540 
   542 
   541 (* nominal *)
   543 (* nominal *)
   542 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
   544 fun prove_stuff ctxt
       
   545     globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
   543   let
   546   let
   544     val Globals {h, domT, ranT, x, ...} = globals
   547     val Globals {h, domT, ranT, x, ...} = globals
   545     val thy = Proof_Context.theory_of ctxt
       
   546 
   548 
   547     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   549     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   548     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   550     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   549       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   551       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   550         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
   552         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
   551           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   553           Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
   552       |> cterm_of thy
   554       |> Thm.cterm_of ctxt
   553 
   555 
   554     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
   556     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
   555     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   557     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   556     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   558     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   557       |> instantiate' [] [NONE, SOME (cterm_of thy h)]
   559       |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
   558     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
   560     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
   559     val ih_inv =  ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
   561     val ih_inv =  ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
   560 
   562 
   561     val _ = trace_msg (K "Proving Replacement lemmas...")
   563     val _ = trace_msg (K "Proving Replacement lemmas...")
   562     val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
   564     val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
   563 
   565 
   564     val _ = trace_msg (K "Proving Equivariance lemmas...")
   566     val _ = trace_msg (K "Proving Equivariance lemmas...")
   565     val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
   567     val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses
   566 
   568 
   567     val _ = trace_msg (K "Proving Invariance lemmas...")
   569     val _ = trace_msg (K "Proving Invariance lemmas...")
   568     val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses
   570     val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses
   569 
   571 
   570     val _ = trace_msg (K "Proving cases for unique existence...")
   572     val _ = trace_msg (K "Proving cases for unique existence...")
   571     val (ex1s, values) =
   573     val (ex1s, values) =
   572       split_list (map (mk_uniqueness_case thy globals G f 
   574       split_list (map (mk_uniqueness_case ctxt globals G f 
   573         ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
   575         ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
   574      
   576      
   575     val _ = trace_msg (K "Proving: Graph is a function")
   577     val _ = trace_msg (K "Proving: Graph is a function")
   576     val graph_is_function = complete
   578     val graph_is_function = complete
   577       |> Thm.forall_elim_vars 0
   579       |> Thm.forall_elim_vars 0
   578       |> fold (curry op COMP) ex1s
   580       |> fold (curry op COMP) ex1s
   579       |> Thm.implies_intr (ihyp)
   581       |> Thm.implies_intr ihyp
   580       |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   582       |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   581       |> Thm.forall_intr (cterm_of thy x)
   583       |> Thm.forall_intr (Thm.cterm_of ctxt x)
   582       |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   584       |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   583       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
   585       |> (fn it =>
       
   586           fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it)
   584 
   587 
   585     val goalstate =  
   588     val goalstate =  
   586          Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt 
   589       Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
   587       |> Thm.close_derivation
   590       |> Thm.close_derivation
   588       |> Goal.protect 0
   591       |> Goal.protect 0
   589       |> fold_rev (Thm.implies_intr o cprop_of) compat
   592       |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
   590       |> Thm.implies_intr (cprop_of complete)
   593       |> Thm.implies_intr (Thm.cprop_of complete)
   591       |> Thm.implies_intr (cprop_of invariant)
   594       |> Thm.implies_intr (Thm.cprop_of invariant)
   592       |> Thm.implies_intr (cprop_of G_eqvt)
   595       |> Thm.implies_intr (Thm.cprop_of G_eqvt)
   593   in
   596   in
   594     (goalstate, values)
   597     (goalstate, values)
   595   end
   598   end
   596 
   599 
   597 (* wrapper -- restores quantifiers in rule specifications *)
   600 (* wrapper -- restores quantifiers in rule specifications *)
   598 fun inductive_def (binding as ((R, T), _)) intrs lthy =
   601 fun inductive_def (binding as ((R, T), _)) intrs lthy =
   599   let 
   602   let 
   600     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
   603     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
   601       lthy
   604       lthy
   602       |> Local_Theory.conceal
   605       |> Proof_Context.concealed
   603       |> Inductive.add_inductive_i
   606       |> Inductive.add_inductive_i
   604           {quiet_mode = true,
   607           {quiet_mode = true,
   605             verbose = ! trace,
   608             verbose = ! trace,
   606             alt_name = Binding.empty,
   609             alt_name = Binding.empty,
   607             coind = false,
   610             coind = false,
   610             skip_mono = true}
   613             skip_mono = true}
   611           [binding] (* relation *)
   614           [binding] (* relation *)
   612           [] (* no parameters *)
   615           [] (* no parameters *)
   613           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
   616           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
   614           [] (* no special monos *)
   617           [] (* no special monos *)
   615       ||> Local_Theory.restore_naming lthy
   618       ||> Proof_Context.restore_naming lthy
   616 
   619 
   617     val cert = cterm_of (Proof_Context.theory_of lthy)
   620     val cert = Thm.cterm_of lthy
   618     fun requantify orig_intro thm =
   621     fun requantify orig_intro thm =
   619       let
   622       let
   620         val (qs, t) = dest_all_all orig_intro
   623         val (qs, t) = dest_all_all orig_intro
   621         val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
   624         val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
   622         val vars = Term.add_vars (prop_of thm) []
   625         val vars = Term.add_vars (Thm.prop_of thm) []
   623         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
   626         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
   624            #> the_default ("",0)
   627            #> the_default ("",0)
   625       in
   628       in
   626         fold_rev (fn Free (n, T) =>
   629         fold_rev (fn Free (n, T) =>
   627           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
   630           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
   638 
   641 
   639     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   642     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   640       let
   643       let
   641         fun mk_h_assm (rcfix, rcassm, rcarg) =
   644         fun mk_h_assm (rcfix, rcassm, rcarg) =
   642           HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
   645           HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
   643           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   646           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
   644           |> fold_rev (Logic.all o Free) rcfix
   647           |> fold_rev (Logic.all o Free) rcfix
   645       in
   648       in
   646         HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
   649         HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
   647         |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   650         |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   648         |> fold_rev (curry Logic.mk_implies) gs
   651         |> fold_rev (curry Logic.mk_implies) gs
   661         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   664         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   662       |> Syntax.check_term lthy
   665       |> Syntax.check_term lthy
   663   in
   666   in
   664     Local_Theory.define
   667     Local_Theory.define
   665       ((Binding.name (function_name fname), mixfix),
   668       ((Binding.name (function_name fname), mixfix),
   666         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   669         ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
   667   end
   670   end
   668 
   671 
   669 (* nominal *)
   672 (* nominal *)
   670 fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
   673 fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
   671   let
   674   let
   672     val RT = domT --> domT --> boolT
   675     val RT = domT --> domT --> boolT
   673     val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
   676     val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
   674 
   677 
   675     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   678     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   676       HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
   679       HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
   677       |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   680       |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
   678       |> fold_rev (curry Logic.mk_implies) gs
   681       |> fold_rev (curry Logic.mk_implies) gs
   679       |> fold_rev (Logic.all o Free) rcfix
   682       |> fold_rev (Logic.all o Free) rcfix
   680       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   683       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   681       (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
   684       (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
   682 
   685 
   689   end
   692   end
   690 
   693 
   691 
   694 
   692 fun fix_globals domT ranT fvar ctxt =
   695 fun fix_globals domT ranT fvar ctxt =
   693   let
   696   let
   694     val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
   697     val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes
   695       ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   698       ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
   696   in
   699   in
   697     (Globals {h = Free (h, domT --> ranT),
   700     (Globals {h = Free (h, domT --> ranT),
   698       y = Free (y, ranT),
   701       y = Free (y, ranT),
   699       x = Free (x, domT),
   702       x = Free (x, domT),
   706       domT = domT,
   709       domT = domT,
   707       ranT = ranT},
   710       ranT = ranT},
   708     ctxt')
   711     ctxt')
   709   end
   712   end
   710 
   713 
   711 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
   714 fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) =
   712   let
   715   let
   713     fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   716     fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   714   in
   717   in
   715     (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
   718     (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg)
   716   end
   719   end
   717 
   720 
   718 
   721 
   719 
   722 
   720 (**********************************************************
   723 (**********************************************************
   721  *                   PROVING THE RULES
   724  *                   PROVING THE RULES
   722  **********************************************************)
   725  **********************************************************)
   723 
   726 
   724 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
   727 fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
   725   let
   728   let
   726     val Globals {domT, z, ...} = globals
   729     val Globals {domT, z, ...} = globals
   727 
   730 
   728     fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   731     fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
   729       let
   732       let
   730         val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   733         val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
   731         val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   734         val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
   732       in
   735       in
   733         ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
   736         ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
   734         |> (fn it => it COMP graph_is_function)
   737         |> (fn it => it COMP graph_is_function)
   735         |> Thm.implies_intr z_smaller
   738         |> Thm.implies_intr z_smaller
   736         |> Thm.forall_intr (cterm_of thy z)
   739         |> Thm.forall_intr (Thm.cterm_of ctxt z)
   737         |> (fn it => it COMP valthm)
   740         |> (fn it => it COMP valthm)
   738         |> Thm.implies_intr lhs_acc
   741         |> Thm.implies_intr lhs_acc
   739         |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff])
   742         |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
   740         |> fold_rev (Thm.implies_intr o cprop_of) ags
   743         |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
   741         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   744         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   742       end
   745       end
   743   in
   746   in
   744     map2 mk_psimp clauses valthms
   747     map2 mk_psimp clauses valthms
   745   end
   748   end
   749 
   752 
   750 
   753 
   751 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
   754 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
   752 
   755 
   753 
   756 
   754 fun mk_partial_induct_rule thy globals R complete_thm clauses =
   757 fun mk_partial_induct_rule ctxt globals R complete_thm clauses =
   755   let
   758   let
   756     val Globals {domT, x, z, a, P, D, ...} = globals
   759     val Globals {domT, x, z, a, P, D, ...} = globals
   757     val acc_R = mk_acc domT R
   760     val acc_R = mk_acc domT R
   758 
   761 
   759     val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
   762     val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x)))
   760     val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
   763     val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a))
   761 
   764 
   762     val D_subset = cterm_of thy (Logic.all x
   765     val D_subset = Thm.cterm_of ctxt (Logic.all x
   763       (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
   766       (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
   764 
   767 
   765     val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   768     val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   766       Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   769       Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
   767         Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   770         Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
   768           HOLogic.mk_Trueprop (D $ z)))))
   771           HOLogic.mk_Trueprop (D $ z)))))
   769       |> cterm_of thy
   772       |> Thm.cterm_of ctxt
   770 
   773 
   771     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   774     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   772     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   775     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   773       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   776       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
   774         HOLogic.mk_Trueprop (P $ Bound 0)))
   777         HOLogic.mk_Trueprop (P $ Bound 0)))
   775       |> cterm_of thy
   778       |> Thm.cterm_of ctxt
   776 
   779 
   777     val aihyp = Thm.assume ihyp
   780     val aihyp = Thm.assume ihyp
   778 
   781 
   779     fun prove_case clause =
   782     fun prove_case clause =
   780       let
   783       let
   781         val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
   784         val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...},
   782           RCs, qglr = (oqs, _, _, _), ...} = clause
   785           RCs, qglr = (oqs, _, _, _), ...} = clause
   783 
   786 
   784         val case_hyp_conv = K (case_hyp RS eq_reflection)
   787         val case_hyp_conv = K (case_hyp RS eq_reflection)
   785         local open Conv in
   788         local open Conv in
   786           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
   789           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
   787           val sih =
   790           val sih =
   788             fconv_rule (Conv.binder_conv
   791             fconv_rule (Conv.binder_conv
   789               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
   792               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp
   790         end
   793         end
   791 
   794 
   792         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
   795         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
   793           |> Thm.forall_elim (cterm_of thy rcarg)
   796           |> Thm.forall_elim (Thm.cterm_of ctxt rcarg)
   794           |> Thm.elim_implies llRI
   797           |> Thm.elim_implies llRI
   795           |> fold_rev (Thm.implies_intr o cprop_of) CCas
   798           |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
   796           |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
   799           |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
   797 
   800 
   798         val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   801         val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   799 
   802 
   800         val step = HOLogic.mk_Trueprop (P $ lhs)
   803         val step = HOLogic.mk_Trueprop (P $ lhs)
   801           |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   804           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
   802           |> fold_rev (curry Logic.mk_implies) gs
   805           |> fold_rev (curry Logic.mk_implies) gs
   803           |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   806           |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
   804           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   807           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   805           |> cterm_of thy
   808           |> Thm.cterm_of ctxt
   806 
   809 
   807         val P_lhs = Thm.assume step
   810         val P_lhs = Thm.assume step
   808           |> fold Thm.forall_elim cqs
   811           |> fold Thm.forall_elim cqs
   809           |> Thm.elim_implies lhs_D
   812           |> Thm.elim_implies lhs_D
   810           |> fold Thm.elim_implies ags
   813           |> fold Thm.elim_implies ags
   811           |> fold Thm.elim_implies P_recs
   814           |> fold Thm.elim_implies P_recs
   812 
   815 
   813         val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
   816         val res =
       
   817           Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x))
   814           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
   818           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
   815           |> Thm.symmetric (* P lhs == P x *)
   819           |> Thm.symmetric (* P lhs == P x *)
   816           |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
   820           |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
   817           |> Thm.implies_intr (cprop_of case_hyp)
   821           |> Thm.implies_intr (Thm.cprop_of case_hyp)
   818           |> fold_rev (Thm.implies_intr o cprop_of) ags
   822           |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
   819           |> fold_rev Thm.forall_intr cqs
   823           |> fold_rev Thm.forall_intr cqs
   820       in
   824       in
   821         (res, step)
   825         (res, step)
   822       end
   826       end
   823 
   827 
   825 
   829 
   826     val istep = complete_thm
   830     val istep = complete_thm
   827       |> Thm.forall_elim_vars 0
   831       |> Thm.forall_elim_vars 0
   828       |> fold (curry op COMP) cases (*  P x  *)
   832       |> fold (curry op COMP) cases (*  P x  *)
   829       |> Thm.implies_intr ihyp
   833       |> Thm.implies_intr ihyp
   830       |> Thm.implies_intr (cprop_of x_D)
   834       |> Thm.implies_intr (Thm.cprop_of x_D)
   831       |> Thm.forall_intr (cterm_of thy x)
   835       |> Thm.forall_intr (Thm.cterm_of ctxt x)
   832 
   836 
   833     val subset_induct_rule =
   837     val subset_induct_rule =
   834       acc_subset_induct
   838       acc_subset_induct
   835       |> (curry op COMP) (Thm.assume D_subset)
   839       |> (curry op COMP) (Thm.assume D_subset)
   836       |> (curry op COMP) (Thm.assume D_dcl)
   840       |> (curry op COMP) (Thm.assume D_dcl)
   841       |> Thm.implies_intr D_dcl
   845       |> Thm.implies_intr D_dcl
   842       |> Thm.implies_intr D_subset
   846       |> Thm.implies_intr D_subset
   843 
   847 
   844     val simple_induct_rule =
   848     val simple_induct_rule =
   845       subset_induct_rule
   849       subset_induct_rule
   846       |> Thm.forall_intr (cterm_of thy D)
   850       |> Thm.forall_intr (Thm.cterm_of ctxt D)
   847       |> Thm.forall_elim (cterm_of thy acc_R)
   851       |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
   848       |> assume_tac 1 |> Seq.hd
   852       |> atac 1 |> Seq.hd
   849       |> (curry op COMP) (acc_downward
   853       |> (curry op COMP) (acc_downward
   850         |> (instantiate' [SOME (ctyp_of thy domT)]
   854         |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
   851              (map (SOME o cterm_of thy) [R, x, z]))
   855              (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   852         |> Thm.forall_intr (cterm_of thy z)
   856         |> Thm.forall_intr (Thm.cterm_of ctxt z)
   853         |> Thm.forall_intr (cterm_of thy x))
   857         |> Thm.forall_intr (Thm.cterm_of ctxt x))
   854       |> Thm.forall_intr (cterm_of thy a)
   858       |> Thm.forall_intr (Thm.cterm_of ctxt a)
   855       |> Thm.forall_intr (cterm_of thy P)
   859       |> Thm.forall_intr (Thm.cterm_of ctxt P)
   856   in
   860   in
   857     simple_induct_rule
   861     simple_induct_rule
   858   end
   862   end
   859 
   863 
   860 
   864 
   861 (* FIXME: broken by design *)
   865 (* FIXME: broken by design *)
   862 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   866 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   863   let
   867   let
   864     val thy = Proof_Context.theory_of ctxt
       
   865     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
   868     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
   866       qglr = (oqs, _, _, _), ...} = clause
   869       qglr = (oqs, _, _, _), ...} = clause
   867     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
   870     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
   868       |> fold_rev (curry Logic.mk_implies) gs
   871       |> fold_rev (curry Logic.mk_implies) gs
   869       |> cterm_of thy
   872       |> Thm.cterm_of ctxt
   870   in
   873   in
   871     Goal.init goal
   874     Goal.init goal
   872     |> (SINGLE (resolve_tac [accI] 1)) |> the
   875     |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
   873     |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
   876     |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1))  |> the
   874     |> (SINGLE (auto_tac ctxt)) |> the
   877     |> (SINGLE (auto_tac ctxt)) |> the
   875     |> Goal.conclude
   878     |> Goal.conclude
   876     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   879     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   877   end
   880   end
   878 
   881 
   882 
   885 
   883 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
   886 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
   884 val wf_in_rel = @{thm Fun_Def.wf_in_rel}
   887 val wf_in_rel = @{thm Fun_Def.wf_in_rel}
   885 val in_rel_def = @{thm Fun_Def.in_rel_def}
   888 val in_rel_def = @{thm Fun_Def.in_rel_def}
   886 
   889 
   887 fun mk_nest_term_case thy globals R' ihyp clause =
   890 fun mk_nest_term_case ctxt globals R' ihyp clause =
   888   let
   891   let
   889     val Globals {z, ...} = globals
   892     val Globals {z, ...} = globals
   890     val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
   893     val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
   891       qglr=(oqs, _, _, _), ...} = clause
   894       qglr=(oqs, _, _, _), ...} = clause
   892 
   895 
   893     val ih_case =
   896     val ih_case =
   894       full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
   897       full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
   895         ihyp
   898         ihyp
   896 
   899 
   897     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
   900     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
   898       let
   901       let
   899         val used = (u @ sub)
   902         val used = (u @ sub)
   900           |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
   903           |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm)
   901 
   904 
   902         val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
   905         val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
   903           |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
   906           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *)
   904           |> Function_Ctx_Tree.export_term (fixes, assumes)
   907           |> Function_Context_Tree.export_term (fixes, assumes)
   905           |> fold_rev (curry Logic.mk_implies o prop_of) ags
   908           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags
   906           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   909           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   907           |> cterm_of thy
   910           |> Thm.cterm_of ctxt
   908 
   911 
   909         val thm = Thm.assume hyp
   912         val thm = Thm.assume hyp
   910           |> fold Thm.forall_elim cqs
   913           |> fold Thm.forall_elim cqs
   911           |> fold Thm.elim_implies ags
   914           |> fold Thm.elim_implies ags
   912           |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
   915           |> Function_Context_Tree.import_thm ctxt (fixes, assumes)
   913           |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
   916           |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
   914 
   917 
   915         val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
   918         val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
   916           |> cterm_of thy |> Thm.assume
   919           |> Thm.cterm_of ctxt |> Thm.assume
   917 
   920 
   918         val acc = thm COMP ih_case
   921         val acc = thm COMP ih_case
   919         val z_acc_local = acc
   922         val z_acc_local = acc
   920           |> Conv.fconv_rule
   923           |> Conv.fconv_rule
   921               (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
   924               (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
   922 
   925 
   923         val ethm = z_acc_local
   926         val ethm = z_acc_local
   924           |> Function_Ctx_Tree.export_thm thy (fixes,
   927           |> Function_Context_Tree.export_thm ctxt (fixes,
   925                z_eq_arg :: case_hyp :: ags @ assumes)
   928                z_eq_arg :: case_hyp :: ags @ assumes)
   926           |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   929           |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   927 
   930 
   928         val sub' = sub @ [(([],[]), acc)]
   931         val sub' = sub @ [(([],[]), acc)]
   929       in
   932       in
   930         (sub', (hyp :: hyps, ethm :: thms))
   933         (sub', (hyp :: hyps, ethm :: thms))
   931       end
   934       end
   932       | step _ _ _ _ = raise Match
   935       | step _ _ _ _ = raise Match
   933   in
   936   in
   934     Function_Ctx_Tree.traverse_tree step tree
   937     Function_Context_Tree.traverse_tree step tree
   935   end
   938   end
   936 
   939 
   937 
   940 
   938 fun mk_nest_term_rule thy globals R R_cases clauses =
   941 fun mk_nest_term_rule ctxt globals R R_cases clauses =
   939   let
   942   let
   940     val Globals { domT, x, z, ... } = globals
   943     val Globals { domT, x, z, ... } = globals
   941     val acc_R = mk_acc domT R
   944     val acc_R = mk_acc domT R
   942 
   945 
   943     val R' = Free ("R", fastype_of R)
   946     val R' = Free ("R", fastype_of R)
   946     val inrel_R = Const (@{const_name Fun_Def.in_rel},
   949     val inrel_R = Const (@{const_name Fun_Def.in_rel},
   947       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   950       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   948 
   951 
   949     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
   952     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
   950       (domT --> domT --> boolT) --> boolT) $ R')
   953       (domT --> domT --> boolT) --> boolT) $ R')
   951       |> cterm_of thy (* "wf R'" *)
   954       |> Thm.cterm_of ctxt (* "wf R'" *)
   952 
   955 
   953     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   956     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   954     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   957     val ihyp = Logic.all_const domT $ Abs ("z", domT,
   955       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
   958       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
   956         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
   959         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
   957       |> cterm_of thy
   960       |> Thm.cterm_of ctxt
   958 
   961 
   959     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
   962     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
   960 
   963 
   961     val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
   964     val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
   962 
   965 
   963     val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
   966     val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
   964   in
   967   in
   965     R_cases
   968     R_cases
   966     |> Thm.forall_elim (cterm_of thy z)
   969     |> Thm.forall_elim (Thm.cterm_of ctxt z)
   967     |> Thm.forall_elim (cterm_of thy x)
   970     |> Thm.forall_elim (Thm.cterm_of ctxt x)
   968     |> Thm.forall_elim (cterm_of thy (acc_R $ z))
   971     |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z))
   969     |> curry op COMP (Thm.assume R_z_x)
   972     |> curry op COMP (Thm.assume R_z_x)
   970     |> fold_rev (curry op COMP) cases
   973     |> fold_rev (curry op COMP) cases
   971     |> Thm.implies_intr R_z_x
   974     |> Thm.implies_intr R_z_x
   972     |> Thm.forall_intr (cterm_of thy z)
   975     |> Thm.forall_intr (Thm.cterm_of ctxt z)
   973     |> (fn it => it COMP accI)
   976     |> (fn it => it COMP accI)
   974     |> Thm.implies_intr ihyp
   977     |> Thm.implies_intr ihyp
   975     |> Thm.forall_intr (cterm_of thy x)
   978     |> Thm.forall_intr (Thm.cterm_of ctxt x)
   976     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
   979     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
   977     |> curry op RS (Thm.assume wfR')
   980     |> curry op RS (Thm.assume wfR')
   978     |> forall_intr_vars
   981     |> forall_intr_vars
   979     |> (fn it => it COMP allI)
   982     |> (fn it => it COMP allI)
   980     |> fold Thm.implies_intr hyps
   983     |> fold Thm.implies_intr hyps
   981     |> Thm.implies_intr wfR'
   984     |> Thm.implies_intr wfR'
   982     |> Thm.forall_intr (cterm_of thy R')
   985     |> Thm.forall_intr (Thm.cterm_of ctxt R')
   983     |> Thm.forall_elim (cterm_of thy (inrel_R))
   986     |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R))
   984     |> curry op RS wf_in_rel
   987     |> curry op RS wf_in_rel
   985     |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def])
   988     |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
   986     |> Thm.forall_intr (cterm_of thy Rrel)
   989     |> Thm.forall_intr (Thm.cterm_of ctxt Rrel)
   987   end
   990   end
   988 
   991 
   989 
   992 
   990 
   993 
   991 (* nominal *)
   994 (* nominal *)
  1012     val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  1015     val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  1013 
  1016 
  1014     val n = length abstract_qglrs
  1017     val n = length abstract_qglrs
  1015 
  1018 
  1016     fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  1019     fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  1017        Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
  1020        Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs
  1018 
  1021 
  1019     val trees = map build_tree clauses
  1022     val trees = map build_tree clauses
  1020     val RCss = map find_calls trees
  1023     val RCss = map find_calls trees
  1021 
  1024 
  1022     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  1025     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  1023       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  1026       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  1024 
  1027 
  1025     val ((f, (_, f_defthm)), lthy) =
  1028     val ((f, (_, f_defthm)), lthy) =
  1026       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  1029       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  1027 
  1030 
  1028     val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
  1031     val RCss = map (map (inst_RC lthy fvar f)) RCss
  1029     val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
  1032     val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
  1030 
  1033 
  1031     val ((R, RIntro_thmss, R_elim), lthy) =
  1034     val ((R, RIntro_thmss, R_elim), lthy) =
  1032       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
  1035       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
  1033 
  1036 
  1034     val (_, lthy) =
  1037     val (_, lthy) =
  1035       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  1038       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  1036 
  1039 
  1037     val newthy = Proof_Context.theory_of lthy
  1040     val newthy = Proof_Context.theory_of lthy
  1038     val clauses = map (transfer_clause_ctx newthy) clauses
  1041     val clauses = map (transfer_clause_ctx newthy) clauses
  1039 
  1042 
  1040     val cert = cterm_of (Proof_Context.theory_of lthy)
  1043     val cert = Thm.cterm_of lthy
  1041 
  1044 
  1042     val xclauses = PROFILE "xclauses"
  1045     val xclauses = PROFILE "xclauses"
  1043       (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
  1046       (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
  1044         RCss GIntro_thms) RIntro_thmss
  1047         RCss GIntro_thms) RIntro_thmss
  1045 
  1048 
  1046     val complete =
  1049     val complete =
  1047       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
  1050       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
  1048 
  1051 
  1060       (prove_stuff lthy globals G f R xclauses complete compat
  1063       (prove_stuff lthy globals G f R xclauses complete compat
  1061          compat_store G_elim G_eqvt invariant) f_defthm
  1064          compat_store G_elim G_eqvt invariant) f_defthm
  1062      
  1065      
  1063     fun mk_partial_rules provedgoal =
  1066     fun mk_partial_rules provedgoal =
  1064       let
  1067       let
  1065         val newthy = theory_of_thm provedgoal (*FIXME*)
  1068         val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
       
  1069         val newctxt = Proof_Context.init_global newthy (*FIXME*)
  1066 
  1070 
  1067         val ((graph_is_function, complete_thm), graph_is_eqvt) =
  1071         val ((graph_is_function, complete_thm), graph_is_eqvt) =
  1068           provedgoal
  1072           provedgoal
  1069           |> Conjunction.elim
  1073           |> Conjunction.elim
  1070           |>> fst o Conjunction.elim
  1074           |>> fst o Conjunction.elim
  1073 
  1077 
  1074         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  1078         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  1075         val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
  1079         val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
  1076 
  1080 
  1077         val psimps = PROFILE "Proving simplification rules"
  1081         val psimps = PROFILE "Proving simplification rules"
  1078           (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  1082           (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function
  1079 
  1083 
  1080         val simple_pinduct = PROFILE "Proving partial induction rule"
  1084         val simple_pinduct = PROFILE "Proving partial induction rule"
  1081           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  1085           (mk_partial_induct_rule newctxt globals R complete_thm) xclauses
  1082 
  1086 
  1083         val total_intro = PROFILE "Proving nested termination rule"
  1087         val total_intro = PROFILE "Proving nested termination rule"
  1084           (mk_nest_term_rule newthy globals R R_elim) xclauses
  1088           (mk_nest_term_rule newctxt globals R R_elim) xclauses
  1085 
  1089 
  1086         val dom_intros =
  1090         val dom_intros =
  1087           if domintros then SOME (PROFILE "Proving domain introduction rules"
  1091           if domintros then SOME (PROFILE "Proving domain introduction rules"
  1088              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  1092              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  1089            else NONE
  1093            else NONE