author | Christian Urban <urbanc@in.tum.de> |
Wed, 22 Dec 2010 09:13:25 +0000 | |
changeset 2617 | e44551d067e6 |
parent 2559 | add799cf0817 |
child 2630 | 8268b277d240 |
permissions | -rw-r--r-- |
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
1 |
theory Lambda |
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2442
diff
changeset
|
2 |
imports "../Nominal2" |
1594 | 3 |
begin |
4 |
||
5 |
atom_decl name |
|
6 |
||
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
7 |
nominal_datatype lam = |
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
8 |
Var "name" |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
9 |
| App "lam" "lam" |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
10 |
| Lam x::"name" l::"lam" bind x in l |
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents:
2425
diff
changeset
|
11 |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
12 |
thm lam.distinct |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
13 |
thm lam.induct |
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
14 |
thm lam.exhaust lam.strong_exhaust |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
15 |
thm lam.fv_defs |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
16 |
thm lam.bn_defs |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
17 |
thm lam.perm_simps |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
18 |
thm lam.eq_iff |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
19 |
thm lam.fv_bn_eqvt |
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
20 |
thm lam.size_eqvt |
2431
331873ebc5cd
can now deal with type variables in nominal datatype definitions
Christian Urban <urbanc@in.tum.de>
parents:
2425
diff
changeset
|
21 |
|
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
parents:
2311
diff
changeset
|
22 |
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
23 |
section {* Strong Induction Lemma via Induct_schema *} |
2497
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
24 |
|
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
25 |
|
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
26 |
lemma strong_induct: |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
27 |
fixes c::"'a::fs" |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
28 |
assumes a1: "\<And>name c. P c (Var name)" |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
29 |
and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
30 |
and a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
2497
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
31 |
shows "P c lam" |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
32 |
using assms |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
33 |
apply(induction_schema) |
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
34 |
apply(rule_tac y="lam" in lam.strong_exhaust) |
2497
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
35 |
apply(blast) |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
36 |
apply(blast) |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
37 |
apply(blast) |
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
38 |
apply(relation "measure (\<lambda>(x,y). size y)") |
2503
cc5d23547341
simplified exhaust proofs
Christian Urban <urbanc@in.tum.de>
parents:
2497
diff
changeset
|
39 |
apply(simp_all add: lam.size) |
2497
7f311ed9204d
test with induct_schema for simpler strong_ind proofs
Christian Urban <urbanc@in.tum.de>
parents:
2454
diff
changeset
|
40 |
done |
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents:
2041
diff
changeset
|
41 |
|
1805 | 42 |
section {* Typing *} |
43 |
||
44 |
nominal_datatype ty = |
|
45 |
TVar string |
|
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
46 |
| TFun ty ty |
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
47 |
|
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
48 |
notation |
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
49 |
TFun ("_ \<rightarrow> _") |
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
50 |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
51 |
(* |
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
52 |
declare ty.perm[eqvt] |
1805 | 53 |
|
54 |
inductive |
|
55 |
valid :: "(name \<times> ty) list \<Rightarrow> bool" |
|
56 |
where |
|
57 |
"valid []" |
|
58 |
| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)" |
|
59 |
||
1828 | 60 |
inductive |
61 |
typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
|
62 |
where |
|
63 |
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
1947 | 64 |
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
1828 | 65 |
| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
66 |
||
1831
16653e702d89
first working version of the automatic equivariance procedure
Christian Urban <urbanc@in.tum.de>
parents:
1828
diff
changeset
|
67 |
equivariance valid |
16653e702d89
first working version of the automatic equivariance procedure
Christian Urban <urbanc@in.tum.de>
parents:
1828
diff
changeset
|
68 |
equivariance typing |
1816
56cebe7f8e24
some small tunings (incompleted work in Lambda.thy)
Christian Urban <urbanc@in.tum.de>
parents:
1814
diff
changeset
|
69 |
|
1831
16653e702d89
first working version of the automatic equivariance procedure
Christian Urban <urbanc@in.tum.de>
parents:
1828
diff
changeset
|
70 |
thm valid.eqvt |
16653e702d89
first working version of the automatic equivariance procedure
Christian Urban <urbanc@in.tum.de>
parents:
1828
diff
changeset
|
71 |
thm typing.eqvt |
1811
ae176476b525
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1810
diff
changeset
|
72 |
thm eqvts |
ae176476b525
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1810
diff
changeset
|
73 |
thm eqvts_raw |
ae176476b525
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1810
diff
changeset
|
74 |
|
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
75 |
thm typing.induct[of "\<Gamma>" "t" "T", no_vars] |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
76 |
|
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
77 |
lemma |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
78 |
fixes c::"'a::fs" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
79 |
assumes a: "\<Gamma> \<turnstile> t : T" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
80 |
and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
81 |
and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
82 |
\<Longrightarrow> P c \<Gamma> (App t1 t2) T2" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
83 |
and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
84 |
\<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
85 |
shows "P c \<Gamma> t T" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
86 |
proof - |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
87 |
from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)" |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
88 |
proof (induct) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
89 |
case (t_Var \<Gamma> x T p c) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
90 |
then show ?case |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
91 |
apply - |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
92 |
apply(perm_strict_simp) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
93 |
apply(rule a1) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
94 |
apply(drule_tac p="p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
95 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
96 |
apply(assumption) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
97 |
apply(rotate_tac 1) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
98 |
apply(drule_tac p="p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
99 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
100 |
apply(assumption) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
101 |
done |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
102 |
next |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
103 |
case (t_App \<Gamma> t1 T1 T2 t2 p c) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
104 |
then show ?case |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
105 |
apply - |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
106 |
apply(perm_strict_simp) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
107 |
apply(rule a2) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
108 |
apply(drule_tac p="p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
109 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
110 |
apply(assumption) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
111 |
apply(assumption) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
112 |
apply(rotate_tac 2) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
113 |
apply(drule_tac p="p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
114 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
115 |
apply(assumption) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
116 |
apply(assumption) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
117 |
done |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
118 |
next |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
119 |
case (t_Lam x \<Gamma> T1 t T2 p c) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
120 |
then show ?case |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
121 |
apply - |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
122 |
apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
123 |
supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q") |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
124 |
apply(erule exE) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
125 |
apply(rule_tac t="p \<bullet> \<Gamma>" and s="(q + p) \<bullet> \<Gamma>" in subst) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
126 |
apply(simp only: permute_plus) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
127 |
apply(rule supp_perm_eq) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
128 |
apply(simp add: supp_Pair fresh_star_union) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
129 |
apply(rule_tac t="p \<bullet> Lam x t" and s="(q + p) \<bullet> Lam x t" in subst) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
130 |
apply(simp only: permute_plus) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
131 |
apply(rule supp_perm_eq) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
132 |
apply(simp add: supp_Pair fresh_star_union) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
133 |
apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
134 |
apply(simp only: permute_plus) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
135 |
apply(rule supp_perm_eq) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
136 |
apply(simp add: supp_Pair fresh_star_union) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
137 |
apply(simp (no_asm) only: eqvts) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
138 |
apply(rule a3) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
139 |
apply(simp only: eqvts permute_plus) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
140 |
apply(simp add: fresh_star_def) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
141 |
apply(drule_tac p="q + p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
142 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
143 |
apply(assumption) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
144 |
apply(rotate_tac 1) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
145 |
apply(drule_tac p="q + p" in permute_boolI) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
146 |
apply(perm_strict_simp add: permute_minus_cancel) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
147 |
apply(assumption) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
148 |
apply(drule_tac x="d" in meta_spec) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
149 |
apply(drule_tac x="q + p" in meta_spec) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
150 |
apply(perm_strict_simp add: permute_minus_cancel) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
151 |
apply(assumption) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
152 |
apply(rule at_set_avoiding2) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
153 |
apply(simp add: finite_supp) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
154 |
apply(simp add: finite_supp) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
155 |
apply(simp add: finite_supp) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
156 |
apply(rule_tac p="-p" in permute_boolE) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
157 |
apply(perm_strict_simp add: permute_minus_cancel) |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
158 |
--"supplied by the user" |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
159 |
apply(simp add: fresh_star_prod) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
160 |
apply(simp add: fresh_star_def) |
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
161 |
sorry |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
162 |
qed |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
163 |
then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" . |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
164 |
then show "P c \<Gamma> t T" by simp |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
165 |
qed |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
166 |
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
1831
diff
changeset
|
167 |
*) |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
1831
diff
changeset
|
168 |
|
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1805
diff
changeset
|
169 |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
170 |
section {* Matching *} |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
171 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
172 |
definition |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
173 |
MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
174 |
where |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
175 |
"MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
176 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
177 |
(* |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
178 |
lemma MATCH_eqvt: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
179 |
shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
180 |
unfolding MATCH_def |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
181 |
apply(perm_simp the_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
182 |
apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
183 |
apply(simp) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
184 |
thm eqvts_raw |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
185 |
apply(subst if_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
186 |
apply(subst ex1_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
187 |
apply(subst permute_fun_def) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
188 |
apply(subst ex_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
189 |
apply(subst permute_fun_def) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
190 |
apply(subst eq_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
191 |
apply(subst permute_fun_app_eq[where f="M"]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
192 |
apply(simp only: permute_minus_cancel) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
193 |
apply(subst permute_prod.simps) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
194 |
apply(subst permute_prod.simps) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
195 |
apply(simp only: permute_minus_cancel) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
196 |
apply(simp only: permute_bool_def) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
197 |
apply(simp) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
198 |
apply(subst ex1_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
199 |
apply(subst permute_fun_def) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
200 |
apply(subst ex_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
201 |
apply(subst permute_fun_def) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
202 |
apply(subst eq_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
203 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
204 |
apply(simp only: eqvts) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
205 |
apply(simp) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
206 |
apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))") |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
207 |
apply(drule sym) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
208 |
apply(simp) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
209 |
apply(rule impI) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
210 |
apply(simp add: perm_bool) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
211 |
apply(rule trans) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
212 |
apply(rule pt_the_eqvt[OF pta at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
213 |
apply(assumption) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
214 |
apply(simp add: pt_ex_eqvt[OF pt at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
215 |
apply(simp add: pt_eq_eqvt[OF ptb at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
216 |
apply(rule cheat) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
217 |
apply(rule trans) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
218 |
apply(rule pt_ex1_eqvt) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
219 |
apply(rule pta) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
220 |
apply(rule at) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
221 |
apply(simp add: pt_ex_eqvt[OF pt at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
222 |
apply(simp add: pt_eq_eqvt[OF ptb at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
223 |
apply(subst pt_pi_rev[OF pta at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
224 |
apply(subst pt_fun_app_eq[OF pt at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
225 |
apply(subst pt_pi_rev[OF pt at]) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
226 |
apply(simp) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
227 |
done |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
228 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
229 |
lemma MATCH_cng: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
230 |
assumes a: "M1 = M2" "d1 = d2" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
231 |
shows "MATCH M1 d1 x = MATCH M2 d2 x" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
232 |
using a by simp |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
233 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
234 |
lemma MATCH_eq: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
235 |
assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
236 |
shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
237 |
using a |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
238 |
unfolding MATCH_def |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
239 |
apply(subst if_P) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
240 |
apply(rule_tac a="r x" in ex1I) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
241 |
apply(rule_tac x="x" in exI) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
242 |
apply(blast) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
243 |
apply(erule exE) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
244 |
apply(drule_tac x="q" in meta_spec) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
245 |
apply(auto)[1] |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
246 |
apply(rule the_equality) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
247 |
apply(blast) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
248 |
apply(erule exE) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
249 |
apply(drule_tac x="q" in meta_spec) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
250 |
apply(auto)[1] |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
251 |
done |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
252 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
253 |
lemma MATCH_eq2: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
254 |
assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
255 |
shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
256 |
sorry |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
257 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
258 |
lemma MATCH_neq: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
259 |
assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> False" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
260 |
shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
261 |
using a |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
262 |
unfolding MATCH_def |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
263 |
apply(subst if_not_P) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
264 |
apply(blast) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
265 |
apply(rule refl) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
266 |
done |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
267 |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
268 |
lemma MATCH_neq2: |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
269 |
assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> False" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
270 |
shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d" |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
271 |
using a |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
272 |
unfolding MATCH_def |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
273 |
apply(subst if_not_P) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
274 |
apply(auto) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
275 |
done |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
276 |
*) |
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1797
diff
changeset
|
277 |
|
1954
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
278 |
ML {* |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
279 |
fun mk_avoids ctxt params name set = |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
280 |
let |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
281 |
val (_, ctxt') = ProofContext.add_fixes |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
282 |
(map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt; |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
283 |
fun mk s = |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
284 |
let |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
285 |
val t = Syntax.read_term ctxt' s; |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
286 |
val t' = list_abs_free (params, t) |> |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
287 |
funpow (length params) (fn Abs (_, _, t) => t) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
288 |
in (t', HOLogic.dest_setT (fastype_of t)) end |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
289 |
handle TERM _ => |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
290 |
error ("Expression " ^ quote s ^ " to be avoided in case " ^ |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
291 |
quote name ^ " is not a set type"); |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
292 |
fun add_set p [] = [p] |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
293 |
| add_set (t, T) ((u, U) :: ps) = |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
294 |
if T = U then |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
295 |
let val S = HOLogic.mk_setT T |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
296 |
in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
297 |
end |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
298 |
else (u, U) :: add_set (t, T) ps |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
299 |
in |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
300 |
(mk #> add_set) set |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
301 |
end; |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
302 |
*} |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
303 |
|
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
304 |
|
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
305 |
ML {* |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
306 |
writeln (commas (map (Syntax.string_of_term @{context} o fst) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
307 |
(mk_avoids @{context} [] "t_Var" "{x}" []))) |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
308 |
*} |
23480003f9c5
some changes to the paper
Christian Urban <urbanc@in.tum.de>
parents:
1950
diff
changeset
|
309 |
|
1947 | 310 |
|
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
311 |
ML {* |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
312 |
|
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
313 |
fun prove_strong_ind (pred_name, avoids) ctxt = |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
314 |
Proof.theorem NONE (K I) [] ctxt |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
315 |
|
2169 | 316 |
local structure P = Parse and K = Keyword in |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
317 |
|
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
318 |
val _ = |
2169 | 319 |
Outer_Syntax.local_theory_to_proof "nominal_inductive" |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
320 |
"proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
321 |
(P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
322 |
(P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind) |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
323 |
|
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
324 |
end; |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
325 |
|
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
326 |
*} |
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
327 |
|
1950
7de54c9f81ac
eliminated command so that all compiles
Christian Urban <urbanc@in.tum.de>
parents:
1949
diff
changeset
|
328 |
(* |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
329 |
nominal_inductive typing |
1950
7de54c9f81ac
eliminated command so that all compiles
Christian Urban <urbanc@in.tum.de>
parents:
1949
diff
changeset
|
330 |
*) |
1949
0b692f37a771
changed theorem_i to theorem....requires new Isabelle
Christian Urban <urbanc@in.tum.de>
parents:
1947
diff
changeset
|
331 |
|
2157 | 332 |
(* Substitution *) |
2159
ce00205e07ab
Single variable substitution
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2158
diff
changeset
|
333 |
|
2165 | 334 |
primrec match_Var_raw where |
335 |
"match_Var_raw (Var_raw x) = Some x" |
|
336 |
| "match_Var_raw (App_raw x y) = None" |
|
337 |
| "match_Var_raw (Lam_raw n t) = None" |
|
338 |
||
339 |
quotient_definition |
|
340 |
"match_Var :: lam \<Rightarrow> name option" |
|
341 |
is match_Var_raw |
|
342 |
||
343 |
lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
|
344 |
apply rule |
|
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
parents:
2503
diff
changeset
|
345 |
apply (induct_tac x y rule: alpha_lam_raw.induct) |
2165 | 346 |
apply simp_all |
347 |
done |
|
348 |
||
349 |
lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
|
350 |
||
351 |
primrec match_App_raw where |
|
352 |
"match_App_raw (Var_raw x) = None" |
|
353 |
| "match_App_raw (App_raw x y) = Some (x, y)" |
|
354 |
| "match_App_raw (Lam_raw n t) = None" |
|
355 |
||
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
356 |
(* |
2165 | 357 |
quotient_definition |
358 |
"match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
|
359 |
is match_App_raw |
|
360 |
||
361 |
lemma [quot_respect]: |
|
362 |
"(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" |
|
363 |
apply (intro fun_relI) |
|
364 |
apply (induct_tac a b rule: alpha_lam_raw.induct) |
|
365 |
apply simp_all |
|
366 |
done |
|
367 |
||
368 |
lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
|
369 |
||
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
370 |
definition new where |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
371 |
"new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
372 |
|
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
373 |
definition |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
374 |
"match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
375 |
(let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
376 |
|
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
377 |
lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
378 |
apply auto |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
379 |
apply (simp only: lam.eq_iff alphas) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
380 |
apply clarify |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
381 |
apply (simp add: eqvts) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
382 |
sorry |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
383 |
|
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
384 |
lemma match_Lam_simps: |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
385 |
"match_Lam S (Var n) = None" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
386 |
"match_Lam S (App l r) = None" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
387 |
"z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
388 |
apply (simp_all add: match_Lam_def) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
389 |
apply (simp add: lam_half_inj) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
390 |
apply auto |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
391 |
done |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
392 |
*) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
393 |
(* |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
394 |
lemma match_Lam_simps2: |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
395 |
"atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
396 |
apply (rule_tac t="Lam n s" |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
397 |
and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
398 |
defer |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
399 |
apply (subst match_Lam_simps(3)) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
400 |
defer |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
401 |
apply simp |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
402 |
*) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
403 |
|
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
404 |
(*primrec match_Lam_raw where |
2165 | 405 |
"match_Lam_raw (S :: atom set) (Var_raw x) = None" |
406 |
| "match_Lam_raw S (App_raw x y) = None" |
|
407 |
| "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))" |
|
408 |
||
409 |
quotient_definition |
|
410 |
"match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option" |
|
411 |
is match_Lam_raw |
|
412 |
||
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
413 |
lemma swap_fresh: |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
414 |
assumes a: "fv_lam_raw t \<sharp>* p" |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
415 |
shows "alpha_lam_raw (p \<bullet> t) t" |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
416 |
using a apply (induct t) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
417 |
apply (simp add: supp_at_base fresh_star_def) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
418 |
apply (rule alpha_lam_raw.intros) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
419 |
apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
420 |
apply (simp) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
421 |
apply (simp only: fresh_star_union) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
422 |
apply clarify |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
423 |
apply (rule alpha_lam_raw.intros) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
424 |
apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
425 |
apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
426 |
apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
427 |
apply (rule alpha_lam_raw.intros) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
428 |
sorry |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
429 |
|
2165 | 430 |
lemma [quot_respect]: |
431 |
"(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw" |
|
432 |
proof (intro fun_relI, clarify) |
|
433 |
fix S t s |
|
434 |
assume a: "alpha_lam_raw t s" |
|
435 |
show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)" |
|
436 |
using a proof (induct t s rule: alpha_lam_raw.induct) |
|
437 |
case goal1 show ?case by simp |
|
438 |
next |
|
439 |
case goal2 show ?case by simp |
|
440 |
next |
|
441 |
case (goal3 x t y s) |
|
442 |
then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and> |
|
443 |
option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1) |
|
444 |
(match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" .. |
|
445 |
then have |
|
446 |
c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and |
|
447 |
d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and |
|
448 |
e: "alpha_lam_raw (p \<bullet> t) s" and |
|
449 |
f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and |
|
450 |
g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+ |
|
451 |
let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))" |
|
452 |
have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp |
|
453 |
show ?case |
|
454 |
unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv |
|
455 |
proof |
|
456 |
show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h) |
|
457 |
next |
|
458 |
have "atom y \<sharp> p" sorry |
|
459 |
have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry |
|
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
460 |
then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
461 |
then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry |
2165 | 462 |
have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry |
463 |
then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry |
|
464 |
then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t) |
|
465 |
((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h . |
|
466 |
qed |
|
467 |
qed |
|
468 |
qed |
|
469 |
||
470 |
lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
471 |
*) |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
472 |
(* |
2165 | 473 |
lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
474 |
by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
|
475 |
||
476 |
lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
|
477 |
apply (induct x rule: lam.induct) |
|
478 |
apply (simp_all add: match_Lam_simps) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
479 |
apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S") |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
480 |
apply (simp add: match_Lam_def) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
481 |
apply (subgoal_tac "\<exists>n s. Lam name lam = Lam n s") |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
482 |
prefer 2 |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
483 |
apply auto[1] |
2165 | 484 |
apply (simp add: Let_def) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
485 |
apply (thin_tac "\<exists>n s. Lam name lam = Lam n s") |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
486 |
apply clarify |
2165 | 487 |
apply (rule conjI) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
488 |
apply (rule_tac t="THE s. Lam name lam = Lam (new (S, Lam name lam)) s" and |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
489 |
s="(name \<leftrightarrow> (new (S, Lam name lam))) \<bullet> lam" in subst) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
490 |
defer |
2165 | 491 |
apply (simp add: lam.eq_iff) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
492 |
apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI) |
2165 | 493 |
apply (simp add: alphas) |
494 |
apply (simp add: eqvts) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
495 |
apply (rule conjI) |
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
496 |
sorry |
2165 | 497 |
|
498 |
function subst where |
|
499 |
"subst v s t = ( |
|
500 |
case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
|
501 |
case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
502 |
case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)" |
2165 | 503 |
by pat_completeness auto |
504 |
||
505 |
termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
|
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
506 |
apply auto[1] |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
507 |
apply (case_tac a) apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
508 |
apply (frule lam_some) apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
509 |
apply (case_tac a) apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
510 |
apply (frule app_some) apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
511 |
apply (case_tac a) apply simp |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
512 |
apply (frule app_some) apply simp |
2165 | 513 |
done |
514 |
||
515 |
lemmas lam_exhaust = lam_raw.exhaust[quot_lifted] |
|
516 |
||
517 |
lemma subst_eqvt: |
|
518 |
"p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
519 |
proof (induct v s t rule: subst.induct) |
|
520 |
case (1 v s t) |
|
521 |
show ?case proof (cases t rule: lam_exhaust) |
|
522 |
fix n |
|
523 |
assume "t = Var n" |
|
524 |
then show ?thesis by (simp add: match_Var_simps) |
|
525 |
next |
|
526 |
fix l r |
|
527 |
assume "t = App l r" |
|
528 |
then show ?thesis |
|
529 |
apply (simp only:) |
|
530 |
apply (subst subst.simps) |
|
531 |
apply (subst match_Var_simps) |
|
532 |
apply (simp only: option.cases) |
|
533 |
apply (subst match_App_simps) |
|
534 |
apply (simp only: option.cases) |
|
535 |
apply (simp only: prod.cases) |
|
536 |
apply (simp only: lam.perm) |
|
537 |
apply (subst (3) subst.simps) |
|
538 |
apply (subst match_Var_simps) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
539 |
apply (simp only: option.cases) |
2165 | 540 |
apply (subst match_App_simps) |
541 |
apply (simp only: option.cases) |
|
542 |
apply (simp only: prod.cases) |
|
543 |
apply (subst 1(2)[of "(l, r)" "l" "r"]) |
|
544 |
apply (simp add: match_Var_simps) |
|
545 |
apply (simp add: match_App_simps) |
|
546 |
apply (rule refl) |
|
547 |
apply (subst 1(3)[of "(l, r)" "l" "r"]) |
|
548 |
apply (simp add: match_Var_simps) |
|
549 |
apply (simp add: match_App_simps) |
|
550 |
apply (rule refl) |
|
551 |
apply (rule refl) |
|
552 |
done |
|
553 |
next |
|
554 |
fix n t' |
|
555 |
assume "t = Lam n t'" |
|
556 |
then show ?thesis |
|
557 |
apply (simp only: ) |
|
558 |
apply (simp only: lam.perm) |
|
559 |
apply (subst subst.simps) |
|
560 |
apply (subst match_Var_simps) |
|
561 |
apply (simp only: option.cases) |
|
562 |
apply (subst match_App_simps) |
|
563 |
apply (simp only: option.cases) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
564 |
apply (rule_tac t="Lam n t'" and s="Lam (new ((v, s), Lam n t')) ((n \<leftrightarrow> new ((v, s), Lam n t')) \<bullet> t')" in subst) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
565 |
defer |
2165 | 566 |
apply (subst match_Lam_simps) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
567 |
defer |
2165 | 568 |
apply (simp only: option.cases) |
569 |
apply (simp only: prod.cases) |
|
570 |
apply (subst (2) subst.simps) |
|
571 |
apply (subst match_Var_simps) |
|
572 |
apply (simp only: option.cases) |
|
573 |
apply (subst match_App_simps) |
|
574 |
apply (simp only: option.cases) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
575 |
apply (rule_tac t="Lam (p \<bullet> n) (p \<bullet> t')" and s="Lam (new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) (((p \<bullet> n) \<leftrightarrow> new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) \<bullet> t')" in subst) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
576 |
defer |
2165 | 577 |
apply (subst match_Lam_simps) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
578 |
defer |
2165 | 579 |
apply (simp only: option.cases) |
580 |
apply (simp only: prod.cases) |
|
581 |
apply (simp only: lam.perm) |
|
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
582 |
thm 1(1) |
2165 | 583 |
sorry |
584 |
qed |
|
585 |
qed |
|
586 |
||
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
587 |
lemma subst_proper_eqs: |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
588 |
"subst y s (Var x) = (if x = y then s else (Var x))" |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
589 |
"subst y s (App l r) = App (subst y s l) (subst y s r)" |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
590 |
"atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
591 |
apply (subst subst.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
592 |
apply (simp only: match_Var_simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
593 |
apply (simp only: option.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
594 |
apply (subst subst.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
595 |
apply (simp only: match_App_simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
596 |
apply (simp only: option.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
597 |
apply (simp only: prod.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
598 |
apply (simp only: match_Var_simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
599 |
apply (simp only: option.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
600 |
apply (subst subst.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
601 |
apply (simp only: match_Var_simps) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
602 |
apply (simp only: option.simps) |
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
603 |
apply (simp only: match_App_simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
604 |
apply (simp only: option.simps) |
2173
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
605 |
apply (rule_tac t="Lam x t" and s="Lam (new ((y, s), Lam x t)) ((x \<leftrightarrow> new ((y, s), Lam x t)) \<bullet> t)" in subst) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
606 |
defer |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
607 |
apply (subst match_Lam_simps) |
477293d841e8
Match_Lam defined on Quotient Level.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2172
diff
changeset
|
608 |
defer |
2172
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
609 |
apply (simp only: option.simps) |
fd5eec72c3f5
More on Function-defined subst.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2170
diff
changeset
|
610 |
apply (simp only: prod.simps) |
2157 | 611 |
sorry |
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
612 |
*) |
1594 | 613 |
end |
614 |
||
615 |
||
616 |