author  haftmann 
Sat, 24 Dec 2011 16:14:58 +0100  
changeset 45979  296d9a9c8d24 
parent 45839  43a5b86bc102 
child 46180  72ee700e1d8f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

1 
(* Title: HOL/Nominal/nominal_atoms.ML 
19494  2 
Author: Christian Urban and Stefan Berghofer, TU Muenchen 
3 

4 
Declaration of atom types to be used in nominal datatypes. 

5 
*) 

18068  6 

7 
signature NOMINAL_ATOMS = 

8 
sig 

9 
val create_nom_typedecls : string list > theory > theory 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

10 
type atom_info 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

11 
val get_atom_infos : theory > atom_info Symtab.table 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

12 
val get_atom_info : theory > string > atom_info option 
28372  13 
val the_atom_info : theory > string > atom_info 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

14 
val fs_class_of : theory > string > string 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

15 
val pt_class_of : theory > string > string 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

16 
val cp_class_of : theory > string > string > string 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

17 
val at_inst_of : theory > string > thm 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

18 
val pt_inst_of : theory > string > thm 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

19 
val cp_inst_of : theory > string > string > thm 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

20 
val dj_thm_of : theory > string > string > thm 
18068  21 
val atoms_of : theory > string list 
22 
val mk_permT : typ > typ 

23 
end 

24 

25 
structure NominalAtoms : NOMINAL_ATOMS = 

26 
struct 

27 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

28 
val finite_emptyI = @{thm "finite.emptyI"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

29 
val Collect_const = @{thm "Collect_const"}; 
21669  30 

24569  31 
val inductive_forall_def = @{thm "induct_forall_def"}; 
32 

21669  33 

22846  34 
(* theory data *) 
18068  35 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

36 
type atom_info = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

37 
{pt_class : string, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

38 
fs_class : string, 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

39 
cp_classes : string Symtab.table, 
28372  40 
at_inst : thm, 
41 
pt_inst : thm, 

28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

42 
cp_inst : thm Symtab.table, 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

43 
dj_thms : thm Symtab.table}; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

44 

33522  45 
structure NominalData = Theory_Data 
22846  46 
( 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

47 
type T = atom_info Symtab.table; 
18068  48 
val empty = Symtab.empty; 
49 
val extend = I; 

33522  50 
fun merge data = Symtab.merge (K true) data; 
22846  51 
); 
18068  52 

28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

53 
fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

54 
{pt_class = pt_class, 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

55 
fs_class = fs_class, 
28372  56 
cp_classes = cp_classes, 
57 
at_inst = at_inst, 

58 
pt_inst = pt_inst, 

28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

59 
cp_inst = cp_inst, 
28372  60 
dj_thms = dj_thms}; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

61 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

62 
val get_atom_infos = NominalData.get; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

63 
val get_atom_info = Symtab.lookup o NominalData.get; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

64 

28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

65 
fun gen_lookup lookup name = case lookup name of 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

66 
SOME info => info 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

67 
 NONE => error ("Unknown atom type " ^ quote name); 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

68 

cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

69 
fun the_atom_info thy = gen_lookup (get_atom_info thy); 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

70 

cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

71 
fun gen_lookup' f thy = the_atom_info thy #> f; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

72 
fun gen_lookup'' f thy = 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

73 
gen_lookup' (f #> Symtab.lookup #> gen_lookup) thy; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

74 

cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

75 
val fs_class_of = gen_lookup' #fs_class; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

76 
val pt_class_of = gen_lookup' #pt_class; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

77 
val at_inst_of = gen_lookup' #at_inst; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

78 
val pt_inst_of = gen_lookup' #pt_inst; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

79 
val cp_class_of = gen_lookup'' #cp_classes; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

80 
val cp_inst_of = gen_lookup'' #cp_inst; 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

81 
val dj_thm_of = gen_lookup'' #dj_thms; 
28372  82 

18068  83 
fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy)); 
84 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

85 
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); 
18068  86 

87 
fun mk_Cons x xs = 

88 
let val T = fastype_of x 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

89 
in Const ("List.list.Cons", T > HOLogic.listT T > HOLogic.listT T) $ x $ xs end; 
18068  90 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

91 
fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

92 
fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args); 
29585  93 

18068  94 
(* this function sets up all matters related to atom *) 
95 
(* kinds; the user specifies a list of atomkind names *) 

96 
(* atom_decl <ak1> ... <akn> *) 

97 
fun create_nom_typedecls ak_names thy = 

98 
let 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

99 

24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

100 
val (_,thy1) = 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

101 
fold_map (fn ak => fn thy => 
45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

102 
let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)]) 
45701  103 
val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy; 
31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset

104 

31784  105 
val injects = maps (#inject o Datatype.the_info thy1) dt_names; 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

106 
val ak_type = Type (Sign.intern_type thy1 ak,[]) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

107 
val ak_sign = Sign.intern_const thy1 ak 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

108 

30595
c87a3350f5a9
proper spacing before ML antiquotations  note that @ may be part of symbolic ML identifiers;
wenzelm
parents:
30345
diff
changeset

109 
val inj_type = @{typ nat} > ak_type 
c87a3350f5a9
proper spacing before ML antiquotations  note that @ may be part of symbolic ML identifiers;
wenzelm
parents:
30345
diff
changeset

110 
val inj_on_type = inj_type > @{typ "nat set"} > @{typ bool} 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

111 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

112 
(* first statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

113 
val stmnt1 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

114 
(Const (@{const_name "inj_on"},inj_on_type) $ 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

115 
Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat}) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

116 

31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset

117 
val simp1 = @{thm inj_on_def} :: injects; 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

118 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

119 
val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

120 
rtac @{thm ballI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

121 
rtac @{thm ballI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

122 
rtac @{thm impI} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

123 
atac 1] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

124 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

125 
val (inj_thm,thy2) = 
29585  126 
add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

127 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

128 
(* second statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

129 
val y = Free ("y",ak_type) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

130 
val stmnt2 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

131 
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0))) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

132 

27128
d2374ba6c02e
InductTacs.case_tac with proper context and proper declaration of local variable;
wenzelm
parents:
27112
diff
changeset

133 
val proof2 = fn {prems, context} => 
45133  134 
Induct_Tacs.case_tac context "y" 1 THEN 
27128
d2374ba6c02e
InductTacs.case_tac with proper context and proper declaration of local variable;
wenzelm
parents:
27112
diff
changeset

135 
asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN 
d2374ba6c02e
InductTacs.case_tac with proper context and proper declaration of local variable;
wenzelm
parents:
27112
diff
changeset

136 
rtac @{thm exI} 1 THEN 
d2374ba6c02e
InductTacs.case_tac with proper context and proper declaration of local variable;
wenzelm
parents:
27112
diff
changeset

137 
rtac @{thm refl} 1 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

138 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

139 
(* third statement *) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

