author | bulwahn |
Mon, 10 Jan 2011 08:18:49 +0100 | |
changeset 41488 | 2110405ed53b |
parent 41487 | e7c1248e39d0 |
child 41489 | 8e2b8649507d |
permissions | -rw-r--r-- |
41467 | 1 |
(* Title: HOL/Tools/list_to_set_comprehension.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
3 |
|
41467 | 4 |
Simproc for rewriting list comprehensions applied to List.set to set |
5 |
comprehension. |
|
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
6 |
*) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
7 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
8 |
signature LIST_TO_SET_COMPREHENSION = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
9 |
sig |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
10 |
val simproc : simpset -> cterm -> thm option |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
11 |
end; |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
12 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
13 |
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
14 |
struct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
15 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
16 |
(* conversion *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
17 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
18 |
fun all_exists_conv cv ctxt ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
19 |
case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
20 |
Const(@{const_name HOL.Ex}, _) $ Abs(_, _, _) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
21 |
Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
22 |
| _ => cv ctxt ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
23 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
24 |
fun all_but_last_exists_conv cv ctxt ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
25 |
case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
26 |
Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
27 |
Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
28 |
| _ => cv ctxt ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
29 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
30 |
fun Collect_conv cv ctxt ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
31 |
(case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
32 |
Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
33 |
| _ => raise CTERM ("Collect_conv", [ct])); |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
34 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
35 |
fun Trueprop_conv cv ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
36 |
(case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
37 |
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
38 |
| _ => raise CTERM ("Trueprop_conv", [ct])); |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
39 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
40 |
fun eq_conv cv1 cv2 ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
41 |
(case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
42 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
43 |
| _ => raise CTERM ("eq_conv", [ct])); |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
44 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
45 |
fun conj_conv cv1 cv2 ct = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
46 |
(case Thm.term_of ct of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
47 |
Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
48 |
| _ => raise CTERM ("conj_conv", [ct])); |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
49 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
50 |
fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
51 |
(Collect_conv (all_exists_conv conv o #2) ctxt)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
52 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
53 |
(* term abstraction of list comprehension patterns *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
54 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
55 |
datatype termlets = If | Case of (typ * int) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
56 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
57 |
fun meta_eq th = th RS @{thm eq_reflection} |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
58 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
59 |
fun rewr_conv' th = Conv.rewr_conv (meta_eq th) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
60 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
61 |
fun simproc ss redex = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
62 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
63 |
val ctxt = Simplifier.the_context ss |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
64 |
val thy = ProofContext.theory_of ctxt |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
65 |
val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
66 |
val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
67 |
val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
68 |
val del_refl_eq = @{lemma "(t = t & P) == P" by simp} |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
69 |
fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
70 |
fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
71 |
fun dest_singleton_list (Const (@{const_name List.Cons}, _) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
72 |
$ t $ (Const (@{const_name List.Nil}, _))) = t |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
73 |
| dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
74 |
(* We check that one case returns a singleton list and all other cases |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
75 |
return [], and return the index of the one singleton list case *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
76 |
fun possible_index_of_singleton_case cases = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
77 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
78 |
fun check (i, case_t) s = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
79 |
(case strip_abs_body case_t of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
80 |
(Const (@{const_name List.Nil}, _)) => s |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
81 |
| t => (case s of NONE => SOME i | SOME s => NONE)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
82 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
83 |
fold_index check cases NONE |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
84 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
85 |
(* returns (case_expr type index chosen_case) option *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
86 |
fun dest_case case_term = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
87 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
88 |
val (case_const, args) = strip_comb case_term |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
89 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
90 |
case try dest_Const case_const of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
91 |
SOME (c, T) => (case Datatype_Data.info_of_case thy c of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
92 |
SOME _ => (case possible_index_of_singleton_case (fst (split_last args)) of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
93 |
SOME i => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
94 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
95 |
val (Ts, _) = strip_type T |
41487 | 96 |
val T' = snd (split_last Ts) |
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
97 |
in SOME (snd (split_last args), T', i, nth args i) end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
98 |
| NONE => NONE) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
99 |
| NONE => NONE) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
100 |
| NONE => NONE |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
101 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
102 |
(* returns condition continuing term option *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
103 |
fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
104 |
SOME (cond, then_t) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
105 |
| dest_if _ = NONE |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
106 |
fun tac _ [] = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
107 |
rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
108 |
| tac ctxt (If :: cont) = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
109 |
Splitter.split_tac [@{thm split_if}] 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
110 |
THEN rtac @{thm conjI} 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
111 |
THEN rtac @{thm impI} 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
112 |
THEN Subgoal.FOCUS (fn {prems, context, ...} => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
113 |
CONVERSION (right_hand_set_comprehension_conv (K |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
114 |
(conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_TrueI})) Conv.all_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
115 |
then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
116 |
THEN tac ctxt cont |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
117 |
THEN rtac @{thm impI} 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
118 |
THEN Subgoal.FOCUS (fn {prems, context, ...} => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
119 |
CONVERSION (right_hand_set_comprehension_conv (K |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
120 |
(conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_FalseI})) Conv.all_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
121 |
then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
122 |
THEN rtac set_Nil_I 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
123 |
| tac ctxt (Case (T, i) :: cont) = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
124 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
125 |
val info = Datatype.the_info thy (fst (dest_Type T)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
126 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
127 |
(* do case distinction *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
128 |
Splitter.split_tac [#split info] 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
129 |
THEN EVERY (map_index (fn (i', case_rewrite) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
130 |
(if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
131 |
THEN REPEAT_DETERM (rtac @{thm allI} 1) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
132 |
THEN rtac @{thm impI} 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
133 |
THEN (if i' = i then |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
134 |
(* continue recursively *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
135 |
Subgoal.FOCUS (fn {prems, context, ...} => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
136 |
CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
137 |
((conj_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
138 |
(eq_conv Conv.all_conv (rewr_conv' (snd (split_last prems))) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
139 |
then_conv (Conv.try_conv (Conv.rewrs_conv (map meta_eq (#inject info))))) Conv.all_conv) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
140 |
then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
141 |
then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
142 |
then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
143 |
Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
144 |
THEN tac ctxt cont |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
145 |
else |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
146 |
Subgoal.FOCUS (fn {prems, context, ...} => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
147 |
CONVERSION ((right_hand_set_comprehension_conv (K |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
148 |
(conj_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
149 |
((eq_conv Conv.all_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
150 |
(rewr_conv' (snd (split_last prems)))) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
151 |
then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) Conv.all_conv |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
152 |
then_conv (rewr_conv' @{thm simp_thms(24)}))) context) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
153 |
then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
154 |
Conv.repeat_conv (Conv.bottom_conv (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1 |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
155 |
THEN rtac set_Nil_I 1)) (#case_rewrites info)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
156 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
157 |
fun make_inner_eqs bound_vs Tis eqs t = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
158 |
case dest_case t of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
159 |
SOME (x, T, i, cont) => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
160 |
let |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
161 |
val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
162 |
val x' = incr_boundvars (length vs) x |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
163 |
val eqs' = map (incr_boundvars (length vs)) eqs |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
164 |
val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
165 |
val constr_t = list_comb (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
166 |
val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x' |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
167 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
168 |
make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
169 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
170 |
| NONE => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
171 |
case dest_if t of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
172 |
SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
173 |
| NONE => |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
174 |
if eqs = [] then NONE (* no rewriting, nothing to be done *) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
175 |
else |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
176 |
let |
41488 | 177 |
val Type (@{type_name List.list}, [rT]) = fastype_of t |
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
178 |
val pat_eq = |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
179 |
case try dest_singleton_list t of |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
180 |
SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
181 |
$ Bound (length bound_vs) $ t' |
41488 | 182 |
| NONE => Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) |
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
183 |
$ Bound (length bound_vs) $ (mk_set rT $ t) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
184 |
val reverse_bounds = curry subst_bounds |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
185 |
((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)]) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
186 |
val eqs' = map reverse_bounds eqs |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
187 |
val pat_eq' = reverse_bounds pat_eq |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
188 |
val inner_t = fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
189 |
(rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq') |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
190 |
val lhs = term_of redex |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
191 |
val rhs = HOLogic.mk_Collect ("x", rT, inner_t) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
192 |
val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
193 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
194 |
SOME ((Goal.prove ctxt [] [] rewrite_rule_t (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
195 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
196 |
in |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
197 |
make_inner_eqs [] [] [] (dest_set (term_of redex)) |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
198 |
end |
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
199 |
|
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
diff
changeset
|
200 |
end |