Skip to content

Commit c054a26

Browse files
jvanbrueggejvanbruegge
committed
Add data types with constructors
This mostly recycles code from the data branch where I used lists for applied constructors
1 parent 3828d5d commit c054a26

File tree

7 files changed

+445
-255
lines changed

7 files changed

+445
-255
lines changed

‎Defs.thy‎

Lines changed: 55 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
theory Defs
2-
imports Syntax Nominal2_Lemmas
2+
imports Syntax Nominal2_Lemmas "HOL-Library.Adhoc_Overloading"
33
begin
44

55
nominal_function isin :: "binder \<Rightarrow> \<Gamma> \<Rightarrow> bool" (infixr "\<in>" 80) where
@@ -27,28 +27,44 @@ proof goal_cases
2727
qed (auto simp: eqvt_def isin_graph_aux_def)
2828
nominal_termination (eqvt) by lexicographic_order
2929

30-
nominal_function
31-
is_value :: "term => bool"
32-
where
33-
"is_value (Var x) = False"
30+
nominal_function head_ctor :: "term \<Rightarrow> bool"
31+
and is_value :: "term => bool" where
32+
"head_ctor (Var _) = False"
33+
| "head_ctor (Lam _ _ _) = False"
34+
| "head_ctor (TyLam _ _ _) = False"
35+
| "head_ctor (App e1 e2) = (head_ctor e1 \<and> is_value e2)"
36+
| "head_ctor (TApp e _) = head_ctor e"
37+
| "head_ctor (Ctor _) = True"
38+
| "head_ctor (Let _ _ _ _) = False"
39+
40+
| "is_value (Var x) = False"
3441
| "is_value (\<lambda> x : \<tau> . e) = True"
3542
| "is_value (\<Lambda> a : k . e) = True"
36-
| "is_value (App e1 e2) = False"
37-
| "is_value (TyApp e \<tau>) = False"
38-
| "is_value Unit = True"
43+
| "is_value (App e1 e2) = (head_ctor e1 \<and> is_value e2)"
44+
| "is_value (TApp e \<tau>) = head_ctor e"
45+
| "is_value (Ctor _) = True"
3946
| "is_value (Let x \<tau> e1 e2) = False"
40-
apply (auto simp: eqvt_def is_value_graph_aux_def)
41-
using term.exhaust by blast
47+
proof goal_cases
48+
case (3 P x)
49+
then show ?case
50+
proof (cases x)
51+
case (Inl a)
52+
then show ?thesis using 3(1-7) by (cases a rule: term.exhaust) auto
53+
next
54+
case (Inr b)
55+
then show ?thesis using 3(8-14) by (cases b rule: term.exhaust) auto
56+
qed
57+
qed (auto simp: eqvt_def head_ctor_is_value_graph_aux_def)
4258
nominal_termination (eqvt) by lexicographic_order
4359

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])"
60+
nominal_function subst_term :: "term => term \<Rightarrow> var => term" where
61+
"subst_term (Var y) e x = (if x = y then e else Var y)"
62+
| "subst_term (App e1 e2) e x = App (subst_term e1 e x) (subst_term e2 e x)"
63+
| "subst_term (TApp e1 \<tau>) e x = TApp (subst_term e1 e x) \<tau>"
64+
| "subst_term (Ctor D) _ _ = Ctor D"
65+
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<lambda> y:\<tau>. e2) e x = (\<lambda> y:\<tau>. subst_term e2 e x)"
66+
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<Lambda> y:k. e2) e x = (\<Lambda> y:k. subst_term e2 e x)"
67+
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (Let y \<tau> e1 e2) e x = Let y \<tau> (subst_term e1 e x) (subst_term e2 e x)"
5268
proof (goal_cases)
5369
case (3 P x)
5470
then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
@@ -68,12 +84,12 @@ next
6884
qed (auto simp: eqvt_def subst_term_graph_aux_def)
6985
nominal_termination (eqvt) by lexicographic_order
7086

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])"
87+
nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" where
88+
"subst_type (TyData T) _ _ = TyData T"
89+
| "subst_type (TyVar b) \<tau> a = (if a=b then \<tau> else TyVar b)"
90+
| "subst_type TyArrow _ _ = TyArrow"
91+
| "subst_type (TyApp \<tau>1 \<tau>2) \<tau> a = TyApp (subst_type \<tau>1 \<tau> a) (subst_type \<tau>2 \<tau> a)"
92+
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_type (\<forall> b:k. \<sigma>) \<tau> a = (\<forall>b:k. subst_type \<sigma> \<tau> a)"
7793
proof goal_cases
7894
case (3 P x)
7995
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
@@ -87,14 +103,14 @@ next
87103
qed (auto simp: eqvt_def subst_type_graph_aux_def)
88104
nominal_termination (eqvt) by lexicographic_order
89105

