612 no_elim = false, |
612 no_elim = false, |
613 no_ind = false, |
613 no_ind = false, |
614 skip_mono = true} |
614 skip_mono = true} |
615 [binding] (* relation *) |
615 [binding] (* relation *) |
616 [] (* no parameters *) |
616 [] (* no parameters *) |
617 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
617 (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *) |
618 [] (* no special monos *) |
618 [] (* no special monos *) |
619 ||> Proof_Context.restore_naming lthy |
619 ||> Proof_Context.restore_naming lthy |
620 ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals) |
620 ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals) |
621 |
621 |
622 val cert = Thm.cterm_of lthy |
622 val cert = Thm.cterm_of lthy |
665 Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
665 Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
666 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
666 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
667 |> Syntax.check_term lthy |
667 |> Syntax.check_term lthy |
668 in |
668 in |
669 Local_Theory.define |
669 Local_Theory.define |
670 ((Binding.name (function_name fname), mixfix), |
670 ((Binding.name (fname ^ "C"), mixfix), |
671 ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy |
671 ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy |
672 end |
672 end |
673 |
673 |
674 (* nominal *) |
674 (* nominal *) |
675 fun define_recursion_relation Rname domT qglrs clauses RCss lthy = |
675 fun define_recursion_relation Rname domT qglrs clauses RCss lthy = |
1023 |
1023 |
1024 val trees = map build_tree clauses |
1024 val trees = map build_tree clauses |
1025 val RCss = map find_calls trees |
1025 val RCss = map find_calls trees |
1026 |
1026 |
1027 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
1027 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
1028 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
1028 PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy |
1029 |
1029 |
1030 val ((f, (_, f_defthm)), lthy) = |
1030 val ((f, (_, f_defthm)), lthy) = |
1031 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1031 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1032 |
1032 |
1033 val RCss = map (map (inst_RC lthy fvar f)) RCss |
1033 val RCss = map (map (inst_RC lthy fvar f)) RCss |
1034 val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees |
1034 val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees |
1035 |
1035 |
1036 val ((R, RIntro_thmss, R_elim), lthy) = |
1036 val ((R, RIntro_thmss, R_elim), lthy) = |
1037 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
1037 PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT abstract_qglrs clauses RCss) lthy |
1038 |
1038 |
1039 val (_, lthy) = |
1039 val (_, lthy) = |
1040 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
1040 Local_Theory.abbrev Syntax.mode_default ((Binding.name (defname ^ "_dom"), NoSyn), mk_acc domT R) lthy |
1041 |
1041 |
1042 val newthy = Proof_Context.theory_of lthy |
1042 val newthy = Proof_Context.theory_of lthy |
1043 val clauses = map (transfer_clause_ctx newthy) clauses |
1043 val clauses = map (transfer_clause_ctx newthy) clauses |
1044 |
1044 |
1045 val cert = Thm.cterm_of lthy |
1045 val cert = Thm.cterm_of lthy |