--- a/src/HOL/Nominal/Examples/Fsub.thy Thu Aug 17 09:24:56 2006 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Thu Aug 17 19:20:43 2006 +0200
@@ -237,24 +237,233 @@
only be defined manually via some laborious proof constructions. Therefore
we just assume them here. Cheat! *}
-consts size_ty :: "ty \<Rightarrow> nat"
+types 'a f1_ty = "tyvrs\<Rightarrow>('a::pt_tyvrs)"
+ 'a f2_ty = "('a::pt_tyvrs)"
+ 'a f3_ty = "ty\<Rightarrow>ty\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_tyvrs)"
+ 'a f4_ty = "tyvrs\<Rightarrow>ty\<Rightarrow>ty\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_tyvrs)"
+
+constdefs
+ rfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> 'a f4_ty \<Rightarrow> ty \<Rightarrow> ('a::pt_tyvrs)"
+ "rfun f1 f2 f3 f4 T \<equiv> (THE r. (T,r) \<in> ty_rec_set f1 f2 f3 f4)"
+
+lemma rfun_Tvar:
+ assumes f1: "finite ((supp f1)::tyvrs set)"
+ and f2: "finite ((supp f2)::tyvrs set)"
+ and f3: "finite ((supp f3)::tyvrs set)"
+ and f4: "finite ((supp f4)::tyvrs set)"
+ and fcb: "\<And>X T1 T2 r1 r2. \<lbrakk>X\<sharp>f4; X\<sharp>T2; X\<sharp>r2\<rbrakk> \<Longrightarrow> X\<sharp>f4 X T1 T2 r1 r2"
+ shows "rfun f1 f2 f3 f4 (Tvar X) = (f1 X)"
+apply(simp add: rfun_def)
+apply(rule trans)
+apply(rule the1_equality)
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule ty_rec_set.intros)
+done
+
+lemma rfun_Top:
+ assumes f1: "finite ((supp f1)::tyvrs set)"
+ and f2: "finite ((supp f2)::tyvrs set)"
+ and f3: "finite ((supp f3)::tyvrs set)"
+ and f4: "finite ((supp f4)::tyvrs set)"
+ and fcb: "\<And>X T1 T2 r1 r2. \<lbrakk>X\<sharp>f4; X\<sharp>T2; X\<sharp>r2\<rbrakk> \<Longrightarrow> X\<sharp>f4 X T1 T2 r1 r2"
+ shows "rfun f1 f2 f3 f4 (Top) = f2"
+apply(simp add: rfun_def)
+apply(rule trans)
+apply(rule the1_equality)
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule ty_rec_set.intros)
+done
+
+lemma rfun_Fun:
+ assumes f1: "finite ((supp f1)::tyvrs set)"
+ and f2: "finite ((supp f2)::tyvrs set)"
+ and f3: "finite ((supp f3)::tyvrs set)"
+ and f4: "finite ((supp f4)::tyvrs set)"
+ and fcb: "\<And>X T1 T2 r1 r2. \<lbrakk>X\<sharp>f4; X\<sharp>T2; X\<sharp>r2\<rbrakk> \<Longrightarrow> X\<sharp>f4 X T1 T2 r1 r2"
+ shows "rfun f1 f2 f3 f4 (T1\<rightarrow>T2) = f3 T1 T2 (rfun f1 f2 f3 f4 T1) (rfun f1 f2 f3 f4 T2)"
+apply(simp add: rfun_def)
+apply(rule trans)
+apply(rule the1_equality)
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule ty_rec_set.intros)
+apply(rule theI')
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule theI')
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+done
+
+lemma rfun_All:
+ assumes f1: "finite ((supp f1)::tyvrs set)"
+ and f2: "finite ((supp f2)::tyvrs set)"
+ and f3: "finite ((supp f3)::tyvrs set)"
+ and f4: "finite ((supp f4)::tyvrs set)"
+ and fcb: "\<And>X T1 T2 r1 r2. \<lbrakk>X\<sharp>f4; X\<sharp>T2; X\<sharp>r2\<rbrakk> \<Longrightarrow> X\<sharp>f4 X T1 T2 r1 r2"
+ and fr: "X\<sharp>f1" "X\<sharp>f2" "X\<sharp>f3" "X\<sharp>f4" "X\<sharp>T2"
+ shows "rfun f1 f2 f3 f4 (\<forall>[X<:T2].T1) = f4 X T1 T2 (rfun f1 f2 f3 f4 T1) (rfun f1 f2 f3 f4 T2)"
+apply(simp add: rfun_def)
+apply(rule trans)
+apply(rule the1_equality)
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule ty_rec_set.intros)
+apply(simp_all add: fr)
+apply(rule theI')
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+apply(rule theI')
+apply(rule ty.rec_unique[where P="\<lambda>_. True"])
+apply(simp_all add: f1 f2 f3 f4 fcb)
+done
+
+constdefs
+ size_ty_Tvar :: "tyvrs \<Rightarrow> nat"
+ "size_ty_Tvar \<equiv> \<lambda>_. 1"
+
+ size_ty_Top :: "nat"
+ "size_ty_Top \<equiv> 1"
+
+ size_ty_Fun :: "ty \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+ "size_ty_Fun \<equiv> \<lambda>_ _ r1 r2. r1 + r2 + 1"
+
+ size_ty_All :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+ "size_ty_All \<equiv> \<lambda>_ _ _ r1 r2. r1 + r2 + 1"
+
+ size_ty :: "ty \<Rightarrow> nat"
+ "size_ty \<equiv> rfun size_ty_Tvar size_ty_Top size_ty_Fun size_ty_All"
+
+lemma fin_size_ty:
+ shows "finite ((supp size_ty_Tvar)::tyvrs set)"
+ and "finite ((supp size_ty_Top)::tyvrs set)"
+ and "finite ((supp size_ty_Fun)::tyvrs set)"
+ and "finite ((supp size_ty_All)::tyvrs set)"
+by (finite_guess add: size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def size_ty_All_def perm_nat_def)+
+
+lemma fcb_size_ty_All:
+ assumes "X\<sharp>size_ty_All" "X\<sharp>T2" "X\<sharp>r2"
+ shows "X\<sharp>(size_ty_All X T1 T2 r1 r2)"
+by (simp add: fresh_def supp_nat)
lemma size_ty[simp]:
shows "size_ty (Tvar X) = 1"
and "size_ty (Top) = 1"
- and "\<lbrakk>size_ty T\<^isub>1 = m; size_ty T\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (T\<^isub>1 \<rightarrow> T\<^isub>2) = m + n + 1"
- and "\<lbrakk>size_ty T\<^isub>1 = m; size_ty T\<^isub>2 = n\<rbrakk> \<Longrightarrow> size_ty (\<forall>[X<:T\<^isub>1].T\<^isub>2) = m + n + 1"
-sorry
+ and "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
+ and "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
+apply(unfold size_ty_def)
+apply(rule trans, rule rfun_Tvar)
+apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(simp add: size_ty_Tvar_def)
+apply(rule trans, rule rfun_Top)
+apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(simp add: size_ty_Top_def)
+apply(rule trans, rule rfun_Fun)
+apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(simp add: size_ty_Fun_def)
+apply(rule trans, rule rfun_All)
+apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(fresh_guess add: perm_nat_def size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def size_ty_All_def)+
+apply(simp add: size_ty_All_def)
+done
+
+constdefs
+ subst_Tvar :: "tyvrs \<Rightarrow>ty \<Rightarrow> tyvrs \<Rightarrow> ty"
+ "subst_Tvar X T \<equiv> \<lambda>Y. (if Y=X then T else (Tvar Y))"
+
+ subst_Top :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty"
+ "subst_Top X T \<equiv> Top"
+
+ subst_Fun :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"
+ "subst_Fun X T \<equiv> \<lambda>_ _ r1 r2. r1 \<rightarrow> r2"
+
+ subst_All :: "tyvrs \<Rightarrow> ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"
+ "subst_All X T \<equiv> \<lambda>Y _ _ r1 r2. \<forall>[Y<:r2].r1"
+
+ subst_ty :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"
+ "subst_ty X T \<equiv> rfun (subst_Tvar X T) (subst_Top X T) (subst_Fun X T) (subst_All X T)"
-consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
+lemma supports_subst_Tvar:
+ shows "((supp (X,T))::tyvrs set) supports (subst_Tvar X T)"
+apply(supports_simp add: subst_Tvar_def)
+apply(rule impI)
+apply(drule pt_bij1[OF pt_tyvrs_inst, OF at_tyvrs_inst])
+apply(perm_simp)
+done
+
+lemma supports_subst_Top:
+ shows "((supp (X,T))::tyvrs set) supports subst_Top X T"
+by (supports_simp add: subst_Top_def)
+
+lemma supports_subst_Fun:
+ shows "((supp (X,T))::tyvrs set) supports subst_Fun X T"
+ by (supports_simp add: subst_Fun_def)
+
+lemma supports_subst_All:
+ shows "((supp (X,T))::tyvrs set) supports subst_All X T"
+apply(supports_simp add: subst_All_def)
+apply(perm_full_simp)
+done
+
+lemma fin_supp_subst:
+ shows "finite ((supp (subst_Tvar X T))::tyvrs set)"
+ and "finite ((supp (subst_Top X T))::tyvrs set)"
+ and "finite ((supp (subst_Fun X T))::tyvrs set)"
+ and "finite ((supp (subst_All X T))::tyvrs set)"
+apply -
+apply(rule supports_finite)
+apply(rule supports_subst_Tvar)
+apply(simp add: fs_tyvrs1)
+apply(finite_guess add: subst_Top_def subst_Fun_def subst_All_def fs_tyvrs1)+
+apply(perm_full_simp)
+done
+
+lemma fcb_subst_All:
+ assumes fr: "X\<sharp>(subst_All Y T)" "X\<sharp>T2" "X\<sharp>r2"
+ shows "X\<sharp>(subst_All Y T) X T1 T2 r1 r2"
+ apply (simp add: subst_All_def abs_fresh fr)
+ done
+
+syntax
+ subst_ty_syn :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
+
+translations
+ "T1[Y:=T2]\<^isub>t\<^isub>y" \<rightleftharpoons> "subst_ty Y T2 T1"
lemma subst_ty[simp]:
- shows "(Tvar X)[Y:=T]\<^isub>t\<^isub>y = (if X=Y then T else (Tvar X))"
+ shows "(Tvar X)[Y:=T]\<^isub>t\<^isub>y= (if X=Y then T else (Tvar X))"
and "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
and "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
- and "X\<sharp>(Y,T) \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
- and "\<lbrakk>X\<sharp>Y; X\<sharp>T\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
-sorry
+ and "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
+apply -
+apply(unfold subst_ty_def)
+apply(rule trans)
+apply(rule rfun_Tvar[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+apply(simp add: subst_Tvar_def)
+apply(rule trans)
+apply(rule rfun_Top[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+apply(simp add: subst_Top_def)
+apply(rule trans)
+apply(rule rfun_Fun[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+apply(simp add: subst_Fun_def)
+apply(rule trans)
+apply(rule rfun_All[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+apply(rule supports_fresh)
+apply(rule supports_subst_Tvar)
+apply(simp add: fs_tyvrs1, simp add: fresh_def)
+apply(fresh_guess add: fresh_prod subst_Top_def fs_tyvrs1)
+apply(fresh_guess add: fresh_prod subst_Fun_def fs_tyvrs1)
+apply(fresh_guess add: fresh_prod subst_All_def fs_tyvrs1)
+apply(perm_full_simp)
+apply(assumption)
+apply(simp add: subst_All_def)
+done
consts subst_tyc :: "ty_context \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty_context" ("_[_:=_]\<^isub>t\<^isub>y\<^isub>c" [100,100,100] 100)
primrec
@@ -800,7 +1009,7 @@
have lh_drv_prm\<^isub>2: "((X,Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" by fact
from `\<forall>[X<:Q\<^isub>1].Q\<^isub>2 = Q`
- have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " by auto
+ have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " using fresh_cond by auto
from rh_drv
have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=\<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2)"
using fresh_cond by (simp add: S_ForallE_left)