|
1 theory Lambda |
|
2 imports "../Nominal/Nominal2" |
|
3 begin |
|
4 |
|
5 section {* Definitions for Lambda Terms *} |
|
6 |
|
7 text {* type of variables *} |
|
8 |
|
9 atom_decl name |
|
10 |
|
11 |
|
12 subsection {* Alpha-Equated Lambda Terms *} |
|
13 |
|
14 nominal_datatype lam = |
|
15 Var "name" |
|
16 | App "lam" "lam" |
|
17 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
|
18 |
|
19 |
|
20 text {* some automatically derived theorems *} |
|
21 |
|
22 thm lam.distinct |
|
23 thm lam.eq_iff |
|
24 thm lam.fresh |
|
25 thm lam.size |
|
26 thm lam.exhaust |
|
27 thm lam.strong_exhaust |
|
28 thm lam.induct |
|
29 thm lam.strong_induct |
|
30 |
|
31 |
|
32 subsection {* Height Function *} |
|
33 |
|
34 nominal_primrec |
|
35 height :: "lam \<Rightarrow> int" |
|
36 where |
|
37 "height (Var x) = 1" |
|
38 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
|
39 | "height (Lam [x].t) = height t + 1" |
|
40 apply(rule_tac y="x" in lam.exhaust) |
|
41 apply(auto simp add: lam.distinct lam.eq_iff) |
|
42 apply(simp add: Abs_eq_iff alphas) |
|
43 apply(clarify) |
|
44 apply(subst (4) supp_perm_eq[where p="p", symmetric]) |
|
45 apply(simp add: pure_supp fresh_star_def) |
|
46 apply(simp add: eqvt_at_def) |
|
47 done |
|
48 |
|
49 termination |
|
50 by (relation "measure size") (simp_all add: lam.size) |
|
51 |
|
52 |
|
53 subsection {* Capture-avoiding Substitution *} |
|
54 |
|
55 nominal_primrec |
|
56 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
|
57 where |
|
58 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
59 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
60 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
61 apply(auto simp add: lam.distinct lam.eq_iff) |
|
62 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
63 apply(blast)+ |
|
64 apply(simp add: fresh_star_def) |
|
65 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
|
66 apply(subst (asm) Abs_eq_iff2) |
|
67 apply(simp add: alphas atom_eqvt) |
|
68 apply(clarify) |
|
69 apply(rule trans) |
|
70 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
71 apply(rule fresh_star_supp_conv) |
|
72 apply(drule fresh_star_perm_set_conv) |
|
73 apply(simp add: finite_supp) |
|
74 apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))") |
|
75 apply(auto simp add: fresh_star_def)[1] |
|
76 apply(simp (no_asm) add: fresh_star_def) |
|
77 apply(rule conjI) |
|
78 apply(simp (no_asm) add: Abs_fresh_iff) |
|
79 apply(clarify) |
|
80 apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at) |
|
81 apply(simp add: finite_supp) |
|
82 apply(simp (no_asm_use) add: fresh_Pair) |
|
83 apply(simp add: Abs_fresh_iff) |
|
84 apply(simp) |
|
85 apply(simp add: Abs_fresh_iff) |
|
86 apply(subgoal_tac "p \<bullet> ya = ya") |
|
87 apply(subgoal_tac "p \<bullet> sa = sa") |
|
88 apply(simp add: atom_eqvt eqvt_at_def) |
|
89 apply(rule perm_supp_eq) |
|
90 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
91 apply(rule perm_supp_eq) |
|
92 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
|
93 apply(rule conjI) |
|
94 apply(simp add: Abs_fresh_iff) |
|
95 apply(drule sym) |
|
96 apply(simp add: Abs_fresh_iff) |
|
97 done |
|
98 |
|
99 termination |
|
100 by (relation "measure (\<lambda>(t,_,_). size t)") |
|
101 (simp_all add: lam.size) |
|
102 |
|
103 lemma subst_eqvt[eqvt]: |
|
104 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
|
105 by (induct t x s rule: subst.induct) (simp_all) |
|
106 |
|
107 |
|
108 subsection {* Single-Step Beta-Reduction *} |
|
109 |
|
110 inductive |
|
111 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80) |
|
112 where |
|
113 b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s" |
|
114 | b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2" |
|
115 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2" |
|
116 | b4[intro]: "App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]" |
|
117 |
|
118 |
|
119 |
|
120 |
|
121 end |
|
122 |
|
123 |
|
124 |