90-
nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" ("_[_'/_]" [1000,0,0] 1000) where
106+
nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" where
91107
"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]"
108+
| "subst_term_type (Ctor D) _ _ = Ctor D"
109+
| "subst_term_type (App e1 e2) \<tau> a = App (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
110+
| "subst_term_type (TApp e \<tau>2) \<tau> a = TApp (subst_term_type e \<tau> a) (subst_type \<tau>2 \<tau> a)"
111+
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:(subst_type \<tau>' \<tau> a). subst_term_type e2 \<tau> a)"
112+
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. subst_term_type e2 \<tau> a)"
113+
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y (subst_type \<tau>' \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
98114
proof goal_cases
99115
case (3 P x)
100116
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
@@ -114,9 +130,9 @@ next
114130
qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
115131
nominal_termination (eqvt) by lexicographic_order
116132

117-
nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" ("_[_'/_]" [1000,0,0] 1000) where
133+
nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" where
118134
"subst_context [] _ _ = []"
119-
| "subst_context (BVar x \<tau> # \<Gamma>) \<tau>' a = BVar x \<tau>[\<tau>'/a] # subst_context \<Gamma> \<tau>' a"
135+
| "subst_context (BVar x \<tau> # \<Gamma>) \<tau>' a = BVar x (subst_type \<tau> \<tau>' a) # subst_context \<Gamma> \<tau>' a"
120136
| "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)"
121137
proof goal_cases
122138
case (3 P x)
@@ -129,4 +145,10 @@ proof goal_cases
129145
qed (auto simp: eqvt_def subst_context_graph_aux_def)
130146
nominal_termination (eqvt) by lexicographic_order
131147

148+
no_notation inverse_divide (infixl "'/" 70)
149+
consts subst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" ("_[_'/_]" [1000,0,0] 1000)
150+
151+
adhoc_overloading
152+
subst subst_term subst_type subst_term_type subst_context
153+
132154
end

‎Determinancy.thy‎

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,27 +2,36 @@ theory Determinancy
22
imports Typing Typing_Lemmas
33
begin
44

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"
5+
lemma unique_ty: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k1 ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<rbrakk> \<Longrightarrow> k1 = k2"
66
proof (nominal_induct \<tau> arbitrary: k1 k2 rule: \<tau>.strong_induct)
77
case (TyVar x)
88
then show ?case using isin_split isin_same(1) by blast
99
next
10-
case (TyConApp \<tau>1 \<tau>2)
10+
case (TyData x)
11+
then show ?case using axiom_isin_split axiom_isin_same(1) axioms_valid(2)[OF TyData(2)] by blast
12+
next
13+
case (TyApp \<tau>1 \<tau>2)
1114
then show ?case by fastforce
1215
next
1316
case (TyForall x1 x2a x3)
1417
then show ?case by (metis Ty_Forall_Inv_2)
1518
qed auto
1619

17-
lemma unique_tm: "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>1 ; \<Gamma> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
20+
lemma unique_tm: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; \<Gamma> , \<Delta> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
1821
proof (nominal_induct e avoiding: \<Gamma> \<tau>1 \<tau>2 rule: term.strong_induct)
1922
case (Var x)
2023
then show ?case using isin_split isin_same(2) by blast
2124
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
25+
case (App e1 e2)
26+
then show ?case by fastforce
27+
next
28+
case (TApp e1 \<tau>)
29+
obtain a1 k1 \<sigma>1 where 1: "\<Gamma> , \<Delta> \<turnstile> e1 : \<forall> a1:k1. \<sigma>1" "\<tau>1 = \<sigma>1[\<tau>/a1]" by (cases rule: Tm.cases[OF TApp(2)]) auto
30+
obtain a2 k2 \<sigma>2 where 2: "\<Gamma> , \<Delta> \<turnstile> e1 : \<forall> a2:k2. \<sigma>2" "\<tau>2 = \<sigma>2[\<tau>/a2]" by (cases rule: Tm.cases[OF TApp(3)]) auto
31+
show ?case using TApp(1)[OF 1(1) 2(1)] subst_type_same 1(2) 2(2) by simp
32+
next
33+
case (Ctor x)
34+
then show ?case using axiom_isin_split axiom_isin_same(2) axioms_valid(3)[OF Ctor(2)] by blast
2635
next
2736
case (Lam x \<tau> e)
2837
then show ?case by (metis T_Abs_Inv)
@@ -32,6 +41,6 @@ next
3241
next
3342
case (Let x \<tau> e1 e2)
3443
then show ?case using T_Let_Inv by blast
35-
qed fastforce+
44+
qed
3645

3746
end

‎Lemmas.thy‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,4 +134,7 @@ lemmas subst_subst = subst_subst_term subst_subst_type subst_subst_term_type sub
134134
lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
135135
by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
136136

137+
lemma head_ctor_is_value: "head_ctor e \<Longrightarrow> is_value e"
138+
by (induction e rule: term.induct) auto
139+
137140
end

‎Semantics.thy‎

Lines changed: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightar
1212

1313
| ST_SubstI: "Let x \<tau> e1 e2 \<longrightarrow> e2[e1/x]"
1414

15-
| ST_BetaTI: "TyApp (\<Lambda> a : k . e) \<tau> \<longrightarrow> e[\<tau>/a]"
15+
| ST_BetaTI: "TApp (\<Lambda> a : k . e) \<tau> \<longrightarrow> e[\<tau>/a]"
1616

17-
| ST_AppTI: "e1 \<longrightarrow> e2 \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
17+
| ST_AppTI: "e1 \<longrightarrow> e2 \<Longrightarrow> TApp e1 \<tau> \<longrightarrow> TApp e2 \<tau>"
1818
equivariance Step
1919
nominal_inductive Step .
2020

@@ -29,8 +29,32 @@ definition stuck :: "term \<Rightarrow> bool" where
2929
"stuck e \<equiv> \<not>is_value e \<and> beta_nf e"
3030

3131
lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
32-
apply (cases v rule: term.exhaust)
33-
using Step.cases beta_nf_def by fastforce+
32+
proof (induction v rule: term.induct)
33+
case (App e1 e2)
34+
show ?case
35+
proof (rule ccontr)
36+
assume "\<not>beta_nf (App e1 e2)"
37+
then obtain e' where "App e1 e2 \<longrightarrow> e'" using beta_nf_def by blast
38+
then show "False" using App head_ctor_is_value beta_nf_def by cases auto
39+
qed
40+
next
41+
case (TApp e \<tau>)
42+
show ?case
43+
proof (rule ccontr)
44+
assume "\<not>beta_nf (TApp e \<tau>)"
45+
then obtain e' where "TApp e \<tau> \<longrightarrow> e'" using beta_nf_def by blast
46+
then show "False" using TApp head_ctor_is_value beta_nf_def by cases auto
47+
qed
48+
next
49+
case (Ctor D)
50+
then show ?case using Step.cases beta_nf_def by fastforce
51+
next
52+
case (Lam x \<tau> e)
53+
then show ?case using Step.cases beta_nf_def by fastforce
54+
next
55+
case (TyLam a k e)
56+
then show ?case using Step.cases beta_nf_def by fastforce
57+
qed auto
3458

3559
lemma Step_deterministic: "\<lbrakk> e \<longrightarrow> e1 ; e \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> e1 = e2"
3660
proof (induction e e1 arbitrary: e2 rule: Step.induct)

‎Syntax.thy‎

Lines changed: 40 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -5,41 +5,71 @@ begin
55
atom_decl "var"
66
atom_decl "tyvar"
77

8+
atom_decl "data_name"
9+
atom_decl "ctor_name"
10+
811
nominal_datatype "\<kappa>" =
912
Star ("\<star>")
10-
| KArrow "\<kappa>" "\<kappa>"
13+
| KArrow "\<kappa>" "\<kappa>" (infixr "\<rightarrow>" 50)
1114

1215
nominal_datatype "\<tau>" =
13-
TyUnit
14-
| TyVar "tyvar"
15-
| TyArrow "\<tau>" "\<tau>" ("_ \<rightarrow> _" 50)
16-
| TyConApp "\<tau>" "\<tau>"
16+
TyVar "tyvar"
17+
| TyData "data_name"
18+
| TyArrow
19+
| TyApp "\<tau>" "\<tau>"
1720
| TyForall a::"tyvar" "\<kappa>" t::"\<tau>" binds a in t ("\<forall> _ : _ . _" 50)
1821

22+
abbreviation arrow_app :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>" (infixr "\<rightarrow>" 50) where
23+
"arrow_app \<tau>1 \<tau>2 \<equiv> TyApp (TyApp TyArrow \<tau>1) \<tau>2"
24+
1925
nominal_datatype "term" =
2026
Var "var"
2127
| App "term" "term"
22-
| TyApp "term" "\<tau>"
23-
| Unit
28+
| TApp "term" "\<tau>"
29+
| Ctor "ctor_name"
2430
| Lam x::"var" "\<tau>" e::"term" binds x in e ("\<lambda> _ : _ . _" 50)
2531
| TyLam a::"tyvar" "\<kappa>" e::"term" binds a in e ("\<Lambda> _ : _ . _" 50)
2632
| Let x::"var" "\<tau>" "term" e2::"term" binds x in e2
2733

2834
nominal_datatype "binder" =
29-
"BVar" "var" "\<tau>"
30-
| "BTyVar" "tyvar" "\<kappa>"
35+
BVar "var" "\<tau>"
36+
| BTyVar "tyvar" "\<kappa>"
37+
38+
nominal_datatype "axiom" =
39+
AxData "data_name" "\<kappa>"
40+
| AxCtor "ctor_name" "\<tau>"
3141

3242
type_synonym "\<Gamma>" = "binder list"
43+
type_synonym "\<Delta>" = "axiom list"
3344

3445
lemma no_vars_in_kinds[simp]: "atom (x :: var) \<sharp> (k :: \<kappa>)"
3546
by (induction k rule: \<kappa>.induct) auto
3647
lemma no_vars_in_ty[simp]: "atom (x :: var) \<sharp> (ty :: \<tau>)"
37-
by (induction ty rule: \<tau>.induct) auto
48+
by (induction rule: \<tau>.induct) auto
49+
lemma no_vars_in_axioms[simp]: "atom (x :: var) \<sharp> (\<Delta> :: \<Delta>)"
50+
proof (induction \<Delta>)
51+
case (Cons a \<Delta>)
52+
then show ?case by (cases a rule: axiom.exhaust) (auto simp: fresh_Cons)
53+
qed (rule fresh_Nil)
54+
55+
lemma perm_axioms_vars[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (\<Delta>::\<Delta>) = \<Delta>"
56+
using flip_fresh_fresh by force
57+
lemma perm_\<tau>_vars[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (\<tau>::\<tau>) = \<tau>"
58+
using flip_fresh_fresh by force
3859

3960
lemma no_tyvars_in_kinds[simp]: "atom (a :: tyvar) \<sharp> (k :: \<kappa>)"
4061
by (induction k rule: \<kappa>.induct) auto
4162

4263
lemma supp_empty_kinds[simp]: "supp (k :: \<kappa>) = {}"
4364
by (induction k rule: \<kappa>.induct) (auto simp: \<kappa>.supp)
4465

66+
lemma perm_data_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (T :: data_name) = T"
67+
using flip_fresh_fresh by force
68+
lemma perm_data_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (T :: data_name) = T"
69+
using flip_fresh_fresh by force
70+
lemma perm_ctor_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
71+
using flip_fresh_fresh by force
72+
lemma perm_ctor_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
73+
using flip_fresh_fresh by force
74+
4575
end

0 commit comments

Comments
 (0)