10 |
10 |
11 nominal_datatype lam = Var "name" |
11 nominal_datatype lam = Var "name" |
12 | App "lam" "lam" |
12 | App "lam" "lam" |
13 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
13 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
14 |
14 |
15 text {* definition of the height-function by "structural recursion" ;o) *} |
15 text {* definition of the height-function *} |
16 |
16 |
17 constdefs |
17 consts |
18 height_Var :: "name \<Rightarrow> int" |
18 height :: "lam \<Rightarrow> int" |
19 "height_Var \<equiv> \<lambda>_. 1" |
|
20 |
|
21 height_App :: "lam\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int\<Rightarrow>int" |
|
22 "height_App \<equiv> \<lambda>_ _ n1 n2. (max n1 n2)+1" |
|
23 |
19 |
24 height_Lam :: "name\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int" |
20 nominal_primrec |
25 "height_Lam \<equiv> \<lambda>_ _ n. n+1" |
21 "height (Var x) = 1" |
|
22 "height (App t1 t2) = (max (height t1) (height t2)) + 1" |
|
23 "height (Lam [a].t) = (height t) + 1" |
|
24 apply(finite_guess add: perm_int_def)+ |
|
25 apply(rule TrueI)+ |
|
26 apply(simp add: fresh_int) |
|
27 apply(fresh_guess add: perm_int_def)+ |
|
28 done |
26 |
29 |
27 height :: "lam \<Rightarrow> int" |
30 text {* definition of capture-avoiding substitution *} |
28 "height \<equiv> lam_rec height_Var height_App height_Lam" |
|
29 |
31 |
30 text {* show that height is a function *} |
32 lemma eq_eqvt: |
31 lemma fin_supp_height: |
33 fixes pi::"name prm" |
32 shows "finite ((supp height_Var)::name set)" |
34 and x::"'a::pt_name" |
33 and "finite ((supp height_App)::name set)" |
35 shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))" |
34 and "finite ((supp height_Lam)::name set)" |
36 apply(simp add: perm_bool perm_bij) |
35 by (finite_guess add: height_Var_def height_App_def height_Lam_def perm_int_def fs_name1)+ |
37 done |
36 |
38 |
37 lemma fcb_height_Lam: |
39 consts |
38 assumes fr: "a\<sharp>height_Lam" |
40 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
39 shows "a\<sharp>height_Lam a t n" |
|
40 apply(simp add: height_Lam_def perm_int_def fresh_def supp_int) |
|
41 done |
|
42 |
41 |
43 text {* derive the characteristic equations for height from the iteration combinator *} |
42 nominal_primrec |
44 |
43 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
45 lemmas lam_recs = lam.recs[where P="\<lambda>_. True" and z="()", simplified] |
44 "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
46 |
45 "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
47 lemma height[simp]: |
46 apply(finite_guess add: eq_eqvt perm_if fs_name1)+ |
48 shows "height (Var c) = 1" |
47 apply(rule TrueI)+ |
49 and "height (App t1 t2) = (max (height t1) (height t2))+1" |
48 apply(simp add: abs_fresh) |
50 and "height (Lam [a].t) = (height t)+1" |
49 apply(fresh_guess add: eq_eqvt perm_if fs_name1)+ |
51 apply(simp add: height_def) |
|
52 apply(simp add: lam_recs fin_supp_height fcb_height_Lam supp_unit) |
|
53 apply(simp add: height_Var_def) |
|
54 apply(simp add: height_def) |
|
55 apply(simp add: lam_recs fin_supp_height fcb_height_Lam supp_unit) |
|
56 apply(simp add: height_App_def) |
|
57 apply(simp add: height_def) |
|
58 apply(rule trans) |
|
59 apply(rule lam_recs) |
|
60 apply(rule fin_supp_height)+ |
|
61 apply(simp add: supp_unit) |
|
62 apply(rule fcb_height_Lam) |
|
63 apply(assumption) |
|
64 apply(fresh_guess add: height_Var_def perm_int_def) |
|
65 apply(fresh_guess add: height_App_def perm_int_def) |
|
66 apply(fresh_guess add: height_Lam_def perm_int_def) |
|
67 apply(simp add: height_Lam_def) |
|
68 done |
|
69 |
|
70 text {* define capture-avoiding substitution *} |
|
71 |
|
72 constdefs |
|
73 subst_Var :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam" |
|
74 "subst_Var x t' \<equiv> \<lambda>y. (if y=x then t' else (Var y))" |
|
75 |
|
76 subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
77 "subst_App x t' \<equiv> \<lambda>_ _ r1 r2. App r1 r2" |
|
78 |
|
79 subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
80 "subst_Lam x t' \<equiv> \<lambda>a _ r. Lam [a].r" |
|
81 |
|
82 subst_lam :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
|
83 "t[x::=t'] \<equiv> (lam_rec (subst_Var x t') (subst_App x t') (subst_Lam x t')) t" |
|
84 |
|
85 lemma supports_subst_Var: |
|
86 shows "((supp (x,t))::name set) supports (subst_Var x t)" |
|
87 apply(supports_simp add: subst_Var_def) |
|
88 apply(rule impI) |
|
89 apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) |
|
90 apply(perm_simp) |
|
91 done |
|
92 |
|
93 lemma fin_supp_subst: |
|
94 shows "finite ((supp (subst_Var x t))::name set)" |
|
95 and "finite ((supp (subst_App x t))::name set)" |
|
96 and "finite ((supp (subst_Lam x t))::name set)" |
|
97 proof - |
|
98 case goal1 |
|
99 have f: "finite ((supp (x,t))::name set)" by (simp add: fs_name1) |
|
100 then have "supp (subst_Var x t) \<subseteq> ((supp (x,t))::name set)" |
|
101 using supp_is_subset[OF supports_subst_Var] by simp |
|
102 then show "finite ((supp (subst_Var x t))::name set)" using f by (simp add: finite_subset) |
|
103 qed (finite_guess add: subst_App_def subst_Lam_def fs_name1)+ |
|
104 |
|
105 lemma fcb_subst_Lam: |
|
106 assumes fr: "a\<sharp>(subst_Lam y t')" |
|
107 shows "a\<sharp>(subst_Lam y t') a t r" |
|
108 by (simp add: subst_Lam_def abs_fresh) |
|
109 |
|
110 lemma subst_lam[simp]: |
|
111 shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
112 and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
113 and "\<lbrakk>a\<sharp>y; a\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [a].t)[y::=t'] = Lam [a].(t[y::=t'])" |
|
114 apply(unfold subst_lam_def) |
|
115 apply(simp add: lam_recs fin_supp_subst fcb_subst_Lam supp_unit) |
|
116 apply(simp add: subst_Var_def) |
|
117 apply(simp add: lam_recs fin_supp_subst fcb_subst_Lam supp_unit) |
|
118 apply(simp only: subst_App_def) |
|
119 apply(rule trans) |
|
120 apply(rule lam_recs) |
|
121 apply(rule fin_supp_subst)+ |
|
122 apply(simp add: supp_unit) |
|
123 apply(rule fcb_subst_Lam) |
|
124 apply(assumption) |
|
125 apply(rule supports_fresh, rule supports_subst_Var, simp add: fs_name1, simp add: fresh_def supp_prod) |
|
126 apply(fresh_guess add: fresh_prod subst_App_def fs_name1) |
|
127 apply(fresh_guess add: fresh_prod subst_Lam_def fs_name1) |
|
128 apply(simp add: subst_Lam_def) |
|
129 done |
50 done |
130 |
51 |
131 text{* the next lemma is needed in the Var-case of the theorem *} |
52 text{* the next lemma is needed in the Var-case of the theorem *} |
132 |
53 |
133 lemma height_ge_one: |
54 lemma height_ge_one: |
134 shows "1 \<le> (height e)" |
55 shows "1 \<le> (height e)" |
135 by (nominal_induct e rule: lam.induct) |
56 by (nominal_induct e rule: lam.induct) |
136 (simp | arith)+ |
57 (simp | arith)+ |
137 |
58 |
138 text {* unlike the proplem suggested by Wang, however, the |
59 text {* unlike the proplem suggested by Wang, however, the |
139 theorem is formulated here entirely by using functions *} |
60 theorem is here formulated here entirely by using |
|
61 functions *} |
140 |
62 |
141 theorem height_subst: |
63 theorem height_subst: |
142 shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))" |
64 shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))" |
143 proof (nominal_induct e avoiding: x e' rule: lam.induct) |
65 proof (nominal_induct e avoiding: x e' rule: lam.induct) |
144 case (Var y) |
66 case (Var y) |