author  haftmann 
Thu, 23 Dec 2010 09:20:43 +0100  
changeset 41395  cf5ab80b6717 
parent 41390  207ee8f8a19c 
child 41472  f6ab14e61604 
permissions  rwrr 
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 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

12 
val type_lifting: string option > term > local_theory > Proof.state 
40582  13 
type entry 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

14 
val entries: Proof.context > entry list 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 

41395  20 
(* bookkeeping *) 
21 

41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

22 
val compN = "comp"; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

23 
val idN = "id"; 
40611  24 
val compositionalityN = "compositionality"; 
40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

25 
val identityN = "identity"; 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

26 

41387  27 
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

28 
comp: thm, id: thm }; 
40582  29 

41388  30 
structure Data = Generic_Data( 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

31 
type T = entry list Symtab.table 
40582  32 
val empty = Symtab.empty 
40614  33 
fun merge (xy : T * T) = Symtab.merge (K true) xy 
40582  34 
val extend = I 
35 
); 

36 

41388  37 
val entries = Data.get o Context.Proof; 
40582  38 

39 

40 
(* type analysis *) 

41 

41389  42 
fun term_with_typ ctxt T t = Envir.subst_term_types 
43 
(Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; 

44 

41388  45 
fun find_atomic ctxt T = 
40582  46 
let 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

47 
val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt); 
40582  48 
fun add_variance is_contra T = 
49 
AList.map_default (op =) (T, (false, false)) 

50 
((if is_contra then apsnd else apfst) (K true)); 

51 
fun analyze' is_contra (_, (co, contra)) T = 

52 
(if co then analyze is_contra T else I) 

53 
#> (if contra then analyze (not is_contra) T else I) 

54 
and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco 

55 
of NONE => add_variance is_contra T 

56 
 SOME variances => fold2 (analyze' is_contra) variances Ts) 

57 
 analyze is_contra T = add_variance is_contra T; 

58 
in analyze false T [] end; 

59 

41388  60 
fun construct_mapper ctxt atomic = 
40582  61 
let 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

62 
val lookup = hd o Symtab.lookup_list (entries ctxt); 
40582  63 
fun constructs is_contra (_, (co, contra)) T T' = 
64 
(if co then [construct is_contra T T'] else []) 

65 
@ (if contra then [construct (not is_contra) T T'] else []) 

66 
and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) = 

67 
let 

41388  68 
val { mapper = raw_mapper, variances, ... } = lookup tyco; 
40582  69 
val args = maps (fn (arg_pattern, (T, T')) => 
70 
constructs is_contra arg_pattern T T') 

71 
(variances ~~ (Ts ~~ Ts')); 

72 
val (U, U') = if is_contra then (T', T) else (T, T'); 

41388  73 
val mapper = term_with_typ ctxt (map fastype_of args > U > U') raw_mapper; 
74 
in list_comb (mapper, args) end 

40582  75 
 construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); 
76 
in construct end; 

77 

78 

79 
(* mapper properties *) 

80 

41387  81 
val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss; 
82 

41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

83 
fun make_comp_prop ctxt variances (tyco, mapper) = 
40582  84 
let 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

85 
val sorts = map fst variances 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

86 
val (((vs3, vs2), vs1), _) = ctxt 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

87 
> Variable.invent_types sorts 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

88 
>> Variable.invent_types sorts 
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 
val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3); 
40582  91 
fun mk_argT ((T, T'), (_, (co, contra))) = 
92 
(if co then [(T > T')] else []) 

93 
@ (if contra then [(T' > T)] else []); 

94 
val contras = maps (fn (_, (co, contra)) => 

95 
(if co then [false] else []) @ (if contra then [true] else [])) variances; 

96 
val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); 

97 
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

98 
fun invents n k nctxt = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

99 
let 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

100 
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

101 
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

102 
val ((names21, names32), nctxt) = Variable.names_of ctxt 
40582  103 
> invents "f" (length Ts21) 
104 
>> invents "f" (length Ts32); 

105 
val T1 = Type (tyco, Ts1); 

106 
val T2 = Type (tyco, Ts2); 

107 
val T3 = Type (tyco, Ts3); 

108 
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); 

109 
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => 

110 
if not is_contra then 

41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

111 
HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) 
40582  112 
else 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

113 
HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) 
40582  114 
) contras (args21 ~~ args32) 
41395  115 
fun mk_mapper T T' args = list_comb 
116 
(term_with_typ ctxt (map fastype_of args > T > T') mapper, args); 

41387  117 
val mapper21 = mk_mapper T2 T1 (map Free args21); 
118 
val mapper32 = mk_mapper T3 T2 (map Free args32); 

119 
val mapper31 = mk_mapper T3 T1 args31; 

41395  120 
val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
121 
(HOLogic.mk_comp (mapper21, mapper32), mapper31); 

41387  122 
val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3) 
41395  123 
val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
124 
(mapper21 $ (mapper32 $ x), mapper31 $ x); 

41387  125 
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1; 
126 
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2; 

127 
fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop 

128 
(K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]] 

129 
THEN' Simplifier.asm_lr_simp_tac compositionality_ss 

130 
THEN_ALL_NEW (Goal.assume_rule_tac ctxt)))); 

131 
in (comp_prop, prove_compositionality) end; 

132 

133 
val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss; 

40582  134 

41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

135 
fun make_id_prop ctxt variances (tyco, mapper) = 
40582  136 
let 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

137 
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

138 
val Ts = map TFree vs; 
40582  139 
fun bool_num b = if b then 1 else 0; 
140 
fun mk_argT (T, (_, (co, contra))) = 

41387  141 
replicate (bool_num co + bool_num contra) T 
142 
val arg_Ts = maps mk_argT (Ts ~~ variances) 

40582  143 
val T = Type (tyco, Ts); 
41387  144 
val head = term_with_typ ctxt (map (fn T => T > T) arg_Ts > T > T) mapper; 
145 
val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); 

146 
val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); 

147 
val rhs = HOLogic.id_const T; 

41395  148 
val (id_prop, identity_prop) = pairself 
149 
(HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); 

41387  150 
fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop 
151 
(K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss))); 

152 
in (id_prop, prove_identity) end; 

40582  153 

154 

40597  155 
(* analyzing and registering mappers *) 
40582  156 

40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

157 
fun consume eq x [] = (false, []) 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

158 
 consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys); 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

159 

40587  160 
fun split_mapper_typ "fun" T = 
161 
let 

162 
val (Ts', T') = strip_type T; 

163 
val (Ts'', T'') = split_last Ts'; 

164 
val (Ts''', T''') = split_last Ts''; 

165 
in (Ts''', T''', T'' > T') end 

166 
 split_mapper_typ tyco T = 

167 
let 

168 
val (Ts', T') = strip_type T; 

169 
val (Ts'', T'') = split_last Ts'; 

170 
in (Ts'', T'', T') end; 

171 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

172 
fun analyze_variances ctxt tyco T = 
40587  173 
let 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

174 
fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T); 
40587  175 
val (Ts, T1, T2) = split_mapper_typ tyco T 
176 
handle List.Empty => bad_typ (); 

177 
val _ = pairself 

178 
((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) 

41387  179 
handle TYPE _ => bad_typ (); 
40587  180 
val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) 
181 
handle TYPE _ => bad_typ (); 

182 
val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) 

183 
then bad_typ () else (); 

40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

184 
fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

185 
let 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

186 
val coT = TFree var1 > TFree var2; 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

187 
val contraT = TFree var2 > TFree var1; 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

188 
val sort = Sign.inter_sort (ProofContext.theory_of ctxt) (sort1, sort2); 
40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

189 
in 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

190 
consume (op =) coT 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

191 
##>> consume (op =) contraT 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

192 
#>> pair sort 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

193 
end; 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

194 
val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts; 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

195 
val _ = if null left_variances then () else bad_typ (); 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

196 
in variances end; 
40587  197 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

198 
fun gen_type_lifting prep_term some_prfx raw_mapper lthy = 
40583  199 
let 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

200 
val input_mapper = prep_term lthy raw_mapper; 
41389  201 
val T = fastype_of input_mapper; 
40587  202 
val _ = Type.no_tvars T; 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

203 
val mapper = singleton (Variable.polymorphic lthy) input_mapper; 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

204 
val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then () 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

205 
else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T); 
40587  206 
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 
207 
 add_tycos _ = I; 

208 
val tycos = add_tycos T []; 

209 
val tyco = if tycos = ["fun"] then "fun" 

210 
else case remove (op =) "fun" tycos 

211 
of [tyco] => tyco 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

212 
 _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T); 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

213 
val prfx = the_default (Long_Name.base_name tyco) some_prfx; 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

214 
val variances = analyze_variances lthy tyco T; 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

215 
val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper); 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

216 
val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper); 
40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset

