Skip to content

Commit 424dafe

Browse files
jvanbrueggejvanbruegge
committed
Require constructor types to have the correct form
1 parent 77de9ba commit 424dafe

File tree

3 files changed

+125
-1
lines changed

3 files changed

+125
-1
lines changed

‎Defs.thy‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,127 @@ proof goal_cases
4141
qed (auto simp: eqvt_def head_ctor_graph_aux_def)
4242
nominal_termination (eqvt) by lexicographic_order
4343

44+
nominal_function ctor_data_app :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
45+
"ctor_data_app (TyVar _) = None"
46+
| "ctor_data_app (TyData T) = Some (T, [])"
47+
| "ctor_data_app TyArrow = None"
48+
| "ctor_data_app (TyApp \<tau>1 (TyVar a)) = (case ctor_data_app \<tau>1 of
49+
Some (T, s) \<Rightarrow> Some (T, a#s)
50+
| None \<Rightarrow> None)"
51+
| "ctor_data_app (TyApp _ (TyData _)) = None"
52+
| "ctor_data_app (TyApp _ TyArrow) = None"
53+
| "ctor_data_app (TyApp _ (TyApp _ _)) = None"
54+
| "ctor_data_app (TyApp _ (TyForall _ _ _)) = None"
55+
| "ctor_data_app (TyForall _ _ _) = None"
56+
proof goal_cases
57+
case 1
58+
then show ?case by (auto simp: eqvt_def ctor_data_app_graph_aux_def split!: option.splits)
59+
next
60+
case (3 P x)
61+
then show ?case
62+
proof (cases x rule: \<tau>.exhaust)
63+
case (TyApp \<tau>1 \<tau>2)
64+
then show ?thesis using 3 by (cases \<tau>2 rule: \<tau>.exhaust) auto
65+
qed (auto simp: 3)
66+
qed auto
67+
nominal_termination (eqvt) by lexicographic_order
68+
69+
nominal_function ctor_type_app :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
70+
"ctor_type_app (TyVar _) = None"
71+
| "ctor_type_app (TyData T) = Some (T, [])"
72+
| "ctor_type_app TyArrow = None"
73+
| "ctor_type_app (TyApp (TyApp TyArrow \<tau>1) \<tau>2) = ctor_type_app \<tau>2"
74+
| "ctor_type_app (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyVar a) \<tau>1) \<tau>2)"
75+
| "ctor_type_app (TyApp (TyApp (TyData T) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyData T) \<tau>1) \<tau>2)"
76+
| "ctor_type_app (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyApp \<tau>1' \<tau>2') \<tau>1) \<tau>2)"
77+
| "ctor_type_app (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2) = ctor_data_app (TyApp (TyApp (TyForall a k e) \<tau>1) \<tau>2)"
78+
| "ctor_type_app (TyApp (TyVar a) \<tau>2) = ctor_data_app (TyApp (TyVar a) \<tau>2)"
79+
| "ctor_type_app (TyApp (TyData T) \<tau>2) = ctor_data_app (TyApp (TyData T) \<tau>2)"
80+
| "ctor_type_app (TyApp TyArrow \<tau>2) = ctor_data_app (TyApp TyArrow \<tau>2)"
81+
| "ctor_type_app (TyApp (TyForall a k e) \<tau>2) = ctor_data_app (TyApp (TyForall a k e) \<tau>2)"
82+
| "ctor_type_app (TyForall _ _ _) = None"
83+
proof goal_cases
84+
case (3 P x)
85+
show ?case using 3(1-3,13)
86+
proof (cases x rule: \<tau>.exhaust)
87+
case outer: (TyApp \<tau>1 \<tau>2)
88+
then show ?thesis using 3(9-12)
89+
proof (cases \<tau>1 rule: \<tau>.exhaust)
90+
case inner: (TyApp \<tau>1' \<tau>2')
91+
then show ?thesis using outer 3(4-8) by (cases \<tau>1' rule: \<tau>.exhaust) blast+
92+
qed blast+
93+
qed blast+
94+
next
95+
case (74 a k e \<tau>1 \<tau>2 a k e \<tau>1 \<tau>2)
96+
then show ?case by (simp add: 74)
97+
next
98+
case (92 a k e \<tau>2 a k e \<tau>2)
99+
then show ?case by (simp add: 92)
100+
qed (auto simp: eqvt_def ctor_type_app_graph_aux_def)
101+
nominal_termination (eqvt) by lexicographic_order
102+
103+
nominal_function ctor_type_forall :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
104+
"ctor_type_forall (TyVar _) = None"
105+
| "ctor_type_forall (TyData T) = Some (T, [])"
106+
| "ctor_type_forall TyArrow = None"
107+
| "ctor_type_forall (TyApp \<tau>1 \<tau>2) = ctor_type_app (TyApp \<tau>1 \<tau>2)"
108+
| "ctor_type_forall (TyForall a _ e) = (case ctor_type_forall e of
109+
Some (T, s) \<Rightarrow> (if a \<in> set s then Some (T, filter (\<lambda>x. x \<noteq> a) s) else None)
110+
| None \<Rightarrow> None)"
111+
proof goal_cases
112+
case 1
113+
then show ?case by (auto simp: eqvt_def ctor_type_forall_graph_aux_def split!: option.splits list.splits)
114+
next
115+
case (3 P x)
116+
then show ?case by (cases x rule: \<tau>.exhaust)
117+
next
118+
case (18 a k e a' k' e')
119+
obtain c::tyvar where P: "atom c \<sharp> (a, e, a', e', ctor_type_forall_sumC e, ctor_type_forall_sumC e')" by (rule obtain_fresh)
120+
then have c: "atom c \<sharp> a" "atom c \<sharp> e" "atom c \<sharp> a'" "atom c \<sharp> e'" "atom c \<sharp> ctor_type_forall_sumC e" "atom c \<sharp> ctor_type_forall_sumC e'" by auto
121+
have 1: "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using Abs_lst_rename_both c(1-4) 18(5) by auto
122+
then have 2: "(a \<leftrightarrow> c) \<bullet> ctor_type_forall_sumC e = (a' \<leftrightarrow> c) \<bullet> ctor_type_forall_sumC e'" using 18(1,2) eqvt_at_def by metis
123+
then have 3: "ctor_type_forall_sumC e = None \<longleftrightarrow> ctor_type_forall_sumC e' = None" using permute_eq_iff by fastforce
124+
then show ?case
125+
proof (cases "ctor_type_forall_sumC e")
126+
case (Some t)
127+
then obtain T s where P1: "t = (T, s)" by fastforce
128+
from Some obtain T' s' where P2: "ctor_type_forall_sumC e' = Some (T', s')" using 3 by auto
129+
have "T = T'" using "2" P1 P2 Some Some_eqvt option.inject perm_data_name_tyvar by auto
130+
have same: "(a \<leftrightarrow> c) \<bullet> s = (a' \<leftrightarrow> c) \<bullet> s'" using "2" P1 P2 Some by auto
131+
have x: "a \<in> set s \<longleftrightarrow> a' \<in> set s'" by (metis flip_at_simps(2) mem_permute_iff permute_flip_cancel same set_eqvt)
132+
have 4: "atom c \<sharp> s" using c(5) Some P1 fresh_Some fresh_Pair by metis
133+
have 5: "atom c \<sharp> s'" using c(6) Some P2 fresh_Some fresh_Pair by metis
134+
have 6: "atom a \<sharp> filter (\<lambda>x. x \<noteq> a) s" "atom a' \<sharp> filter (\<lambda>x. x \<noteq> a') s'" "atom c \<sharp> filter (\<lambda>x. x \<noteq> a) s" "atom c \<sharp> filter (\<lambda>x. x \<noteq> a') s'" using 4 5 fresh_filter by auto
135+
have 8: "filter (\<lambda>x. x \<noteq> a) s = (a \<leftrightarrow> c) \<bullet> filter (\<lambda>x. x \<noteq> a) s" using 6 flip_fresh_fresh by metis
136+
also have "... = filter (\<lambda>x. x \<noteq> c) ((a \<leftrightarrow> c) \<bullet> s)" by auto
137+
also have "... = filter (\<lambda>x. x \<noteq> c) ((a' \<leftrightarrow> c) \<bullet> s')" using same by argo
138+
also have "... = (a' \<leftrightarrow> c) \<bullet> filter (\<lambda>x. x \<noteq> a') s'" by simp
139+
also have "... = filter (\<lambda>x. x \<noteq> a') s'" using 6 flip_fresh_fresh by blast
140+
finally have 9: "Some (T, filter (\<lambda>x. x \<noteq> a) s) = Some (T', filter (\<lambda>x. x \<noteq> a') s')" using \<open>T = T'\<close> by blast
141+
then show ?thesis using Some P1 P2 x by simp
142+
qed simp
143+
qed auto
144+
nominal_termination (eqvt) by lexicographic_order
145+
146+
(* This function checks if a type has the form \<forall>[a:k]. [\<tau>] \<rightarrow> T [a] *)
147+
nominal_function ctor_type :: "\<tau> \<Rightarrow> data_name option" where
148+
"ctor_type (TyVar a) = None"
149+
| "ctor_type (TyData T) = Some T"
150+
| "ctor_type TyArrow = None"
151+
| "ctor_type (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
152+
| "ctor_type (TyForall a k e) = (case ctor_type_forall (TyForall a k e) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
153+
proof goal_cases
154+
case 1
155+
then show ?case by (auto simp: eqvt_def ctor_type_graph_aux_def split!: option.splits list.splits)
156+
next
157+
case (3 P x)
158+
then show ?case by (cases x rule: \<tau>.exhaust)
159+
next
160+
case (18 a k e a' k' e')
161+
then show ?case by (simp add: 18)
162+
qed auto
163+
nominal_termination (eqvt) by lexicographic_order
164+
44165
nominal_function is_value :: "term => bool" where
45166
"is_value (Var x) = False"
46167
| "is_value (\<lambda> x : \<tau> . e) = True"

‎Nominal2_Lemmas.thy‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,4 +79,7 @@ lemma Abs_rename_body:
7979
shows "(a \<leftrightarrow> b) \<bullet> e1 = e2"
8080
by (metis Abs1_eq_iff'(3) Nominal2_Base.swap_self assms flip_commute flip_def fresh_star_zero supp_perm_eq_test)
8181

82+
lemma fresh_filter: "a = b \<or> atom a \<sharp> xs \<Longrightarrow> atom a \<sharp> filter (\<lambda>x. x \<noteq> b) xs"
83+
by (induction xs) (auto simp: fresh_Cons fresh_Nil)
84+
8285
end

‎Typing.thy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -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> ; 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 ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
1616

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

0 commit comments

Comments
 (0)