Skip to content

Commit df8f5dc

Browse files
jvanbrueggejvanbruegge
committed
Merge remote-tracking branch 'origin/popl2025_updated' into popl2025_updated
2 parents 325f112 + 1e971a2 commit df8f5dc

File tree

3 files changed

+141
-137
lines changed

3 files changed

+141
-137
lines changed

‎thys/POPLmark/POPLmark_1A.thy‎

Lines changed: 65 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,25 @@ begin
44

55
(********************* Actual formalization ************************)
66

7-
lemma ty_refl: "\<lbrakk>wf \<Gamma> ; T closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T <: T"
8-
proof (binder_induction T arbitrary: \<Gamma> avoiding: "dom \<Gamma>" rule: Type.strong_induct)
9-
case (TyVar x \<Gamma>)
10-
then show ?case by blast
7+
declare ty.intros[intro]
8+
9+
lemma well_scoped:
10+
assumes "\<Gamma> \<turnstile> S <: T"
11+
shows "FFVars_sftypeP S \<subseteq> dom \<Gamma>" "FFVars_sftypeP T \<subseteq> dom \<Gamma>"
12+
using assms proof (induction \<Gamma> S T rule: ty.induct)
13+
case (SA_Trans_TVar x U \<Gamma> T) {
14+
case 1 then show ?case using SA_Trans_TVar
15+
by (metis fst_conv imageI singletonD subsetI sftypeP.set(1))
16+
next
17+
case 2 then show ?case using SA_Trans_TVar by simp
18+
} qed auto
19+
20+
declare SA_Refl_TVar[intro!]
21+
22+
lemma ty_refl: "\<lbrakk>wf \<Gamma> ; FFVars_sftypeP T \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T <: T"
23+
proof (binder_induction T arbitrary: \<Gamma> avoiding: "dom \<Gamma>" rule: sftypeP.strong_induct)
24+
case (TVr x \<Gamma>)
25+
then show ?case by (simp add: SA_Refl_TVar)
1126
qed (auto simp: Diff_single_insert SA_All wf_Cons)
1227

1328
lemma ty_permute: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; wf \<Delta> ; set \<Gamma> = set \<Delta> \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> S <: T"
@@ -29,7 +44,7 @@ proof (induction \<Delta> rule: wf.induct)
2944
using wf_Cons by auto
3045
qed auto
3146

32-
lemma weaken_closed: "\<lbrakk> S closed_in \<Gamma> ; \<Gamma> \<bottom> \<Delta> \<rbrakk> \<Longrightarrow> S closed_in \<Gamma>,,\<Delta>"
47+
lemma weaken_closed: "\<lbrakk> FFVars_sftypeP S \<subseteq> dom \<Gamma> ; \<Gamma> \<bottom> \<Delta> \<rbrakk> \<Longrightarrow> FFVars_sftypeP S \<subseteq> dom (\<Gamma>,,\<Delta>)"
3348
by auto
3449

3550
lemma wf_concat_disjoint: "wf (\<Gamma>,, \<Delta>) \<Longrightarrow> \<Gamma> \<bottom> \<Delta>"
@@ -39,7 +54,7 @@ proof (induction \<Delta>)
3954
by (smt (verit, del_insts) Un_iff append_Cons disjoint_iff fst_conv image_iff inf.idem insertE list.inject list.simps(15) set_append set_empty2 wf.cases)
4055
qed simp
4156

42-
lemma wf_insert: "\<lbrakk> wf (\<Gamma>,,\<Delta>); x \<notin> dom \<Gamma> ; x \<notin> dom \<Delta> ; T closed_in \<Gamma> \<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T,,\<Delta>)"
57+
lemma wf_insert: "\<lbrakk> wf (\<Gamma>,,\<Delta>); x \<notin> dom \<Gamma> ; x \<notin> dom \<Delta> ; FFVars_sftypeP T \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T,,\<Delta>)"
4358
by (induction \<Delta>) auto
4459

