equal
deleted
inserted
replaced
195 | @{const Not} $ _ => abstr1 cvs ct |
195 | @{const Not} $ _ => abstr1 cvs ct |
196 | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct |
196 | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct |
197 | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct |
197 | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct |
198 | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct |
198 | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct |
199 | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct |
199 | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct |
200 | Const (@{const_name SMT.distinct}, _) $ _ => |
200 | Const (@{const_name distinct}, _) $ _ => |
201 if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct |
201 if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct |
202 else fresh_abstraction cvs ct |
202 else fresh_abstraction cvs ct |
203 | Const (@{const_name If}, _) $ _ $ _ $ _ => |
203 | Const (@{const_name If}, _) $ _ $ _ $ _ => |
204 if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct |
204 if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct |
205 | Const (@{const_name All}, _) $ _ => |
205 | Const (@{const_name All}, _) $ _ => |
256 |
256 |
257 fun set_conv ct = |
257 fun set_conv ct = |
258 (Conv.rewrs_conv [set1, set2, set3, set4] else_conv |
258 (Conv.rewrs_conv [set1, set2, set3, set4] else_conv |
259 (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct |
259 (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct |
260 |
260 |
261 val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)} |
261 val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)} |
262 val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)} |
262 val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)} |
263 val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs" |
263 val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs" |
264 by (simp add: distinct_def)} |
264 by (simp add: distinct_def)} |
265 |
265 |
266 fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
266 fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 |
267 in |
267 in |
268 fun unfold_distinct_conv ct = |
268 fun unfold_distinct_conv ct = |