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