4560
lemma ty_weakening:
@@ -50,7 +65,8 @@ using assms proof (binder_induction \<Gamma> S T avoiding: "dom \<Delta>" \<Gamm
5065
then show ?case using ty.SA_Top weaken_closed wf_concat_disjoint by presburger
5166
next
5267
case (SA_Refl_TVar \<Gamma> x)
53-
then show ?case using ty.SA_Refl_TVar weaken_closed wf_concat_disjoint by presburger
68+
then show ?case using ty.SA_Refl_TVar weaken_closed wf_concat_disjoint
69+
by (meson ty_refl well_scoped(1))
5470
next
5571
case (SA_All \<Gamma> T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2)
5672
have 1: "wf (\<Gamma>,, x <: T\<^sub>1,, \<Delta>)"
@@ -60,7 +76,7 @@ next
6076
show ?case using ty_permute[OF _ 2] 1 SA_All by auto
6177
qed auto
6278

63-
corollary ty_weakening_extend: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; X \<notin> dom \<Gamma> ; Q closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma>,,X<:Q \<turnstile> S <: T"
79+
corollary ty_weakening_extend: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; X \<notin> dom \<Gamma> ; FFVars_sftypeP Q \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma>,,X<:Q \<turnstile> S <: T"
6480
using ty_weakening[of _ _ _ "[(X, Q)]"] by (metis append_Cons append_Nil wf_Cons wf_context)
6581

6682
lemma wf_concatD: "wf (\<Gamma>,, \<Delta>) \<Longrightarrow> wf \<Gamma>"
@@ -73,7 +89,7 @@ proof (induction \<Delta>)
7389
by (metis Pair_inject append_Nil fst_conv image_eqI set_ConsD wf_ConsE)
7490
qed auto
7591

76-
lemma narrow_wf: "\<lbrakk> wf ((\<Gamma> ,, X <: Q),, \<Delta>) ; R closed_in \<Gamma> \<rbrakk> \<Longrightarrow> wf ((\<Gamma>,, X <: R),, \<Delta>)"
92+
lemma narrow_wf: "\<lbrakk> wf ((\<Gamma> ,, X <: Q),, \<Delta>) ; FFVars_sftypeP R \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> wf ((\<Gamma>,, X <: R),, \<Delta>)"
7793
proof (induction \<Delta>)
7894
case (Cons a \<Delta>)
7995
then have "wf (\<Gamma>,, X <: R,, \<Delta>)" by auto
@@ -83,24 +99,22 @@ proof (induction \<Delta>)
8399
then show ?case unfolding 1 using Cons 2 by auto
84100
qed auto
85101

86-
(* todo for A: look at this and the next *)
87-
(* TODO: Automatically derive these from strong induction *)
88102
lemma SA_AllE1[consumes 2, case_names SA_Trans_TVar SA_All]:
89103
assumes "\<Gamma> \<turnstile> \<forall>X<:S\<^sub>1. S\<^sub>2 <: T" "X \<notin> dom \<Gamma>"
90-
and Top: "\<And>\<Gamma>. \<lbrakk>wf \<Gamma>; \<forall>X<:S\<^sub>1. S\<^sub>2 closed_in \<Gamma> \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) Top"
104+
and Top: "\<And>\<Gamma>. \<lbrakk>wf \<Gamma>; FFVars_sftypeP (\<forall>X<:S\<^sub>1. S\<^sub>2) \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) Top"
91105
and Forall: "\<And>\<Gamma> T\<^sub>1 T\<^sub>2. \<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) (\<forall>X<:T\<^sub>1 . T\<^sub>2)"
92106
shows "R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) T"
93107
using assms(1,2) proof (binder_induction \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T avoiding: \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T rule: ty.strong_induct)
94108
case (SA_All \<Gamma> T\<^sub>1 R\<^sub>1 Y R\<^sub>2 T\<^sub>2)
95-
have 1: "\<forall>Y<:T\<^sub>1 . T\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) T\<^sub>2"
109+
have 1: "\<forall>Y<:T\<^sub>1 . T\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) T\<^sub>2"
96110
apply (rule Forall_swap)
97111
using SA_All(6,9) well_scoped(2) by fastforce
98-
have fresh: "X \<notin> FFVars_Type T\<^sub>1"
112+
have fresh: "X \<notin> FFVars_sftypeP T\<^sub>1"
99113
by (meson SA_All(4,9) in_mono well_scoped(1))
100-
have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) Type_inject(3) by blast
101-
have x: "\<forall>Y<:S\<^sub>1. R\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) R\<^sub>2"
114+
have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) sftypeP_inject(3) by blast
115+
have x: "\<forall>Y<:S\<^sub>1. R\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) R\<^sub>2"
102116
apply (rule Forall_swap)
103-
by (metis (no_types, lifting) SA_All(8) assms(1,2) in_mono sup.bounded_iff Type.set(4) well_scoped(1))
117+
by (metis (no_types, lifting) SA_All(8) assms(1,2) in_mono sup.bounded_iff sftypeP.set(4) well_scoped(1))
104118
show ?case unfolding 1
105119
apply (rule Forall)
106120
using same SA_All(4) apply simp
@@ -119,27 +133,27 @@ qed (auto simp: Top)
119133

