equal
deleted
inserted
replaced
85 in mk_meta_eq rl' handle THM _ => |
85 in mk_meta_eq rl' handle THM _ => |
86 if can Logic.dest_equals (concl_of rl') then rl' |
86 if can Logic.dest_equals (concl_of rl') then rl' |
87 else error "Conclusion of congruence rules must be =-equality" |
87 else error "Conclusion of congruence rules must be =-equality" |
88 end); |
88 end); |
89 |
89 |
90 fun mk_atomize pairs = |
90 fun mk_atomize ctxt pairs = |
91 let |
91 let |
92 fun atoms thm = |
92 fun atoms thm = |
93 let |
93 let |
94 fun res th = map (fn rl => th RS rl); (*exception THM*) |
94 fun res th = map (fn rl => th RS rl); (*exception THM*) |
|
95 val thm_ctxt = Variable.declare_thm thm ctxt; |
95 fun res_fixed rls = |
96 fun res_fixed rls = |
96 if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls |
97 if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls |
97 else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm]; |
98 else Variable.trade (K (fn [thm'] => res thm' rls)) thm_ctxt [thm]; |
98 in |
99 in |
99 case concl_of thm |
100 case concl_of thm |
100 of Const (@{const_name Trueprop}, _) $ p => (case head_of p |
101 of Const (@{const_name Trueprop}, _) $ p => (case head_of p |
101 of Const (a, _) => (case AList.lookup (op =) pairs a |
102 of Const (a, _) => (case AList.lookup (op =) pairs a |
102 of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) |
103 of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) |
104 | _ => [thm]) |
105 | _ => [thm]) |
105 | _ => [thm] |
106 | _ => [thm] |
106 end; |
107 end; |
107 in atoms end; |
108 in atoms end; |
108 |
109 |
109 fun mksimps pairs (_: Proof.context) = |
110 fun mksimps pairs ctxt = |
110 map_filter (try mk_eq) o mk_atomize pairs o gen_all; |
111 map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all; |
111 |
112 |
112 val simp_legacy_precond = |
113 val simp_legacy_precond = |
113 Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) |
114 Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) |
114 |
115 |
115 fun unsafe_solver_tac ctxt = |
116 fun unsafe_solver_tac ctxt = |