equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
|
5 inductive |
|
6 even :: "nat \<Rightarrow> bool" and |
|
7 odd :: "nat \<Rightarrow> bool" |
|
8 where |
|
9 "even 0" |
|
10 | "odd n \<Longrightarrow> even (Suc n)" |
|
11 | "even n \<Longrightarrow> odd (Suc n)" |
|
12 |
|
13 thm even_odd_def |
|
14 |
|
15 lemma |
|
16 shows "p \<bullet> (even n) = even (p \<bullet> n)" |
|
17 unfolding even_def |
|
18 unfolding even_odd_def |
|
19 apply(perm_simp) |
|
20 apply(rule refl) |
|
21 done |
5 |
22 |
6 atom_decl name |
23 atom_decl name |
7 |
24 |
8 nominal_datatype lam = |
25 nominal_datatype lam = |
9 Var "name" |
26 Var "name" |
10 | App "lam" "lam" |
27 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
28 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 |
29 |
|
30 |
13 inductive |
31 inductive |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
32 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 where |
33 where |
16 Var: "triv (Var x) n" |
34 Var: "triv (Var x) n" |
|
35 | App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n" |
17 |
36 |
18 lemma |
37 lemma |
19 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
38 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
20 unfolding triv_def |
39 unfolding triv_def |
21 apply(perm_simp) |
40 apply(perm_simp) |
|
41 apply(rule refl) |
22 oops |
42 oops |
23 (*apply(perm_simp)*) |
43 (*apply(perm_simp)*) |
|
44 |
|
45 ML {* |
|
46 Inductive.the_inductive @{context} "Lambda.triv" |
|
47 *} |
|
48 |
|
49 thm triv_def |
24 |
50 |
25 equivariance triv |
51 equivariance triv |
26 nominal_inductive triv avoids Var: "{}::name set" |
52 nominal_inductive triv avoids Var: "{}::name set" |
27 apply(auto simp add: fresh_star_def) |
53 apply(auto simp add: fresh_star_def) |
28 done |
54 done |