120134
lemma SA_AllE2[consumes 2, case_names SA_Trans_TVar SA_All]:
121135
assumes "\<Gamma> \<turnstile> S <: \<forall>X<:T\<^sub>1. T\<^sub>2" "X \<notin> dom \<Gamma>"
122-
and TyVar: "\<And>\<Gamma> x U. \<lbrakk> x<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: \<forall> X <: T\<^sub>1 . T\<^sub>2 ; R \<Gamma> U (\<forall>X<:T\<^sub>1. T\<^sub>2) \<rbrakk> \<Longrightarrow> R \<Gamma> (TyVar x) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
136+
and TVr: "\<And>\<Gamma> x U. \<lbrakk> x<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: \<forall> X <: T\<^sub>1 . T\<^sub>2 ; R \<Gamma> U (\<forall>X<:T\<^sub>1. T\<^sub>2) \<rbrakk> \<Longrightarrow> R \<Gamma> (TVr x) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
123137
and Forall: "\<And>\<Gamma> S\<^sub>1 S\<^sub>2. \<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) (\<forall> X <: T\<^sub>1 . T\<^sub>2)"
124138
shows "R \<Gamma> S (\<forall>X<:T\<^sub>1. T\<^sub>2)"
125139
using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^sub>2" avoiding: \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^sub>2" rule: ty.strong_induct)
126140
case (SA_All \<Gamma> R\<^sub>1 S\<^sub>1 Y S\<^sub>2 R\<^sub>2)
127-
have 1: "\<forall>Y<:S\<^sub>1. S\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) S\<^sub>2"
141+
have 1: "\<forall>Y<:S\<^sub>1. S\<^sub>2 = \<forall>X<:S\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) S\<^sub>2"
128142
apply (rule Forall_swap)
129143
using SA_All(6,9) well_scoped(1) by fastforce
130144
have fresh: "X \<notin> dom \<Gamma>" "Y \<notin> dom \<Gamma>"
131145
using SA_All(9) apply blast
132146
by (metis SA_All(6) fst_conv wf_ConsE wf_context)
133-
have fresh2: "X \<notin> FFVars_Type T\<^sub>1" "Y \<notin> FFVars_Type T\<^sub>1"
134-
apply (metis SA_All(4,8) in_mono fresh(1) Type_inject(3) well_scoped(1))
135-
by (metis SA_All(4,8) in_mono fresh(2) Type_inject(3) well_scoped(1))
136-
have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) Type_inject(3) by blast
137-
have x: "\<forall>Y<:T\<^sub>1 . R\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_Type (id(Y:=X,X:=Y)) R\<^sub>2"
147+
have fresh2: "X \<notin> FFVars_sftypeP T\<^sub>1" "Y \<notin> FFVars_sftypeP T\<^sub>1"
148+
apply (metis SA_All(4,8) in_mono fresh(1) sftypeP_inject(3) well_scoped(1))
149+
by (metis SA_All(4,8) in_mono fresh(2) sftypeP_inject(3) well_scoped(1))
150+
have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) sftypeP_inject(3) by blast
151+
have x: "\<forall>Y<:T\<^sub>1 . R\<^sub>2 = \<forall>X<:T\<^sub>1. rrename_sftypeP (id(Y:=X,X:=Y)) R\<^sub>2"
138152
apply (rule Forall_swap)
139-
by (metis SA_All(8) Un_iff assms(1,2) in_mono Type.set(4) well_scoped(2))
153+
by (metis SA_All(8) Un_iff assms(1,2) in_mono sftypeP.set(4) well_scoped(2))
140154
show ?case unfolding 1
141155
apply (rule Forall)
142-
apply (metis SA_All(4,8) Type_inject(3))
156+
apply (metis SA_All(4,8) sftypeP_inject(3))
143157
apply (rule iffD2[OF arg_cong3[OF _ refl, of _ _ _ _ ty], rotated -1])
144158
apply (rule ty.equiv)
145159
apply (rule bij_swap supp_swap_bound infinite_var)+
@@ -149,42 +163,42 @@ using assms(1,2) proof (binder_induction \<Gamma> S "\<forall>X<:T\<^sub>1. T\<^
149163
apply (rule arg_cong3[of _ _ _ _ _ _ extend])
150164
using fresh apply (metis bij_swap SA_All(4) Un_iff context_map_cong_id fun_upd_apply id_apply infinite_var supp_swap_bound wf_FFVars wf_context)
151165
apply simp
152-
using fresh2 unfolding same apply (metis bij_swap fun_upd_apply id_apply infinite_var supp_swap_bound Type.rrename_cong_ids)
166+
using fresh2 unfolding same apply (metis bij_swap fun_upd_apply id_apply infinite_var supp_swap_bound sftypeP.rrename_cong_ids)
153167
using SA_All(8) x Forall_inject_same unfolding same by simp
154-
qed (auto simp: TyVar)
168+
qed (auto simp: TVr)
155169

156170
lemma ty_transitivity : "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
157171
and ty_narrowing : "\<lbrakk> (\<Gamma> ,, X <: Q),, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
158172
proof -
159173
have
160174
ty_trans: "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
161175
and ty_narrow: "\<lbrakk> (\<Gamma>,, X <: Q),, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q ; wf (\<Gamma>,, X <: R,, \<Delta>) ;
162-
M closed_in (\<Gamma>,, X <: R,, \<Delta>) ; N closed_in (\<Gamma>,, X <: R,, \<Delta>) \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
163-
proof (binder_induction Q arbitrary: \<Gamma> \<Delta> S T M N X R avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: Type.strong_induct)
164-
case (TyVar Y \<Gamma> \<Delta> S T M N X R)
176+
FFVars_sftypeP M \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>) ; FFVars_sftypeP N \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>) \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
177+
proof (binder_induction Q arbitrary: \<Gamma> \<Delta> S T M N X R avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: sftypeP.strong_induct)
178+
case (TVr Y \<Gamma> \<Delta> S T M N X R)
165179
{
166180
fix \<Gamma> S T
167-
show ty_trans: "\<Gamma> \<turnstile> S <: TyVar Y \<Longrightarrow> \<Gamma> \<turnstile> TyVar Y <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
168-
by (induction \<Gamma> S "TyVar Y" rule: ty.induct) auto
181+
show ty_trans: "\<Gamma> \<turnstile> S <: TVr Y \<Longrightarrow> \<Gamma> \<turnstile> TVr Y <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
182+
by (induction \<Gamma> S "TVr Y" rule: ty.induct) auto
169183
} note ty_trans = this
170184
{
171185
case 2
172186
then show ?case
173-
proof (binder_induction "\<Gamma>,, X <: TyVar Y,, \<Delta>" M N arbitrary: \<Delta> avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: ty.strong_induct)
187+
proof (binder_induction "\<Gamma>,, X <: TVr Y,, \<Delta>" M N arbitrary: \<Delta> avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: ty.strong_induct)
174188
case (SA_Trans_TVar Z U T \<Delta>')
175189
show ?case
176190
proof (cases "X = Z")
177191
case True
178-
then have u: "U = TyVar Y" using SA_Trans_TVar(1,2) context_determ wf_context by blast
179-
have "TyVar Y closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
180-
then have "\<Gamma>,, Z <: R ,, \<Delta>' \<turnstile> TyVar Y <: T" using SA_Trans_TVar True u by auto
181-
moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: TyVar Y" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
192+
then have u: "U = TVr Y" using SA_Trans_TVar(1,2) context_determ wf_context by blast
193+
have "FFVars_sftypeP (TVr Y) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
194+
then have "\<Gamma>,, Z <: R ,, \<Delta>' \<turnstile> TVr Y <: T" using SA_Trans_TVar True u by auto
195+
moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: TVr Y" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
182196
by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
183197
ultimately have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: T" using ty_trans by blast
184198
then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
185199
next
186200
case False
187-
have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
201+
have x: "FFVars_sftypeP (U) \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
188202
show ?thesis
189203
apply (rule ty.SA_Trans_TVar)
190204
using SA_Trans_TVar False x by auto
@@ -220,7 +234,7 @@ proof -
220234
then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
221235
next
222236
case False
223-
have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
237+
have x: "FFVars_sftypeP (U) \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
224238
show ?thesis
225239
apply (rule ty.SA_Trans_TVar)
226240
using SA_Trans_TVar False x by auto
@@ -252,7 +266,7 @@ proof -
252266
then show ?thesis by (meson left(1,3) ty.SA_Arrow ty.SA_Top well_scoped(1))
253267
next
254268
case right: (SA_Arrow U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2)
255-
then show ?thesis using left by (metis Fun(1,3) SA_Arrow Type_inject(2))
269+
then show ?thesis using left by (metis Fun(1,3) SA_Arrow sftypeP_inject(2))
256270
qed auto
257271
qed auto
258272
} note ty_trans = this
@@ -265,15 +279,15 @@ proof -
265279
proof (cases "X = Z")
266280
case True
267281
then have u: "U = (Q\<^sub>1 \<rightarrow> Q\<^sub>2)" using SA_Trans_TVar(1,2) context_determ wf_context by blast
268-
have "(Q\<^sub>1 \<rightarrow> Q\<^sub>2) closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
282+
have "FFVars_sftypeP (Q\<^sub>1 \<rightarrow> Q\<^sub>2) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
269283
then have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> (Q\<^sub>1 \<rightarrow> Q\<^sub>2) <: T" using SA_Trans_TVar True u by auto
270284
moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: (Q\<^sub>1 \<rightarrow> Q\<^sub>2)" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
271285
by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
272286
ultimately have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: T" using ty_trans by blast
273287
then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
274288
next
275289
case False
276-
have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
290+
have x: "FFVars_sftypeP U \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
277291
show ?thesis
278292
apply (rule ty.SA_Trans_TVar)
279293
using SA_Trans_TVar False x by auto
@@ -326,7 +340,7 @@ proof -
326340
proof (cases "Y = Z")
327341
case True
328342
then have u: "U = \<forall> X <: Q\<^sub>1 . Q\<^sub>2" using SA_Trans_TVar(1,2) context_determ wf_context by blast
329-
have "\<forall> X <: Q\<^sub>1 . Q\<^sub>2 closed_in \<Gamma>,, Z <: R,, \<Delta>'" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
343+
have "FFVars_sftypeP (\<forall> X <: Q\<^sub>1 . Q\<^sub>2) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
330344
then have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> \<forall> X <: Q\<^sub>1 . Q\<^sub>2 <: T" using SA_Trans_TVar True u by auto
331345
moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: \<forall> X <: Q\<^sub>1 . Q\<^sub>2" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
332346
by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
@@ -394,10 +408,10 @@ proof -
394408
qed
395409

396410
theorem ty_transitivity2: "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
397-
proof (binder_induction Q arbitrary: \<Gamma> S T avoiding: "dom \<Gamma>" rule: Type.strong_induct)
398-
case (TyVar x \<Gamma> S T)
411+
proof (binder_induction Q arbitrary: \<Gamma> S T avoiding: "dom \<Gamma>" rule: sftypeP.strong_induct)
412+
case (TVr x \<Gamma> S T)
399413
then show ?case
400-
by (induction \<Gamma> S "TyVar x") auto
414+
by (induction \<Gamma> S "TVr x") auto
401415
next
402416
case (Fun x1 x2 \<Gamma> S T)
403417
from Fun(4,3) show ?case
@@ -411,8 +425,8 @@ next
411425
case (SA_Arrow \<Gamma> U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2)
412426
show ?case
413427
apply (rule ty.SA_Arrow)
414-
apply (metis Fun(1) SA_Arrow(1,5,6,8) Type_inject(2))
415-
by (metis Fun(2) SA_Arrow(3,5,7,8) Type_inject(2))
428+
apply (metis Fun(1) SA_Arrow(1,5,6,8) sftypeP_inject(2))
429+
by (metis Fun(2) SA_Arrow(3,5,7,8) sftypeP_inject(2))
416430
qed auto
417431
qed auto
418432
next
@@ -435,9 +449,9 @@ next
435449
qed blast
436450
qed auto
437451

438-
(*
452+
439453
corollary ty_narrowing2: "\<lbrakk> \<Gamma>,, X <: Q,, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q \<rbrakk> \<Longrightarrow> \<Gamma>,, X <: R,, \<Delta> \<turnstile> M <: N"
440454
using ty_narrowing_aux ty_transitivity2 by blast
441-
*)
455+
442456

443457
end

0 commit comments

Comments
 (0)