author | urbanc |
Fri, 02 Feb 2007 17:16:16 +0100 | |
changeset 22231 | f76f187c91f9 |
permissions | -rw-r--r-- |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
1 |
(* ID: "$Id$" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
2 |
Authors: Julien Narboux and Christian Urban |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
3 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
4 |
This file introduces the infrastructure for the lemma |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
5 |
declaration "eqvt" "bij" and "fresh". |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
6 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
7 |
By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
8 |
in a data-slot in the theory context. Possible modifiers |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
9 |
are [tag add] and [tag del] for adding and deleting, |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
10 |
respectively the lemma from the data-slot. |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
11 |
*) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
12 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
13 |
signature EQVT_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
14 |
sig |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
15 |
val print_eqvtset: Proof.context -> unit |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
16 |
val eqvt_add: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
17 |
val eqvt_del: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
18 |
val setup: theory -> theory |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
19 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
20 |
val EQVT_DEBUG : bool ref |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
21 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
22 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
23 |
structure EqvtRules: EQVT_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
24 |
struct |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
25 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
26 |
structure Data = GenericDataFun |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
27 |
( |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
28 |
val name = "HOL/Nominal/eqvt"; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
29 |
type T = thm list; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
30 |
val empty = []; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
31 |
val extend = I; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
32 |
fun merge _ = Drule.merge_rules; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
33 |
fun print context rules = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
34 |
Pretty.writeln (Pretty.big_list "Equivariance lemmas:" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
35 |
(map (ProofContext.pretty_thm (Context.proof_of context)) rules)); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
36 |
); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
37 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
38 |
(* Exception for when a theorem does not conform with form of an equivariance lemma. *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
39 |
(* There are two forms: one is an implication (for relations) and the other is an *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
40 |
(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
41 |
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
42 |
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
43 |
(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
44 |
(* the implicational case it is also checked that the variables and permutation fit *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
45 |
(* together, i.e. are of the right "pt_class", so that a stronger version of the *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
46 |
(* eqality-lemma can be derived. *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
47 |
exception EQVT_FORM; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
48 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
49 |
val print_eqvtset = Data.print o Context.Proof; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
50 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
51 |
(* FIXME: should be a function in a library *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
52 |
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
53 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
54 |
val perm_bool = thm "perm_bool"; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
55 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
56 |
val EQVT_DEBUG = ref false; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
57 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
58 |
fun tactic (msg,tac) = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
59 |
if !EQVT_DEBUG |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
60 |
then (EVERY [tac, print_tac ("after "^msg)]) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
61 |
else tac |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
62 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
63 |
fun tactic_eqvt ctx orig_thm pi typi = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
64 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
65 |
val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
66 |
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
67 |
val perm_pi_simp = PureThy.get_thms ctx (Name "perm_pi_simp") |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
68 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
69 |
EVERY [tactic ("iffI applied",rtac iffI 1), |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
70 |
tactic ("simplifies with orig_thm and perm_bool", |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
71 |
asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
72 |
tactic ("applies orig_thm instantiated with rev pi", |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
73 |
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
74 |
tactic ("getting rid of all remaining perms", |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
75 |
full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
76 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
77 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
78 |
fun get_derived_thm thy hyp concl orig_thm pi typi = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
79 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
80 |
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
81 |
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
82 |
val _ = Display.print_cterm (cterm_of thy goal_term) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
83 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
84 |
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
85 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
86 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
87 |
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
88 |
(* the eqvt_thm_list to the user, we have to manually update the context and the *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
89 |
(* thm-list eqvt *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
90 |
fun update_context flag thms context = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
91 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
92 |
val context' = fold (fn thm => Data.map (flag thm)) thms context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
93 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
94 |
Context.mapping (snd o PureThy.add_thmss [(("eqvt",Data.get context'),[])]) I context' |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
95 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
96 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
97 |
(* replaces every variable, say x, in t with pi o x *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
98 |
fun apply_pi trm (pi,typi) = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
99 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
100 |
fun only_vars t = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
101 |
(case t of |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
102 |
Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty))) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
103 |
| _ => t) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
104 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
105 |
map_aterms only_vars trm |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
106 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
107 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
108 |
(* returns *the* pi which is in front of all variables, provided there *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
109 |
(* exists such a pi; otherwise raises EQVT_FORM *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
110 |
fun get_pi t thy = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
111 |
let fun get_pi_aux s = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
112 |
(case s of |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
113 |
(Const ("Nominal.perm",typrm) $ |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
114 |
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
115 |
(Var (n,ty))) => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
116 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
117 |
(* FIXME: this should be an operation the library *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
118 |
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
119 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
120 |
if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
121 |
then [(pi,typi)] |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
122 |
else raise EQVT_FORM |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
123 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
124 |
| Abs (_,_,t1) => get_pi_aux t1 |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
125 |
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
126 |
| _ => []) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
127 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
128 |
(* collect first all pi's in front of variables in t and then use distinct *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
129 |
(* to ensure that all pi's must have been the same, i.e. distinct returns *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
130 |
(* a singleton-list *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
131 |
(case (distinct (op =) (get_pi_aux t)) of |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
132 |
[(pi,typi)] => (pi,typi) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
133 |
| _ => raise EQVT_FORM) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
134 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
135 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
136 |
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
137 |
(* lemma list depending on flag. To be added the lemma has to satisfy a *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
138 |
(* certain form. *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
139 |
fun eqvt_add_del_aux flag orig_thm context = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
140 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
141 |
val thy = Context.theory_of context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
142 |
val thms_to_be_added = (case (prop_of orig_thm) of |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
143 |
(* case: eqvt-lemma is of the implicational form *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
144 |
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
145 |
let |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
146 |
val (pi,typi) = get_pi concl thy |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
147 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
148 |
if (apply_pi hyp (pi,typi) = concl) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
149 |
then |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
150 |
(warning ("equivariance lemma of the relational form"); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
151 |
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
152 |
else raise EQVT_FORM |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
153 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
154 |
(* case: eqvt-lemma is of the equational form *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
155 |
| (Const ("Trueprop", _) $ (Const ("op =", _) $ |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
156 |
(Const ("Nominal.perm",_) $ Var (pi,typi) $ lhs) $ rhs)) => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
157 |
(if (apply_pi lhs (pi,typi)) = rhs |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
158 |
then [orig_thm] |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
159 |
else raise EQVT_FORM) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
160 |
| _ => raise EQVT_FORM) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
161 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
162 |
update_context flag thms_to_be_added context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
163 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
164 |
handle EQVT_FORM => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
165 |
error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma.") |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
166 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
167 |
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux Drule.add_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
168 |
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux Drule.del_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
169 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
170 |
val setup = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
171 |
Data.init #> |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
172 |
Attrib.add_attributes [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance rules")]; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
173 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
174 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
175 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
176 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
177 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
178 |
signature BIJ_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
179 |
sig |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
180 |
val print_bijset: Proof.context -> unit |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
181 |
val bij_add: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
182 |
val bij_del: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
183 |
val setup: theory -> theory |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
184 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
185 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
186 |
structure BijRules: BIJ_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
187 |
struct |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
188 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
189 |
structure Data = GenericDataFun |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
190 |
( |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
191 |
val name = "HOL/Nominal/bij"; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
192 |
type T = thm list; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
193 |
val empty = []; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
194 |
val extend = I; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
195 |
fun merge _ = Drule.merge_rules; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
196 |
fun print context rules = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
197 |
Pretty.writeln (Pretty.big_list "Bijection lemmas:" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
198 |
(map (ProofContext.pretty_thm (Context.proof_of context)) rules)); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
199 |
); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
200 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
201 |
val print_bijset = Data.print o Context.Proof; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
202 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
203 |
fun bij_add_del_aux f = fn th => fn context => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
204 |
let val new_context = Data.map (f th) context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
205 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
206 |
Context.mapping (snd o PureThy.add_thmss [(("bij",Data.get new_context),[])]) I new_context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
207 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
208 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
209 |
val bij_add = Thm.declaration_attribute (bij_add_del_aux Drule.add_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
210 |
val bij_del = Thm.declaration_attribute (bij_add_del_aux Drule.del_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
211 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
212 |
val setup = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
213 |
Data.init #> |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
214 |
Attrib.add_attributes [("bij", Attrib.add_del_args bij_add bij_del, "bijection rules")]; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
215 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
216 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
217 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
218 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
219 |
signature FRESH_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
220 |
sig |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
221 |
val print_freshset: Proof.context -> unit |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
222 |
val fresh_add: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
223 |
val fresh_del: attribute |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
224 |
val setup: theory -> theory |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
225 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
226 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
227 |
structure FreshRules: FRESH_RULES = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
228 |
struct |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
229 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
230 |
structure Data = GenericDataFun |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
231 |
( |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
232 |
val name = "HOL/Nominal/fresh"; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
233 |
type T = thm list; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
234 |
val empty = []; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
235 |
val extend = I; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
236 |
fun merge _ = Drule.merge_rules; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
237 |
fun print context rules = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
238 |
Pretty.writeln (Pretty.big_list "Freshness lemmas:" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
239 |
(map (ProofContext.pretty_thm (Context.proof_of context)) rules)); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
240 |
); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
241 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
242 |
val print_freshset = Data.print o Context.Proof; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
243 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
244 |
fun fresh_add_del_aux f = fn th => fn context => |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
245 |
let val new_context = Data.map (f th) context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
246 |
in |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
247 |
Context.mapping (snd o PureThy.add_thmss [(("fresh",Data.get new_context),[])]) I new_context |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
248 |
end |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
249 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
250 |
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux Drule.add_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
251 |
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux Drule.del_rule); |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
252 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
253 |
val setup = |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
254 |
Data.init #> |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
255 |
Attrib.add_attributes [("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness rules")]; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
256 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
257 |
end; |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
258 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
259 |
(* Thm.declaration_attribute is of type (thm -> Context.generic -> Context.generic) -> attribute *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
260 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
261 |
(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
262 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
263 |
(* Drule.add_rule has type thm -> thm list -> thm list *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
264 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
265 |
(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *) |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
266 |
|
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
diff
changeset
|
267 |
(* add_del_args is of type attribute -> attribute -> src -> attribute *) |