author  Christian Urban <urbanc@in.tum.de> 
Mon, 27 Apr 2009 00:29:54 +0200  
changeset 30991  c814a34f687e 
parent 30986  047fa04a9fe8 
child 32091  30e2ffbba718 
permissions  rwrr 
30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

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

2 

22846  3 
This file introduces the infrastructure for the lemma 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

4 
collection "eqvts". 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

5 

30991  6 
By attaching [eqvt] or [eqvt_force] to a lemma, it will get 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

7 
stored in a dataslot in the context. Possible modifiers 
30991  8 
are [... add] and [... del] for adding and deleting, 
9 
respectively, the lemma from the dataslot. 

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

10 
*) 
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 
signature NOMINAL_THMDECLS = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

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

15 
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

16 
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

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

18 
val setup: theory > theory 
24571  19 
val get_eqvt_thms: Proof.context > thm list 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

20 

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

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

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

23 

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

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

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

26 

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

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

28 
( 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

29 
type T = thm list 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

30 
val empty = []:T 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

31 
val extend = I 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

32 
fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2) 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

34 

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

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

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

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

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

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

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

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

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

43 
(* equalitylemma can be derived. *) 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

45 

30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

47 

30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

48 
fun tactic (msg, tac) = 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

49 
if !NOMINAL_EQVT_DEBUG 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

50 
then tac THEN' (K (print_tac ("after " ^ msg))) 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

52 

30991  53 
fun prove_eqvt_tac ctxt orig_thm pi pi' = 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

54 
let 
30991  55 
val mypi = Thm.cterm_of ctxt pi 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

56 
val T = fastype_of pi' 
30991  57 
val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T > T) $ pi') 
58 
val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp" 

30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

59 
in 
30991  60 
EVERY1 [tactic ("iffI applied", rtac @{thm iffI}), 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

61 
tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}), 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

62 
tactic ("solve with orig_thm", etac orig_thm), 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

63 
tactic ("applies orig_thm instantiated with rev pi", 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

64 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

65 
tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}), 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

66 
tactic ("getting rid of all remaining perms", 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

67 
full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))] 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

69 

30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

70 
fun get_derived_thm ctxt hyp concl orig_thm pi typi = 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

71 
let 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

72 
val thy = ProofContext.theory_of ctxt; 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

73 
val pi' = Var (pi, typi); 
30991  74 
val lhs = Const (@{const_name "perm"}, typi > HOLogic.boolT > HOLogic.boolT) $ pi' $ hyp; 
30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

75 
val ([goal_term, pi''], ctxt') = Variable.import_terms false 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

76 
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

77 
val _ = Display.print_cterm (cterm_of thy goal_term) 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

78 
in 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

79 
Goal.prove ctxt' [] [] goal_term 
30991  80 
(fn _ => prove_eqvt_tac thy orig_thm pi' pi'') > 
30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

81 
singleton (ProofContext.export ctxt' ctxt) 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

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

83 

30991  84 
(* replaces in t every variable, say x, with pi o x *) 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

85 
fun apply_pi trm (pi, typi) = 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

86 
let 
30991  87 
fun replace n ty = 
88 
let 

89 
val c = Const (@{const_name "perm"}, typi > ty > ty) 

90 
val v1 = Var (pi, typi) 

91 
val v2 = Var (n, ty) 

92 
in 

93 
c $ v1 $ v2 

94 
end 

30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

95 
in 
30991  96 
map_aterms (fn Var (n, ty) => replace n ty  t => t) trm 
97 
end 

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

98 

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

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

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

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

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

103 
(case s of 
30991  104 
(Const (@{const_name "perm"} ,typrm) $ 
105 
(Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $ 

22846  106 
(Var (n,ty))) => 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

108 
(* FIXME: this should be an operation the library *) 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

109 
val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm) 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset

110 
in 
24271  111 
if (Sign.of_sort thy (ty,[class_name])) 
22846  112 
then [(pi,typi)] 
113 
else raise 

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

115 
end 

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

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

117 
 (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 
22846  118 
 _ => []) 
119 
in 

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

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

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

122 
(* a singletonlist *) 
22846  123 
(case (distinct (op =) (get_pi_aux t)) of 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

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

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

127 

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

129 
(* lemma list depending on flag. To be added the lemma has to satisfy a *) 
22846  130 
(* 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

131 

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

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

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

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

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

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

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

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

143 
(warning ("equivariance lemma of the relational form"); 
30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

144 
[orig_thm, 
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

145 
get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi]) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

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

147 
end 
22846  148 
(* case: eqvtlemma is of the equational form *) 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

149 
 (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ 
30991  150 
(Const (@{const_name "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

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

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

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

154 
 _ => raise EQVT_FORM "Type unknown") 
22846  155 
in 
26652  156 
fold (fn thm => Data.map (flag thm)) thms_to_be_added context 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

157 
end 
22846  158 
handle EQVT_FORM s => 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

159 
error (Display.string_of_thm orig_thm ^ 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

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

161 

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

162 

30991  163 
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm)); 
164 
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm)); 

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

165 

30991  166 
val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm); 
167 
val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm); 

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

168 

30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

169 
val get_eqvt_thms = Context.Proof #> Data.get; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset

170 

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

171 
val setup = 
30986
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

172 
Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

173 
"equivariance theorem declaration" 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

174 
#> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

175 
"equivariance theorem declaration (without checking the form of the lemma)" 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

176 
#> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
047fa04a9fe8
deleted thmattributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
Christian Urban <urbanc@in.tum.de>
parents:
30528
diff
changeset

177 

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

178 

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

179 
end; 