140 
val (inject_thm,thy3) = 
29585  141 
add_thms_string [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

142 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

143 
val stmnt3 = HOLogic.mk_Trueprop 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

144 
(HOLogic.mk_not 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

145 
(Const ("Finite_Set.finite", HOLogic.mk_setT ak_type > HOLogic.boolT) $ 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

146 
HOLogic.mk_UNIV ak_type)) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

147 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

148 
val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

149 
val simp3 = [@{thm UNIV_def}] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

150 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

151 
val proof3 = fn _ => EVERY [cut_facts_tac inj_thm 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

152 
dtac @{thm range_inj_infinite} 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

153 
asm_full_simp_tac (HOL_basic_ss addsimps simp2) 1, 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

154 
simp_tac (HOL_basic_ss addsimps simp3) 1] 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

155 

c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

156 
val (inf_thm,thy4) = 
29585  157 
add_thms_string [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3 
24677
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

158 
in 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

159 
((inj_thm,inject_thm,inf_thm),thy4) 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

160 
end) ak_names thy 
c6295d2dce48
changed the representation of atoms to datatypes over nats
urbanc
parents:
24569
diff
changeset

161 

18068  162 
(* produces a list consisting of pairs: *) 
163 
(* fst component is the atomkind name *) 

164 
(* snd component is its type *) 

21289
920b7b893d9c
deleted all uses of sign_of as it's now the identity function
urbanc
parents:
20377
diff
changeset

165 
val full_ak_names = map (Sign.intern_type thy1) ak_names; 
18068  166 
val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names; 
167 

168 
(* declares a swapping function for every atomkind, it is *) 

169 
(* const swap_<ak> :: <akT> * <akT> => <akT> => <akT> *) 

170 
(* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *) 

171 
(* overloades then the general swapfunction *) 

20179  172 
val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy => 
18068  173 
let 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

174 
val thy' = Sign.add_path "rec" thy; 
18068  175 
val swapT = HOLogic.mk_prodT (T, T) > T > T; 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

176 
val swap_name = "swap_" ^ ak_name; 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

177 
val full_swap_name = Sign.full_bname thy' swap_name; 
18068  178 
val a = Free ("a", T); 
179 
val b = Free ("b", T); 

180 
val c = Free ("c", T); 

181 
val ab = Free ("ab", HOLogic.mk_prodT (T, T)) 

182 
val cif = Const ("HOL.If", HOLogic.boolT > T > T > T); 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

183 
val cswap_akname = Const (full_swap_name, swapT); 
19494  184 
val cswap = Const ("Nominal.swap", swapT) 
18068  185 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

186 
val name = swap_name ^ "_def"; 
18068  187 
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

188 
(Free (swap_name, swapT) $ HOLogic.mk_prod (a,b) $ c, 
18068  189 
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c))) 
190 
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) 

191 
in 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

192 
thy' > 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

193 
Primrec.add_primrec_global 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

194 
[(Binding.name swap_name, SOME swapT, NoSyn)] 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

195 
[(Attrib.empty_binding, def1)] > 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

196 
Sign.parent_path >> 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

197 
Global_Theory.add_defs_unchecked true 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

198 
[((Binding.name name, def2), [])] >> (snd o fst) 
26398
fccb74555d9e
removed redundant axiomatizations of XXX_infinite (fact already proven);
wenzelm
parents:
26343
diff
changeset

199 
end) ak_names_types thy1; 
18068  200 

201 
(* declares a permutation function for every atomkind acting *) 

202 
(* on such atoms *) 

203 
(* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT *) 

204 
(* <ak>_prm_<ak> [] a = a *) 

205 
(* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a) *) 

20179  206 
val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy => 
18068  207 
let 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

208 
val thy' = Sign.add_path "rec" thy; 
18068  209 
val swapT = HOLogic.mk_prodT (T, T) > T > T; 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

210 
val swap_name = Sign.full_bname thy' ("swap_" ^ ak_name) 
18068  211 
val prmT = mk_permT T > T > T; 
212 
val prm_name = ak_name ^ "_prm_" ^ ak_name; 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

213 
val prm = Free (prm_name, prmT); 
18068  214 
val x = Free ("x", HOLogic.mk_prodT (T, T)); 
215 
val xs = Free ("xs", mk_permT T); 

216 
val a = Free ("a", T) ; 

217 

218 
val cnil = Const ("List.list.Nil", mk_permT T); 

219 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

220 
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a)); 
18068  221 

222 
val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

223 
(prm $ mk_Cons x xs $ a, 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

224 
Const (swap_name, swapT) $ x $ (prm $ xs $ a))); 
18068  225 
in 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

226 
thy' > 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

227 
Primrec.add_primrec_global 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

228 
[(Binding.name prm_name, SOME prmT, NoSyn)] 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

229 
[(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] > 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

230 
Sign.parent_path 
20179  231 
end) ak_names_types thy3; 
18068  232 

233 
(* defines permutation functions for all combinations of atomkinds; *) 

234 
(* there are a trivial cases and nontrivial cases *) 

235 
(* nontrivial case: *) 

236 
(* <ak>_prm_<ak>_def: perm pi a == <ak>_prm_<ak> pi a *) 

237 
(* trivial case with <ak> != <ak'> *) 

238 
(* <ak>_prm<ak'>_def[simp]: perm pi a == a *) 

239 
(* *) 

240 
(* the trivial cases are added to the simplifier, while the non *) 

241 
(* have their own rules proved below *) 

18366  242 
val (perm_defs, thy5) = fold_map (fn (ak_name, T) => fn thy => 
243 
fold_map (fn (ak_name', T') => fn thy' => 

18068  244 
let 
245 
val perm_def_name = ak_name ^ "_prm_" ^ ak_name'; 

246 
val pi = Free ("pi", mk_permT T); 

247 
val a = Free ("a", T'); 

19494  248 
val cperm = Const ("Nominal.perm", mk_permT T > T' > T'); 
41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

249 
val thy'' = Sign.add_path "rec" thy' 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

250 
val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T > T' > T'); 
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

251 
val thy''' = Sign.parent_path thy''; 
18068  252 

253 
val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def"; 

254 
val def = Logic.mk_equals 

255 
(cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a) 

256 
in 

41562
90fb3d7474df
Finally removed old primrec package, since Primrec.add_primrec_global
berghofe
parents:
41163
diff
changeset

257 
Global_Theory.add_defs_unchecked true [((Binding.name name, def), [])] thy''' 
18366  258 
end) ak_names_types thy) ak_names_types thy4; 
18068  259 

260 
(* proves that every atomkind is an instance of at *) 

261 
(* lemma at_<ak>_inst: *) 

262 
(* at TYPE(<ak>) *) 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

263 
val (prm_cons_thms,thy6) = 
29585  264 
thy5 > add_thms_string (map (fn (ak_name, T) => 
18068  265 
let 
28965  266 
val ak_name_qu = Sign.full_bname thy5 (ak_name); 
18068  267 
val i_type = Type(ak_name_qu,[]); 
26337  268 
val cat = Const ("Nominal.at",(Term.itselfT i_type) > HOLogic.boolT); 
18068  269 
val at_type = Logic.mk_type i_type; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

270 
val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy5) 
26337  271 
["at_def", 
272 
ak_name ^ "_prm_" ^ ak_name ^ "_def", 

273 
ak_name ^ "_prm_" ^ ak_name ^ ".simps", 

274 
"swap_" ^ ak_name ^ "_def", 

275 
"swap_" ^ ak_name ^ ".simps", 

276 
ak_name ^ "_infinite"] 

277 

278 
val name = "at_"^ak_name^ "_inst"; 

18068  279 
val statement = HOLogic.mk_Trueprop (cat $ at_type); 
280 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

281 
val proof = fn _ => simp_tac simp_s 1 
18068  282 

283 
in 

20046  284 
((name, Goal.prove_global thy5 [] [] statement proof), []) 
18068  285 
end) ak_names_types); 
286 

287 
(* declares a permaxclass for every atomkind *) 

288 
(* axclass pt_<ak> *) 

289 
(* pt_<ak>1[simp]: perm [] x = x *) 

290 
(* pt_<ak>2: perm (pi1@pi2) x = perm pi1 (perm pi2 x) *) 

291 
(* pt_<ak>3: pi1 ~ pi2 ==> perm pi1 x = perm pi2 x *) 

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

292 
val (pt_ax_classes,thy7) = fold_map (fn (ak_name, T) => fn thy => 
18068  293 
let 
26337  294 
val cl_name = "pt_"^ak_name; 
18068  295 
val ty = TFree("'a",["HOL.type"]); 
296 
val x = Free ("x", ty); 

297 
val pi1 = Free ("pi1", mk_permT T); 

298 
val pi2 = Free ("pi2", mk_permT T); 

19494  299 
val cperm = Const ("Nominal.perm", mk_permT T > ty > ty); 
18068  300 
val cnil = Const ("List.list.Nil", mk_permT T); 
23029  301 
val cappend = Const ("List.append",mk_permT T > mk_permT T > mk_permT T); 
19494  302 
val cprm_eq = Const ("Nominal.prm_eq",mk_permT T > mk_permT T > HOLogic.boolT); 
18068  303 
(* nil axiom *) 
304 
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

305 
(cperm $ cnil $ x, x)); 

306 
(* append axiom *) 

307 
val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq 

308 
(cperm $ (cappend $ pi1 $ pi2) $ x, cperm $ pi1 $ (cperm $ pi2 $ x))); 

309 
(* permeq axiom *) 

310 
val axiom3 = Logic.mk_implies 

311 
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2), 

312 
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x))); 

313 
in 

30345  314 
AxClass.define_class (Binding.name cl_name, ["HOL.type"]) [] 
28965  315 
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]), 
316 
((Binding.name (cl_name ^ "2"), []), [axiom2]), 

317 
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy 

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

318 
end) ak_names_types thy6; 
18068  319 

320 
(* proves that every pt_<ak>type together with <ak>type *) 

321 
(* instance of pt *) 

322 
(* lemma pt_<ak>_inst: *) 

323 
(* pt TYPE('x::pt_<ak>) TYPE(<ak>) *) 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

324 
val (prm_inst_thms,thy8) = 
29585  325 
thy7 > add_thms_string (map (fn (ak_name, T) => 
18068  326 
let 
28965  327 
val ak_name_qu = Sign.full_bname thy7 ak_name; 
328 
val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name); 

18068  329 
val i_type1 = TFree("'x",[pt_name_qu]); 
330 
val i_type2 = Type(ak_name_qu,[]); 

26337  331 
val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
18068  332 
val pt_type = Logic.mk_type i_type1; 
333 
val at_type = Logic.mk_type i_type2; 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

334 
val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy7) 
26337  335 
["pt_def", 
336 
"pt_" ^ ak_name ^ "1", 

337 
"pt_" ^ ak_name ^ "2", 

338 
"pt_" ^ ak_name ^ "3"]; 

18068  339 

26337  340 
val name = "pt_"^ak_name^ "_inst"; 
18068  341 
val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type); 
342 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

343 
val proof = fn _ => simp_tac simp_s 1; 
18068  344 
in 
20046  345 
((name, Goal.prove_global thy7 [] [] statement proof), []) 
18068  346 
end) ak_names_types); 
347 

348 
(* declares an fsaxclass for every atomkind *) 

349 
(* axclass fs_<ak> *) 

350 
(* fs_<ak>1: finite ((supp x)::<ak> set) *) 

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

351 
val (fs_ax_classes,thy11) = fold_map (fn (ak_name, T) => fn thy => 
18068  352 
let 
26337  353 
val cl_name = "fs_"^ak_name; 
28965  354 
val pt_name = Sign.full_bname thy ("pt_"^ak_name); 
18068  355 
val ty = TFree("'a",["HOL.type"]); 
356 
val x = Free ("x", ty); 

19494  357 
val csupp = Const ("Nominal.supp", ty > HOLogic.mk_setT T); 
22274  358 
val cfinite = Const ("Finite_Set.finite", HOLogic.mk_setT T > HOLogic.boolT) 
18068  359 

22274  360 
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x)); 
18068  361 

362 
in 

30345  363 
AxClass.define_class (Binding.name cl_name, [pt_name]) [] 
364 
[((Binding.name (cl_name ^ "1"), []), [axiom1])] thy 

18438
b8d867177916
made the changes according to Florian's rearranging of
urbanc
parents:
18437
diff
changeset

365 
end) ak_names_types thy8; 
26337  366 

18068  367 
(* proves that every fs_<ak>type together with <ak>type *) 
368 
(* instance of fstype *) 

369 
(* lemma abst_<ak>_inst: *) 

370 
(* fs TYPE('x::pt_<ak>) TYPE (<ak>) *) 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

371 
val (fs_inst_thms,thy12) = 
29585  372 
thy11 > add_thms_string (map (fn (ak_name, T) => 
18068  373 
let 
28965  374 
val ak_name_qu = Sign.full_bname thy11 ak_name; 
375 
val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name); 

18068  376 
val i_type1 = TFree("'x",[fs_name_qu]); 
377 
val i_type2 = Type(ak_name_qu,[]); 

26337  378 
val cfs = Const ("Nominal.fs", 
18068  379 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
380 
val fs_type = Logic.mk_type i_type1; 

381 
val at_type = Logic.mk_type i_type2; 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

382 
val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy11) 
26337  383 
["fs_def", 
384 
"fs_" ^ ak_name ^ "1"]; 

18068  385 

26337  386 
val name = "fs_"^ak_name^ "_inst"; 
18068  387 
val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type); 
388 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

389 
val proof = fn _ => simp_tac simp_s 1; 
18068  390 
in 
20046  391 
((name, Goal.prove_global thy11 [] [] statement proof), []) 
18068  392 
end) ak_names_types); 
393 

394 
(* declares for every atomkind combination an axclass *) 

395 
(* cp_<ak1>_<ak2> giving a composition property *) 

396 
(* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x) *) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

397 
val (cp_ax_classes,thy12b) = fold_map (fn (ak_name, T) => fn thy => 
26337  398 
fold_map (fn (ak_name', T') => fn thy' => 
399 
let 

400 
val cl_name = "cp_"^ak_name^"_"^ak_name'; 

401 
val ty = TFree("'a",["HOL.type"]); 

18068  402 
val x = Free ("x", ty); 
403 
val pi1 = Free ("pi1", mk_permT T); 

26337  404 
val pi2 = Free ("pi2", mk_permT T'); 
405 
val cperm1 = Const ("Nominal.perm", mk_permT T > ty > ty); 

19494  406 
val cperm2 = Const ("Nominal.perm", mk_permT T' > ty > ty); 
407 
val cperm3 = Const ("Nominal.perm", mk_permT T > mk_permT T' > mk_permT T'); 

18068  408 

409 
val ax1 = HOLogic.mk_Trueprop 

26337  410 
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
18068  411 
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x))); 
26337  412 
in 
30345  413 
AxClass.define_class (Binding.name cl_name, ["HOL.type"]) [] 
28965  414 
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy' 
26337  415 
end) ak_names_types thy) ak_names_types thy12; 
18068  416 

417 
(* proves for every <ak>combination a cp_<ak1>_<ak2>_inst theorem; *) 

418 
(* lemma cp_<ak1>_<ak2>_inst: *) 

419 
(* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>) *) 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

420 
val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy => 
26337  421 
fold_map (fn (ak_name', T') => fn thy' => 
18068  422 
let 
28965  423 
val ak_name_qu = Sign.full_bname thy' (ak_name); 
424 
val ak_name_qu' = Sign.full_bname thy' (ak_name'); 

425 
val cp_name_qu = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); 

18068  426 
val i_type0 = TFree("'a",[cp_name_qu]); 
427 
val i_type1 = Type(ak_name_qu,[]); 

428 
val i_type2 = Type(ak_name_qu',[]); 

26337  429 
val ccp = Const ("Nominal.cp", 
18068  430 
(Term.itselfT i_type0)>(Term.itselfT i_type1)> 
431 
(Term.itselfT i_type2)>HOLogic.boolT); 

432 
val at_type = Logic.mk_type i_type1; 

433 
val at_type' = Logic.mk_type i_type2; 

26337  434 
val cp_type = Logic.mk_type i_type0; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

435 
val simp_s = HOL_basic_ss addsimps maps (Global_Theory.get_thms thy') ["cp_def"]; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

436 
val cp1 = Global_Theory.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1"); 
18068  437 

26337  438 
val name = "cp_"^ak_name^ "_"^ak_name'^"_inst"; 
18068  439 
val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type'); 
440 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

441 
val proof = fn _ => EVERY [simp_tac simp_s 1, 
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

442 
rtac allI 1, rtac allI 1, rtac allI 1, 
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

443 
rtac cp1 1]; 
26337  444 
in 
29585  445 
yield_singleton add_thms_string ((name, 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

446 
Goal.prove_global thy' [] [] statement proof), []) thy' 
26337  447 
end) 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

448 
ak_names_types thy) ak_names_types thy12b; 
18068  449 

450 
(* proves for every nontrivial <ak>combination a disjointness *) 

451 
(* theorem; i.e. <ak1> != <ak2> *) 

452 
(* lemma ds_<ak1>_<ak2>: *) 

453 
(* dj TYPE(<ak1>) TYPE(<ak2>) *) 

18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

454 
val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy => 
26337  455 
fold_map (fn (ak_name',T') => fn thy' => 
18068  456 
(if not (ak_name = ak_name') 
457 
then 

26337  458 
let 
28965  459 
val ak_name_qu = Sign.full_bname thy' ak_name; 
460 
val ak_name_qu' = Sign.full_bname thy' ak_name'; 

18068  461 
val i_type1 = Type(ak_name_qu,[]); 
462 
val i_type2 = Type(ak_name_qu',[]); 

26337  463 
val cdj = Const ("Nominal.disjoint", 
18068  464 
(Term.itselfT i_type1)>(Term.itselfT i_type2)>HOLogic.boolT); 
465 
val at_type = Logic.mk_type i_type1; 

466 
val at_type' = Logic.mk_type i_type2; 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

467 
val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy') 
26337  468 
["disjoint_def", 
469 
ak_name ^ "_prm_" ^ ak_name' ^ "_def", 

470 
ak_name' ^ "_prm_" ^ ak_name ^ "_def"]; 

18068  471 

26337  472 
val name = "dj_"^ak_name^"_"^ak_name'; 
18068  473 
val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type'); 
474 

24527
888d56a8d9d3
modified proofs so that they are not using claset()
urbanc
parents:
24218
diff
changeset

475 
val proof = fn _ => simp_tac simp_s 1; 
26337  476 
in 
29585  477 
add_thms_string [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' 
26337  478 
end 
18068  479 
else 
18381
246807ef6dfb
changed the types in accordance with Florian's changes
urbanc
parents:
18366
diff
changeset

480 
([],thy'))) (* do nothing branch, if ak_name = ak_name' *) 
26337  481 
ak_names_types thy) ak_names_types thy12c; 
18068  482 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

483 
(******** pt_<ak> class instances ********) 
18068  484 
(*=========================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

485 
(* some abbreviations for theorems *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

486 
val pt1 = @{thm "pt1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

487 
val pt2 = @{thm "pt2"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

488 
val pt3 = @{thm "pt3"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

489 
val at_pt_inst = @{thm "at_pt_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

490 
val pt_unit_inst = @{thm "pt_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

491 
val pt_prod_inst = @{thm "pt_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

492 
val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

493 
val pt_list_inst = @{thm "pt_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

494 
val pt_optn_inst = @{thm "pt_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

495 
val pt_noptn_inst = @{thm "pt_noption_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

496 
val pt_fun_inst = @{thm "pt_fun_inst"}; 
45979  497 
val pt_set_inst = @{thm "pt_set_inst"}; 
18068  498 

18435  499 
(* for all atomkind combinations <ak>/<ak'> show that *) 
500 
(* every <ak> is an instance of pt_<ak'>; the proof for *) 

501 
(* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *) 

18431  502 
val thy13 = fold (fn ak_name => fn thy => 
26337  503 
fold (fn ak_name' => fn thy' => 
18431  504 
let 
28965  505 
val qu_name = Sign.full_bname thy' ak_name'; 
506 
val cls_name = Sign.full_bname thy' ("pt_"^ak_name); 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

507 
val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); 
18431  508 

24218  509 
val proof1 = EVERY [Class.intro_classes_tac [], 
18068  510 
rtac ((at_inst RS at_pt_inst) RS pt1) 1, 
511 
rtac ((at_inst RS at_pt_inst) RS pt2) 1, 

512 
rtac ((at_inst RS at_pt_inst) RS pt3) 1, 

513 
atac 1]; 

18431  514 
val simp_s = HOL_basic_ss addsimps 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

515 
maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]; 
24218  516 
val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; 
18431  517 

518 
in 

519 
thy' 

19275  520 
> AxClass.prove_arity (qu_name,[],[cls_name]) 
18431  521 
(if ak_name = ak_name' then proof1 else proof2) 
26484  522 
end) ak_names thy) ak_names thy12d; 
18068  523 

18430  524 
(* show that *) 
525 
(* fun(pt_<ak>,pt_<ak>) *) 

18579
002d371401f5
changed the name of the type "nOption" to "noption".
urbanc
parents:
18438
diff
changeset

526 
(* noption(pt_<ak>) *) 
18430  527 
(* option(pt_<ak>) *) 
528 
(* list(pt_<ak>) *) 

529 
(* *(pt_<ak>,pt_<ak>) *) 

18600  530 
(* nprod(pt_<ak>,pt_<ak>) *) 
18430  531 
(* unit *) 
532 
(* set(pt_<ak>) *) 

533 
(* are instances of pt_<ak> *) 

18431  534 
val thy18 = fold (fn ak_name => fn thy => 
18068  535 
let 
28965  536 
val cls_name = Sign.full_bname thy ("pt_"^ak_name); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

537 
val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

538 
val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

539 

18430  540 
fun pt_proof thm = 
24218  541 
EVERY [Class.intro_classes_tac [], 
18430  542 
rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; 
543 

544 
val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); 

45979  545 
val pt_thm_set = at_thm RS (pt_inst RS pt_set_inst); 
18430  546 
val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
547 
val pt_thm_optn = pt_inst RS pt_optn_inst; 

548 
val pt_thm_list = pt_inst RS pt_list_inst; 

549 
val pt_thm_prod = pt_inst RS (pt_inst RS pt_prod_inst); 

18600  550 
val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst); 
18430  551 
val pt_thm_unit = pt_unit_inst; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

552 
in 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

553 
thy 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

554 
> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) 
45979  555 
> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set) 
19494  556 
> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
30086
diff
changeset

557 
> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) 
19275  558 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

559 
> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) 
19494  560 
> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
18600  561 
(pt_proof pt_thm_nprod) 
19275  562 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) 
18430  563 
end) ak_names thy13; 
18068  564 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

565 
(******** fs_<ak> class instances ********) 
18068  566 
(*=========================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

567 
(* abbreviations for some lemmas *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

568 
val fs1 = @{thm "fs1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

569 
val fs_at_inst = @{thm "fs_at_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

570 
val fs_unit_inst = @{thm "fs_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

571 
val fs_prod_inst = @{thm "fs_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

572 
val fs_nprod_inst = @{thm "fs_nprod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

573 
val fs_list_inst = @{thm "fs_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

574 
val fs_option_inst = @{thm "fs_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

575 
val dj_supp = @{thm "dj_supp"}; 
18068  576 

577 
(* shows that <ak> is an instance of fs_<ak> *) 

578 
(* uses the theorem at_<ak>_inst *) 

18431  579 
val thy20 = fold (fn ak_name => fn thy => 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

580 
fold (fn ak_name' => fn thy' => 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

581 
let 
28965  582 
val qu_name = Sign.full_bname thy' ak_name'; 
583 
val qu_class = Sign.full_bname thy' ("fs_"^ak_name); 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

584 
val proof = 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

585 
(if ak_name = ak_name' 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

586 
then 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

587 
let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); 
24218  588 
in EVERY [Class.intro_classes_tac [], 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

589 
rtac ((at_thm RS fs_at_inst) RS fs1) 1] end 
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

590 
else 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

591 
let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); 
22274  592 
val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; 
24218  593 
in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

594 
in 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

595 
AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' 
18437
ee0283e5dfe3
added proofs to show that every atomkind combination
urbanc
parents:
18436
diff
changeset

596 
end) ak_names thy) ak_names thy18; 
18068  597 

18431  598 
(* shows that *) 
599 
(* unit *) 

600 
(* *(fs_<ak>,fs_<ak>) *) 

18600  601 
(* nprod(fs_<ak>,fs_<ak>) *) 
18431  602 
(* list(fs_<ak>) *) 
603 
(* option(fs_<ak>) *) 

604 
(* are instances of fs_<ak> *) 

18068  605 

18431  606 
val thy24 = fold (fn ak_name => fn thy => 
607 
let 

28965  608 
val cls_name = Sign.full_bname thy ("fs_"^ak_name); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

609 
val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); 
24218  610 
fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; 
18068  611 

18600  612 
val fs_thm_unit = fs_unit_inst; 
613 
val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); 

614 
val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); 

615 
val fs_thm_list = fs_inst RS fs_list_inst; 

616 
val fs_thm_optn = fs_inst RS fs_option_inst; 

18431  617 
in 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

618 
thy 
19275  619 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

620 
> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
19494  621 
> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
18600  622 
(fs_proof fs_thm_nprod) 
19275  623 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) 
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
30086
diff
changeset

624 
> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

625 
end) ak_names thy20; 
18431  626 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

627 
(******** cp_<ak>_<ai> class instances ********) 
18068  628 
(*==============================================*) 
18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

629 
(* abbreviations for some lemmas *) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

630 
val cp1 = @{thm "cp1"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

631 
val cp_unit_inst = @{thm "cp_unit_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

632 
val cp_bool_inst = @{thm "cp_bool_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

633 
val cp_prod_inst = @{thm "cp_prod_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

634 
val cp_list_inst = @{thm "cp_list_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

635 
val cp_fun_inst = @{thm "cp_fun_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

636 
val cp_option_inst = @{thm "cp_option_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

637 
val cp_noption_inst = @{thm "cp_noption_inst"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

638 
val pt_perm_compose = @{thm "pt_perm_compose"}; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

639 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

640 
val dj_pp_forget = @{thm "dj_perm_perm_forget"}; 
18068  641 

642 
(* shows that <aj> is an instance of cp_<ak>_<ai> *) 

18432  643 
(* for every <ak>/<ai>combination *) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

644 
val thy25 = fold (fn ak_name => fn thy => 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

645 
fold (fn ak_name' => fn thy' => 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

646 
fold (fn ak_name'' => fn thy'' => 
18068  647 
let 
28965  648 
val name = Sign.full_bname thy'' ak_name; 
649 
val cls_name = Sign.full_bname thy'' ("cp_"^ak_name'^"_"^ak_name''); 

18068  650 
val proof = 
651 
(if (ak_name'=ak_name'') then 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

652 
(let 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

653 
val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst"); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

654 
val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

655 
in 
26337  656 
EVERY [Class.intro_classes_tac [], 
18068  657 
rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] 
658 
end) 

26337  659 
else 
660 
(let 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

661 
val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); 
26337  662 
val simp_s = HOL_basic_ss addsimps 
18068  663 
((dj_inst RS dj_pp_forget):: 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

664 
(maps (Global_Theory.get_thms thy'') 
26337  665 
[ak_name' ^"_prm_"^ak_name^"_def", 
666 
ak_name''^"_prm_"^ak_name^"_def"])); 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

667 
in 
24218  668 
EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] 
18068  669 
end)) 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

670 
in 
19275  671 
AxClass.prove_arity (name,[],[cls_name]) proof thy'' 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

672 
end) ak_names thy') ak_names thy) ak_names thy24; 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

673 

18432  674 
(* shows that *) 
675 
(* units *) 

676 
(* products *) 

677 
(* lists *) 

678 
(* functions *) 

679 
(* options *) 

680 
(* noptions *) 

22536
35debf264656
made the type sets instance of the "cp" typeclass
urbanc
parents:
22535
diff
changeset

681 
(* sets *) 
18432  682 
(* are instances of cp_<ak>_<ai> for every <ak>/<ai>combination *) 
683 
val thy26 = fold (fn ak_name => fn thy => 

26337  684 
fold (fn ak_name' => fn thy' => 
18432  685 
let 
28965  686 
val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

687 
val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

688 
val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

689 
val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); 
18432  690 

24218  691 
fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; 
26337  692 

18432  693 
val cp_thm_unit = cp_unit_inst; 
694 
val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); 

695 
val cp_thm_list = cp_inst RS cp_list_inst; 

696 
val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst))); 

697 
val cp_thm_optn = cp_inst RS cp_option_inst; 

698 
val cp_thm_noptn = cp_inst RS cp_noption_inst; 

699 
in 

700 
thy' 

19275  701 
> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

702 
> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) 
19275  703 
> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) 
704 
> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) 

30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
30086
diff
changeset

705 
> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) 
19494  706 
> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) 
18432  707 
end) ak_names thy) ak_names thy25; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

708 

be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

709 
(* show that discrete nominal types are permutation types, finitely *) 
18432  710 
(* supported and have the commutation property *) 
711 
(* discrete types have a permutation operation defined as pi o x = x; *) 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

712 
(* which renders the proofs to be simple "simp_all"proofs. *) 
18432  713 
val thy32 = 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

714 
let 
26337  715 
fun discrete_pt_inst discrete_ty defn = 
716 
fold (fn ak_name => fn thy => 

717 
let 

28965  718 
val qu_class = Sign.full_bname thy ("pt_"^ak_name); 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

719 
val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn]; 
24218  720 
val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

721 
in 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

722 
AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy 
18432  723 
end) ak_names; 
18068  724 

18432  725 
fun discrete_fs_inst discrete_ty defn = 
26337  726 
fold (fn ak_name => fn thy => 
727 
let 

28965  728 
val qu_class = Sign.full_bname thy ("fs_"^ak_name); 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

729 
val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

730 
val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn]; 
24218  731 
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

732 
in 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

733 
AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

734 
end) ak_names; 
18068  735 

18432  736 
fun discrete_cp_inst discrete_ty defn = 
26337  737 
fold (fn ak_name' => (fold (fn ak_name => fn thy => 
738 
let 

28965  739 
val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name'); 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

740 
val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

741 
val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn]; 
24218  742 
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

743 
in 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

744 
AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

745 
end) ak_names)) ak_names; 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

746 

18432  747 
in 
748 
thy26 

44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

749 
> discrete_pt_inst @{type_name nat} @{thm perm_nat_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

750 
> discrete_fs_inst @{type_name nat} @{thm perm_nat_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

751 
> discrete_cp_inst @{type_name nat} @{thm perm_nat_def} 
44689  752 
> discrete_pt_inst @{type_name bool} @{thm perm_bool_def} 
753 
> discrete_fs_inst @{type_name bool} @{thm perm_bool_def} 

754 
> discrete_cp_inst @{type_name bool} @{thm perm_bool_def} 

44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

755 
> discrete_pt_inst @{type_name int} @{thm perm_int_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

756 
> discrete_fs_inst @{type_name int} @{thm perm_int_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

757 
> discrete_cp_inst @{type_name int} @{thm perm_int_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

758 
> discrete_pt_inst @{type_name char} @{thm perm_char_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

759 
> discrete_fs_inst @{type_name char} @{thm perm_char_def} 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
41562
diff
changeset

760 
> discrete_cp_inst @{type_name char} @{thm perm_char_def} 
18432  761 
end; 
762 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

763 

18262  764 
(* abbreviations for some lemmas *) 
765 
(*===============================*) 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

766 
val abs_fun_pi = @{thm "Nominal.abs_fun_pi"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

767 
val abs_fun_pi_ineq = @{thm "Nominal.abs_fun_pi_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

768 
val abs_fun_eq = @{thm "Nominal.abs_fun_eq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

769 
val abs_fun_eq' = @{thm "Nominal.abs_fun_eq'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

770 
val abs_fun_fresh = @{thm "Nominal.abs_fun_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

771 
val abs_fun_fresh' = @{thm "Nominal.abs_fun_fresh'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

772 
val dj_perm_forget = @{thm "Nominal.dj_perm_forget"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

773 
val dj_pp_forget = @{thm "Nominal.dj_perm_perm_forget"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

774 
val fresh_iff = @{thm "Nominal.fresh_abs_fun_iff"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

775 
val fresh_iff_ineq = @{thm "Nominal.fresh_abs_fun_iff_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

776 
val abs_fun_supp = @{thm "Nominal.abs_fun_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

777 
val abs_fun_supp_ineq = @{thm "Nominal.abs_fun_supp_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

778 
val pt_swap_bij = @{thm "Nominal.pt_swap_bij"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

779 
val pt_swap_bij' = @{thm "Nominal.pt_swap_bij'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

780 
val pt_fresh_fresh = @{thm "Nominal.pt_fresh_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

781 
val pt_bij = @{thm "Nominal.pt_bij"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

782 
val pt_perm_compose = @{thm "Nominal.pt_perm_compose"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

783 
val pt_perm_compose' = @{thm "Nominal.pt_perm_compose'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

784 
val perm_app = @{thm "Nominal.pt_fun_app_eq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

785 
val at_fresh = @{thm "Nominal.at_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

786 
val at_fresh_ineq = @{thm "Nominal.at_fresh_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

787 
val at_calc = @{thms "Nominal.at_calc"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

788 
val at_swap_simps = @{thms "Nominal.at_swap_simps"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

789 
val at_supp = @{thm "Nominal.at_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

790 
val dj_supp = @{thm "Nominal.dj_supp"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

791 
val fresh_left_ineq = @{thm "Nominal.pt_fresh_left_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

792 
val fresh_left = @{thm "Nominal.pt_fresh_left"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

793 
val fresh_right_ineq = @{thm "Nominal.pt_fresh_right_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

794 
val fresh_right = @{thm "Nominal.pt_fresh_right"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

795 
val fresh_bij_ineq = @{thm "Nominal.pt_fresh_bij_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

796 
val fresh_bij = @{thm "Nominal.pt_fresh_bij"}; 
26773  797 
val fresh_star_bij_ineq = @{thms "Nominal.pt_fresh_star_bij_ineq"}; 
798 
val fresh_star_bij = @{thms "Nominal.pt_fresh_star_bij"}; 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

799 
val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

800 
val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"}; 
30086  801 
val fresh_star_eqvt = @{thms "Nominal.pt_fresh_star_eqvt"}; 
802 
val fresh_star_eqvt_ineq= @{thms "Nominal.pt_fresh_star_eqvt_ineq"}; 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

803 
val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

804 
val in_eqvt = @{thm "Nominal.pt_in_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

805 
val eq_eqvt = @{thm "Nominal.pt_eq_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

806 
val all_eqvt = @{thm "Nominal.pt_all_eqvt"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

807 
val ex_eqvt = @{thm "Nominal.pt_ex_eqvt"}; 
28011  808 
val ex1_eqvt = @{thm "Nominal.pt_ex1_eqvt"}; 
809 
val the_eqvt = @{thm "Nominal.pt_the_eqvt"}; 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

810 
val pt_pi_rev = @{thm "Nominal.pt_pi_rev"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

811 
val pt_rev_pi = @{thm "Nominal.pt_rev_pi"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

812 
val at_exists_fresh = @{thm "Nominal.at_exists_fresh"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

813 
val at_exists_fresh' = @{thm "Nominal.at_exists_fresh'"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

814 
val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"}; 
26337  815 
val fresh_perm_app = @{thm "Nominal.pt_fresh_perm_app"}; 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

816 
val fresh_aux = @{thm "Nominal.pt_fresh_aux"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

817 
val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"}; 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23158
diff
changeset

818 
val pt_perm_supp = @{thm "Nominal.pt_perm_supp"}; 
26090  819 
val subseteq_eqvt = @{thm "Nominal.pt_subseteq_eqvt"}; 
29128
4c243e6a71b2
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
Christian Urban <urbanc@in.tum.de>
parents:
28965
diff
changeset

820 
val insert_eqvt = @{thm "Nominal.pt_insert_eqvt"}; 
4c243e6a71b2
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
Christian Urban <urbanc@in.tum.de>
parents:
28965
diff
changeset

821 
val set_eqvt = @{thm "Nominal.pt_set_eqvt"}; 
26820  822 
val perm_set_eq = @{thm "Nominal.perm_set_eq"}; 
22786  823 

18262  824 
(* Now we collect and instantiate some lemmas w.r.t. all atom *) 
825 
(* types; this allows for example to use abs_perm (which is a *) 

826 
(* collection of theorems) instead of thm abs_fun_pi with explicit *) 

827 
(* instantiations. *) 

20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

828 
val (_, thy33) = 
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

829 
let 
18651
0cb5a8f501aa
added the thmscollection "pt_id" (collection of all pt_<ak>1 lemmas)
urbanc
parents:
18626
diff
changeset

830 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

831 
(* takes a theorem thm and a list of theorems [t1,..,tn] *) 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

832 
(* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
18262  833 
fun instR thm thms = map (fn ti => ti RS thm) thms; 
18068  834 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

835 
(* takes a theorem thm and a list of theorems [(t1,m1),..,(tn,mn)] *) 
26773  836 
(* produces a list of theorems of the form [[t1,m1] MRS thm,..,[tn,mn] MRS thm] *) 
837 
fun instRR thm thms = map (fn (ti,mi) => [ti,mi] MRS thm) thms; 

838 

18262  839 
(* takes two theorem lists (hopefully of the same length ;o) *) 
840 
(* produces a list of theorems of the form *) 

841 
(* [t1 RS m1,..,tn RS mn] where [t1,..,tn] is thms1 and [m1,..,mn] is thms2 *) 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

842 
fun inst_zip thms1 thms2 = map (fn (t1,t2) => t1 RS t2) (thms1 ~~ thms2); 
18068  843 

18262  844 
(* takes a theorem list of the form [l1,...,ln] *) 
845 
(* and a list of theorem lists of the form *) 

846 
(* [[h11,...,h1m],....,[hk1,....,hkm] *) 

847 
(* produces the list of theorem lists *) 

848 
(* [[l1 RS h11,...,l1 RS h1m],...,[ln RS hk1,...,ln RS hkm]] *) 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

849 
fun inst_mult thms thmss = map (fn (t,ts) => instR t ts) (thms ~~ thmss); 
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

850 

f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

851 
(* FIXME: these lists do not need to be created dynamically again *) 
18262  852 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

853 

18068  854 
(* list of all at_insttheorems *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

855 
val ats = map (fn ak => Global_Theory.get_thm thy32 ("at_"^ak^"_inst")) ak_names 
18068  856 
(* list of all pt_insttheorems *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

857 
val pts = map (fn ak => Global_Theory.get_thm thy32 ("pt_"^ak^"_inst")) ak_names 
18262  858 
(* list of all cp_insttheorems as a collection of lists*) 
18068  859 
val cps = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

860 
let fun cps_fun ak1 ak2 = Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst") 
26337  861 
in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
18262  862 
(* list of all cp_insttheorems that have different atom types *) 
863 
val cps' = 

26337  864 
let fun cps'_fun ak1 ak2 = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

865 
if ak1=ak2 then NONE else SOME (Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")) 
32952  866 
in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end; 
18068  867 
(* list of all dj_insttheorems *) 
868 
val djs = 

26337  869 
let fun djs_fun ak1 ak2 = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

870 
if ak1=ak2 then NONE else SOME(Global_Theory.get_thm thy32 ("dj_"^ak2^"_"^ak1)) 
26337  871 
in map_filter I (map_product djs_fun ak_names ak_names) end; 
18262  872 
(* list of all fs_insttheorems *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

873 
val fss = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"_inst")) ak_names 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

874 
(* list of all at_insttheorems *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

875 
val fs_axs = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"1")) ak_names 
20097
be2d96bbf39c
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
webertj
parents:
20046
diff
changeset

876 

25538  877 
fun inst_pt thms = maps (fn ti => instR ti pts) thms; 
878 
fun inst_at thms = maps (fn ti => instR ti ats) thms; 

879 
fun inst_fs thms = maps (fn ti => instR ti fss) thms; 

880 
fun inst_cp thms cps = flat (inst_mult thms cps); 

26773  881 
fun inst_pt_at thms = maps (fn ti => instRR ti (pts ~~ ats)) thms; 
25538  882 
fun inst_dj thms = maps (fn ti => instR ti djs) thms; 
26337  883 
fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; 
18262  884 
fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms)); 
26337  885 
fun inst_pt_pt_at_cp thms = 
886 
let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms)); 

18436
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

887 
val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps'; 
26337  888 
in i_pt_pt_at_cp end; 
18396
b3e7da94b51f
added a fresh_left lemma that contains all instantiation
urbanc
parents:
18381
diff
changeset

889 
fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); 
18068  890 
in 
18262  891 
thy32 
29585  892 
> add_thmss_string [(("alpha", inst_pt_at [abs_fun_eq]),[])] 
893 
>> add_thmss_string [(("alpha'", inst_pt_at [abs_fun_eq']),[])] 

894 
>> add_thmss_string [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] 

895 
>> add_thmss_string [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] 

896 
>> add_thmss_string [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] 

897 
>> add_thmss_string 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

898 
let val thms1 = inst_at at_swap_simps 
27399
1fb3d1219c12
added facts to lemma swap_simps and tuned lemma calc_atms
urbanc
parents:
27216
diff
changeset

899 
and thms2 = inst_dj [dj_perm_forget] 
1fb3d1219c12
added facts to lemma swap_simps and tuned lemma calc_atms
urbanc
parents:
27216
diff
changeset

900 
in [(("swap_simps", thms1 @ thms2),[])] end 
29585  901 
>> add_thmss_string 
26337  902 
let val thms1 = inst_pt_at [pt_pi_rev]; 
903 
val thms2 = inst_pt_at [pt_rev_pi]; 

19139  904 
in [(("perm_pi_simp",thms1 @ thms2),[])] end 
29585  905 
>> add_thmss_string [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] 
906 
>> add_thmss_string [(("perm_bij", inst_pt_at [pt_bij]),[])] 

907 
>> add_thmss_string 

26337  908 
let val thms1 = inst_pt_at [pt_perm_compose]; 
909 
val thms2 = instR cp1 (Library.flat cps'); 

18436
9649e24bc10e
added thms to perm_compose (so far only composition
urbanc
parents:
18435
diff
changeset

910 
in [(("perm_compose",thms1 @ thms2),[])] end 
29585  911 
>> add_thmss_string [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
912 
>> add_thmss_string [(("perm_app", inst_pt_at [perm_app]),[])] 

913 
>> add_thmss_string [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] 

914 
>> add_thmss_string [(("exists_fresh", inst_at [at_exists_fresh]),[])] 

915 
>> add_thmss_string [(("exists_fresh'", inst_at [at_exists_fresh']),[])] 

916 
>> add_thmss_string 

24569  917 
let 
918 
val thms1 = inst_pt_at [all_eqvt]; 

919 
val thms2 = map (fold_rule [inductive_forall_def]) thms1 

920 
in 

921 
[(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])] 

922 
end 

29585  923 
>> add_thmss_string [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])] 
924 
>> add_thmss_string [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])] 

925 
>> add_thmss_string [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])] 

926 
>> add_thmss_string 

26337  927 
let val thms1 = inst_at [at_fresh] 
928 
val thms2 = inst_dj [at_fresh_ineq] 

929 
in [(("fresh_atm", thms1 @ thms2),[])] end 

29585  930 
>> add_thmss_string 
27399
1fb3d1219c12
added facts to lemma swap_simps and tuned lemma calc_atms
urbanc
parents:
27216
diff
changeset

931 
let val thms1 = inst_at at_calc 
1fb3d1219c12
added facts to lemma swap_simps and tuned lemma calc_atms
urbanc
parents:
27216
diff
changeset

932 
and thms2 = inst_dj [dj_perm_forget] 
1fb3d1219c12
added facts to lemma swap_simps and tuned lemma calc_atms
urbanc
parents:
27216
diff
changeset

933 
in [(("calc_atm", thms1 @ thms2),[])] end 
29585  934 
>> add_thmss_string 
26337  935 
let val thms1 = inst_pt_at [abs_fun_pi] 
936 
and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] 

937 
in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 

29585  938 
>> add_thmss_string 
26337  939 
let val thms1 = inst_dj [dj_perm_forget] 
940 
and thms2 = inst_dj [dj_pp_forget] 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18262
diff
changeset

941 
in [(("perm_dj", thms1 @ thms2),[])] end 
29585  942 
>> add_thmss_string 
26337  943 
let val thms1 = inst_pt_at_fs [fresh_iff] 
18626  944 
and thms2 = inst_pt_at [fresh_iff] 
26337  945 
and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] 
946 
in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end 

29585  947 
>> add_thmss_string 
26337  948 
let val thms1 = inst_pt_at [abs_fun_supp] 
949 
and thms2 = inst_pt_at_fs [abs_fun_supp] 

950 
and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] 

951 
in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end 

29585  952 
>> add_thmss_string 
26337  953 
let val thms1 = inst_pt_at [fresh_left] 
954 
and thms2 = inst_pt_pt_at_cp [fresh_left_ineq] 

955 
in [(("fresh_left", thms1 @ thms2),[])] end 

29585  956 
>> add_thmss_string 
26337  957 
let val thms1 = inst_pt_at [fresh_right] 
958 
and thms2 = inst_pt_pt_at_cp [fresh_right_ineq] 

959 
in [(("fresh_right", thms1 @ thms2),[])] end 

29585  960 
>> add_thmss_string 
26337  961 
let val thms1 = inst_pt_at [fresh_bij] 
962 
and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] 

963 
in [(("fresh_bij", thms1 @ thms2),[])] end 

29585  964 
>> add_thmss_string 
26773  965 
let val thms1 = inst_pt_at fresh_star_bij 
30086  966 
and thms2 = maps (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq 
26773  967 
in [(("fresh_star_bij", thms1 @ thms2),[])] end 
29585  968 
>> add_thmss_string 
26337  969 
let val thms1 = inst_pt_at [fresh_eqvt] 
22535
cbee450f88a6
added extended the lemma for equivariance of freshness
urbanc
parents:
22418
diff
changeset

970 
and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] 
26337  971 
in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 
29585  972 
>> add_thmss_string 
30086  973 
let val thms1 = inst_pt_at fresh_star_eqvt 
974 
and thms2 = maps (fn ti => inst_pt_pt_at_cp_dj [ti]) fresh_star_eqvt_ineq 

975 
in [(("fresh_star_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 

976 
>> add_thmss_string 

26337  977 
let val thms1 = inst_pt_at [in_eqvt] 
978 
in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 

29585  979 
>> add_thmss_string 
26337  980 
let val thms1 = inst_pt_at [eq_eqvt] 
981 
in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 

29585  982 
>> add_thmss_string 
26337  983 
let val thms1 = inst_pt_at [set_diff_eqvt] 
984 
in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 

29585  985 
>> add_thmss_string 
26337  986 
let val thms1 = inst_pt_at [subseteq_eqvt] 
987 
in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end 

29585  988 
>> add_thmss_string [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])] 
989 
>> add_thmss_string [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])] 

990 
>> add_thmss_string [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])] 

991 
>> add_thmss_string 

26337  992 
let val thms1 = inst_pt_at [fresh_aux] 
993 
and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 

994 
in [(("fresh_aux", thms1 @ thms2),[])] end 

29585  995 
>> add_thmss_string 
26337  996 
let val thms1 = inst_pt_at [fresh_perm_app] 
997 
and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 

998 
in [(("fresh_perm_app", thms1 @ thms2),[])] end 

29585  999 
>> add_thmss_string 
26337  1000 
let val thms1 = inst_pt_at [pt_perm_supp] 
1001 
and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 

1002 
in [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end 

29585  1003 
>> add_thmss_string [(("fin_supp",fs_axs),[])] 
26337  1004 
end; 
18068  1005 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

1006 
in 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

1007 
NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

1008 
(pt_ax_classes ~~ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

1009 
fs_ax_classes ~~ 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

1010 
map (fn cls => Symtab.make (full_ak_names ~~ cls)) cp_ax_classes ~~ 
28372  1011 
prm_cons_thms ~~ prm_inst_thms ~~ 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

1012 
map (fn ths => Symtab.make (full_ak_names ~~ ths)) cp_thms ~~ 
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

1013 
map (fn thss => Symtab.make 
32952  1014 
(map_filter (fn (s, [th]) => SOME (s, th)  _ => NONE) 
28729
cfd169f1dae2
Some more functions for accessing information about atoms.
berghofe
parents:
28372
diff
changeset

1015 
(full_ak_names ~~ thss))) dj_thms))) thy33 
18068  1016 
end; 
1017 

1018 

1019 
(* syntax und parsing *) 

1020 

24867  1021 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
33522
diff
changeset

1022 
Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
33522
diff
changeset

1023 
(Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls)); 
18068  1024 

1025 
end; 