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