|
1 theory LetRecB |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype let_rec: |
|
8 trm = |
|
9 Var "name" |
|
10 | App "trm" "trm" |
|
11 | Lam x::"name" t::"trm" bind x in t |
|
12 | Let_Rec bp::"bp" t::"trm" bind "bn bp" in bp t |
|
13 and bp = |
|
14 Bp "name" "trm" |
|
15 binder |
|
16 bn::"bp \<Rightarrow> atom list" |
|
17 where |
|
18 "bn (Bp x t) = [atom x]" |
|
19 |
|
20 thm let_rec.distinct |
|
21 thm let_rec.induct |
|
22 thm let_rec.exhaust |
|
23 thm let_rec.fv_defs |
|
24 thm let_rec.bn_defs |
|
25 thm let_rec.perm_simps |
|
26 thm let_rec.eq_iff |
|
27 thm let_rec.fv_bn_eqvt |
|
28 thm let_rec.size_eqvt |
|
29 |
|
30 |
|
31 lemma Abs_lst_fcb2: |
|
32 fixes as bs :: "atom list" |
|
33 and x y :: "'b :: fs" |
|
34 and c::"'c::fs" |
|
35 assumes eq: "[as]lst. x = [bs]lst. y" |
|
36 and fcb1: "(set as) \<sharp>* f as x c" |
|
37 and fresh1: "set as \<sharp>* c" |
|
38 and fresh2: "set bs \<sharp>* c" |
|
39 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
|
40 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
|
41 shows "f as x c = f bs y c" |
|
42 proof - |
|
43 have "supp (as, x, c) supports (f as x c)" |
|
44 unfolding supports_def fresh_def[symmetric] |
|
45 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
|
46 then have fin1: "finite (supp (f as x c))" |
|
47 by (auto intro: supports_finite simp add: finite_supp) |
|
48 have "supp (bs, y, c) supports (f bs y c)" |
|
49 unfolding supports_def fresh_def[symmetric] |
|
50 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
|
51 then have fin2: "finite (supp (f bs y c))" |
|
52 by (auto intro: supports_finite simp add: finite_supp) |
|
53 obtain q::"perm" where |
|
54 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
55 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
56 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
57 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
58 fin1 fin2 |
|
59 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
60 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
61 also have "\<dots> = Abs_lst as x" |
|
62 by (simp only: fr2 perm_supp_eq) |
|
63 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
64 then obtain r::perm where |
|
65 qq1: "q \<bullet> x = r \<bullet> y" and |
|
66 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
67 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
68 apply(drule_tac sym) |
|
69 apply(simp only: Abs_eq_iff2 alphas) |
|
70 apply(erule exE) |
|
71 apply(erule conjE)+ |
|
72 apply(drule_tac x="p" in meta_spec) |
|
73 apply(simp add: set_eqvt) |
|
74 apply(blast) |
|
75 done |
|
76 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
|
77 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
|
78 by (simp add: permute_bool_def) |
|
79 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
80 apply(simp add: fresh_star_eqvt set_eqvt) |
|
81 apply(subst (asm) perm1) |
|
82 using inc fresh1 fr1 |
|
83 apply(auto simp add: fresh_star_def fresh_Pair) |
|
84 done |
|
85 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
86 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
|
87 apply(simp add: fresh_star_eqvt set_eqvt) |
|
88 apply(subst (asm) perm2[symmetric]) |
|
89 using qq3 fresh2 fr1 |
|
90 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
|
91 done |
|
92 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
93 have "f as x c = q \<bullet> (f as x c)" |
|
94 apply(rule perm_supp_eq[symmetric]) |
|
95 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
|
96 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
|
97 apply(rule perm1) |
|
98 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
|
99 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
|
100 also have "\<dots> = r \<bullet> (f bs y c)" |
|
101 apply(rule perm2[symmetric]) |
|
102 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
|
103 also have "... = f bs y c" |
|
104 apply(rule perm_supp_eq) |
|
105 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
|
106 finally show ?thesis by simp |
|
107 qed |
|
108 |
|
109 |
|
110 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
|
111 by (simp add: permute_pure) |
|
112 |
|
113 nominal_primrec |
|
114 height_trm :: "trm \<Rightarrow> nat" |
|
115 and height_bp :: "bp \<Rightarrow> nat" |
|
116 where |
|
117 "height_trm (Var x) = 1" |
|
118 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
119 | "height_trm (Lam v b) = 1 + (height_trm b)" |
|
120 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)" |
|
121 | "height_bp (Bp v t) = height_trm t" |
|
122 --"eqvt" |
|
123 apply (simp only: eqvt_def height_trm_height_bp_graph_def) |
|
124 apply (rule, perm_simp, rule, rule TrueI) |
|
125 --"completeness" |
|
126 apply (case_tac x) |
|
127 apply (case_tac a rule: let_rec.exhaust(1)) |
|
128 apply (auto)[4] |
|
129 apply (case_tac b rule: let_rec.exhaust(2)) |
|
130 apply blast |
|
131 apply(simp_all) |
|
132 apply (erule_tac c="()" in Abs_lst_fcb2) |
|
133 apply (simp_all add: fresh_star_def pure_fresh)[3] |
|
134 apply (simp add: eqvt_at_def) |
|
135 apply (simp add: eqvt_at_def) |
|
136 --"HERE" |
|
137 thm Abs_lst_fcb2 |
|
138 apply(rule Abs_lst_fcb2) |
|
139 --" does not fit the assumption " |
|
140 |
|
141 apply (drule_tac c="()" in Abs_lst_fcb2) |
|
142 prefer 6 |
|
143 apply(assumption) |
|
144 apply (drule_tac c="()" in Abs_lst_fcb2) |
|
145 apply (simp add: Abs_eq_iff2) |
|
146 apply (simp add: alphas) |
|
147 apply clarify |
|
148 apply (rule trans) |
|
149 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
150 apply (simp add: pure_supp fresh_star_def) |
|
151 apply (simp only: eqvts) |
|
152 apply (simp add: eqvt_at_def) |
|
153 done |
|
154 |
|
155 termination by lexicographic_order |
|
156 |
|
157 end |
|
158 |
|
159 |
|
160 |