|
1 theory Classical |
|
2 imports "../Parser" |
|
3 begin |
|
4 |
|
5 (* example from my Urban's PhD *) |
|
6 |
|
7 (* |
|
8 alpha_trm_raw is incorrectly defined, therefore the equivalence proof |
|
9 does not go through; below the correct definition is given |
|
10 *) |
|
11 ML {* val _ = cheat_equivp := true *} |
|
12 |
|
13 atom_decl name |
|
14 atom_decl coname |
|
15 |
|
16 nominal_datatype trm = |
|
17 Ax "name" "coname" |
|
18 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
|
19 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
|
20 | AndL1 n::"name" t::"trm" "name" bind n in t |
|
21 | AndL2 n::"name" t::"trm" "name" bind n in t |
|
22 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
|
23 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n in t, bind c in t |
|
24 |
|
25 |
|
26 thm trm.fv |
|
27 thm trm.eq_iff |
|
28 thm trm.bn |
|
29 thm trm.perm |
|
30 thm trm.induct |
|
31 thm trm.distinct |
|
32 thm trm.fv[simplified trm.supp] |
|
33 |
|
34 (* correct alpha definition *) |
|
35 |
|
36 inductive |
|
37 alpha |
|
38 where |
|
39 "\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow> |
|
40 alpha (Ax_raw name coname) (Ax_raw namea conamea)" |
|
41 | "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); |
|
42 \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow> |
|
43 alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2) |
|
44 (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)" |
|
45 | "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); |
|
46 \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a); |
|
47 coname3 = coname3a\<rbrakk> \<Longrightarrow> |
|
48 alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3) |
|
49 (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)" |
|
50 | "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); |
|
51 name2 = name2a\<rbrakk> \<Longrightarrow> |
|
52 alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)" |
|
53 | "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa); |
|
54 name2 = name2a\<rbrakk> \<Longrightarrow> |
|
55 alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)" |
|
56 | "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a); |
|
57 \<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a); |
|
58 name2 = name2a\<rbrakk> \<Longrightarrow> |
|
59 alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2) |
|
60 (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)" |
|
61 | "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi |
|
62 ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow> |
|
63 alpha (ImpR_raw coname1 name trm_raw coname2) |
|
64 (ImpR_raw coname1a namea trm_rawa coname2a)" |
|
65 |
|
66 |
|
67 end |
|
68 |
|
69 |
|
70 |