author  wenzelm 
Mon, 07 May 2007 00:49:59 +0200  
changeset 22846  fb79144af9a3 
parent 22715  381e6c45f13b 
child 24039  273698405054 
permissions  rwrr 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

1 
(* ID: "$Id$" 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

2 
Authors: Julien Narboux and Christian Urban 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

3 

22846  4 
This file introduces the infrastructure for the lemma 
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

5 
declaration "eqvts" "bijs" and "freshs". 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

6 

22846  7 
By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

8 
in a dataslot in the theory context. Possible modifiers 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

9 
are [attribute add] and [attribute del] for adding and deleting, 
22846  10 
respectively the lemma from the dataslot. 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

11 
*) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

12 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

13 
signature NOMINAL_THMDECLS = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

14 
sig 
22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

15 
val print_data: Proof.context > unit 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

16 
val eqvt_add: attribute 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

17 
val eqvt_del: attribute 
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

18 
val eqvt_force_add: attribute 
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

19 
val eqvt_force_del: attribute 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

20 
val setup: theory > theory 
22286  21 
val get_eqvt_thms: theory > thm list 
22 
val get_fresh_thms: theory > thm list 

23 
val get_bij_thms: theory > thm list 

22846  24 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

25 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

26 
val NOMINAL_EQVT_DEBUG : bool ref 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

27 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

28 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

29 
structure NominalThmDecls: NOMINAL_THMDECLS = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

30 
struct 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

31 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

32 
structure Data = GenericDataFun 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

