|
1 (* Title: HOL/BNF/Tools/ctr_sugar_util.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Library for wrapping existing freely generated type's constructors. |
|
6 *) |
|
7 |
|
8 signature CTR_SUGAR_UTIL = |
|
9 sig |
|
10 val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
|
11 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
|
12 val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> |
|
13 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list |
|
14 val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c |
|
15 val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> |
|
16 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd |
|
17 val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list |
|
18 val transpose: 'a list list -> 'a list list |
|
19 val pad_list: 'a -> int -> 'a list -> 'a list |
|
20 val splice: 'a list -> 'a list -> 'a list |
|
21 val permute_like: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list |
|
22 |
|
23 val mk_names: int -> string -> string list |
|
24 val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context |
|
25 val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context |
|
26 val mk_TFrees: int -> Proof.context -> typ list * Proof.context |
|
27 val mk_Frees': string -> typ list -> Proof.context -> |
|
28 (term list * (string * typ) list) * Proof.context |
|
29 val mk_Freess': string -> typ list list -> Proof.context -> |
|
30 (term list list * (string * typ) list list) * Proof.context |
|
31 val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context |
|
32 val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context |
|
33 val resort_tfree: sort -> typ -> typ |
|
34 val variant_types: string list -> sort list -> Proof.context -> |
|
35 (string * sort) list * Proof.context |
|
36 val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
|
37 |
|
38 val mk_predT: typ list -> typ |
|
39 val mk_pred1T: typ -> typ |
|
40 |
|
41 val mk_disjIN: int -> int -> thm |
|
42 |
|
43 val mk_unabs_def: int -> thm -> thm |
|
44 |
|
45 val mk_IfN: typ -> term list -> term list -> term |
|
46 val mk_Trueprop_eq: term * term -> term |
|
47 |
|
48 val rapp: term -> term -> term |
|
49 |
|
50 val list_all_free: term list -> term -> term |
|
51 val list_exists_free: term list -> term -> term |
|
52 |
|
53 val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv |
|
54 |
|
55 val unfold_thms: Proof.context -> thm list -> thm -> thm |
|
56 |
|
57 val certifyT: Proof.context -> typ -> ctyp |
|
58 val certify: Proof.context -> term -> cterm |
|
59 |
|
60 val standard_binding: binding |
|
61 val equal_binding: binding |
|
62 val parse_binding: binding parser |
|
63 |
|
64 val ss_only: thm list -> Proof.context -> Proof.context |
|
65 end; |
|
66 |
|
67 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL = |
|
68 struct |
|
69 |
|
70 fun map3 _ [] [] [] = [] |
|
71 | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s |
|
72 | map3 _ _ _ _ = raise ListPair.UnequalLengths; |
|
73 |
|
74 fun map4 _ [] [] [] [] = [] |
|
75 | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s |
|
76 | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
77 |
|
78 fun map5 _ [] [] [] [] [] = [] |
|
79 | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = |
|
80 f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s |
|
81 | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
82 |
|
83 fun fold_map2 _ [] [] acc = ([], acc) |
|
84 | fold_map2 f (x1::x1s) (x2::x2s) acc = |
|
85 let |
|
86 val (x, acc') = f x1 x2 acc; |
|
87 val (xs, acc'') = fold_map2 f x1s x2s acc'; |
|
88 in (x :: xs, acc'') end |
|
89 | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; |
|
90 |
|
91 fun fold_map3 _ [] [] [] acc = ([], acc) |
|
92 | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = |
|
93 let |
|
94 val (x, acc') = f x1 x2 x3 acc; |
|
95 val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; |
|
96 in (x :: xs, acc'') end |
|
97 | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
98 |
|
99 fun seq_conds f n k xs = |
|
100 if k = n then |
|
101 map (f false) (take (k - 1) xs) |
|
102 else |
|
103 let val (negs, pos) = split_last (take k xs) in |
|
104 map (f false) negs @ [f true pos] |
|
105 end; |
|
106 |
|
107 fun transpose [] = [] |
|
108 | transpose ([] :: xss) = transpose xss |
|
109 | transpose xss = map hd xss :: transpose (map tl xss); |
|
110 |
|
111 fun pad_list x n xs = xs @ replicate (n - length xs) x; |
|
112 |
|
113 fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); |
|
114 |
|
115 fun permute_like eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs'; |
|
116 |
|
117 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); |
|
118 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; |
|
119 |
|
120 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; |
|
121 |
|
122 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); |
|
123 |
|
124 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); |
|
125 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; |
|
126 |
|
127 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); |
|
128 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; |
|
129 |
|
130 fun resort_tfree S (TFree (s, _)) = TFree (s, S); |
|
131 |
|
132 fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre; |
|
133 |
|
134 fun variant_types ss Ss ctxt = |
|
135 let |
|
136 val (tfrees, _) = |
|
137 fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); |
|
138 val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
|
139 in (tfrees, ctxt') end; |
|
140 |
|
141 fun variant_tfrees ss = |
|
142 apfst (map TFree) o |
|
143 variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); |
|
144 |
|
145 fun mk_predT Ts = Ts ---> HOLogic.boolT; |
|
146 fun mk_pred1T T = mk_predT [T]; |
|
147 |
|
148 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} |
|
149 | mk_disjIN _ 1 = disjI1 |
|
150 | mk_disjIN 2 2 = disjI2 |
|
151 | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; |
|
152 |
|
153 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong); |
|
154 |
|
155 fun mk_IfN _ _ [t] = t |
|
156 | mk_IfN T (c :: cs) (t :: ts) = |
|
157 Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; |
|
158 |
|
159 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
160 |
|
161 fun rapp u t = betapply (t, u); |
|
162 |
|
163 fun list_quant_free quant_const = |
|
164 fold_rev (fn free => fn P => |
|
165 let val (x, T) = Term.dest_Free free; |
|
166 in quant_const T $ Term.absfree (x, T) P end); |
|
167 |
|
168 val list_all_free = list_quant_free HOLogic.all_const; |
|
169 val list_exists_free = list_quant_free HOLogic.exists_const; |
|
170 |
|
171 fun fo_match ctxt t pat = |
|
172 let val thy = Proof_Context.theory_of ctxt in |
|
173 Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) |
|
174 end; |
|
175 |
|
176 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); |
|
177 |
|
178 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) |
|
179 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); |
|
180 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); |
|
181 |
|
182 (* The standard binding stands for a name generated following the canonical convention (e.g., |
|
183 "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no |
|
184 binding at all, depending on the context. *) |
|
185 val standard_binding = @{binding _}; |
|
186 val equal_binding = @{binding "="}; |
|
187 |
|
188 val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; |
|
189 |
|
190 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; |
|
191 |
|
192 end; |