author | Christian Urban <urbanc@in.tum.de> |
Thu, 28 Jan 2010 14:20:26 +0100 | |
changeset 983 | 31b4ac97cfea |
parent 981 | bc739536b715 |
child 984 | 8e2dd0b29466 |
permissions | -rw-r--r-- |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory LamEx |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
lemma in_permute_iff: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
apply(unfold mem_def permute_fun_def)[1] |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
apply(simp add: permute_bool_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
lemma fresh_star_permute_iff: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
apply(simp add: fresh_star_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
apply(drule_tac x="p \<bullet> xa" in bspec) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
apply(unfold mem_def permute_fun_def)[1] |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
apply(simp add: eqvts) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
apply(simp add: fresh_permute_iff) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
apply(drule_tac x="- p \<bullet> xa" in bspec) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
lemma fresh_minus_perm: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
fixes p::perm |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
apply(simp add: fresh_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
apply(simp only: supp_minus_perm) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
lemma fresh_plus: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
fixes p q::perm |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
unfolding fresh_def |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
using supp_plus_perm |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
lemma fresh_star_plus: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
fixes p q::perm |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
unfolding fresh_star_def |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
by (simp add: fresh_plus) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
atom_decl name |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
datatype rlam = |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
rVar "name" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
| rApp "rlam" "rlam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
| rLam "name" "rlam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
fun |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
rfv :: "rlam \<Rightarrow> atom set" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
where |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
rfv_var: "rfv (rVar a) = {atom a}" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
| rfv_lam: "rfv (rLam a t) = (rfv t) - {atom a}" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
instantiation rlam :: pt |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
begin |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
primrec |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
permute_rlam |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
where |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
"permute_rlam pi (rVar a) = rVar (pi \<bullet> a)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
| "permute_rlam pi (rLam a t) = rLam (pi \<bullet> a) (permute_rlam pi t)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
instance |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
apply default |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
apply(induct_tac [!] x) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
end |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
instantiation rlam :: fs |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
begin |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
lemma neg_conj: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
"\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
by simp |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
lemma infinite_Un: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
"infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
by simp |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
instance |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
apply default |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
apply(induct_tac x) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
(* var case *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
apply(simp add: supp_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
apply(fold supp_def)[1] |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
apply(simp add: supp_at_base) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
(* app case *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
apply(simp only: supp_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
apply(simp only: permute_rlam.simps) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
105 |
apply(simp only: rlam.inject) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
apply(simp only: neg_conj) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
apply(simp only: Collect_disj_eq) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
apply(simp only: infinite_Un) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
apply(simp only: Collect_disj_eq) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
(* lam case *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
apply(simp only: supp_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
apply(simp only: permute_rlam.simps) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
apply(simp only: rlam.inject) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
apply(simp only: neg_conj) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
116 |
apply(simp only: Collect_disj_eq) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
apply(simp only: infinite_Un) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
apply(simp only: Collect_disj_eq) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
apply(fold supp_def)[1] |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
apply(simp add: supp_at_base) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
end |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
125 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
126 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
(* for the eqvt proof of the alpha-equivalence *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
declare permute_rlam.simps[eqvt] |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
lemma rfv_eqvt[eqvt]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
apply(induct t) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
apply(simp add: permute_set_eq atom_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
apply(simp add: union_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
apply(simp add: Diff_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
apply(simp add: permute_set_eq atom_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
inductive |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
where |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
146 |
\<Longrightarrow> rLam a t \<approx> rLam b s" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
text {* should be automatic with new version of eqvt-machinery *} |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
149 |
lemma alpha_eqvt: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
apply(induct rule: alpha.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
apply(simp add: a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
apply(simp add: a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
154 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
apply(erule conjE) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
apply(erule exE) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
apply(erule conjE) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
apply(rule_tac x="pi \<bullet> pia" in exI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
apply(rule conjI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
161 |
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
162 |
apply(simp add: eqvts atom_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
163 |
apply(rule conjI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
164 |
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
apply(simp add: eqvts atom_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
166 |
apply(rule conjI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
167 |
apply(subst permute_eqvt[symmetric]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
168 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
apply(subst permute_eqvt[symmetric]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
lemma alpha_refl: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
174 |
shows "t \<approx> t" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
175 |
apply(induct t rule: rlam.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
176 |
apply(simp add: a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
177 |
apply(simp add: a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
178 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
apply(rule_tac x="0" in exI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
apply(simp_all add: fresh_star_def fresh_zero_perm) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
183 |
lemma alpha_sym: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
184 |
shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
185 |
apply(induct rule: alpha.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
186 |
apply(simp add: a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
apply(simp add: a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
189 |
apply(erule exE) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
190 |
apply(rule_tac x="- pi" in exI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
191 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
192 |
apply(simp add: fresh_star_def fresh_minus_perm) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
193 |
apply(rule conjI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
194 |
apply(erule conjE)+ |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
195 |
apply(rotate_tac 3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
196 |
apply(drule_tac pi="- pi" in alpha_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
197 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
198 |
apply(clarify) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
199 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
200 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
201 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
202 |
lemma alpha_trans: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
203 |
shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
204 |
apply(induct arbitrary: t3 rule: alpha.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
205 |
apply(erule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
206 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
207 |
apply(simp add: a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
208 |
apply(rotate_tac 4) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
209 |
apply(erule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
210 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
211 |
apply(simp add: a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
212 |
apply(rotate_tac 1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
213 |
apply(erule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
214 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
215 |
apply(erule conjE)+ |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
216 |
apply(erule exE)+ |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
217 |
apply(erule conjE)+ |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
218 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
219 |
apply(rule_tac x="pia + pi" in exI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
220 |
apply(simp add: fresh_star_plus) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
221 |
apply(drule_tac x="- pia \<bullet> sa" in spec) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
222 |
apply(drule mp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
223 |
apply(rotate_tac 8) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
224 |
apply(drule_tac pi="- pia" in alpha_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
225 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
226 |
apply(rotate_tac 11) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
227 |
apply(drule_tac pi="pia" in alpha_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
228 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
229 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
230 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
231 |
lemma alpha_equivp: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
232 |
shows "equivp alpha" |
981
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
233 |
apply(rule equivpI) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
234 |
unfolding reflp_def symp_def transp_def |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
235 |
apply(auto intro: alpha_refl alpha_sym alpha_trans) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
236 |
done |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
237 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
238 |
lemma alpha_rfv: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
239 |
shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
981
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
240 |
apply(induct rule: alpha.induct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
241 |
apply(simp_all) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
242 |
done |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
243 |
|
983
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
244 |
inductive |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
245 |
alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
246 |
where |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
247 |
a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
248 |
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
249 |
| a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
250 |
|
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
251 |
lemma |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
252 |
assumes a1: "t \<approx>2 s" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
253 |
shows "t \<approx> s" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
254 |
using a1 |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
255 |
apply(induct) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
256 |
apply(rule alpha.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
257 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
258 |
apply(rule alpha.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
259 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
260 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
261 |
apply(rule alpha.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
262 |
apply(erule disjE) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
263 |
apply(rule_tac x="0" in exI) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
264 |
apply(simp add: fresh_star_def fresh_zero_perm) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
265 |
apply(erule conjE)+ |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
266 |
apply(drule alpha_rfv) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
267 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
268 |
apply(rule_tac x="(a \<leftrightarrow> b)" in exI) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
269 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
270 |
apply(erule conjE)+ |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
271 |
apply(rule conjI) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
272 |
apply(drule alpha_rfv) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
273 |
apply(drule sym) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
274 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
275 |
defer |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
276 |
apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})") |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
277 |
apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})") |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
278 |
defer |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
279 |
sorry |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
280 |
|
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
281 |
lemma |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
282 |
assumes a1: "t \<approx> s" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
283 |
shows "t \<approx>2 s" |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
284 |
using a1 |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
285 |
apply(induct) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
286 |
apply(rule alpha2.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
287 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
288 |
apply(rule alpha2.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
289 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
290 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
291 |
apply(clarify) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
292 |
apply(rule alpha2.intros) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
293 |
apply(frule alpha_rfv) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
294 |
apply(rotate_tac 4) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
295 |
apply(drule sym) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
296 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
297 |
apply(drule sym) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
298 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
299 |
apply(case_tac "a = pi \<bullet> a") |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
300 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
301 |
defer |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
302 |
apply(simp) |
31b4ac97cfea
attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents:
981
diff
changeset
|
303 |
sorry |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
304 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
305 |
quotient_type lam = rlam / alpha |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
306 |
by (rule alpha_equivp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
307 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
308 |
quotient_definition |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
309 |
"Var :: name \<Rightarrow> lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
310 |
as |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
311 |
"rVar" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
312 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
313 |
quotient_definition |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
314 |
"App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
315 |
as |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
316 |
"rApp" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
317 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
318 |
quotient_definition |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
319 |
"Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
320 |
as |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
321 |
"rLam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
322 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
323 |
quotient_definition |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
324 |
"fv :: lam \<Rightarrow> atom set" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
325 |
as |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
326 |
"rfv" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
327 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
328 |
lemma perm_rsp[quot_respect]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
329 |
"(op = ===> alpha ===> alpha) permute permute" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
330 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
331 |
apply(rule alpha_eqvt) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
332 |
apply(simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
333 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
334 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
335 |
lemma rVar_rsp[quot_respect]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
336 |
"(op = ===> alpha) rVar rVar" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
337 |
by (auto intro: a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
338 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
339 |
lemma rApp_rsp[quot_respect]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
340 |
"(alpha ===> alpha ===> alpha) rApp rApp" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
341 |
by (auto intro: a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
342 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
343 |
lemma rLam_rsp[quot_respect]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
344 |
"(op = ===> alpha ===> alpha) rLam rLam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
345 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
346 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
347 |
apply(rule_tac x="0" in exI) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
348 |
unfolding fresh_star_def |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
349 |
apply(simp add: fresh_star_def fresh_zero_perm) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
350 |
apply(simp add: alpha_rfv) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
351 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
352 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
353 |
lemma rfv_rsp[quot_respect]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
354 |
"(alpha ===> op =) rfv rfv" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
355 |
apply(simp add: alpha_rfv) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
356 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
357 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
358 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
359 |
section {* lifted theorems *} |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
360 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
361 |
lemma lam_induct: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
362 |
"\<lbrakk>\<And>name. P (Var name); |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
363 |
\<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
364 |
\<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
365 |
\<Longrightarrow> P lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
366 |
apply (lifting rlam.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
367 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
368 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
369 |
instantiation lam :: pt |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
370 |
begin |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
371 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
372 |
quotient_definition |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
373 |
"permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
374 |
as |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
375 |
"permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
376 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
377 |
lemma permute_lam [simp]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
378 |
shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
379 |
and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
380 |
and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
381 |
apply(lifting permute_rlam.simps) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
382 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
383 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
384 |
instance |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
385 |
apply default |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
386 |
apply(induct_tac [!] x rule: lam_induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
387 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
388 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
389 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
390 |
end |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
391 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
392 |
lemma fv_lam [simp]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
393 |
shows "fv (Var a) = {atom a}" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
394 |
and "fv (App t1 t2) = fv t1 \<union> fv t2" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
395 |
and "fv (Lam a t) = fv t - {atom a}" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
396 |
apply(lifting rfv_var rfv_app rfv_lam) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
397 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
398 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
399 |
lemma a1: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
400 |
"a = b \<Longrightarrow> Var a = Var b" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
401 |
by (lifting a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
402 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
403 |
lemma a2: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
404 |
"\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
405 |
by (lifting a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
406 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
407 |
lemma a3: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
408 |
"\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
409 |
\<Longrightarrow> Lam a t = Lam b s" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
410 |
apply (lifting a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
411 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
412 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
413 |
lemma alpha_cases: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
414 |
"\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
415 |
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
416 |
\<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
417 |
\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
418 |
\<Longrightarrow> P\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
419 |
\<Longrightarrow> P" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
420 |
by (lifting alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
421 |
|
975
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
422 |
(* not sure whether needed *) |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
423 |
lemma alpha_induct: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
424 |
"\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
425 |
\<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
426 |
\<And>t a s b. |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
427 |
\<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
428 |
(fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
429 |
\<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
430 |
\<Longrightarrow> qxb qx qxa" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
431 |
by (lifting alpha.induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
432 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
433 |
(* should they lift automatically *) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
434 |
lemma lam_inject [simp]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
435 |
shows "(Var a = Var b) = (a = b)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
436 |
and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
437 |
apply(lifting rlam.inject(1) rlam.inject(2)) |
981
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
438 |
apply(regularize) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
439 |
prefer 2 |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
440 |
apply(regularize) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
441 |
prefer 2 |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
442 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
443 |
apply(drule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
444 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
445 |
apply(simp add: alpha.a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
446 |
apply(drule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
447 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
448 |
apply(drule alpha.cases) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
449 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
450 |
apply(rule alpha.a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
451 |
apply(simp_all) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
452 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
453 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
454 |
lemma rlam_distinct: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
455 |
shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
456 |
and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
457 |
and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
458 |
and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
459 |
and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
460 |
and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
461 |
apply auto |
981
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
462 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
463 |
apply (simp_all only: rlam.distinct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
464 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
465 |
apply (simp_all only: rlam.distinct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
466 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
467 |
apply (simp_all only: rlam.distinct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
468 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
469 |
apply (simp_all only: rlam.distinct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
470 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
471 |
apply (simp_all only: rlam.distinct) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
472 |
apply (erule alpha.cases) |
bc739536b715
Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
975
diff
changeset
|
473 |
apply (simp_all only: rlam.distinct) |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
474 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
475 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
476 |
lemma lam_distinct[simp]: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
477 |
shows "Var nam \<noteq> App lam1' lam2'" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
478 |
and "App lam1' lam2' \<noteq> Var nam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
479 |
and "Var nam \<noteq> Lam nam' lam'" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
480 |
and "Lam nam' lam' \<noteq> Var nam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
481 |
and "App lam1 lam2 \<noteq> Lam nam' lam'" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
482 |
and "Lam nam' lam' \<noteq> App lam1 lam2" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
483 |
apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6)) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
484 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
485 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
486 |
lemma var_supp1: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
487 |
shows "(supp (Var a)) = (supp a)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
488 |
apply (simp add: supp_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
489 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
490 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
491 |
lemma var_supp: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
492 |
shows "(supp (Var a)) = {a:::name}" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
493 |
using var_supp1 by (simp add: supp_at_base) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
494 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
495 |
lemma app_supp: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
496 |
shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
497 |
apply(simp only: permute_lam supp_def lam_inject) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
498 |
apply(simp add: Collect_imp_eq Collect_neg_eq) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
499 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
500 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
501 |
(* needs thinking *) |
975
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
502 |
lemma lam_supp1: |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
503 |
shows "(supp (atom x, t)) supports (Lam x t) " |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
504 |
apply(simp add: supports_def) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
505 |
apply(fold fresh_def) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
506 |
apply(simp add: fresh_Pair swap_fresh_fresh) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
507 |
apply(clarify) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
508 |
apply(subst swap_at_base_simps(3)) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
509 |
apply(simp_all add: fresh_atom) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
510 |
done |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
511 |
|
975
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
512 |
lemma lam_fsupp1: |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
513 |
assumes a: "finite (supp t)" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
514 |
shows "finite (supp (Lam x t))" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
515 |
apply(rule supports_finite) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
516 |
apply(rule lam_supp1) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
517 |
apply(simp add: a supp_Pair supp_atom) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
518 |
done |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
519 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
520 |
instance lam :: fs |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
521 |
apply(default) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
522 |
apply(induct_tac x rule: lam_induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
523 |
apply(simp add: var_supp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
524 |
apply(simp add: app_supp) |
975
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
525 |
apply(simp add: lam_fsupp1) |
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
526 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
527 |
|
975
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
528 |
lemma lam_fresh1: |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
529 |
assumes f: "finite (supp t)" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
530 |
and a1: "b \<sharp> t" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
531 |
and a2: "atom a \<noteq> b" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
532 |
shows "b \<sharp> Lam a t" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
533 |
proof - |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
534 |
have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
535 |
then obtain c where fr1: "c \<noteq> b" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
536 |
and fr2: "c \<noteq> atom a" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
537 |
and fr3: "c \<sharp> t" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
538 |
and fr4: "c \<sharp> Lam a t" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
539 |
and fr5: "sort_of b = sort_of c" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
540 |
apply(auto simp add: fresh_Pair fresh_atom) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
541 |
sorry |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
542 |
have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2 |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
543 |
by simp |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
544 |
from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
545 |
by (simp only: fresh_permute_iff) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
546 |
then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
547 |
by simp |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
548 |
then show ?thesis using a1 fr3 |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
549 |
by (simp only: swap_fresh_fresh) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
550 |
qed |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
551 |
|
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
552 |
lemma lam_fresh2: |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
553 |
assumes f: "finite (supp t)" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
554 |
shows "(atom a) \<sharp> Lam a t" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
555 |
sorry |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
556 |
|
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
557 |
|
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
558 |
lemma lam_supp: |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
559 |
shows "supp (Lam x t) = ((supp t) - {atom x})" |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
560 |
apply(default) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
561 |
apply(simp_all add: supp_conv_fresh) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
562 |
apply(auto) |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
563 |
sorry |
513ebe332964
test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents:
947
diff
changeset
|
564 |
|
947
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
565 |
lemma fresh_lam: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
566 |
"(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
567 |
apply(simp add: fresh_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
568 |
apply(simp add: lam_supp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
569 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
570 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
571 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
572 |
lemma lam_induct_strong: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
573 |
fixes a::"'a::fs" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
574 |
assumes a1: "\<And>name b. P b (Var name)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
575 |
and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
576 |
and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
577 |
shows "P a lam" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
578 |
proof - |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
579 |
have "\<And>pi a. P a (pi \<bullet> lam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
580 |
proof (induct lam rule: lam_induct) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
581 |
case (1 name pi) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
582 |
show "P a (pi \<bullet> Var name)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
583 |
apply (simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
584 |
apply (rule a1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
585 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
586 |
next |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
587 |
case (2 lam1 lam2 pi) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
588 |
have b1: "\<And>pi a. P a (pi \<bullet> lam1)" by fact |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
589 |
have b2: "\<And>pi a. P a (pi \<bullet> lam2)" by fact |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
590 |
show "P a (pi \<bullet> App lam1 lam2)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
591 |
apply (simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
592 |
apply (rule a2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
593 |
apply (rule b1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
594 |
apply (rule b2) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
595 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
596 |
next |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
597 |
case (3 name lam pi a) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
598 |
have b: "\<And>pi a. P a (pi \<bullet> lam)" by fact |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
599 |
obtain c::name where fr: "atom c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
600 |
apply(rule obtain_atom) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
601 |
apply(auto) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
602 |
sorry |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
603 |
from b fr have p: "P a (Lam c (((c \<leftrightarrow> (pi \<bullet> name)) + pi)\<bullet>lam))" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
604 |
apply - |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
605 |
apply(rule a3) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
606 |
apply(blast) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
607 |
apply(simp add: fresh_Pair) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
608 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
609 |
have eq: "(atom c \<rightleftharpoons> atom (pi\<bullet>name)) \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
610 |
apply(rule swap_fresh_fresh) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
611 |
using fr |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
612 |
apply(simp add: fresh_lam fresh_Pair) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
613 |
apply(simp add: fresh_lam fresh_Pair) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
614 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
615 |
show "P a (pi \<bullet> Lam name lam)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
616 |
apply (simp) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
617 |
apply(subst eq[symmetric]) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
618 |
using p |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
619 |
apply(simp only: permute_lam) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
620 |
apply(simp add: flip_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
621 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
622 |
qed |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
623 |
then have "P a (0 \<bullet> lam)" by blast |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
624 |
then show "P a lam" by simp |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
625 |
qed |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
626 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
627 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
628 |
lemma var_fresh: |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
629 |
fixes a::"name" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
630 |
shows "(atom a \<sharp> (Var b)) = (atom a \<sharp> b)" |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
631 |
apply(simp add: fresh_def) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
632 |
apply(simp add: var_supp1) |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
633 |
done |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
634 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
635 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
636 |
|
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
637 |
end |
fa810f01f7b5
added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
638 |