author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42616  92715b528e78 
child 51717  9e7d1c139569 
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 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

22 

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

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

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

25 

33519  26 
structure Data = Generic_Data 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

28 
type T = thm list 
33519  29 
val empty = [] 
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 
val extend = I 
33519  31 
val merge = Thm.merge_thms 
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

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

33 

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

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

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

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

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

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

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

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

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

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

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

44 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42361
diff
changeset

45 
val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false); 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

46 

38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

47 
fun tactic ctxt (msg, tac) = 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

48 
if Config.get ctxt nominal_eqvt_debug 
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 
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

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

51 

30991  52 
fun prove_eqvt_tac ctxt orig_thm pi pi' = 
38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

53 
let 
42361  54 
val thy = Proof_Context.theory_of ctxt 
38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

55 
val mypi = Thm.cterm_of thy pi 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

56 
val T = fastype_of pi' 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

57 
val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T > T) $ pi') 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38864
diff
changeset

58 
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp" 
38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

59 
in 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

60 
EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}), 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

61 
tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}), 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

62 
tactic ctxt ("solve with orig_thm", etac orig_thm), 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

63 
tactic ctxt ("applies orig_thm instantiated with rev pi", 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

64 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

65 
tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}), 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

66 
tactic ctxt ("getting rid of all remaining perms", 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

67 
full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))] 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
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 
42361  72 
val thy = Proof_Context.theory_of ctxt; 
30088
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 
32429
54758ca53fd6
modernized messages  eliminated old Display.print_cterm;
wenzelm
parents:
32091
diff
changeset

77 
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

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 
38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

80 
(fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') > 
42361  81 
singleton (Proof_Context.export ctxt' ctxt) 
30088
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) $ 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

105 
(Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [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 *) 
38558  137 
(Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name 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 *) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38808
diff
changeset

149 
 (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ 
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 => 
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

159 
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

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 = 
38807
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

172 
Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

173 
"equivariance theorem declaration" #> 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

174 
Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) 
378ffc903bed
eliminated Unsynchronized.ref in favour of configuration option;
wenzelm
parents:
38558
diff
changeset

175 
"equivariance theorem declaration (without checking the form of the lemma)" #> 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38864
diff
changeset

176 
Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.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

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; 