| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Tue, 11 May 2010 17:16:57 +0200 | |
| changeset 2104 | 2205b572bc9b |
| parent 2064 | 2725853f43b9 |
| child 2105 | e25b0fff0dd2 |
| permissions | -rw-r--r-- |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Classical |
|
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
parents:
1866
diff
changeset
|
2 |
imports "../NewParser" |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
(* example from my Urban's PhD *) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
(* |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
alpha_trm_raw is incorrectly defined, therefore the equivalence proof |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
does not go through; below the correct definition is given |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
*) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
atom_decl name |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
atom_decl coname |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
2031
d361a4699176
Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
15 |
ML {* val _ = cheat_alpha_eqvt := true *}
|
|
d361a4699176
Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
16 |
ML {* val _ = cheat_equivp := true *}
|
|
d361a4699176
Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
17 |
ML {* val _ = cheat_fv_rsp := true *}
|
|
d361a4699176
Added cheats to classical
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
18 |
|
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
nominal_datatype trm = |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
Ax "name" "coname" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
| AndL1 n::"name" t::"trm" "name" bind n in t |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
| AndL2 n::"name" t::"trm" "name" bind n in t |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
|
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
parents:
1866
diff
changeset
|
26 |
| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
thm trm.fv |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
thm trm.eq_iff |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
thm trm.bn |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
thm trm.perm |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
thm trm.induct |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
thm trm.distinct |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
thm trm.fv[simplified trm.supp] |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
(* correct alpha definition *) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
inductive |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
alpha |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
where |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
"\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow> |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
alpha (Ax_raw name coname) (Ax_raw namea conamea)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
\<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow>
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
(Cut_raw coname1a trm_raw1a coname2a trm_raw2a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
\<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
coname3 = coname3a\<rbrakk> \<Longrightarrow> |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
(AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
name2 = name2a\<rbrakk> \<Longrightarrow> |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
name2 = name2a\<rbrakk> \<Longrightarrow> |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
| "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
\<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a);
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
name2 = name2a\<rbrakk> \<Longrightarrow> |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
(ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
| "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow>
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
alpha (ImpR_raw coname1 name trm_raw coname2) |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
(ImpR_raw coname1a namea trm_rawa coname2a)" |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
|
|
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
69 |
thm alpha.intros |
|
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
70 |
|
|
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
71 |
declare permute_trm_raw.simps[eqvt] |
|
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
72 |
|
|
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
73 |
equivariance alpha |
|
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents:
2031
diff
changeset
|
74 |
equivariance alpha_trm_raw |
|
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
75 |
thm eqvts_raw |
|
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1792
diff
changeset
|
76 |
|
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
end |
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |