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 |
12 |
13 lemma cheat: "P" sorry |
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 |
|
42 |
|
43 |
|
44 inductive |
|
45 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
46 where |
|
47 Var: "triv (Var x) n" |
|
48 | App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n" |
|
49 |
|
50 lemma |
|
51 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
|
52 unfolding triv_def |
|
53 apply(perm_simp) |
|
54 apply(rule refl) |
|
55 oops |
|
56 (*apply(perm_simp)*) |
|
57 |
|
58 ML {* |
|
59 Inductive.the_inductive @{context} "Lambda.triv" |
|
60 *} |
|
61 |
|
62 thm triv_def |
|
63 |
|
64 equivariance triv |
|
65 nominal_inductive triv avoids Var: "{}::name set" |
|
66 apply(auto simp add: fresh_star_def) |
|
67 done |
|
68 |
|
69 inductive |
|
70 triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
71 where |
|
72 Var1: "triv2 (Var x) 0" |
|
73 | Var2: "triv2 (Var x) (n + n)" |
|
74 | Var3: "triv2 (Var x) n" |
|
75 |
|
76 equivariance triv2 |
|
77 nominal_inductive triv2 . |
|
78 |
14 |
79 lemma Abs1_eq_fdest: |
15 lemma Abs1_eq_fdest: |
80 fixes x y :: "'a :: at_base" |
16 fixes x y :: "'a :: at_base" |
81 and S T :: "'b :: fs" |
17 and S T :: "'b :: fs" |
82 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
18 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
94 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
30 apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
95 apply(rule fresh_star_supp_conv) |
31 apply(rule fresh_star_supp_conv) |
96 apply(simp add: supp_swap fresh_star_def) |
32 apply(simp add: supp_swap fresh_star_def) |
97 apply(simp add: swap_commute) |
33 apply(simp add: swap_commute) |
98 done |
34 done |
|
35 |
|
36 lemma fresh_fun_eqvt_app3: |
|
37 assumes a: "eqvt f" |
|
38 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
|
39 shows "a \<sharp> f x y z" |
|
40 using fresh_fun_eqvt_app[OF a b(1)] a b |
|
41 by (metis fresh_fun_app) |
|
42 |
|
43 nominal_primrec |
|
44 f :: "(name \<Rightarrow> 'a\<Colon>{pt}) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a" |
|
45 where |
|
46 "f f1 f2 f3 (Var x) = f1 x" |
|
47 | "f f1 f2 f3 (App t1 t2) = f2 t1 t2 (f f1 f2 f3 t1) (f f1 f2 f3 t2)" |
|
48 | "(\<And>a t r. atom a \<sharp> f3 a t r) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t)) = f3 x t (f f1 f2 f3 t)" |
|
49 apply (simp add: eqvt_def f_graph_def) |
|
50 apply (rule, perm_simp, rule) |
|
51 apply(case_tac x) |
|
52 apply(rule_tac y="d" and c="z" in lam.strong_exhaust) |
|
53 apply(auto simp add: fresh_star_def) |
|
54 apply(blast) |
|
55 defer |
|
56 apply(simp add: fresh_Pair_elim) |
|
57 apply(erule Abs1_eq_fdest) |
|
58 apply simp_all |
|
59 apply (rule_tac f="f3a" in fresh_fun_eqvt_app3) |
|
60 apply assumption |
|
61 apply (simp add: fresh_at_base) |
|
62 apply assumption |
|
63 apply (erule fresh_eqvt_at) |
|
64 apply (simp add: supp_Pair supp_fun_eqvt finite_supp) |
|
65 apply (simp add: fresh_Pair) |
|
66 apply (subgoal_tac "\<And>p y r. p \<bullet> (f3a x y r) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)") |
|
67 apply (simp add: eqvt_at_def eqvt_def) |
|
68 apply (simp add: permute_fun_app_eq) |
|
69 apply (simp add: eqvt_def) |
|
70 sorry (*this could be defined *) |
|
71 |
|
72 termination sorry |
|
73 |
|
74 thm f.simps |
|
75 |
|
76 |
|
77 |
|
78 |
|
79 inductive |
|
80 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
81 where |
|
82 Var: "triv (Var x) n" |
|
83 | App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n" |
|
84 |
|
85 lemma |
|
86 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
|
87 unfolding triv_def |
|
88 apply(perm_simp) |
|
89 apply(rule refl) |
|
90 oops |
|
91 (*apply(perm_simp)*) |
|
92 |
|
93 ML {* |
|
94 Inductive.the_inductive @{context} "Lambda.triv" |
|
95 *} |
|
96 |
|
97 thm triv_def |
|
98 |
|
99 equivariance triv |
|
100 nominal_inductive triv avoids Var: "{}::name set" |
|
101 apply(auto simp add: fresh_star_def) |
|
102 done |
|
103 |
|
104 inductive |
|
105 triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
106 where |
|
107 Var1: "triv2 (Var x) 0" |
|
108 | Var2: "triv2 (Var x) (n + n)" |
|
109 | Var3: "triv2 (Var x) n" |
|
110 |
|
111 equivariance triv2 |
|
112 nominal_inductive triv2 . |
|
113 |
99 |
114 |
100 text {* height function *} |
115 text {* height function *} |
101 |
116 |
102 nominal_primrec |
117 nominal_primrec |
103 height :: "lam \<Rightarrow> int" |
118 height :: "lam \<Rightarrow> int" |