author  haftmann 
Tue, 21 Dec 2010 17:52:23 +0100  
changeset 41373  48503e4e96b6 
parent 41371  35d2241c169c 
child 41387  fb81cb128e7e 
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 

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 usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

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

24 

40582  25 
(** functorial mappers and their properties **) 
26 

27 
(* bookkeeping *) 

28 

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

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

30 
comp: thm, id: thm }; 
40582  31 

32 
structure Data = Theory_Data( 

33 
type T = entry Symtab.table 

34 
val empty = Symtab.empty 

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

38 

39 
val entries = Data.get; 

40 

41 

42 
(* type analysis *) 

43 

44 
fun find_atomic thy T = 

45 
let 

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

47 
fun add_variance is_contra T = 

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

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

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

51 
(if co then analyze is_contra T else I) 

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

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

54 
of NONE => add_variance is_contra T 

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

56 
 analyze is_contra T = add_variance is_contra T; 

57 
in analyze false T [] end; 

58 

59 
fun construct_mapper thy atomic = 

60 
let 

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

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

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

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

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

66 
let 

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

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

69 
constructs is_contra arg_pattern T T') 

70 
(variances ~~ (Ts ~~ Ts')); 

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

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

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

74 
in construct end; 

75 

76 

77 
(* mapper properties *) 

78 

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

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

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

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

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

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

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

86 
val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3); 
40582  87 
fun mk_argT ((T, T'), (_, (co, contra))) = 
88 
(if co then [(T > T')] else []) 

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

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

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

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

93 
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

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

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

96 
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

97 
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

98 
val ((names21, names32), nctxt) = Variable.names_of ctxt 
40582  99 
> invents "f" (length Ts21) 
100 
>> invents "f" (length Ts32); 

101 
val T1 = Type (tyco, Ts1); 

102 
val T2 = Type (tyco, Ts2); 

103 
val T3 = Type (tyco, Ts3); 

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 

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

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

109 
HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) 
40582  110 
) contras (args21 ~~ args32) 
111 
fun mk_mapper T T' args = list_comb (Const (mapper, 

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

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

113 
val lhs = HOLogic.mk_comp (mk_mapper T2 T1 (map Free args21), mk_mapper T3 T2 (map Free args32)); 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

114 
val rhs = mk_mapper T3 T1 args31; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

115 
in fold_rev Logic.all (map Free (args21 @ args32)) ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end; 
40582  116 

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

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

119 
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

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

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

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

125 
val T = Type (tyco, Ts); 

126 
val lhs = list_comb (Const (mapper, Ts' > T > T), 

41373  127 
map (HOLogic.id_const o domain_type) Ts'); 
128 
in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end; 

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

129 

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

130 
val comp_apply = Simpdata.mk_eq @{thm o_apply}; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

131 
val id_def = Simpdata.mk_eq @{thm id_def}; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

132 

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

133 
fun make_compositionality ctxt thm = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

135 
val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

136 
val thm'' = @{thm fun_cong} OF [thm']; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

137 
val thm''' = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

138 
(Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o Conv.rewr_conv) comp_apply thm''; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

139 
in singleton (Variable.export ctxt' ctxt) thm''' end; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

140 

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

141 
fun args_conv k conv = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

142 
if k <= 0 then Conv.all_conv 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

143 
else Conv.combination_conv (args_conv (k  1) conv) conv; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

144 

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

145 
fun make_identity ctxt variances thm = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

147 
val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

148 
fun bool_num b = if b then 1 else 0; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

149 
val num_args = Integer.sum 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

150 
(map (fn (_, (co, contra)) => bool_num co + bool_num contra) variances); 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

151 
val thm'' = 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

152 
(Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o args_conv num_args o Conv.rewr_conv) id_def thm'; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

153 
in singleton (Variable.export ctxt' ctxt) thm'' end; 
40582  154 

155 

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

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

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

159 
 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

160 

40587  161 
fun split_mapper_typ "fun" T = 
162 
let 

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

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

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

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

167 
 split_mapper_typ tyco T = 

168 
let 

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

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

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

172 

173 
fun analyze_variances thy tyco T = 

174 
let 

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

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

177 
handle List.Empty => bad_typ (); 

178 
val _ = pairself 

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

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; 
fae1da97bb5e
infer variances of usergiven mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset

188 
val sort = Sign.inter_sort thy (sort1, sort2); 
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 

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

198 
fun gen_type_lifting prep_term some_prfx raw_t thy = 
40583  199 
let 
40587  200 
val (mapper, T) = case prep_term thy raw_t 
201 
of Const cT => cT 

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

203 
val _ = Type.no_tvars T; 

204 
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 

205 
 add_tycos _ = I; 

206 
val tycos = add_tycos T []; 

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

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

209 
of [tyco] => tyco 

210 
 _ => 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

211 
val prfx = the_default (Long_Name.base_name tyco) some_prfx; 
40587  212 
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

213 
val ctxt = ProofContext.init_global thy; 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

214 
val comp_prop = make_comp_prop ctxt variances (tyco, mapper); 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

216 
val qualify = Binding.qualify true prfx o Binding.name; 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

217 
fun after_qed [single_comp, single_id] lthy = 
40587  218 
lthy 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

219 
> Local_Theory.note ((qualify compN, []), single_comp) 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

220 
>> Local_Theory.note ((qualify idN, []), single_id) 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

221 
> (fn ((_, [comp]), (_, [id])) => fn lthy => 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

223 
> Local_Theory.note ((qualify compositionalityN, []), [make_compositionality lthy comp]) 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

225 
> Local_Theory.note ((qualify identityN, []), [make_identity lthy variances id]) 
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

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

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

228 
(Symtab.update (tyco, { mapper = mapper, variances = variances, 
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset

229 
comp = comp, id = id }))); 
40583  230 
in 
231 
thy 

232 
> Named_Target.theory_init 

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

233 
> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) 
40583  234 
end 
235 

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

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

237 
val type_lifting_cmd = gen_type_lifting Syntax.read_term_global; 
40583  238 

239 
val _ = 

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

240 
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

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

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

40582  244 
end; 