equal
deleted
inserted
replaced
1 theory Ex4 |
1 theory Ex4 |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 declare [[STEPS = 4]] |
5 declare [[STEPS = 5]] |
6 (* alpha does not work for this type *) |
|
7 |
6 |
8 atom_decl name |
7 atom_decl name |
9 |
8 |
10 nominal_datatype trm = |
9 nominal_datatype trm = |
11 Var "name" |
10 Var "name" |
26 | "f (PD p1 p2) = (f p1) \<union> (f p2)" |
25 | "f (PD p1 p2) = (f p1) \<union> (f p2)" |
27 |
26 |
28 thm permute_trm_raw_permute_pat_raw.simps |
27 thm permute_trm_raw_permute_pat_raw.simps |
29 thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps |
28 thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps |
30 |
29 |
31 (* thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]*) |
30 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] |
32 |
31 |
|
32 (* |
33 inductive |
33 inductive |
34 alpha_trm_raw and alpha_pat_raw and alpha_f_raw |
34 alpha_trm_raw and alpha_pat_raw and alpha_f_raw |
35 where |
35 where |
36 (* alpha_trm_raw *) |
36 (* alpha_trm_raw *) |
37 "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)" |
37 "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)" |
58 (* alpha_f_raw *) |
58 (* alpha_f_raw *) |
59 | "alpha_f_raw PN_raw PN_raw" |
59 | "alpha_f_raw PN_raw PN_raw" |
60 | "alpha_f_raw (PS_raw name) (PS_raw namea)" |
60 | "alpha_f_raw (PS_raw name) (PS_raw namea)" |
61 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
61 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
62 \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
62 \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
|
63 *) |
63 |
64 |
64 lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros |
65 lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros |
65 |
66 |
66 lemma |
67 lemma |
67 shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x)) |
68 shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x)) |
76 apply(perm_simp) |
77 apply(perm_simp) |
77 apply(simp) |
78 apply(simp) |
78 apply(rule all) |
79 apply(rule all) |
79 done |
80 done |
80 |
81 |
81 |
82 |
82 |
83 |
83 end |
84 end |
84 |
85 |
85 |
86 |
86 |
87 |