author | haftmann |
Wed, 22 Dec 2010 20:57:13 +0100 | |
changeset 41388 | 945b42e3b3c2 |
parent 41387 | fb81cb128e7e |
child 41389 | d06a6d15a958 |
permissions | -rw-r--r-- |
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
1 |
(* Title: HOL/Tools/type_lifting.ML |
40582 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
4 |
Functorial structure of types. |
40582 | 5 |
*) |
6 |
||
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
7 |
signature TYPE_LIFTING = |
40582 | 8 |
sig |
41388 | 9 |
val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list |
10 |
val construct_mapper: Proof.context -> (string * bool -> term) |
|
40582 | 11 |
-> bool -> typ -> typ -> term |
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
12 |
val type_lifting: string option -> term -> theory -> Proof.state |
40582 | 13 |
type entry |
41388 | 14 |
val entries: Proof.context -> entry Symtab.table |
40582 | 15 |
end; |
16 |
||
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
17 |
structure Type_Lifting : TYPE_LIFTING = |
40582 | 18 |
struct |
19 |
||
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
20 |
val compN = "comp"; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
21 |
val idN = "id"; |
40611 | 22 |
val compositionalityN = "compositionality"; |
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
23 |
val identityN = "identity"; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
24 |
|
40582 | 25 |
(** functorial mappers and their properties **) |
26 |
||
27 |
(* bookkeeping *) |
|
28 |
||
41387 | 29 |
fun term_with_typ ctxt T t = Envir.subst_term_types |
30 |
(Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; |
|
31 |
||
32 |
type entry = { mapper: term, variances: (sort * (bool * bool)) list, |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
33 |
comp: thm, id: thm }; |
40582 | 34 |
|
41388 | 35 |
structure Data = Generic_Data( |
40582 | 36 |
type T = entry Symtab.table |
37 |
val empty = Symtab.empty |
|
40614 | 38 |
fun merge (xy : T * T) = Symtab.merge (K true) xy |
40582 | 39 |
val extend = I |
40 |
); |
|
41 |
||
41388 | 42 |
val entries = Data.get o Context.Proof; |
40582 | 43 |
|
44 |
||
45 |
(* type analysis *) |
|
46 |
||
41388 | 47 |
fun find_atomic ctxt T = |
40582 | 48 |
let |
41388 | 49 |
val variances_of = Option.map #variances o Symtab.lookup (entries ctxt); |
40582 | 50 |
fun add_variance is_contra T = |
51 |
AList.map_default (op =) (T, (false, false)) |
|
52 |
((if is_contra then apsnd else apfst) (K true)); |
|
53 |
fun analyze' is_contra (_, (co, contra)) T = |
|
54 |
(if co then analyze is_contra T else I) |
|
55 |
#> (if contra then analyze (not is_contra) T else I) |
|
56 |
and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco |
|
57 |
of NONE => add_variance is_contra T |
|
58 |
| SOME variances => fold2 (analyze' is_contra) variances Ts) |
|
59 |
| analyze is_contra T = add_variance is_contra T; |
|
60 |
in analyze false T [] end; |
|
61 |
||
41388 | 62 |
fun construct_mapper ctxt atomic = |
40582 | 63 |
let |
41388 | 64 |
val lookup = the o Symtab.lookup (entries ctxt); |
40582 | 65 |
fun constructs is_contra (_, (co, contra)) T T' = |
66 |
(if co then [construct is_contra T T'] else []) |
|
67 |
@ (if contra then [construct (not is_contra) T T'] else []) |
|
68 |
and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) = |
|
69 |
let |
|
41388 | 70 |
val { mapper = raw_mapper, variances, ... } = lookup tyco; |
40582 | 71 |
val args = maps (fn (arg_pattern, (T, T')) => |
72 |
constructs is_contra arg_pattern T T') |
|
73 |
(variances ~~ (Ts ~~ Ts')); |
|
74 |
val (U, U') = if is_contra then (T', T) else (T, T'); |
|
41388 | 75 |
val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper; |
76 |
in list_comb (mapper, args) end |
|
40582 | 77 |
| construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); |
78 |
in construct end; |
|
79 |
||
80 |
||
81 |
(* mapper properties *) |
|
82 |
||
41387 | 83 |
val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss; |
84 |
||
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
85 |
fun make_comp_prop ctxt variances (tyco, mapper) = |
40582 | 86 |
let |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
87 |
val sorts = map fst variances |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
88 |
val (((vs3, vs2), vs1), _) = ctxt |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
89 |
|> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
90 |
||>> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
91 |
||>> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
92 |
val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3); |
40582 | 93 |
fun mk_argT ((T, T'), (_, (co, contra))) = |
94 |
(if co then [(T --> T')] else []) |
|
95 |
@ (if contra then [(T' --> T)] else []); |
|
96 |
val contras = maps (fn (_, (co, contra)) => |
|
97 |
(if co then [false] else []) @ (if contra then [true] else [])) variances; |
|
98 |
val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); |
|
99 |
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
100 |
fun invents n k nctxt = |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
101 |
let |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
102 |
val names = Name.invents nctxt n k; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
103 |
in (names, fold Name.declare names nctxt) end; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
104 |
val ((names21, names32), nctxt) = Variable.names_of ctxt |
40582 | 105 |
|> invents "f" (length Ts21) |
106 |
||>> invents "f" (length Ts32); |
|
107 |
val T1 = Type (tyco, Ts1); |
|
108 |
val T2 = Type (tyco, Ts2); |
|
109 |
val T3 = Type (tyco, Ts3); |
|
110 |
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); |
|
111 |
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => |
|
112 |
if not is_contra then |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
113 |
HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) |
40582 | 114 |
else |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
115 |
HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) |
40582 | 116 |
) contras (args21 ~~ args32) |
41387 | 117 |
fun mk_mapper T T' args = list_comb (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args); |
118 |
val mapper21 = mk_mapper T2 T1 (map Free args21); |
|
119 |
val mapper32 = mk_mapper T3 T2 (map Free args32); |
|
120 |
val mapper31 = mk_mapper T3 T1 args31; |
|
121 |
val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (HOLogic.mk_comp (mapper21, mapper32), mapper31); |
|
122 |
val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3) |
|
123 |
val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (mapper21 $ (mapper32 $ x), mapper31 $ x); |
|
124 |
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1; |
|
125 |
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2; |
|
126 |
fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop |
|
127 |
(K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]] |
|
128 |
THEN' Simplifier.asm_lr_simp_tac compositionality_ss |
|
129 |
THEN_ALL_NEW (Goal.assume_rule_tac ctxt)))); |
|
130 |
in (comp_prop, prove_compositionality) end; |
|
131 |
||
132 |
val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss; |
|
40582 | 133 |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
134 |
fun make_id_prop ctxt variances (tyco, mapper) = |
40582 | 135 |
let |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
136 |
val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
137 |
val Ts = map TFree vs; |
40582 | 138 |
fun bool_num b = if b then 1 else 0; |
139 |
fun mk_argT (T, (_, (co, contra))) = |
|
41387 | 140 |
replicate (bool_num co + bool_num contra) T |
141 |
val arg_Ts = maps mk_argT (Ts ~~ variances) |
|
40582 | 142 |
val T = Type (tyco, Ts); |
41387 | 143 |
val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper; |
144 |
val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); |
|
145 |
val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); |
|
146 |
val rhs = HOLogic.id_const T; |
|
147 |
val (id_prop, identity_prop) = pairself (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); |
|
148 |
fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop |
|
149 |
(K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss))); |
|
150 |
in (id_prop, prove_identity) end; |
|
40582 | 151 |
|
152 |
||
40597 | 153 |
(* analyzing and registering mappers *) |
40582 | 154 |
|
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
155 |
fun consume eq x [] = (false, []) |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
156 |
| consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys); |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
157 |
|
40587 | 158 |
fun split_mapper_typ "fun" T = |
159 |
let |
|
160 |
val (Ts', T') = strip_type T; |
|
161 |
val (Ts'', T'') = split_last Ts'; |
|
162 |
val (Ts''', T''') = split_last Ts''; |
|
163 |
in (Ts''', T''', T'' --> T') end |
|
164 |
| split_mapper_typ tyco T = |
|
165 |
let |
|
166 |
val (Ts', T') = strip_type T; |
|
167 |
val (Ts'', T'') = split_last Ts'; |
|
168 |
in (Ts'', T'', T') end; |
|
169 |
||
170 |
fun analyze_variances thy tyco T = |
|
171 |
let |
|
172 |
fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T); |
|
173 |
val (Ts, T1, T2) = split_mapper_typ tyco T |
|
174 |
handle List.Empty => bad_typ (); |
|
175 |
val _ = pairself |
|
176 |
((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) |
|
41387 | 177 |
handle TYPE _ => bad_typ (); |
40587 | 178 |
val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) |
179 |
handle TYPE _ => bad_typ (); |
|
180 |
val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) |
|
181 |
then bad_typ () else (); |
|
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
182 |
fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
183 |
let |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
184 |
val coT = TFree var1 --> TFree var2; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
185 |
val contraT = TFree var2 --> TFree var1; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
186 |
val sort = Sign.inter_sort thy (sort1, sort2); |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
187 |
in |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
188 |
consume (op =) coT |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
189 |
##>> consume (op =) contraT |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
190 |
#>> pair sort |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
191 |
end; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
192 |
val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
193 |
val _ = if null left_variances then () else bad_typ (); |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
194 |
in variances end; |
40587 | 195 |
|
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
196 |
fun gen_type_lifting prep_term some_prfx raw_t thy = |
40583 | 197 |
let |
41387 | 198 |
val mapper_fixT = prep_term thy raw_t; |
199 |
val T = fastype_of mapper_fixT; |
|
40587 | 200 |
val _ = Type.no_tvars T; |
41387 | 201 |
val mapper = singleton (Variable.polymorphic (ProofContext.init_global thy)) mapper_fixT; |
40587 | 202 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
203 |
| add_tycos _ = I; |
|
204 |
val tycos = add_tycos T []; |
|
205 |
val tyco = if tycos = ["fun"] then "fun" |
|
206 |
else case remove (op =) "fun" tycos |
|
207 |
of [tyco] => tyco |
|
208 |
| _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T); |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
209 |
val prfx = the_default (Long_Name.base_name tyco) some_prfx; |
40587 | 210 |
val variances = analyze_variances thy tyco T; |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
211 |
val ctxt = ProofContext.init_global thy; |
41387 | 212 |
val (comp_prop, prove_compositionality) = make_comp_prop ctxt variances (tyco, mapper); |
213 |
val (id_prop, prove_identity) = make_id_prop ctxt variances (tyco, mapper); |
|
214 |
val _ = Thm.cterm_of thy id_prop; |
|
40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset
|
215 |
val qualify = Binding.qualify true prfx o Binding.name; |
41387 | 216 |
fun after_qed [single_comp_thm, single_id_thm] lthy = |
40587 | 217 |
lthy |
41387 | 218 |
|> Local_Theory.note ((qualify compN, []), single_comp_thm) |
219 |
||>> Local_Theory.note ((qualify idN, []), single_id_thm) |
|
220 |
|-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy => |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
221 |
lthy |
41388 | 222 |
|> Local_Theory.note ((qualify compositionalityN, []), |
223 |
[prove_compositionality lthy comp_thm]) |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
224 |
|> snd |
41388 | 225 |
|> Local_Theory.note ((qualify identityN, []), |
226 |
[prove_identity lthy id_thm]) |
|
227 |
|> snd |
|
228 |
|> Local_Theory.declaration false (fn phi => Data.map |
|
229 |
(Symtab.update (tyco, { mapper = Morphism.term phi mapper, variances = variances, |
|
230 |
comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm })))) |
|
40583 | 231 |
in |
232 |
thy |
|
233 |
|> Named_Target.theory_init |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
234 |
|> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) |
40583 | 235 |
end |
236 |
||
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
237 |
val type_lifting = gen_type_lifting Sign.cert_term; |
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
238 |
val type_lifting_cmd = gen_type_lifting Syntax.read_term_global; |
40583 | 239 |
|
240 |
val _ = |
|
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
241 |
Outer_Syntax.command "type_lifting" "register operations managing the functorial structure of a type" Keyword.thy_goal |
40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset
|
242 |
(Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term |
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
243 |
>> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_lifting_cmd prfx t)))); |
40583 | 244 |
|
40582 | 245 |
end; |