Skip to content

Commit 7be5d6d

Browse files
jvanbrueggejvanbruegge
committed
WIP
1 parent 9b53bd3 commit 7be5d6d

File tree

3 files changed

+120
-10
lines changed

3 files changed

+120
-10
lines changed

‎Defs.thy‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,12 @@ nominal_function zip_with :: "('a::pt \<Rightarrow> 'b::pt \<Rightarrow> 'c::pt)
215215
| "zip_with f (a#as) (b#bs) = f a b # zip_with f as bs"
216216
proof goal_cases
217217
case (3 P x)
218-
then show ?case sorry
218+
then obtain f xs ys where P: "x = (f, xs, ys)" by (metis prod.exhaust)
219+
then show ?case using 3
220+
proof (cases xs)
221+
case (Cons a list)
222+
then show ?thesis using 3 P by (cases ys) auto
223+
qed simp
219224
qed (auto simp: eqvt_def zip_with_graph_aux_def)
220225
nominal_termination (eqvt) by lexicographic_order
221226

‎Defs2.thy‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
theory Defs2
2+
imports Lemmas
3+
begin
4+
5+
nominal_function ctor_data_app_subst :: "\<tau> \<Rightarrow> bool" where
6+
"ctor_data_app_subst (TyVar _) = False"
7+
| "ctor_data_app_subst (TyData _) = True"
8+
| "ctor_data_app_subst TyArrow = False"
9+
| "ctor_data_app_subst (TyApp \<tau>1 _) = ctor_data_app_subst \<tau>1"
10+
| "ctor_data_app_subst (TyForall _ _ _) = False"
11+
proof goal_cases
12+
case (3 P x)
13+
then show ?case by (cases x rule: \<tau>.exhaust) auto
14+
qed (auto simp: eqvt_def ctor_data_app_subst_graph_aux_def)
15+
nominal_termination (eqvt) by lexicographic_order
16+
17+
nominal_function ctor_args :: "\<tau> \<Rightarrow> \<tau> list option" where
18+
"ctor_args (TyVar _) = None"
19+
| "ctor_args (TyData T) = Some []"
20+
| "ctor_args TyArrow = None"
21+
| "ctor_args (TyApp (TyApp TyArrow \<tau>1) \<tau>2) = (case ctor_args \<tau>2 of
22+
Some tys \<Rightarrow> Some (\<tau>1#tys)
23+
| None \<Rightarrow> None)"
24+
| "ctor_args (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2) = (if ctor_data_app_subst (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2) then Some [] else None)"
25+
| "ctor_args (TyApp (TyApp (TyData T) \<tau>1) \<tau>2) = (if ctor_data_app_subst (TyApp (TyApp (TyData T) \<tau>1) \<tau>2) then Some [] else None)"
26+
| "ctor_args (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2) = (if ctor_data_app_subst (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2) then Some [] else None)"
27+
| "ctor_args (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2) = (if ctor_data_app_subst (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2) then Some [] else None)"
28+
| "ctor_args (TyApp (TyVar a) \<tau>2) = (if ctor_data_app_subst (TyApp (TyVar a) \<tau>2) then Some [] else None)"
29+
| "ctor_args (TyApp (TyData T) \<tau>2) = (if ctor_data_app_subst (TyApp (TyData T) \<tau>2) then Some [] else None)"
30+
| "ctor_args (TyApp TyArrow \<tau>2) = (if ctor_data_app_subst (TyApp TyArrow \<tau>2) then Some [] else None)"
31+
| "ctor_args (TyApp (TyForall a k e) \<tau>2) = (if ctor_data_app_subst (TyApp (TyForall a k e) \<tau>2) then Some [] else None)"
32+
| "ctor_args (TyForall _ _ _) = None"
33+
proof goal_cases
34+
case 1
35+
then show ?case by (auto simp: eqvt_def ctor_args_graph_aux_def split!: option.splits)
36+
next
37+
case (3 P x)
38+
then show ?case
39+
proof (cases x rule: \<tau>.exhaust)
40+
case outer: (TyApp \<tau>1 \<tau>2)
41+
then show ?thesis using 3
42+
proof (cases \<tau>1 rule: \<tau>.exhaust)
43+
case (TyApp \<sigma>1 \<sigma>2)
44+
then show ?thesis using outer 3 by (cases \<sigma>1 rule: \<tau>.exhaust) auto
45+
qed auto
46+
qed auto
47+
qed auto
48+
nominal_termination (eqvt) by lexicographic_order
49+
50+
nominal_function subst_ctor :: "\<tau> \<Rightarrow> \<tau> list \<Rightarrow> \<tau> list option" where
51+
"subst_ctor (TyVar _) _ = None"
52+
| "subst_ctor TyArrow _ = None"
53+
| "subst_ctor (TyData _) [] = Some []"
54+
| "subst_ctor (TyData _) (_#_) = None"
55+
| "subst_ctor (TyApp \<tau>1 \<tau>2) [] = ctor_args (TyApp \<tau>1 \<tau>2)"
56+
| "subst_ctor (TyApp _ _) (_#_) = None"
57+
| "subst_ctor (TyForall _ _ _) [] = None"
58+
| "subst_ctor (TyForall a _ e) (\<tau>#\<tau>s) = subst_ctor e[\<tau>/a] \<tau>s"
59+
proof goal_cases
60+
case (3 P x)
61+
then obtain t xs where P: "x = (t, xs)" by fastforce
62+
then show ?case using 3
63+
proof (cases t rule: \<tau>.exhaust)
64+
case TyData
65+
then show ?thesis using P 3 by (cases xs) auto
66+
next
67+
case TyApp
68+
then show ?thesis using P 3 by (cases xs) auto
69+
next
70+
case TyForall
71+
then show ?thesis using P 3 by (cases xs) auto
72+
qed auto
73+
next
74+
case (39 a k e \<tau> \<tau>s a' k' e' \<tau>' \<tau>s')
75+
then show ?case by (metis Pair_inject \<tau>.eq_iff(5) list.inject subst_same(2))
76+
qed (auto simp: eqvt_def subst_ctor_graph_aux_def)
77+
nominal_termination (eqvt) by lexicographic_order
78+
79+
end

‎Typing.thy‎

Lines changed: 35 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
theory Typing
2-
imports Syntax Defs Lemmas
2+
imports Syntax Defs Defs2 Lemmas
33
begin
44

55
no_notation Set.member ("(_/ : _)" [51, 51] 50)
@@ -12,7 +12,7 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
1212

1313
| Ax_Data: "\<lbrakk> \<turnstile> \<Delta> ; atom T \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxData T \<kappa> # \<Delta>"
1414

15-
| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some (T, ks, tys) ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
15+
| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some (T, ks) ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
1616

1717
(* ------------------------------ *)
1818

@@ -55,12 +55,13 @@ inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow
5555
| Tm_Case: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; head_data \<tau>1 = Some (T, \<sigma>s) ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ;
5656
exhaustive alts \<Delta> T ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Case e alts : \<tau>"
5757

58-
| Alts_Nil: "Alts _ _ _ _ _ ANil _"
58+
| Alts_Nil: "Alts \<Gamma> _ _ _ _ ANil _"
5959

6060
| Alts_Var: "\<lbrakk> BVar x \<tau>1#\<Gamma>, \<Delta> \<turnstile> e : \<tau> ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<rbrakk> \<Longrightarrow> Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 (ACons (MatchVar x e) alts) \<tau>"
6161

62-
| Alts_Ctor: "\<lbrakk> AxCtor K cty \<in> set \<Delta> ; ctor_type cty = Some (T, ks, args) ; length ks = length tys ;
63-
length args = length vals ; (zip_with BVar vals args) @ (zip_with BTyVar tys ks) @ \<Gamma>, \<Delta> \<turnstile> e : \<tau> ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau>
62+
| Alts_Ctor: "\<lbrakk> AxCtor K cty \<in> set \<Delta> ; ctor_type cty = Some (T, ks) ; length ks = length tys ;
63+
subst_ctor cty \<sigma>s = Some args ; length args = length vals ;
64+
zip_with BVar vals args @ zip_with BTyVar tys ks @ \<Gamma>, \<Delta> \<turnstile> e : \<tau> ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau>
6465
\<rbrakk> \<Longrightarrow> Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 (ACons (MatchCtor K tys vals e) alts) \<tau>"
6566

6667
equivariance Tm
@@ -101,6 +102,20 @@ lemma Ty_induct[consumes 1, case_names Var App Data Arrow Forall]:
101102
shows "P \<Gamma> \<Delta> \<tau> \<kappa>"
102103
using Ax_Ctx_Ty.inducts(3)[OF assms(1), of "\<lambda>a. True" P "\<lambda>a b. True"] assms(2-6) by simp
103104

105+
lemma Tm_induct[consumes 1, case_names Var Abs App TAbs TApp Ctor Let Case]:
106+
fixes P::"\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow> \<tau> \<Rightarrow> bool"
107+
assumes "\<Gamma> , \<Delta> \<turnstile> e : \<tau>"
108+
and "\<And>\<Gamma> \<Delta> x \<tau>. \<lbrakk> \<Delta> \<turnstile> \<Gamma> ; BVar x \<tau> \<in> \<Gamma> \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (Var x) \<tau>"
109+
and "\<And>x \<tau>1 \<Gamma> \<Delta> e \<tau>2. \<lbrakk> BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e : \<tau>2 ; P (BVar x \<tau>1 # \<Gamma>) \<Delta> e \<tau>2 \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (\<lambda> x : \<tau>1 . e) (\<tau>1 \<rightarrow> \<tau>2)"
110+
and "\<And>\<Gamma> \<Delta> e1 \<tau>1 \<tau>2 e2. \<lbrakk> \<Gamma> , \<Delta> \<turnstile> e1 : \<tau>1 \<rightarrow> \<tau>2 ; P \<Gamma> \<Delta> e1 (\<tau>1 \<rightarrow> \<tau>2) ; \<Gamma> , \<Delta> \<turnstile> e2 : \<tau>1 ; P \<Gamma> \<Delta> e2 \<tau>1 \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (App e1 e2) \<tau>2"
111+
and "\<And>a k \<Gamma> \<Delta> e \<sigma>. \<lbrakk> BTyVar a k # \<Gamma> , \<Delta> \<turnstile> e : \<sigma> ; P (BTyVar a k # \<Gamma>) \<Delta> e \<sigma> \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (\<Lambda> a : k . e) (\<forall> a : k . \<sigma>)"
112+
and "\<And>\<Gamma> \<Delta> e a k \<sigma> \<tau>. \<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<forall> a : k . \<sigma> ; P \<Gamma> \<Delta> e (\<forall> a : k . \<sigma>) ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (TApp e \<tau>) \<sigma>[\<tau>/a]"
113+
and "\<And>\<Delta> \<Gamma> D \<tau>. \<lbrakk> \<Delta> \<turnstile> \<Gamma> ; AxCtor D \<tau> \<in> set \<Delta> \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (Ctor D) \<tau>"
114+
and "\<And>\<Gamma> \<Delta> e1 \<tau>1 x e2 \<tau>2. \<lbrakk> \<Gamma> , \<Delta> \<turnstile> e1 : \<tau>1 ; P \<Gamma> \<Delta> e1 \<tau>1 ; BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e2 : \<tau>2 ; P (BVar x \<tau>1 # \<Gamma>) \<Delta> e2 \<tau>2 \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (Let x \<tau>1 e1 e2) \<tau>2"
115+
and "\<And>\<Gamma> \<Delta> e \<tau>1 T \<sigma>s \<tau> alts. \<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; P \<Gamma> \<Delta> e \<tau>1 ; head_data \<tau>1 = Some (T, \<sigma>s) ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; exhaustive alts \<Delta> T ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<rbrakk> \<Longrightarrow> P \<Gamma> \<Delta> (Case e alts) \<tau>"
116+
shows "P \<Gamma> \<Delta> e \<tau>"
117+
using Tm_Alts.inducts(1)[OF assms(1), of _ "\<lambda>_ _ _ _ _ _ _. True"] assms(2-9) by auto
118+
104119
(* axiom validity *)
105120
lemma axioms_valid_aux:
106121
shows "\<Delta> \<turnstile> \<Gamma> \<longrightarrow> \<turnstile> \<Delta>"
@@ -115,7 +130,7 @@ lemma axioms_valid_context: "\<Delta> \<turnstile> \<Gamma> \<Longrightarrow> \<
115130
lemma axioms_valid_ty: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k \<Longrightarrow> \<turnstile> \<Delta>"
116131
using axioms_valid_aux by simp
117132
lemma axioms_valid_tm: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longrightarrow> \<turnstile> \<Delta>"
118-
by (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct) (auto simp: axioms_valid_context axioms_valid_ty)
133+
by (induction \<Gamma> \<Delta> e \<tau> rule: Tm_induct) (auto simp: axioms_valid_context axioms_valid_ty)
119134
lemmas axioms_valid = axioms_valid_context axioms_valid_ty axioms_valid_tm
120135

121136
lemma Ctx_Ty_induct_split[case_names Ctx_Empty Ctx_TyVar Ctx_Var Ty_Var Ty_App Ty_Data Ty_Arrow Ty_Forall]:
@@ -184,7 +199,7 @@ qed
184199
lemma context_valid_ty: "\<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<kappa> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>"
185200
by (induction \<Gamma> \<Delta> \<tau> \<kappa> rule: Ty_induct) auto
186201
lemma context_valid_tm: "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<Longrightarrow> \<Delta> \<turnstile> \<Gamma>"
187-
by (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct) (auto simp: context_valid_ty)
202+
by (induction \<Gamma> \<Delta> e \<tau> rule: Tm_induct) (auto simp: context_valid_ty)
188203
lemmas context_valid = context_valid_ty context_valid_tm
189204

190205
(* \<lbrakk> \<Gamma> \<turnstile> e : t ; atom x \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom x \<sharp> e *)
@@ -194,10 +209,21 @@ proof (induction \<Gamma> \<Delta> \<tau> k rule: Ty_induct)
194209
then show ?case using fresh_at_base(2) fresh_not_isin_tyvar by fastforce
195210
qed (auto simp: fresh_Cons)
196211

212+
thm Tm_Alts.induct[of "\<lambda>_ _ e _. atom x \<sharp> e" "\<lambda>_ _ _ _ _ alts _. atom x \<sharp> alts" \<Gamma> \<Delta> e \<tau> \<Gamma> \<Delta> T \<sigma> \<tau>1 alts \<tau>]
213+
214+
lemma fresh_in_context_term_var:
215+
assumes "atom (x::var) \<sharp> \<Gamma>"
216+
shows "\<Gamma> , \<Delta> \<turnstile> e : \<tau> \<longrightarrow> atom x \<sharp> e"
217+
and "Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<longrightarrow> atom x \<sharp> alts"
218+
proof (induction \<Gamma> \<Delta> e \<tau> and \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> rule: Tm_Alts.induct)
219+
197220
lemma fresh_in_context_term_var: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (x::var) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom x \<sharp> e"
198-
proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm.induct)
199-
case (Tm_Var \<Gamma> \<Delta> x \<tau>)
221+
proof (induction \<Gamma> \<Delta> e \<tau> rule: Tm_induct)
222+
case (Var \<Gamma> \<Delta> x \<tau>)
200223
then show ?case using fresh_ineq_at_base fresh_not_isin_var by force
224+
next
225+
case (Case \<Gamma> \<Delta> e \<tau>1 T \<sigma>s \<tau> alts)
226+
then show ?case sorry
201227
qed (auto simp: fresh_Cons)
202228

203229
lemma fresh_in_context_term_tyvar: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau> ; atom (a::tyvar) \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> e"

0 commit comments

Comments
 (0)