author  haftmann 
Fri, 17 Dec 2010 22:00:54 +0100  
changeset 41298  aad679ca38d2 
parent 40968  a6fcd305f7dc 
child 41371  35d2241c169c 
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 
9 
val find_atomic: theory > typ > (typ * (bool * bool)) list 

10 
val construct_mapper: theory > (string * bool > term) 

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 
14 
val entries: theory > entry Symtab.table 

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 

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

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

22 

40582  23 
(** functorial mappers and their properties **) 
24 

25 
(* bookkeeping *) 

26 

27 
type entry = { mapper: string, variances: (sort * (bool * bool)) list, 

40611  28 
compositionality: thm, identity: thm }; 
40582  29 

30 
structure Data = Theory_Data( 

31 
type T = entry Symtab.table 

32 
val empty = Symtab.empty 

40614  33 
fun merge (xy : T * T) = Symtab.merge (K true) xy 
40582  34 
val extend = I 
35 
); 

36 

37 
val entries = Data.get; 

38 

39 

40 
(* type analysis *) 

41 

42 
fun find_atomic thy T = 

43 
let 

44 
val variances_of = Option.map #variances o Symtab.lookup (Data.get thy); 

45 
fun add_variance is_contra T = 

46 
AList.map_default (op =) (T, (false, false)) 

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

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

49 
(if co then analyze is_contra T else I) 

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

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

52 
of NONE => add_variance is_contra T 

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

54 
 analyze is_contra T = add_variance is_contra T; 

55 
in analyze false T [] end; 

56 

57 
fun construct_mapper thy atomic = 

58 
let 

59 
val lookup = the o Symtab.lookup (Data.get thy); 

60 
fun constructs is_contra (_, (co, contra)) T T' = 

61 
(if co then [construct is_contra T T'] else []) 

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

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

64 
let 

65 
val { mapper, variances, ... } = lookup tyco; 

66 
val args = maps (fn (arg_pattern, (T, T')) => 

67 
constructs is_contra arg_pattern T T') 

68 
(variances ~~ (Ts ~~ Ts')); 

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

70 
in list_comb (Const (mapper, map fastype_of args > U > U'), args) end 

71 
 construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); 

72 
in construct end; 

73 

74 

75 
(* mapper properties *) 

76 

40611  77 
fun make_compositionality_prop variances (tyco, mapper) = 
40582  78 
let 
79 
fun invents n k nctxt = 

80 
let 

81 
val names = Name.invents nctxt n k; 

82 
in (names, fold Name.declare names nctxt) end; 

41298  83 
val (((vs3, vs2), vs1), _) = Name.context 
40582  84 
> invents Name.aT (length variances) 
85 
>> invents Name.aT (length variances) 

86 
>> invents Name.aT (length variances); 

87 
fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort)) 

88 
vs variances; 

89 
val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3); 

90 
fun mk_argT ((T, T'), (_, (co, contra))) = 

91 
(if co then [(T > T')] else []) 

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

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

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

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

96 
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); 

97 
val ((names21, names32), nctxt) = Name.context 

98 
> invents "f" (length Ts21) 

99 
>> invents "f" (length Ts32); 

100 
val T1 = Type (tyco, Ts1); 

101 
val T2 = Type (tyco, Ts2); 

102 
val T3 = Type (tyco, Ts3); 

40857  103 
val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3); 
40582  104 
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); 
105 
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => 

106 
if not is_contra then 

107 
Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0)) 

108 
else 

109 
Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0)) 

110 
) contras (args21 ~~ args32) 

111 
fun mk_mapper T T' args = list_comb (Const (mapper, 

112 
map fastype_of args > T > T'), args); 

113 
val lhs = mk_mapper T2 T1 (map Free args21) $ 

114 
(mk_mapper T3 T2 (map Free args32) $ x); 

115 
val rhs = mk_mapper T3 T1 args31 $ x; 

40597  116 
in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end; 
40582  117 

118 
fun make_identity_prop variances (tyco, mapper) = 

119 
let 

120 
val vs = Name.invents Name.context Name.aT (length variances); 

121 
val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances; 

122 
fun bool_num b = if b then 1 else 0; 

123 
fun mk_argT (T, (_, (co, contra))) = 

124 
replicate (bool_num co + bool_num contra) (T > T) 

125 
val Ts' = maps mk_argT (Ts ~~ variances) 

126 
val T = Type (tyco, Ts); 

40857  127 
val x = Free (Long_Name.base_name tyco, T); 
40582  128 
val lhs = list_comb (Const (mapper, Ts' > T > T), 
129 
map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x; 

130 
in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end; 

131 

132 

40597  133 
(* analyzing and registering mappers *) 
40582  134 

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

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

136 
 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

137 

40587  138 
fun split_mapper_typ "fun" T = 
139 
let 

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

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

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

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

144 
 split_mapper_typ tyco T = 

145 
let 

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

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

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

149 

150 
fun analyze_variances thy tyco T = 

151 
let 

152 
fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T); 

153 
val (Ts, T1, T2) = split_mapper_typ tyco T 

154 
handle List.Empty => bad_typ (); 

155 
val _ = pairself 

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

157 
val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) 

158 
handle TYPE _ => bad_typ (); 

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

160 
then bad_typ () else (); 

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

161 
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

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

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

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

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

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

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

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

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

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

171 
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

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

173 
in variances end; 
40587  174 

40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset

175 
fun gen_type_lifting prep_term some_prfx raw_t thy = 
40583  176 
let 
40587  177 
val (mapper, T) = case prep_term thy raw_t 
178 
of Const cT => cT 

179 
 t => error ("No constant: " ^ Syntax.string_of_term_global thy t); 

40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset

180 
val prfx = the_default (Long_Name.base_name mapper) some_prfx; 
40587  181 
val _ = Type.no_tvars T; 
182 
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 

183 
 add_tycos _ = I; 

184 
val tycos = add_tycos T []; 

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

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

187 
of [tyco] => tyco 

188 
 _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T); 

189 
val variances = analyze_variances thy tyco T; 

40611  190 
val compositionality_prop = uncurry (fold_rev Logic.all) 
191 
(make_compositionality_prop variances (tyco, mapper)); 

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

192 
val identity_prop = uncurry Logic.all 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

193 
(make_identity_prop variances (tyco, mapper)); 
40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset

194 
val qualify = Binding.qualify true prfx o Binding.name; 
40611  195 
fun after_qed [single_compositionality, single_identity] lthy = 
40587  196 
lthy 
40611  197 
> Local_Theory.note ((qualify compositionalityN, []), single_compositionality) 
40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

198 
>> Local_Theory.note ((qualify identityN, []), single_identity) 
40611  199 
> (fn ((_, [compositionality]), (_, [identity])) => 
40594
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

200 
(Local_Theory.background_theory o Data.map) 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

201 
(Symtab.update (tyco, { mapper = mapper, variances = variances, 
40611  202 
compositionality = compositionality, identity = identity }))); 
40583  203 
in 
204 
thy 

205 
> Named_Target.theory_init 

40611  206 
> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop]) 
40583  207 
end 
208 

40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset

209 
val type_lifting = gen_type_lifting Sign.cert_term; 
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset

210 
val type_lifting_cmd = gen_type_lifting Syntax.read_term_global; 
40583  211 

212 
val _ = 

40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset

213 
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

214 
(Scan.option (Parse.name  Parse.$$$ ":")  Parse.term 
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset

215 
>> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_lifting_cmd prfx t)))); 
40583  216 

40582  217 
end; 