|
1 header {* Definition of Lambda terms and convertibility *} |
|
2 |
|
3 theory LambdaTerms imports "../../Nominal2" begin |
|
4 |
|
5 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x" |
|
6 unfolding fresh_def by blast |
|
7 |
|
8 atom_decl var |
|
9 |
|
10 nominal_datatype lam = |
|
11 Var "var" |
|
12 | App "lam" "lam" |
|
13 | Lam x::"var" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
14 |
|
15 notation |
|
16 App (infixl "\<cdot>" 98) and |
|
17 Lam ("\<integral> _. _" [97, 97] 99) |
|
18 |
|
19 nominal_primrec |
|
20 subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
21 where |
|
22 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
23 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])" |
|
24 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])" |
|
25 proof auto |
|
26 fix a b :: lam and aa :: var and P |
|
27 assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P" |
|
28 "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P" |
|
29 "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P" |
|
30 then show "P" |
|
31 by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
32 (blast, blast, simp add: fresh_star_def) |
|
33 next |
|
34 fix x :: var and t and xa :: var and ya sa ta |
|
35 assume *: "eqvt_at subst_sumC (t, ya, sa)" |
|
36 "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)" |
|
37 "[[atom x]]lst. t = [[atom xa]]lst. ta" |
|
38 then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)" |
|
39 apply - |
|
40 apply (erule Abs_lst1_fcb) |
|
41 apply(simp (no_asm) add: Abs_fresh_iff) |
|
42 apply(drule_tac a="atom xa" in fresh_eqvt_at) |
|
43 apply(simp add: finite_supp) |
|
44 apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff) |
|
45 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
|
46 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
|
47 apply(simp add: atom_eqvt eqvt_at_def) |
|
48 apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+ |
|
49 done |
|
50 next |
|
51 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
|
52 by (rule, perm_simp, rule) |
|
53 qed |
|
54 |
|
55 termination (eqvt) by lexicographic_order |
|
56 |
|
57 lemma forget[simp]: |
|
58 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
|
59 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
|
60 (auto simp add: lam.fresh fresh_at_base) |
|
61 |
|
62 lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t" |
|
63 by (simp add: fresh_def) |
|
64 |
|
65 lemma subst_id[simp]: "M [x ::= Var x] = M" |
|
66 by (rule_tac lam="M" and c="x" in lam.strong_induct) |
|
67 (simp_all add: fresh_star_def lam.fresh fresh_Pair) |
|
68 |
|
69 inductive |
|
70 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80) |
|
71 where |
|
72 bI: "(\<integral>x. M) \<cdot> N \<approx> M[x ::= N]" |
|
73 | b1: "M \<approx> M" |
|
74 | b2: "M \<approx> N \<Longrightarrow> N \<approx> M" |
|
75 | b3: "M \<approx> N \<Longrightarrow> N \<approx> L \<Longrightarrow> M \<approx> L" |
|
76 | b4: "M \<approx> N \<Longrightarrow> Z \<cdot> M \<approx> Z \<cdot> N" |
|
77 | b5: "M \<approx> N \<Longrightarrow> M \<cdot> Z \<approx> N \<cdot> Z" |
|
78 | b6: "M \<approx> N \<Longrightarrow> \<integral>x. M \<approx> \<integral>x. N" |
|
79 |
|
80 lemmas [trans] = b3 |
|
81 equivariance beta |
|
82 |
|
83 end |