Skip to content

Commit 769e697

Browse files
jvanbrueggejvanbruegge
committed
Prepare the code for datatypes (#11)
2 parents 3bbe5bc + b2059f0 commit 769e697

File tree

12 files changed

+942
-459
lines changed

12 files changed

+942
-459
lines changed

‎BetaEquivalence.thy‎ renamed to ‎Confluence.thy‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
theory BetaEquivalence
1+
theory Confluence
22
imports Semantics
33
begin
44

@@ -73,13 +73,12 @@ proof -
7373
qed
7474
qed
7575

76-
lemma beta_equivalence: "\<lbrakk> e1 \<longrightarrow>* e1' ; e2 \<longrightarrow>* e2' ; e1 = e2 ; beta_nf e1' ; beta_nf e2' \<rbrakk> \<Longrightarrow> e1' = e2'"
77-
proof (induction e1 e1' arbitrary: e2 e2' rule: Steps_fwd_induct)
78-
case (refl x)
79-
then show ?case by simp
80-
next
81-
case (trans x y z)
82-
then show ?case by (metis Steps.simps Steps_path beta_same path.elims(2) Step_deterministic)
83-
qed
76+
lemma confluence: "\<lbrakk> a \<longrightarrow>* b ; a \<longrightarrow>* c \<rbrakk> \<Longrightarrow> \<exists>d. b \<longrightarrow>* d \<and> c \<longrightarrow>* d"
77+
apply (induction a b arbitrary: c rule: Steps_fwd_induct)
78+
using Steps.refl apply blast
79+
by (metis Step_deterministic Steps.trans Steps_concat Steps_path path.elims(2))
80+
81+
corollary beta_equivalence: "\<lbrakk> e1 \<longrightarrow>* e1' ; e2 \<longrightarrow>* e2' ; e1 = e2 ; beta_nf e1' ; beta_nf e2' \<rbrakk> \<Longrightarrow> e1' = e2'"
82+
using beta_same confluence by blast
8483

8584
end

‎Defs.thy‎

Lines changed: 57 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -41,78 +41,92 @@ where
4141
using term.exhaust by blast
4242
nominal_termination (eqvt) by lexicographic_order
4343

44-
(** substitutions *)
45-
nominal_function subst_term :: "term => var => term => term" where
46-
"subst_term e x (Var y) = (if x=y then e else Var y)"
47-
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (\<lambda> y : \<tau> . e2) = (Lam y \<tau> (subst_term e x e2))"
48-
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (\<Lambda> y : k . e2) = (\<Lambda> y : k . subst_term e x e2)"
49-
| "subst_term e x (App e1 e2) = (App (subst_term e x e1) (subst_term e x e2))"
50-
| "subst_term e x (TyApp e1 \<tau>) = (TyApp (subst_term e x e1) \<tau>)"
51-
| "subst_term _ _ Unit = Unit"
52-
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (Let y \<tau> e1 e2) = (Let y \<tau> (subst_term e x e1) (subst_term e x e2))"
53-
proof goal_cases
44+
nominal_function subst_term :: "term => term \<Rightarrow> var => term" ("_[_'/_]" [1000,0,0] 1000) where
45+
"(Var y)[e/x] = (if x = y then e else Var y)"
46+
| "(App e1 e2)[e/x] = App e1[e/x] e2[e/x]"
47+
| "(TyApp e1 \<tau>)[e/x] = TyApp e1[e/x] \<tau>"
48+
| "Unit[_/_] = Unit"
49+
| "atom y \<sharp> (e, x) \<Longrightarrow> (\<lambda> y:\<tau>. e2)[e/x] = (\<lambda> y:\<tau>. e2[e/x])"
50+
| "atom y \<sharp> (e, x) \<Longrightarrow> (\<Lambda> y:k. e2)[e/x] = (\<Lambda> y:k. e2[e/x])"
51+
| "atom y \<sharp> (e, x) \<Longrightarrow> (Let y \<tau> e1 e2)[e/x] = (Let y \<tau> e1[e/x] e2[e/x])"
52+
proof (goal_cases)
5453
case (3 P x)
55-
then obtain e y t where P: "x = (e, y, t)" by (metis prod.exhaust)
54+
then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
5655
then show ?case
5756
apply (cases t rule: term.strong_exhaust[of _ _ "(e, y)"])
58-
apply (auto simp: 3)
59-
using 3(2) 3(3) 3(7) P fresh_star_def by blast+
57+
apply (auto simp: 3)
58+
using 3(5-7) P fresh_star_def by blast+
6059
next
61-
case (11 y x e \<tau> e2 y' x' e' \<tau>' e2')
62-
then show ?case using Abs_sumC[OF 11(5) 11(6) 11(1) 11(2)] by fastforce
60+
case (26 y e x \<tau> e2 y' e' x' \<tau>' e2')
61+
then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
6362
next
64-
case (17 y x e e2 y' x' e' e2')
65-
then show ?case using Abs_sumC[OF 17(5) 17(6) 17(1) 17(2)] by fastforce
63+
case (29 y e x k e2 y' e' x' k' e2')
64+
then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
6665
next
67-
case (31 y x e \<tau> e1 e2 y' x' e' \<tau>' e1' e2')
68-
then show ?case using Abs_sumC[OF 31(9) 31(10) 31(2) 31(4)] by fastforce
66+
case (31 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
67+
then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
6968
qed (auto simp: eqvt_def subst_term_graph_aux_def)
7069
nominal_termination (eqvt) by lexicographic_order
7170

72-
nominal_function subst_type :: "\<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau> \<Rightarrow> \<tau>" where
73-
"subst_type _ _ TyUnit = TyUnit"
74-
| "subst_type \<tau> a (TyVar b) = (if a=b then \<tau> else TyVar b)"
75-
| "subst_type \<tau> a (TyArrow \<tau>1 \<tau>2) = TyArrow (subst_type \<tau> a \<tau>1) (subst_type \<tau> a \<tau>2)"
76-
| "subst_type \<tau> a (TyConApp \<tau>1 \<tau>2) = TyConApp (subst_type \<tau> a \<tau>1) (subst_type \<tau> a \<tau>2)"
77-
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_type \<tau> a (TyForall b k \<sigma>) = TyForall b k (subst_type \<tau> a \<sigma>)"
71+
nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" ("_[_'/_]" [1000,0,0] 1000) where
72+
"TyUnit[_/_] = TyUnit"
73+
| "(TyVar b)[\<tau>/a] = (if a=b then \<tau> else TyVar b)"
74+
| "(\<tau>1 \<rightarrow> \<tau>2)[\<tau>/a] = (\<tau>1[\<tau>/a] \<rightarrow> \<tau>2[\<tau>/a])"
75+
| "(TyConApp \<tau>1 \<tau>2)[\<tau>/a] = TyConApp \<tau>1[\<tau>/a] \<tau>2[\<tau>/a]"
76+
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> (\<forall> b:k. \<sigma>)[\<tau>/a] = (\<forall>b:k. \<sigma>[\<tau>/a])"
7877
proof goal_cases
7978
case (3 P x)
80-
then obtain \<tau> a t where P: "x = (\<tau>, a, t)" by (metis prod.exhaust)
79+
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
8180
then show ?case
8281
apply (cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
8382
apply (auto simp: 3)
8483
using 3(5) P fresh_star_def by blast
8584
next
8685
case (18 b \<tau> a k \<sigma> b' \<tau>' a' k' \<sigma>')
87-
then show ?case using Abs_sumC[OF 18(5) 18(6) 18(1) 18(2)] by fastforce
86+
then show ?case using Abs_sumC[OF 18(5,6,1,2)] by fastforce
8887
qed (auto simp: eqvt_def subst_type_graph_aux_def)
8988
nominal_termination (eqvt) by lexicographic_order
9089

91-
nominal_function subst_term_type :: "\<tau> \<Rightarrow> tyvar \<Rightarrow> term \<Rightarrow> term" where
92-
"subst_term_type _ _ (Var x) = Var x"
93-
| "subst_term_type _ _ Unit = Unit"
94-
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (\<lambda> y : \<tau>' . e2) = (Lam y (subst_type \<tau> a \<tau>') (subst_term_type \<tau> a e2))"
95-
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (\<Lambda> b : k . e2) = (TyLam b k (subst_term_type \<tau> a e2))"
96-
| "subst_term_type \<tau> a (App e1 e2) = App (subst_term_type \<tau> a e1) (subst_term_type \<tau> a e2)"
97-
| "subst_term_type \<tau> a (TyApp e \<tau>2) = TyApp (subst_term_type \<tau> a e) (subst_type \<tau> a \<tau>2)"
98-
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (Let y \<tau>' e1 e2) = Let y (subst_type \<tau> a \<tau>') (subst_term_type \<tau> a e1) (subst_term_type \<tau> a e2)"
90+
nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" ("_[_'/_]" [1000,0,0] 1000) where
91+
"subst_term_type (Var x) _ _ = Var x"
92+
| "subst_term_type Unit _ _ = Unit"
93+
| "subst_term_type (App e1 e2) \<tau> a = App e1[\<tau>/a] e2[\<tau>/a]"
94+
| "subst_term_type (TyApp e \<tau>2) \<tau> a = TyApp e[\<tau>/a] \<tau>2[\<tau>/a]"
95+
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:\<tau>'[\<tau>/a]. e2[\<tau>/a])"
96+
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. e2[\<tau>/a])"
97+
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y \<tau>'[\<tau>/a] e1[\<tau>/a] e2[\<tau>/a]"
9998
proof goal_cases
10099
case (3 P x)
101-
then obtain \<tau> a t where P: "x = (\<tau>, a, t)" by (metis prod.exhaust)
100+
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
102101
then show ?case
103102
apply (cases t rule: term.strong_exhaust[of _ _ "(\<tau>, a)"])
104103
using 3 P apply auto[4]
105-
using 3(3) 3(4) 3(7) P fresh_star_def by blast+
104+
using 3(5,6,7) P fresh_star_def by blast+
106105
next
107-
case (17 y \<tau> a \<tau>2 e y' \<tau>' a' \<tau>2' e')
108-
then show ?case using Abs_sumC[OF 17(5) 17(6) 17(1) 17(2)] by fastforce
106+
case (26 y \<tau> a \<tau>1 e2 y' \<tau>' a' \<tau>1' e2')
107+
then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
109108
next
110-
case (22 b \<tau> a e b' \<tau>' a' e')
111-
then show ?case using Abs_sumC[OF 22(5) 22(6) 22(1) 22(2)] by fastforce
109+
case (29 b \<tau> a k e2 b' \<tau>' a' k' e2')
110+
then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
112111
next
113-
case (31 y a \<tau> \<tau>2 e1 e2 y' a' \<tau>' \<tau>2' e1' e2')
114-
then show ?case using Abs_sumC[OF 31(9) 31(10) 31(2) 31(4)] by fastforce
112+
case (31 y \<tau> a \<tau>1 e1 e2 y' \<tau>' a' \<tau>1' e1' e2')
113+
then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
115114
qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
116115
nominal_termination (eqvt) by lexicographic_order
117116

117+
nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" ("_[_'/_]" [1000,0,0] 1000) where
118+
"subst_context [] _ _ = []"
119+
| "subst_context (BVar x \<tau> # \<Gamma>) \<tau>' a = BVar x \<tau>[\<tau>'/a] # subst_context \<Gamma> \<tau>' a"
120+
| "subst_context (BTyVar b k # \<Gamma>) \<tau>' a = (if a = b then subst_context \<Gamma> \<tau>' a else BTyVar b k # subst_context \<Gamma> \<tau>' a)"
121+
proof goal_cases
122+
case (3 P x)
123+
then obtain xs \<tau>' a where P: "x = (xs, \<tau>', a)" by (metis prod.exhaust)
124+
then show ?case using 3
125+
proof (cases xs)
126+
case (Cons a list)
127+
then show ?thesis using 3 P by (cases a rule: binder.exhaust) auto
128+
qed auto
129+
qed (auto simp: eqvt_def subst_context_graph_aux_def)
130+
nominal_termination (eqvt) by lexicographic_order
131+
118132
end

‎Determinancy.thy‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
theory Determinancy
2+
imports Typing Typing_Lemmas
3+
begin
4+
5+
lemma unique_ty: "\<lbrakk> \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k1 ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<rbrakk> \<Longrightarrow> k1 = k2"
6+
proof (nominal_induct \<tau> arbitrary: k1 k2 rule: \<tau>.strong_induct)
7+
case (TyVar x)
8+
then show ?case using isin_split isin_same(1) by blast
9+
next
10+
case (TyConApp \<tau>1 \<tau>2)
11+
then show ?case by fastforce
12+
next
13+
case (TyForall x1 x2a x3)
14+
then show ?case by (metis Ty_Forall_Inv_2)
15+
qed auto
16+
17+
lemma unique_tm: "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>1 ; \<Gamma> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
18+
proof (nominal_induct e avoiding: \<Gamma> \<tau>1 \<tau>2 rule: term.strong_induct)
19+
case (Var x)
20+
then show ?case using isin_split isin_same(2) by blast
21+
next
22+
case (TyApp e1 \<tau>)
23+
obtain a1 k1 \<sigma>1 where 1: "\<Gamma> \<turnstile> e1 : \<forall> a1:k1. \<sigma>1" "\<tau>1 = \<sigma>1[\<tau>/a1]" by (cases rule: Tm.cases[OF TyApp(2)]) auto
24+
obtain a2 k2 \<sigma>2 where 2: "\<Gamma> \<turnstile> e1 : \<forall> a2:k2. \<sigma>2" "\<tau>2 = \<sigma>2[\<tau>/a2]" by (cases rule: Tm.cases[OF TyApp(3)]) auto
25+
show ?case using TyApp(1)[OF 1(1) 2(1)] subst_type_same 1(2) 2(2) by simp
26+
next
27+
case (Lam x \<tau> e)
28+
then show ?case by (metis T_Abs_Inv)
29+
next
30+
case (TyLam a k e)
31+
then show ?case by (metis T_AbsT_Inv)
32+
next
33+
case (Let x \<tau> e1 e2)
34+
then show ?case using T_Let_Inv by blast
35+
qed fastforce+
36+
37+
end

0 commit comments

Comments
 (0)