author urbanc Thu, 17 Aug 2006 19:20:43 +0200 changeset 20395 9a60e3151244 parent 20394 21227c43ba26 child 20396 4d0c33719348
added definition for size and substitution using the recursion combinator
```--- 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(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(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(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(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
+
+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)"

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(rule trans, rule rfun_Top)
+apply(rule trans, rule rfun_Fun)
+apply(rule trans, rule rfun_All)
+apply(fresh_guess add: perm_nat_def size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def 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(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"
+
+lemma supports_subst_Fun:
+  shows "((supp (X,T))::tyvrs set) supports subst_Fun X T"
+
+lemma supports_subst_All:
+  shows "((supp (X,T))::tyvrs set) supports subst_All X T"
+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(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(rule trans)
+apply(rule rfun_Top[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+apply(rule trans)
+apply(rule rfun_Fun[OF fin_supp_subst, OF fcb_subst_All])
+apply(assumption)+
+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(perm_full_simp)
+apply(assumption)