1 theory Lambda |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 |
|
6 atom_decl name |
|
7 |
|
8 nominal_datatype lam = |
|
9 Var "name" |
|
10 | App "lam" "lam" |
|
11 | Lam x::"name" l::"lam" bind x in l |
|
12 |
|
13 thm lam.distinct |
|
14 thm lam.induct |
|
15 thm lam.exhaust lam.strong_exhaust |
|
16 thm lam.fv_defs |
|
17 thm lam.bn_defs |
|
18 thm lam.perm_simps |
|
19 thm lam.eq_iff |
|
20 thm lam.fv_bn_eqvt |
|
21 thm lam.size_eqvt |
|
22 |
|
23 |
|
24 section {* Typing *} |
|
25 |
|
26 nominal_datatype ty = |
|
27 TVar string |
|
28 | TFun ty ty ("_ \<rightarrow> _") |
|
29 |
|
30 lemma ty_fresh: |
|
31 fixes x::"name" |
|
32 and T::"ty" |
|
33 shows "atom x \<sharp> T" |
|
34 apply (nominal_induct T rule: ty.strong_induct) |
|
35 apply (simp_all add: ty.fresh pure_fresh) |
|
36 done |
|
37 |
|
38 inductive |
|
39 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
|
40 where |
|
41 v_Nil[intro]: "valid []" |
|
42 | v_Cons[intro]: "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)" |
|
43 |
|
44 inductive |
|
45 typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
|
46 where |
|
47 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
48 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
|
49 | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2" |
|
50 |
|
51 thm typing.intros |
|
52 thm typing.induct |
|
53 |
|
54 equivariance valid |
|
55 equivariance typing |
|
56 |
|
57 nominal_inductive typing |
|
58 avoids t_Lam: "x" |
|
59 by (simp_all add: fresh_star_def ty_fresh lam.fresh) |
|
60 |
|
61 |
|
62 thm typing.strong_induct |
|
63 |
|
64 abbreviation |
|
65 "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) |
|
66 where |
|
67 "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x, T) \<in> set \<Gamma>1 \<longrightarrow> (x, T) \<in> set \<Gamma>2" |
|
68 |
|
69 text {* Now it comes: The Weakening Lemma *} |
|
70 |
|
71 text {* |
|
72 The first version is, after setting up the induction, |
|
73 completely automatic except for use of atomize. *} |
|
74 |
|
75 lemma weakening_version2: |
|
76 fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list" |
|
77 and t ::"lam" |
|
78 and \<tau> ::"ty" |
|
79 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
80 and b: "valid \<Gamma>2" |
|
81 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
|
82 shows "\<Gamma>2 \<turnstile> t : T" |
|
83 using a b c |
|
84 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
|
85 case (t_Var \<Gamma>1 x T) (* variable case *) |
|
86 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
|
87 moreover |
|
88 have "valid \<Gamma>2" by fact |
|
89 moreover |
|
90 have "(x,T)\<in> set \<Gamma>1" by fact |
|
91 ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto |
|
92 next |
|
93 case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *) |
|
94 have vc: "atom x \<sharp> \<Gamma>2" by fact (* variable convention *) |
|
95 have ih: "\<lbrakk>valid ((x, T1) # \<Gamma>2); (x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2\<rbrakk> \<Longrightarrow> (x, T1) # \<Gamma>2 \<turnstile> t : T2" by fact |
|
96 have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact |
|
97 then have "(x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2" by simp |
|
98 moreover |
|
99 have "valid \<Gamma>2" by fact |
|
100 then have "valid ((x, T1) # \<Gamma>2)" using vc by (simp add: v_Cons) |
|
101 ultimately have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp |
|
102 with vc show "\<Gamma>2 \<turnstile> Lam x t : T1 \<rightarrow> T2" by auto |
|
103 qed (auto) (* app case *) |
|
104 |
|
105 lemma weakening_version1: |
|
106 fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list" |
|
107 assumes a: "\<Gamma>1 \<turnstile> t : T" |
|
108 and b: "valid \<Gamma>2" |
|
109 and c: "\<Gamma>1 \<subseteq> \<Gamma>2" |
|
110 shows "\<Gamma>2 \<turnstile> t : T" |
|
111 using a b c |
|
112 apply (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct) |
|
113 apply (auto | atomize)+ |
|
114 done |
|
115 |
|
116 |
|
117 inductive |
|
118 Acc :: "('a::pt \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
119 where |
|
120 AccI: "(\<And>y. R y x \<Longrightarrow> Acc R y) \<Longrightarrow> Acc R x" |
|
121 |
|
122 |
|
123 lemma Acc_eqvt [eqvt]: |
|
124 fixes p::"perm" |
|
125 assumes a: "Acc R x" |
|
126 shows "Acc (p \<bullet> R) (p \<bullet> x)" |
|
127 using a |
|
128 apply(induct) |
|
129 apply(rule AccI) |
|
130 apply(rotate_tac 1) |
|
131 apply(drule_tac x="-p \<bullet> y" in meta_spec) |
|
132 apply(simp) |
|
133 apply(drule meta_mp) |
|
134 apply(rule_tac p="p" in permute_boolE) |
|
135 apply(perm_simp add: permute_minus_cancel) |
|
136 apply(assumption) |
|
137 apply(assumption) |
|
138 done |
|
139 |
|
140 |
|
141 nominal_inductive Acc . |
|
142 |
|
143 thm Acc.strong_induct |
|
144 |
|
145 |
|
146 end |
|
147 |
|
148 |
|
149 |
|