40 | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) |
40 | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) |
41 |
41 |
42 val { termination, fs, R, add_simps, case_names, psimps, |
42 val { termination, fs, R, add_simps, case_names, psimps, |
43 pinducts, defname, eqvts, ...} = info |
43 pinducts, defname, eqvts, ...} = info |
44 val domT = domain_type (fastype_of R) |
44 val domT = domain_type (fastype_of R) |
|
45 |
45 val goal = HOLogic.mk_Trueprop |
46 val goal = HOLogic.mk_Trueprop |
46 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
47 (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
47 fun afterqed [[totality]] lthy = |
48 fun afterqed [[totality]] lthy = |
48 let |
49 let |
49 val totality = Thm.close_derivation totality |
50 val totality = Thm.close_derivation totality |
50 val remove_domain_condition = |
51 val remove_domain_condition = |
51 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
52 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
52 val tsimps = map remove_domain_condition psimps |
53 val tsimps = map remove_domain_condition psimps |
53 val tinduct = map remove_domain_condition pinducts |
54 val tinducts = map remove_domain_condition pinducts |
54 val teqvts = map remove_domain_condition eqvts |
55 val teqvts = map remove_domain_condition eqvts |
55 |
|
56 val _ = tracing ("tot psimps1:\n" ^ cat_lines (map @{make_string} psimps)) |
|
57 val _ = tracing ("tot psimps2:\n" ^ cat_lines (map @{make_string} tsimps)) |
|
58 val _ = tracing ("tot induct1:\n" ^ cat_lines (map @{make_string} pinducts)) |
|
59 val _ = tracing ("tot induct2:\n" ^ cat_lines (map @{make_string} tinduct)) |
|
60 |
56 |
61 fun qualify n = Binding.name n |
57 fun qualify n = Binding.name n |
62 |> Binding.qualify true defname |
58 |> Binding.qualify true defname |
63 in |
59 in |
64 lthy |
60 lthy |
65 |> add_simps I "simps" I simp_attribs tsimps |
61 |> add_simps I "simps" I simp_attribs tsimps |
66 ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts) |
62 ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts) |
67 ||>> Local_Theory.note |
63 ||>> Local_Theory.note |
68 ((qualify "induct", |
64 ((qualify "induct", |
69 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
65 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
70 tinduct) |
66 tinducts) |
71 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
67 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
72 let val info' = { is_partial=false, defname=defname, add_simps=add_simps, |
68 let val info' = { is_partial=false, defname=defname, add_simps=add_simps, |
73 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
69 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
74 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } |
70 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } |
75 in |
71 in |