50 val remove_domain_condition = |
50 val remove_domain_condition = |
51 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
51 full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
52 val tsimps = map remove_domain_condition psimps |
52 val tsimps = map remove_domain_condition psimps |
53 val tinduct = map remove_domain_condition pinducts |
53 val tinduct = map remove_domain_condition pinducts |
54 val teqvts = map remove_domain_condition eqvts |
54 val teqvts = map remove_domain_condition eqvts |
55 |
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 fun qualify n = Binding.name n |
61 fun qualify n = Binding.name n |
57 |> Binding.qualify true defname |
62 |> Binding.qualify true defname |
58 in |
63 in |
59 lthy |
64 lthy |
60 |> add_simps I "simps" I simp_attribs tsimps |
65 |> add_simps I "simps" I simp_attribs tsimps |
64 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
69 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
65 tinduct) |
70 tinduct) |
66 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
71 |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => |
67 let val info' = { is_partial=false, defname=defname, add_simps=add_simps, |
72 let val info' = { is_partial=false, defname=defname, add_simps=add_simps, |
68 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
73 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
69 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=eqvts } |
74 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } |
70 in |
75 in |
71 (info', |
76 (info', |
72 lthy |
77 lthy |
73 |> Local_Theory.declaration false (add_function_data o morph_function_data info') |
78 |> Local_Theory.declaration false (add_function_data o morph_function_data info') |
74 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
79 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |