author  haftmann 
Tue, 30 Sep 2008 12:49:18 +0200  
changeset 28423  9fc3befd8191 
parent 28394  b9c8e3a12a98 
child 28664  d89ac2917157 
permissions  rwrr 
20426  1 
(* Title: HOL/Tools/typecopy_package.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

20855  5 
Introducing copies of types using trivial typedefs; datatypelike abstraction. 
20426  6 
*) 
7 

8 
signature TYPECOPY_PACKAGE = 

9 
sig 

10 
type info = { 

11 
vs: (string * sort) list, 

12 
constr: string, 

13 
typ: typ, 

14 
inject: thm, 

15 
proj: string * typ, 

16 
proj_def: thm 

17 
} 

18 
val add_typecopy: bstring * string list > typ > (bstring * bstring) option 

20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset

19 
> theory > (string * info) * theory 
20426  20 
val get_typecopies: theory > string list 
25506  21 
val get_info: theory > string > info option 
25489  22 
val interpretation: (string > theory > theory) > theory > theory 
22846  23 
val print_typecopies: theory > unit 
20426  24 
val setup: theory > theory 
25 
end; 

26 

27 
structure TypecopyPackage: TYPECOPY_PACKAGE = 

28 
struct 

29 

30 
(* theory data *) 

31 

32 
type info = { 

33 
vs: (string * sort) list, 

34 
constr: string, 

35 
typ: typ, 

36 
inject: thm, 

37 
proj: string * typ, 

38 
proj_def: thm 

39 
}; 

40 

41 
structure TypecopyData = TheoryDataFun 

22846  42 
( 
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

43 
type T = info Symtab.table; 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

44 
val empty = Symtab.empty; 
20426  45 
val copy = I; 
46 
val extend = I; 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

47 
fun merge _ = Symtab.merge (K true); 
22846  48 
); 
49 

50 
fun print_typecopies thy = 

51 
let 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

52 
val tab = TypecopyData.get thy; 
22846  53 
fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) = 
54 
(Pretty.block o Pretty.breaks) [ 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26732
diff
changeset

55 
Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)), 
22846  56 
Pretty.str "=", 
57 
(Pretty.str o Sign.extern_const thy) constr, 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26732
diff
changeset

58 
Syntax.pretty_typ_global thy typ, 
22846  59 
Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]]; 
20426  60 
in 
22846  61 
(Pretty.writeln o Pretty.block o Pretty.fbreaks) 
62 
(Pretty.str "type copies:" :: map mk (Symtab.dest tab)) 

20426  63 
end; 
64 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

65 
val get_typecopies = Symtab.keys o TypecopyData.get; 
25506  66 
val get_info = Symtab.lookup o TypecopyData.get; 
20426  67 

68 

25489  69 
(* interpretation of type copies *) 
20426  70 

24711  71 
structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =); 
25489  72 
val interpretation = TypecopyInterpretation.interpretation; 
20426  73 

74 

75 
(* add a type copy *) 

76 

77 
local 

78 

20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset

79 
fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy = 
20426  80 
let 
81 
val ty = prep_typ thy raw_ty; 

82 
val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs; 

83 
val tac = Tactic.rtac UNIV_witness 1; 

20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset

84 
fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, 
20426  85 
Rep_name = c_rep, Abs_inject = inject, 
21708  86 
Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
20426  87 
let 
88 
val exists_thm = 

89 
UNIV_I 

90 
> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []; 

91 
val inject' = inject OF [exists_thm, exists_thm]; 

92 
val proj_def = inverse OF [exists_thm]; 

93 
val info = { 

94 
vs = vs, 

95 
constr = c_abs, 

96 
typ = ty_rep, 

97 
inject = inject', 

98 
proj = (c_rep, ty_abs > ty_rep), 

99 
proj_def = proj_def 

100 
}; 

101 
in 

102 
thy 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

103 
> (TypecopyData.map o Symtab.update_new) (tyco, info) 
24711  104 
> TypecopyInterpretation.data tyco 
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset

105 
> pair (tyco, info) 
20426  106 
end 
107 
in 

108 
thy 

26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
25864
diff
changeset

109 
> TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn) 
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
25864
diff
changeset

110 
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac 
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset

111 
> (fn (tyco, info) => add_info tyco info) 
20426  112 
end; 
113 

114 
in 

115 

116 
val add_typecopy = gen_add_typecopy Sign.certify_typ; 

117 

22846  118 
end; 
20426  119 

120 

25489  121 
(* code generator setup *) 
20835  122 

25489  123 
fun add_typecopy_spec tyco thy = 
124 
let 

28423  125 
val SOME { constr, proj_def, inject, vs = raw_vs, ... } = get_info thy tyco; 
126 
val vs = (map o apsnd) 

127 
(curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) raw_vs; 

128 
val ty = Type (tyco, map TFree vs); 

28350  129 
val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr); 
26513  130 
fun add_def tyco lthy = 
131 
let 

132 
fun mk_side const_name = Const (const_name, ty > ty > HOLogic.boolT) 

133 
$ Free ("x", ty) $ Free ("y", ty); 

134 
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq 

26732  135 
(mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="})); 
26513  136 
val def' = Syntax.check_term lthy def; 
137 
val ((_, (_, thm)), lthy') = Specification.definition 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

138 
(NONE, (Attrib.no_binding, def')) lthy; 
26513  139 
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); 
140 
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; 

141 
in (thm', lthy') end; 

142 
fun tac thms = Class.intro_classes_tac [] 

143 
THEN ALLGOALS (ProofContext.fact_tac thms); 

28350  144 
fun add_eq_thms thy = 
26513  145 
let 
146 
val eq = inject 

28423  147 
> Code_Unit.constrain_thm thy [HOLogic.class_eq] 
26513  148 
> Simpdata.mk_eq 
28423  149 
> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}] 
150 
> AxClass.unoverload thy; 

28350  151 
val eq_refl = @{thm HOL.eq_refl} 
152 
> Thm.instantiate 

28423  153 
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) 
154 
> AxClass.unoverload thy; 

28350  155 
in 
156 
thy 

28370  157 
> Code.add_eqn eq 
158 
> Code.add_nonlinear_eqn eq_refl 

28350  159 
end; 
25489  160 
in 
25506  161 
thy 
28350  162 
> Code.add_datatype [(constr, ty_constr)] 
28370  163 
> Code.add_eqn proj_def 
28423  164 
> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq]) 
26513  165 
> add_def tyco 
166 
> (fn thm => Class.prove_instantiation_instance (K (tac [thm])) 

28394  167 
#> LocalTheory.exit_global 
28370  168 
#> Code.del_eqn thm 
28350  169 
#> add_eq_thms) 
25489  170 
end; 
20426  171 

25489  172 
val setup = 
173 
TypecopyInterpretation.init 

174 
#> interpretation add_typecopy_spec 

20426  175 

22846  176 
end; 