33 
( 
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

34 
type T = {eqvts:thm list, freshs:thm list, bijs:thm list}; 
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

35 
val empty = ({eqvts=[], freshs=[], bijs=[]}:T); 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

36 
val extend = I; 
22846  37 
fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2), 
38 
freshs = Drule.merge_rules (#freshs r1, #freshs r2), 

22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

39 
bijs = Drule.merge_rules (#bijs r1, #bijs r2)} 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

40 
); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

41 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

42 
(* Exception for when a theorem does not conform with form of an equivariance lemma. *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

43 
(* There are two forms: one is an implication (for relations) and the other is an *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

44 
(* equality (for functions). In the implicationcase, say P ==> Q, Q must be equal *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

45 
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

46 
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

47 
(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

48 
(* the implicational case it is also checked that the variables and permutation fit *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

49 
(* together, i.e. are of the right "pt_class", so that a stronger version of the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

50 
(* eqalitylemma can be derived. *) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

51 
exception EQVT_FORM of string; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

52 

22846  53 
fun print_data ctxt = 
54 
let 

55 
val data = Data.get (Context.Proof ctxt); 

56 
fun pretty_thms msg thms = 

57 
Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms); 

58 
in 

59 
Pretty.writeln (Pretty.chunks 

60 
[pretty_thms "Equivariance lemmas:" (#eqvts data), 

61 
pretty_thms "Freshness lemmas:" (#freshs data), 

62 
pretty_thms "Bijection lemmas:" (#bijs data)]) 

63 
end; 

64 

65 

22541
c33b542394f3
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvtlemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset

66 
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts; 
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

67 
val get_fresh_thms = Context.Theory #> Data.get #> #freshs; 
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

68 
val get_bij_thms = Context.Theory #> Data.get #> #bijs; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

69 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

70 
(* FIXME: should be a function in a library *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

71 
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

72 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

73 
val perm_bool = thm "perm_bool"; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

74 
val perm_fun_def = thm "perm_fun_def"; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

75 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

76 
val NOMINAL_EQVT_DEBUG = ref false; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

77 

22846  78 
fun tactic (msg,tac) = 
79 
if !NOMINAL_EQVT_DEBUG 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

80 
then (EVERY [tac, print_tac ("after "^msg)]) 
22846  81 
else tac 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

82 

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

83 
fun dynamic_thms thy name = PureThy.get_thms thy (Name name) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

84 

22846  85 
fun tactic_eqvt ctx orig_thm pi typi = 
86 
let 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

87 
val mypi = Thm.cterm_of ctx (Var (pi,typi)) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

88 
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi > typi) $ Free (fst pi,typi)) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

89 
val perm_pi_simp = dynamic_thms ctx "perm_pi_simp" 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

90 
in 
22846  91 
EVERY [tactic ("iffI applied",rtac iffI 1), 
92 
tactic ("simplifies with orig_thm and perm_bool", 

93 
asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

94 
tactic ("applies orig_thm instantiated with rev pi", 
22846  95 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

96 
tactic ("getting rid of all remaining perms", 
22846  97 
full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

98 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

99 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

100 
fun get_derived_thm thy hyp concl orig_thm pi typi = 
22846  101 
let 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

102 
val lhs = (Const("Nominal.perm", typi > HOLogic.boolT > HOLogic.boolT) $ Var(pi,typi) $ hyp) 
22846  103 
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
104 
val _ = Display.print_cterm (cterm_of thy goal_term) 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

105 
in 
22846  106 
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

107 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

108 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

109 
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

110 
(* the eqvt_thm_list to the user, we have to manually update the context and the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

111 
(* thmlist eqvt *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

112 
fun update_context flag thms context = 
22846  113 
let 
114 
val context' = fold (fn thm => Data.map (flag thm)) thms context 

115 
in 

22541
c33b542394f3
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvtlemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset

116 
Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context' 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

117 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

118 

22846  119 
(* replaces every variable x in t with pi o x *) 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

120 
fun apply_pi trm (pi,typi) = 
22846  121 
let 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

122 
fun only_vars t = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

123 
(case t of 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

124 
Var (n,ty) => (Const ("Nominal.perm",typi > ty > ty) $ (Var (pi,typi)) $ (Var (n,ty))) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

125 
 _ => t) 
22846  126 
in 
127 
map_aterms only_vars trm 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

128 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

129 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

130 
(* returns *the* pi which is in front of all variables, provided there *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

131 
(* exists such a pi; otherwise raises EQVT_FORM *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

132 
fun get_pi t thy = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

133 
let fun get_pi_aux s = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

134 
(case s of 
22846  135 
(Const ("Nominal.perm",typrm) $ 
136 
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 

137 
(Var (n,ty))) => 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

138 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

139 
(* FIXME: this should be an operation the library *) 
22846  140 
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
141 
in 

142 
if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 

143 
then [(pi,typi)] 

144 
else raise 

145 
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) 

146 
end 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

147 
 Abs (_,_,t1) => get_pi_aux t1 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

148 
 (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 
22846  149 
 _ => []) 
150 
in 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

151 
(* collect first all pi's in front of variables in t and then use distinct *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

152 
(* to ensure that all pi's must have been the same, i.e. distinct returns *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

153 
(* a singletonlist *) 
22846  154 
(case (distinct (op =) (get_pi_aux t)) of 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

155 
[(pi,typi)] => (pi,typi) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

156 
 _ => raise EQVT_FORM "All permutation should be the same") 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

157 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

158 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

159 
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

160 
(* lemma list depending on flag. To be added the lemma has to satisfy a *) 
22846  161 
(* certain form. *) 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

162 
fun eqvt_add_del_aux flag orig_thm context = 
22846  163 
let 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

164 
val thy = Context.theory_of context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

165 
val thms_to_be_added = (case (prop_of orig_thm) of 
22846  166 
(* case: eqvtlemma is of the implicational form *) 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

167 
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => 
22846  168 
let 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

169 
val (pi,typi) = get_pi concl thy 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

170 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

171 
if (apply_pi hyp (pi,typi) = concl) 
22846  172 
then 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

173 
(warning ("equivariance lemma of the relational form"); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

174 
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

175 
else raise EQVT_FORM "Type Implication" 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

176 
end 
22846  177 
(* case: eqvtlemma is of the equational form *) 
178 
 (Const ("Trueprop", _) $ (Const ("op =", _) $ 

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

179 
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => 
22846  180 
(if (apply_pi lhs (pi,typi)) = rhs 
22437
b3526cd2a336
removes some unused code that used to try to derive a simpler version of the eqvt lemmas
narboux
parents:
22418
diff
changeset

181 
then [orig_thm] 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

182 
else raise EQVT_FORM "Type Equality") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

183 
 _ => raise EQVT_FORM "Type unknown") 
22846  184 
in 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

185 
update_context flag thms_to_be_added context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

186 
end 
22846  187 
handle EQVT_FORM s => 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

188 
error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

189 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

190 
(* in cases of bij and freshness, we just add the lemmas to the *) 
22846  191 
(* dataslot *) 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

192 

22846  193 
fun simple_add_del_aux record_access name flag th context = 
194 
let 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

195 
val context' = Data.map (flag th) context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

196 
in 
22846  197 
Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

198 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

199 

22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

200 
fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f 
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

201 
fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f 
22541
c33b542394f3
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvtlemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset

202 
fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

203 

22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

204 
fun eqvt_map f th (r:Data.T) = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r}; 
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

205 
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r}; 
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

206 
fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))}; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

207 

22846  208 
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
209 
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 

210 
val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 

211 
val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 

22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

212 

22846  213 
val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

214 
val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule)); 
22846  215 
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

216 
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

217 

22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

218 

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

219 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

220 
val setup = 
22846  221 
Attrib.add_attributes 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

222 
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"), 
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

223 
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del, 
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset

224 
"equivariance theorem declaration (without checking the form of the lemma)"), 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

225 
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

226 
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")]; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

227 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

228 
end; 