1 theory Lambda |
|
2 imports "../Nominal/Nominal2" |
|
3 begin |
|
4 |
|
5 section {* Definitions for Lambda Terms *} |
|
6 |
|
7 |
|
8 text {* type of variables *} |
|
9 |
|
10 atom_decl name |
|
11 |
|
12 |
|
13 subsection {* Alpha-Equated Lambda Terms *} |
|
14 |
|
15 nominal_datatype lam = |
|
16 Var "name" |
|
17 | App "lam" "lam" |
|
18 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
19 |
|
20 |
|
21 text {* some automatically derived theorems *} |
|
22 |
|
23 thm lam.distinct |
|
24 thm lam.eq_iff |
|
25 thm lam.fresh |
|
26 thm lam.size |
|
27 thm lam.exhaust |
|
28 thm lam.strong_exhaust |
|
29 thm lam.induct |
|
30 thm lam.strong_induct |
|
31 |
|
32 |
|
33 subsection {* Height Function *} |
|
34 |
|
35 nominal_primrec |
|
36 height :: "lam \<Rightarrow> int" |
|
37 where |
|
38 "height (Var x) = 1" |
|
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
|
40 | "height (Lam [x].t) = height t + 1" |
|
41 apply(simp add: eqvt_def height_graph_def) |
|
42 apply (rule, perm_simp, rule) |
|
43 apply(rule TrueI) |
|
44 apply(rule_tac y="x" in lam.exhaust) |
|
45 apply(auto) |
|
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
|
48 done |
|
49 |
|
50 termination (eqvt) |
|
51 by lexicographic_order |
|
52 |
|
53 |
|
54 subsection {* Capture-Avoiding Substitution *} |
|
55 |
|
56 nominal_primrec |
|
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
|
58 where |
|
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
62 unfolding eqvt_def subst_graph_def |
|
63 apply(rule, perm_simp, rule) |
|
64 apply(rule TrueI) |
|
65 apply(auto) |
|
66 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
67 apply(blast)+ |
|
68 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
|
69 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
70 apply(simp_all add: Abs_fresh_iff) |
|
71 apply(simp add: fresh_star_def fresh_Pair) |
|
72 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
73 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
74 done |
|
75 |
|
76 termination (eqvt) |
|
77 by lexicographic_order |
|
78 |
|
79 lemma fresh_fact: |
|
80 assumes a: "atom z \<sharp> s" |
|
81 and b: "z = y \<or> atom z \<sharp> t" |
|
82 shows "atom z \<sharp> t[y ::= s]" |
|
83 using a b |
|
84 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
|
85 (auto simp add: lam.fresh fresh_at_base) |
|
86 |
|
87 |
|
88 end |
|
89 |
|
90 |
|
91 |
|