equal
deleted
inserted
replaced
1 theory Ex2 |
1 theory Ex2 |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 2 *} |
5 text {* example 2 *} |
|
6 declare [[STEPS = 8]] |
6 |
7 |
7 atom_decl name |
8 atom_decl name |
8 |
9 |
9 nominal_datatype trm = |
10 nominal_datatype trm = |
10 Var "name" |
11 Var "name" |
19 f::"pat \<Rightarrow> atom set" |
20 f::"pat \<Rightarrow> atom set" |
20 where |
21 where |
21 "f PN = {}" |
22 "f PN = {}" |
22 | "f (PD x y) = {atom x, atom y}" |
23 | "f (PD x y) = {atom x, atom y}" |
23 | "f (PS x) = {atom x}" |
24 | "f (PS x) = {atom x}" |
|
25 |
|
26 thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars] |
|
27 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] |
|
28 |
|
29 |
|
30 |
|
31 |
24 thm trm_pat.bn |
32 thm trm_pat.bn |
25 thm trm_pat.perm |
33 thm trm_pat.perm |
26 thm trm_pat.induct |
34 thm trm_pat.induct |
27 thm trm_pat.distinct |
35 thm trm_pat.distinct |
28 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
36 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |