equal
deleted
inserted
replaced
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 * thm (* goalstate *) |
21 * thm (* goalstate *) |
22 * (thm -> Function_Common.function_result) (* continuation *) |
22 * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) |
23 ) * local_theory |
23 ) * local_theory |
24 |
24 |
25 end |
25 end |
26 |
26 |
27 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
27 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = |
1060 |> Conjunction.elim |
1060 |> Conjunction.elim |
1061 |> apfst (Thm.forall_elim_vars 0) |
1061 |> apfst (Thm.forall_elim_vars 0) |
1062 |
1062 |
1063 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
1063 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
1064 |
1064 |
|
1065 val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) |
|
1066 |
1065 val psimps = PROFILE "Proving simplification rules" |
1067 val psimps = PROFILE "Proving simplification rules" |
1066 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
1068 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
1067 |
1069 |
1068 val simple_pinduct = PROFILE "Proving partial induction rule" |
1070 val simple_pinduct = PROFILE "Proving partial induction rule" |
1069 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
1071 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
1075 if domintros then SOME (PROFILE "Proving domain introduction rules" |
1077 if domintros then SOME (PROFILE "Proving domain introduction rules" |
1076 (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
1078 (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
1077 else NONE |
1079 else NONE |
1078 |
1080 |
1079 in |
1081 in |
1080 FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1082 NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1081 psimps=psimps, simple_pinducts=[simple_pinduct], |
1083 psimps=psimps, simple_pinducts=[simple_pinduct], |
1082 termination=total_intro, domintros=dom_intros} |
1084 termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} |
1083 end |
1085 end |
1084 in |
1086 in |
1085 ((f, goalstate, mk_partial_rules), lthy) |
1087 ((f, goalstate, mk_partial_rules), lthy) |
1086 end |
1088 end |
1087 |
1089 |