src/HOL/Nominal/Examples/Fsub.thy

 text {* In the current version of the nominal datatype package even simple 
   functions (such as size of types and capture-avoiding substitution) can 
   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
-
-consts subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
+  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)"
+
+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
 "([])[Y:=T]\<^isub>t\<^isub>y\<^isub>c= []"
 "(XT#\<Gamma>)[Y:=T]\<^isub>t\<^isub>y\<^isub>c = (fst XT,(snd XT)[Y:=T]\<^isub>t\<^isub>y)#(\<Gamma>[Y:=T]\<^isub>t\<^isub>y\<^isub>c)"

       hence rh_drv: "\<Gamma> \<turnstile> \<forall>[X<:Q\<^isub>1].Q\<^isub>2 <: T" by simp
       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
       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)
       moreover
       have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in ((X,Q\<^isub>1)#\<Gamma>)"