author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37469  1436d6f28f17 
child 38348  cf7b2121ad9d 
permissions  rwrr 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset

1 
(* Title: HOL/Tools/typecopy.ML 
20426  2 
Author: Florian Haftmann, TU Muenchen 
3 

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

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset

7 
signature TYPECOPY = 
20426  8 
sig 
37469  9 
type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string, 
10 
constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm } 

11 
val typecopy: binding * (string * sort) list > typ > binding > binding 

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

12 
> theory > (string * info) * theory 
25506  13 
val get_info: theory > string > info option 
25489  14 
val interpretation: (string > theory > theory) > theory > theory 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

15 
val add_default_code: string > theory > theory 
20426  16 
val setup: theory > theory 
17 
end; 

18 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset

19 
structure Typecopy: TYPECOPY = 
20426  20 
struct 
21 

22 
(* theory data *) 

23 

24 
type info = { 

25 
vs: (string * sort) list, 

37469  26 
typ: typ, 
20426  27 
constr: string, 
37469  28 
proj: string, 
29 
constr_inject: thm, 

30 
proj_inject: thm, 

31 
constr_proj: thm, 

32 
proj_constr: thm 

20426  33 
}; 
34 

37469  35 
structure Typecopy_Data = Theory_Data 
22846  36 
( 
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

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

38 
val empty = Symtab.empty; 
20426  39 
val extend = I; 
33522  40 
fun merge data = Symtab.merge (K true) data; 
22846  41 
); 
42 

37469  43 
val get_info = Symtab.lookup o Typecopy_Data.get; 
20426  44 

45 

25489  46 
(* interpretation of type copies *) 
20426  47 

33314  48 
structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =); 
49 
val interpretation = Typecopy_Interpretation.interpretation; 

20426  50 

31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

51 

31735  52 
(* introducing typecopies *) 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

53 

37469  54 
fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...}, 
55 
{ Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy = 

56 
let 

57 
val exists_thm = 

58 
UNIV_I 

59 
> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] []; 

60 
val constr_inject = Abs_inject OF [exists_thm, exists_thm]; 

61 
val proj_constr = Abs_inverse OF [exists_thm]; 

62 
val info = { 

63 
vs = vs, 

64 
typ = rep_type, 

65 
constr = Abs_name, 

66 
proj = Rep_name, 

67 
constr_inject = constr_inject, 

68 
proj_inject = Rep_inject, 

69 
constr_proj = Rep_inverse, 

70 
proj_constr = proj_constr 

71 
}; 

72 
in 

73 
thy 

74 
> (Typecopy_Data.map o Symtab.update_new) (tyco, info) 

75 
> Typecopy_Interpretation.data tyco 

76 
> pair (tyco, info) 

77 
end 

78 

79 
fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy = 

20426  80 
let 
28664  81 
val ty = Sign.certify_typ thy raw_ty; 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36156
diff
changeset

82 
val ctxt = ProofContext.init_global thy > Variable.declare_typ ty; 
36156  83 
val vs = map (ProofContext.check_tfree ctxt) raw_vs; 
20426  84 
val tac = Tactic.rtac UNIV_witness 1; 
85 
in 

86 
thy 

36150
123f721c9a37
typecopy: observe given sort constraints more precisely;
wenzelm
parents:
35994
diff
changeset

87 
> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) 
37469  88 
(HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac 
89 
> (fn (tyco, info) => add_info tyco vs info) 

20426  90 
end; 
91 

92 

31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

93 
(* default code setup *) 
20835  94 

31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

95 
fun add_default_code tyco thy = 
25489  96 
let 
37469  97 
val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } = 
98 
get_info thy tyco; 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35842
diff
changeset

99 
val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c)); 
28423  100 
val ty = Type (tyco, map TFree vs); 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

101 
val proj = Const (proj, ty > ty_rep); 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

102 
val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

103 
val eq_lhs = Const (@{const_name eq_class.eq}, ty > ty > HOLogic.boolT) 
28664  104 
$ t_x $ t_y; 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

105 
val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y); 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

106 
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs); 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

107 
fun tac eq_thm = Class.intro_classes_tac [] 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

108 
THEN (Simplifier.rewrite_goals_tac 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

109 
(map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject])) 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

110 
THEN ALLGOALS (rtac @{thm refl}); 
28664  111 
fun mk_eq_refl thy = @{thm HOL.eq_refl} 
112 
> Thm.instantiate 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35842
diff
changeset

113 
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], []) 
28664  114 
> AxClass.unoverload thy; 
25489  115 
in 
25506  116 
thy 
28664  117 
> Code.add_datatype [constr] 
37469  118 
> Code.add_eqn proj_constr 
33553  119 
> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq]) 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

120 
> `(fn lthy => Syntax.check_term lthy eq) 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

121 
> (fn eq => Specification.definition 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

122 
(NONE, (Attrib.empty_binding, eq))) 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

123 
> (fn (_, (_, eq_thm)) => 
28664  124 
Class.prove_instantiation_exit_result Morphism.thm 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

125 
(fn _ => fn eq_thm => tac eq_thm) eq_thm) 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

126 
> (fn eq_thm => Code.add_eqn eq_thm) 
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

127 
> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy) 
25489  128 
end; 
20426  129 

25489  130 
val setup = 
33314  131 
Typecopy_Interpretation.init 
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset

132 
#> interpretation add_default_code 
20426  133 

22846  134 
end; 