217 
val qualify = Binding.qualify true prfx o Binding.name; 
41389  218 
fun mapper_declaration comp_thm id_thm phi context = 
219 
let 

220 
val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context)); 

221 
val mapper' = Morphism.term phi mapper; 

222 
val T_T' = pairself fastype_of (mapper, mapper'); 

223 
in if typ_instance T_T' andalso typ_instance (swap T_T') 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

224 
then (Data.map o Symtab.cons_list) (tyco, 
41389  225 
{ mapper = mapper', variances = variances, 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

226 
comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context 
41389  227 
else context 
228 
end; 

41387  229 
fun after_qed [single_comp_thm, single_id_thm] lthy = 
40587  230 
lthy 
41387  231 
> Local_Theory.note ((qualify compN, []), single_comp_thm) 
232 
>> Local_Theory.note ((qualify idN, []), single_id_thm) 

233 
> (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

234 
lthy 
41388  235 
> Local_Theory.note ((qualify compositionalityN, []), 
236 
[prove_compositionality lthy comp_thm]) 

41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

237 
> snd 
41388  238 
> Local_Theory.note ((qualify identityN, []), 
239 
[prove_identity lthy id_thm]) 

240 
> snd 

41389  241 
> Local_Theory.declaration false (mapper_declaration comp_thm id_thm)) 
40583  242 
in 
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

243 
lthy 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

244 
> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) 
40583  245 
end 
246 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

247 
val type_lifting = gen_type_lifting Syntax.check_term; 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

248 
val type_lifting_cmd = gen_type_lifting Syntax.read_term; 
40583  249 

41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

250 
val _ = Outer_Syntax.local_theory_to_proof "type_lifting" 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

251 
"register operations managing the functorial structure of a type" 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

252 
Keyword.thy_goal (Scan.option (Parse.name  Parse.$$$ ":")  Parse.term 
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset

253 
>> (fn (prfx, t) => type_lifting_cmd prfx t)); 
40583  254 

40582  255 
end; 