equal
deleted
inserted
replaced
7 |
7 |
8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
|
12 |
|
13 lemma cheat: "P" sorry |
|
14 |
|
15 nominal_primrec |
|
16 f |
|
17 where |
|
18 "f f1 f2 f3 (Var x) = f1 x" |
|
19 | "f f1 f2 f3 (App t1 t2) = f2 t1 t2 (f f1 f2 f3 t1) (f f1 f2 f3 t2)" |
|
20 | "atom x \<sharp> (f1,f2,f3) \<Longrightarrow> f f1 f2 f3 (Lam [x].t) = f3 x t (f f1 f2 f3 t)" |
|
21 unfolding eqvt_def f_graph_def |
|
22 apply (rule, perm_simp, rule) |
|
23 apply(case_tac x) |
|
24 apply(simp) |
|
25 apply(rule_tac y="d" in lam.exhaust) |
|
26 apply(auto)[1] |
|
27 apply(auto simp add: lam.distinct lam.eq_iff)[3] |
|
28 apply(blast) |
|
29 apply(rule cheat) (* this can be solved *) |
|
30 apply(simp) |
|
31 apply(simp) |
|
32 apply(simp) |
|
33 apply(simp) |
|
34 apply(simp) |
|
35 sorry (*this could be defined *) |
|
36 |
|
37 termination sorry |
|
38 |
|
39 thm f.simps |
|
40 |
|
41 |
12 |
42 |
13 |
43 |
14 inductive |
44 inductive |
15 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
45 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
16 where |
46 where |