1 (* Title: HOL/Tools/ctr_sugar_util.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012, 2013 |
|
5 |
|
6 Library for wrapping existing freely generated type's constructors. |
|
7 *) |
|
8 |
|
9 signature CTR_SUGAR_UTIL = |
|
10 sig |
|
11 val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
|
12 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
|
13 val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> |
|
14 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list |
|
15 val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c |
|
16 val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> |
|
17 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd |
|
18 val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list |
|
19 val transpose: 'a list list -> 'a list list |
|
20 val pad_list: 'a -> int -> 'a list -> 'a list |
|
21 val splice: 'a list -> 'a list -> 'a list |
|
22 val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list |
|
23 |
|
24 val mk_names: int -> string -> string list |
|
25 val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context |
|
26 val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context |
|
27 val mk_TFrees: int -> Proof.context -> typ list * Proof.context |
|
28 val mk_Frees': string -> typ list -> Proof.context -> |
|
29 (term list * (string * typ) list) * Proof.context |
|
30 val mk_Freess': string -> typ list list -> Proof.context -> |
|
31 (term list list * (string * typ) list list) * Proof.context |
|
32 val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context |
|
33 val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context |
|
34 val resort_tfree: sort -> typ -> typ |
|
35 val variant_types: string list -> sort list -> Proof.context -> |
|
36 (string * sort) list * Proof.context |
|
37 val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
|
38 |
|
39 val typ_subst_nonatomic: (typ * typ) list -> typ -> typ |
|
40 val subst_nonatomic_types: (typ * typ) list -> term -> term |
|
41 |
|
42 val mk_predT: typ list -> typ |
|
43 val mk_pred1T: typ -> typ |
|
44 |
|
45 val mk_disjIN: int -> int -> thm |
|
46 |
|
47 val mk_unabs_def: int -> thm -> thm |
|
48 |
|
49 val mk_IfN: typ -> term list -> term list -> term |
|
50 val mk_Trueprop_eq: term * term -> term |
|
51 |
|
52 val rapp: term -> term -> term |
|
53 |
|
54 val list_all_free: term list -> term -> term |
|
55 val list_exists_free: term list -> term -> term |
|
56 |
|
57 val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv |
|
58 |
|
59 val cterm_instantiate_pos: cterm option list -> thm -> thm |
|
60 val unfold_thms: Proof.context -> thm list -> thm -> thm |
|
61 |
|
62 val certifyT: Proof.context -> typ -> ctyp |
|
63 val certify: Proof.context -> term -> cterm |
|
64 |
|
65 val standard_binding: binding |
|
66 val equal_binding: binding |
|
67 val parse_binding: binding parser |
|
68 |
|
69 val ss_only: thm list -> Proof.context -> Proof.context |
|
70 |
|
71 val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic |
|
72 val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> |
|
73 tactic |
|
74 val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic |
|
75 val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic |
|
76 val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic |
|
77 val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic |
|
78 end; |
|
79 |
|
80 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL = |
|
81 struct |
|
82 |
|
83 fun map3 _ [] [] [] = [] |
|
84 | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s |
|
85 | map3 _ _ _ _ = raise ListPair.UnequalLengths; |
|
86 |
|
87 fun map4 _ [] [] [] [] = [] |
|
88 | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s |
|
89 | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
90 |
|
91 fun map5 _ [] [] [] [] [] = [] |
|
92 | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = |
|
93 f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s |
|
94 | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
95 |
|
96 fun fold_map2 _ [] [] acc = ([], acc) |
|
97 | fold_map2 f (x1::x1s) (x2::x2s) acc = |
|
98 let |
|
99 val (x, acc') = f x1 x2 acc; |
|
100 val (xs, acc'') = fold_map2 f x1s x2s acc'; |
|
101 in (x :: xs, acc'') end |
|
102 | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; |
|
103 |
|
104 fun fold_map3 _ [] [] [] acc = ([], acc) |
|
105 | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = |
|
106 let |
|
107 val (x, acc') = f x1 x2 x3 acc; |
|
108 val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; |
|
109 in (x :: xs, acc'') end |
|
110 | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
111 |
|
112 fun seq_conds f n k xs = |
|
113 if k = n then |
|
114 map (f false) (take (k - 1) xs) |
|
115 else |
|
116 let val (negs, pos) = split_last (take k xs) in |
|
117 map (f false) negs @ [f true pos] |
|
118 end; |
|
119 |
|
120 fun transpose [] = [] |
|
121 | transpose ([] :: xss) = transpose xss |
|
122 | transpose xss = map hd xss :: transpose (map tl xss); |
|
123 |
|
124 fun pad_list x n xs = xs @ replicate (n - length xs) x; |
|
125 |
|
126 fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); |
|
127 |
|
128 fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs'; |
|
129 |
|
130 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); |
|
131 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; |
|
132 |
|
133 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; |
|
134 |
|
135 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); |
|
136 |
|
137 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); |
|
138 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; |
|
139 |
|
140 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); |
|
141 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; |
|
142 |
|
143 fun resort_tfree S (TFree (s, _)) = TFree (s, S); |
|
144 |
|
145 fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre; |
|
146 |
|
147 fun variant_types ss Ss ctxt = |
|
148 let |
|
149 val (tfrees, _) = |
|
150 fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); |
|
151 val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
|
152 in (tfrees, ctxt') end; |
|
153 |
|
154 fun variant_tfrees ss = |
|
155 apfst (map TFree) o |
|
156 variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); |
|
157 |
|
158 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) |
|
159 fun typ_subst_nonatomic [] = I |
|
160 | typ_subst_nonatomic inst = |
|
161 let |
|
162 fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts)) |
|
163 | subst T = perhaps (AList.lookup (op =) inst) T; |
|
164 in subst end; |
|
165 |
|
166 fun subst_nonatomic_types [] = I |
|
167 | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst); |
|
168 |
|
169 fun mk_predT Ts = Ts ---> HOLogic.boolT; |
|
170 fun mk_pred1T T = mk_predT [T]; |
|
171 |
|
172 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} |
|
173 | mk_disjIN _ 1 = disjI1 |
|
174 | mk_disjIN 2 2 = disjI2 |
|
175 | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; |
|
176 |
|
177 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong); |
|
178 |
|
179 fun mk_IfN _ _ [t] = t |
|
180 | mk_IfN T (c :: cs) (t :: ts) = |
|
181 Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; |
|
182 |
|
183 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
184 |
|
185 fun rapp u t = betapply (t, u); |
|
186 |
|
187 fun list_quant_free quant_const = |
|
188 fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P); |
|
189 |
|
190 val list_all_free = list_quant_free HOLogic.all_const; |
|
191 val list_exists_free = list_quant_free HOLogic.exists_const; |
|
192 |
|
193 fun fo_match ctxt t pat = |
|
194 let val thy = Proof_Context.theory_of ctxt in |
|
195 Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) |
|
196 end; |
|
197 |
|
198 fun cterm_instantiate_pos cts thm = |
|
199 let |
|
200 val cert = Thm.cterm_of (Thm.theory_of_thm thm); |
|
201 val vars = Term.add_vars (prop_of thm) []; |
|
202 val vars' = rev (drop (length vars - length cts) vars); |
|
203 val ps = map_filter (fn (_, NONE) => NONE |
|
204 | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts); |
|
205 in |
|
206 Drule.cterm_instantiate ps thm |
|
207 end; |
|
208 |
|
209 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); |
|
210 |
|
211 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) |
|
212 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); |
|
213 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); |
|
214 |
|
215 (* The standard binding stands for a name generated following the canonical convention (e.g., |
|
216 "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no |
|
217 binding at all, depending on the context. *) |
|
218 val standard_binding = @{binding _}; |
|
219 val equal_binding = @{binding "="}; |
|
220 |
|
221 val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; |
|
222 |
|
223 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; |
|
224 |
|
225 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) |
|
226 fun WRAP gen_before gen_after xs core_tac = |
|
227 fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac; |
|
228 |
|
229 fun WRAP' gen_before gen_after xs core_tac = |
|
230 fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac; |
|
231 |
|
232 fun CONJ_WRAP_GEN conj_tac gen_tac xs = |
|
233 let val (butlast, last) = split_last xs; |
|
234 in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end; |
|
235 |
|
236 fun CONJ_WRAP_GEN' conj_tac gen_tac xs = |
|
237 let val (butlast, last) = split_last xs; |
|
238 in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end; |
|
239 |
|
240 (*not eta-converted because of monotype restriction*) |
|
241 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac; |
|
242 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac; |
|
243 |
|
244 end; |
|