author | wenzelm |
Sun, 29 Jul 2007 14:29:54 +0200 | |
changeset 24039 | 273698405054 |
parent 22846 | fb79144af9a3 |
child 24265 | 4d5917cc60c4 |
permissions | -rw-r--r-- |
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 data-slot 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 data-slot. |
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 implication-case, say P ==> Q, Q must be equal *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
45 |
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
46 |
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
47 |
(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
48 |
(* the implicational case it is also checked that the variables and permutation fit *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
49 |
(* together, i.e. are of the right "pt_class", so that a stronger version of the *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
50 |
(* eqality-lemma 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 eqvt-lemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset
|
66 |
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts; |
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
67 |
val get_fresh_thms = Context.Theory #> Data.get #> #freshs; |
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
68 |
val get_bij_thms = Context.Theory #> Data.get #> #bijs; |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
69 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
70 |
(* FIXME: should be a function in a library *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
71 |
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
72 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
73 |
val perm_bool = thm "perm_bool"; |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
74 |
val perm_fun_def = thm "perm_fun_def"; |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
75 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
76 |
val NOMINAL_EQVT_DEBUG = ref false; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
77 |
|
22846 | 78 |
fun tactic (msg,tac) = |
79 |
if !NOMINAL_EQVT_DEBUG |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
80 |
then (EVERY [tac, print_tac ("after "^msg)]) |
22846 | 81 |
else tac |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
82 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
83 |
fun dynamic_thms thy name = PureThy.get_thms thy (Name name) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
84 |
|
22846 | 85 |
fun tactic_eqvt ctx orig_thm pi typi = |
86 |
let |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
87 |
val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
88 |
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
89 |
val perm_pi_simp = dynamic_thms ctx "perm_pi_simp" |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
90 |
in |
22846 | 91 |
EVERY [tactic ("iffI applied",rtac iffI 1), |
92 |
tactic ("simplifies with orig_thm and perm_bool", |
|
93 |
asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
94 |
tactic ("applies orig_thm instantiated with rev pi", |
22846 | 95 |
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
96 |
tactic ("getting rid of all remaining perms", |
22846 | 97 |
full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
98 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
99 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
100 |
fun get_derived_thm thy hyp concl orig_thm pi typi = |
22846 | 101 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
102 |
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp) |
22846 | 103 |
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) |
104 |
val _ = Display.print_cterm (cterm_of thy goal_term) |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
105 |
in |
22846 | 106 |
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
107 |
end |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
108 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
109 |
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
110 |
(* the eqvt_thm_list to the user, we have to manually update the context and the *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
111 |
(* thm-list eqvt *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
112 |
fun update_context flag thms context = |
22846 | 113 |
let |
114 |
val context' = fold (fn thm => Data.map (flag thm)) thms context |
|
115 |
in |
|
22541
c33b542394f3
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset
|
116 |
Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context' |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
117 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
118 |
|
22846 | 119 |
(* replaces every variable x in t with pi o x *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
120 |
fun apply_pi trm (pi,typi) = |
22846 | 121 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
122 |
fun only_vars t = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
123 |
(case t of |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
124 |
Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty))) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
125 |
| _ => t) |
22846 | 126 |
in |
127 |
map_aterms only_vars trm |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
128 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
129 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
130 |
(* returns *the* pi which is in front of all variables, provided there *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
131 |
(* exists such a pi; otherwise raises EQVT_FORM *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
132 |
fun get_pi t thy = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
133 |
let fun get_pi_aux s = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
134 |
(case s of |
22846 | 135 |
(Const ("Nominal.perm",typrm) $ |
136 |
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ |
|
137 |
(Var (n,ty))) => |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
138 |
let |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
139 |
(* FIXME: this should be an operation the library *) |
22846 | 140 |
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
|
141 |
in |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
142 |
if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) |
22846 | 143 |
then [(pi,typi)] |
144 |
else raise |
|
145 |
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) |
|
146 |
end |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
147 |
| Abs (_,_,t1) => get_pi_aux t1 |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
148 |
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 |
22846 | 149 |
| _ => []) |
150 |
in |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
151 |
(* collect first all pi's in front of variables in t and then use distinct *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
152 |
(* to ensure that all pi's must have been the same, i.e. distinct returns *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
153 |
(* a singleton-list *) |
22846 | 154 |
(case (distinct (op =) (get_pi_aux t)) of |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
155 |
[(pi,typi)] => (pi,typi) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
156 |
| _ => raise EQVT_FORM "All permutation should be the same") |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
157 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
158 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
159 |
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
160 |
(* lemma list depending on flag. To be added the lemma has to satisfy a *) |
22846 | 161 |
(* certain form. *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
162 |
fun eqvt_add_del_aux flag orig_thm context = |
22846 | 163 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
164 |
val thy = Context.theory_of context |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
165 |
val thms_to_be_added = (case (prop_of orig_thm) of |
22846 | 166 |
(* case: eqvt-lemma is of the implicational form *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
167 |
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => |
22846 | 168 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
169 |
val (pi,typi) = get_pi concl thy |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
170 |
in |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
171 |
if (apply_pi hyp (pi,typi) = concl) |
22846 | 172 |
then |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
173 |
(warning ("equivariance lemma of the relational form"); |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
174 |
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
175 |
else raise EQVT_FORM "Type Implication" |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
176 |
end |
22846 | 177 |
(* case: eqvt-lemma is of the equational form *) |
178 |
| (Const ("Trueprop", _) $ (Const ("op =", _) $ |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
179 |
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
180 |
(if (apply_pi lhs (pi,typi)) = rhs |
22437
b3526cd2a336
removes some unused code that used to try to derive a simpler version of the eqvt lemmas
narboux
parents:
22418
diff
changeset
|
181 |
then [orig_thm] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
182 |
else raise EQVT_FORM "Type Equality") |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
183 |
| _ => raise EQVT_FORM "Type unknown") |
22846 | 184 |
in |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
185 |
update_context flag thms_to_be_added context |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
186 |
end |
22846 | 187 |
handle EQVT_FORM s => |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
188 |
error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
189 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
190 |
(* in cases of bij- and freshness, we just add the lemmas to the *) |
22846 | 191 |
(* data-slot *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
192 |
|
22846 | 193 |
fun simple_add_del_aux record_access name flag th context = |
194 |
let |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
195 |
val context' = Data.map (flag th) context |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
196 |
in |
22846 | 197 |
Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
198 |
end |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
199 |
|
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
200 |
fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f |
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
201 |
fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f |
22541
c33b542394f3
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
urbanc
parents:
22495
diff
changeset
|
202 |
fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
203 |
|
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
204 |
fun eqvt_map f th (r:Data.T) = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r}; |
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
205 |
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r}; |
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
206 |
fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))}; |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
207 |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
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
|
216 |
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
|
217 |
|
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
218 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
219 |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
220 |
val setup = |
22846 | 221 |
Attrib.add_attributes |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
222 |
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"), |
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
223 |
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del, |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
224 |
"equivariance theorem declaration (without checking the form of the lemma)"), |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
225 |
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
226 |
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")]; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
227 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
228 |
end; |