45 fun conj_conv cv1 cv2 ct = |
45 fun conj_conv cv1 cv2 ct = |
46 (case Thm.term_of ct of |
46 (case Thm.term_of ct of |
47 Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
47 Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
48 | _ => raise CTERM ("conj_conv", [ct])); |
48 | _ => raise CTERM ("conj_conv", [ct])); |
49 |
49 |
|
50 fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) |
|
51 |
|
52 fun conjunct_assoc_conv ct = Conv.try_conv |
|
53 ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct |
|
54 |
50 fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv |
55 fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv |
51 (Collect_conv (all_exists_conv conv o #2) ctxt)) |
56 (Collect_conv (all_exists_conv conv o #2) ctxt)) |
52 |
57 |
53 (* term abstraction of list comprehension patterns *) |
58 (* term abstraction of list comprehension patterns *) |
54 |
59 |
55 datatype termlets = If | Case of (typ * int) |
60 datatype termlets = If | Case of (typ * int) |
56 |
|
57 fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) |
|
58 |
61 |
59 fun simproc ss redex = |
62 fun simproc ss redex = |
60 let |
63 let |
61 val ctxt = Simplifier.the_context ss |
64 val ctxt = Simplifier.the_context ss |
62 val thy = ProofContext.theory_of ctxt |
65 val thy = ProofContext.theory_of ctxt |
134 CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K |
137 CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K |
135 ((conj_conv |
138 ((conj_conv |
136 (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) |
139 (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) |
137 then_conv (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) Conv.all_conv) |
140 then_conv (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) Conv.all_conv) |
138 then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) |
141 then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) |
139 then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context |
142 then_conv conjunct_assoc_conv)) context |
140 then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => |
143 then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => |
141 Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 |
144 Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 |
142 THEN tac ctxt cont |
145 THEN tac ctxt cont |
143 else |
146 else |
144 Subgoal.FOCUS (fn {prems, context, ...} => |
147 Subgoal.FOCUS (fn {prems, context, ...} => |
170 SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont |
173 SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont |
171 | NONE => |
174 | NONE => |
172 if eqs = [] then NONE (* no rewriting, nothing to be done *) |
175 if eqs = [] then NONE (* no rewriting, nothing to be done *) |
173 else |
176 else |
174 let |
177 let |
175 val Type (@{type_name List.list}, [rT]) = fastype_of t |
178 val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t) |
176 val pat_eq = |
179 val pat_eq = |
177 case try dest_singleton_list t of |
180 case try dest_singleton_list t of |
178 SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) |
181 SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) |
179 $ Bound (length bound_vs) $ t' |
182 $ Bound (length bound_vs) $ t' |
180 | NONE => Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) |
183 | NONE => Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) |