author  wenzelm 
Tue, 14 Aug 2007 23:22:51 +0200  
changeset 24271  499608101177 
parent 24265  4d5917cc60c4 
child 24571  a6d0428dea8e 
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; 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

37 
fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

38 
freshs = Thm.merge_thms (#freshs r1, #freshs r2), 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

39 
bijs = Thm.merge_thms (#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 *) 
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

50 
(* equalitylemma 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 

24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

73 
val perm_boolE = thm "perm_boolE"; 
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

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

75 
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

76 

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

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

78 

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

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

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

83 

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

84 
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

85 

22846  86 
fun tactic_eqvt ctx orig_thm pi typi = 
87 
let 

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

88 
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

89 
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

90 
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

91 
in 
22846  92 
EVERY [tactic ("iffI applied",rtac iffI 1), 
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

93 
tactic ("remove pi with perm_boolE", 
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

94 
(dtac perm_boolE 1)), 
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

95 
tactic ("solve with orig_thm", 
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

96 
(etac orig_thm 1)), 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

97 
tactic ("applies orig_thm instantiated with rev pi", 
22846  98 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

99 
tactic ("getting rid of the pi on the right", 
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

100 
(rtac perm_boolI 1)), 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

101 
tactic ("getting rid of all remaining perms", 
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

102 
full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)] 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

104 

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

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

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

24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

110 
in 
22846  111 
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

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

113 

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

114 
(* 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

115 
(* 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

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

117 
fun update_context flag thms context = 
22846  118 
let 
119 
val context' = fold (fn thm => Data.map (flag thm)) thms context 

120 
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

121 
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

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

123 

22846  124 
(* 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

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

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

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

129 
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

130 
 _ => t) 
22846  131 
in 
132 
map_aterms only_vars trm 

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

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

134 

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

135 
(* 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

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

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

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

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

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

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

143 
let 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

144 
(* FIXME: this should be an operation the library *) 
22846  145 
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

146 
in 
24271  147 
if (Sign.of_sort thy (ty,[class_name])) 
22846  148 
then [(pi,typi)] 
149 
else raise 

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

151 
end 

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

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

153 
 (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 
22846  154 
 _ => []) 
155 
in 

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

156 
(* 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

157 
(* 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

158 
(* a singletonlist *) 
22846  159 
(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

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

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

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

163 

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

164 
(* 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

165 
(* lemma list depending on flag. To be added the lemma has to satisfy a *) 
22846  166 
(* certain form. *) 
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

167 

4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset

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

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

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

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

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

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

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

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

180 
[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

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

182 
end 
22846  183 
(* case: eqvtlemma is of the equational form *) 
184 
 (Const ("Trueprop", _) $ (Const ("op =", _) $ 

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

185 
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

186 
(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

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

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

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

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

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

194 
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

195 

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

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

198 

22846  199 
fun simple_add_del_aux record_access name flag th context = 
200 
let 

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

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

202 
in 
22846  203 
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

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

205 

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

206 
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

207 
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

208 
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

209 

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

210 
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

211 
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

212 
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

213 

24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

214 
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.add_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

215 
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Thm.del_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

216 
val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.add_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

217 
val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Thm.del_thm)); 
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 

24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

219 
val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.add_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

220 
val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Thm.del_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

221 
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Thm.add_thm)); 
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

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

223 

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

224 

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

225 

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

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

228 
[("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

229 
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del, 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

230 
"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

231 
("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

232 
("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

233 

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

234 
end; 