equal
deleted
inserted
replaced
16 -> string (* defname *) |
16 -> string (* defname *) |
17 -> ((bstring * typ) * mixfix) list (* defined symbol *) |
17 -> ((bstring * typ) * mixfix) list (* defined symbol *) |
18 -> ((bstring * typ) list * term list * term * term) list (* specification *) |
18 -> ((bstring * typ) list * term list * term * term) list (* specification *) |
19 -> local_theory |
19 -> local_theory |
20 -> (term (* f *) |
20 -> (term (* f *) |
|
21 * term (* G(raph) *) |
|
22 * thm list (* GIntros *) |
|
23 * thm (* Ginduct *) |
21 * thm (* goalstate *) |
24 * thm (* goalstate *) |
22 * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) |
25 * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) |
23 ) * local_theory |
26 ) * local_theory |
24 |
27 |
|
28 val inductive_def : (binding * typ) * mixfix -> term list -> local_theory |
|
29 -> (term * thm list * thm * thm) * local_theory |
25 end |
30 end |
26 |
31 |
27 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
32 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
28 struct |
33 struct |
29 |
34 |
584 (goalstate, values) |
589 (goalstate, values) |
585 end |
590 end |
586 |
591 |
587 (* wrapper -- restores quantifiers in rule specifications *) |
592 (* wrapper -- restores quantifiers in rule specifications *) |
588 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
593 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
589 let |
594 let |
590 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
595 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
591 lthy |
596 lthy |
592 |> Local_Theory.conceal |
597 |> Local_Theory.conceal |
593 |> Inductive.add_inductive_i |
598 |> Inductive.add_inductive_i |
594 {quiet_mode = true, |
599 {quiet_mode = true, |
1081 NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1086 NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1082 psimps=psimps, simple_pinducts=[simple_pinduct], |
1087 psimps=psimps, simple_pinducts=[simple_pinduct], |
1083 termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} |
1088 termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} |
1084 end |
1089 end |
1085 in |
1090 in |
1086 ((f, goalstate, mk_partial_rules), lthy) |
1091 ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy) |
1087 end |
1092 end |
1088 |
1093 |
1089 |
1094 |
1090 end |
1095 end |