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 thm lam.strong_exhaust |
|
16 |
|
17 lemma lam_strong_exhaust2: |
|
18 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
|
19 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
|
20 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
|
21 finite (supp c)\<rbrakk> |
|
22 \<Longrightarrow> P" |
|
23 sorry |
|
24 |
|
25 abbreviation |
|
26 "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" |
14 |
27 |
15 lemma Abs1_eq_fdest: |
28 lemma Abs1_eq_fdest: |
16 fixes x y :: "'a :: at_base" |
29 fixes x y :: "'a :: at_base" |
17 and S T :: "'b :: fs" |
30 and S T :: "'b :: fs" |
18 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
31 assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
38 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
51 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
39 shows "a \<sharp> f x y z" |
52 shows "a \<sharp> f x y z" |
40 using fresh_fun_eqvt_app[OF a b(1)] a b |
53 using fresh_fun_eqvt_app[OF a b(1)] a b |
41 by (metis fresh_fun_app) |
54 by (metis fresh_fun_app) |
42 |
55 |
43 nominal_primrec |
56 locale test = |
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" |
57 fixes f1::"name \<Rightarrow> ('a::pt)" |
45 where |
58 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
46 "f f1 f2 f3 (Var x) = f1 x" |
59 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
47 | "f f1 f2 f3 (App t1 t2) = f2 t1 t2 (f f1 f2 f3 t1) (f f1 f2 f3 t2)" |
60 assumes fs: "finite (supp (f1, f2, f3))" |
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)" |
61 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
|
62 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
|
63 begin |
|
64 |
|
65 nominal_primrec |
|
66 f :: "lam \<Rightarrow> ('a::pt)" |
|
67 where |
|
68 "f (Var x) = f1 x" |
|
69 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
|
70 | "atom x \<sharp> (f1, f2, f3) \<Longrightarrow> f (Lam [x].t) = f3 x t (f t)" |
49 apply (simp add: eqvt_def f_graph_def) |
71 apply (simp add: eqvt_def f_graph_def) |
50 apply (rule, perm_simp, rule) |
72 apply (perm_simp) |
51 apply(case_tac x) |
73 apply(simp add: eq[simplified eqvt_def]) |
52 apply(rule_tac y="d" and c="z" in lam.strong_exhaust) |
74 apply(rule_tac y="x" and c="(f1,f2,f3)" in lam_strong_exhaust2) |
53 apply(auto simp add: fresh_star_def) |
75 apply(auto simp add: fresh_star_def) |
54 apply(blast) |
76 apply(rule fs) |
55 defer |
|
56 apply(simp add: fresh_Pair_elim) |
77 apply(simp add: fresh_Pair_elim) |
57 apply(erule Abs1_eq_fdest) |
78 apply(erule Abs1_eq_fdest) |
58 apply simp_all |
79 apply simp_all |
59 apply (rule_tac f="f3a" in fresh_fun_eqvt_app3) |
80 apply(simp add: fcb) |
60 apply assumption |
81 apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)") |
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) |
82 apply (simp add: eqvt_at_def eqvt_def) |
68 apply (simp add: permute_fun_app_eq) |
83 apply (simp add: permute_fun_app_eq eq[simplified eqvt_def]) |
69 apply (simp add: eqvt_def) |
84 sorry |
70 sorry (*this could be defined *) |
|
71 |
85 |
72 termination sorry |
86 termination sorry |
73 |
87 |
74 thm f.simps |
88 end |
75 |
89 |
|
90 thm test.f.simps |
|
91 |
|
92 thm test_def |
76 |
93 |
77 |
94 |
78 |
95 |
79 inductive |
96 inductive |
80 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
97 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |