author  wenzelm 
Sat, 17 Oct 2009 14:43:18 +0200  
changeset 32960  69916a850301 
parent 32740  9dd0a2f83429 
child 33519  e31a85f92ce9 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

1 
(* Title: HOL/Nominal/nominal_thmdecls.ML 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

2 
Author: Julien Narboux, TU Muenchen 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

3 
Author: Christian Urban, TU Muenchen 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

4 

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

5 
Infrastructure for the lemma collection "eqvts". 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

6 

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

7 
By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

8 
a dataslot in the context. Possible modifiers are [... add] and 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

9 
[... del] for adding and deleting, respectively, the lemma from the 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

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

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

16 
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

17 
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

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

19 
val setup: theory > theory 
24571  20 
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

21 

32740  22 
val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

24 

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

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

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

27 

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

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

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

30 
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

31 
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

32 
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

33 
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

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

35 

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

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

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

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

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

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

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

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

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

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

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

46 

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

48 

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

49 
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

50 
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

51 
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

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

53 

30991  54 
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

55 
let 
30991  56 
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

57 
val T = fastype_of pi' 
30991  58 
val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T > T) $ pi') 
59 
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

60 
in 
30991  61 
EVERY1 [tactic ("iffI applied", rtac @{thm iffI}), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

62 
tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}), 
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

63 
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

64 
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

65 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

66 
tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}), 
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

67 
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

68 
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

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

70 

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

71 
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

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

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

74 
val pi' = Var (pi, typi); 
30991  75 
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

76 
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

77 
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32091
diff
changeset

78 
val _ = writeln (Syntax.string_of_term ctxt' goal_term); 
30088
fe6eac03b816
Replaced Logic.unvarify by Variable.import_terms to make declaration of
berghofe
parents:
29585
diff
changeset

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

80 
Goal.prove ctxt' [] [] goal_term 
30991  81 
(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

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

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

84 

30991  85 
(* 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

86 
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

87 
let 
30991  88 
fun replace n ty = 
89 
let 

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

91 
val v1 = Var (pi, typi) 

92 
val v2 = Var (n, ty) 

93 
in 

94 
c $ v1 $ v2 

95 
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

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

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

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

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

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

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

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

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

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

110 
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

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

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

116 
end 

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

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

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

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

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

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

123 
(* a singletonlist *) 
22846  124 
(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

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

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

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

128 

26652  129 
(* 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

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

132 

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

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

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

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

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

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

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

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

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

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

146 
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

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

148 
end 
22846  149 
(* 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

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

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

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

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

155 
 _ => raise EQVT_FORM "Type unknown") 
22846  156 
in 
26652  157 
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

158 
end 
22846  159 
handle EQVT_FORM s => 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30991
diff
changeset

160 
error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
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

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

162 

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

163 

30991  164 
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm)); 
165 
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

166 

30991  167 
val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm); 
168 
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

169 

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

170 
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

171 

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

172 
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

173 
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

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

175 
#> 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

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

177 
#> 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

178 

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

179 

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

180 
end; 