
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -2,7 +2,7 @@
 imports "../Nominal2"
 begin
 
-section {*** Type Schemes defined as two separate nominal datatypes ***}
+section {* Type Schemes defined as two separate nominal datatypes *}
 
 atom_decl name 
 
@@ -26,6 +26,40 @@
 thm tys.supp
 thm tys.fresh
 
+subsection {* Some Tests about Alpha-Equality *}
+
+lemma
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+  done
+
+lemma
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
+  done
+
+lemma
+  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+done
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
+  using a
+  apply(simp add: Abs_eq_iff)
+  apply(clarify)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+  apply auto
+  done
+
+
 subsection {* Substitution function for types and type schemes *}
 
 type_synonym 
@@ -39,10 +73,7 @@
 
 lemma lookup_eqvt[eqvt]:
   shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
+  by (induct Ts T rule: lookup.induct) (simp_all)
 
 nominal_primrec
   subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
@@ -124,69 +155,14 @@
 termination (eqvt)
   by (lexicographic_order)
 
-text {* Some Tests about Alpha-Equality *}
 
-lemma
-  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-  done
-
-lemma
-  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
-  done
-
-lemma
-  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-done
+subsection {* Generalisation of types and type-schemes*}
 
-lemma
-  assumes a: "a \<noteq> b"
-  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
-  using a
-  apply(simp add: Abs_eq_iff)
-  apply(clarify)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-  apply auto
-  done
-
-
-text {* HERE *}
-
-fun 
-  compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
+fun
+  subst_dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")
 where
-  "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
-| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
-
-lemma compose_eqvt:
-  fixes  \<theta>1 \<theta>2::"Subst"
-  shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"
-apply(induct \<theta>2) 
-apply(auto simp add: subst.eqvt)
-done
-
-lemma compose_ty:
-  fixes  \<theta>1 :: "Subst"
-  and    \<theta>2 :: "Subst"
-  and    T :: "ty"
-  shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
-proof (induct T rule: ty.induct)
-  case (Var X) 
-  have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" 
-    by (induct \<theta>2) (auto)
-  then show ?case by simp
-next
-  case (Fun T1 T2)
-  then show ?case by simp
-qed
+  "[]|p = []"
+| "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)" 
 
 fun
   subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>"  [100,60] 120)
@@ -194,12 +170,6 @@
   "\<theta><[]> = []"
 | "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"
 
-lemma redundant1:
-  fixes \<theta>1::"Subst"
-  and   \<theta>2::"Subst"
-  shows "\<theta>1 \<circ> \<theta>2 = (\<theta>1<\<theta>2>)@\<theta>1"
-by (induct \<theta>2) (auto)
-
 fun
   dom :: "Subst \<Rightarrow> name fset"
 where
@@ -207,38 +177,24 @@
 | "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
 
 lemma dom_eqvt[eqvt]:
-  shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
-apply(induct \<theta> rule: dom.induct)
-apply(simp_all)
-done
+  shows "p \<bullet> (dom \<theta>) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
 
-lemma dom_compose:
-  shows "dom (\<theta>1 \<circ> \<theta>2) = dom \<theta>1 |\<union>| dom \<theta>2"
-apply(induct rule: dom.induct)
-apply(simp)
-apply(simp)
-by (metis sup_commute union_insert_fset)
-
-lemma redundant3:
-  fixes \<theta>1::"Subst"
-  and   \<theta>2::"Subst"
+lemma dom_subst:
+  fixes \<theta>1 \<theta>2::"Subst"
   shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
 by (induct \<theta>1) (auto)
 
 lemma dom_pi:
-  shows "(p \<bullet> (dom \<theta>)) = dom (map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>)"
-apply(induct \<theta>)
-apply(auto)
-done
+  shows "dom (\<theta>|p) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
 
 lemma dom_fresh_lookup:
   fixes \<theta>::"Subst"
-  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
-  shows "lookup \<theta> name = Var name"
+  assumes "\<forall>Y \<in> fset (dom \<theta>). atom Y \<sharp> X"
+  shows "lookup \<theta> X = Var X"
 using assms
-apply(induct \<theta>)
-apply(auto simp add: fresh_at_base)
-done 
+by (induct \<theta>) (auto simp add: fresh_at_base)
 
 lemma dom_fresh_ty:
   fixes \<theta>::"Subst"
@@ -246,30 +202,20 @@
   assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
   shows "\<theta><T> = T"
 using assms
-apply(induct T rule: ty.induct)
-apply(auto simp add: ty.fresh dom_fresh_lookup)
-done 
+by (induct T rule: ty.induct) (auto simp add: ty.fresh dom_fresh_lookup)
 
 lemma dom_fresh_subst:
   fixes \<theta> \<theta>'::"Subst"
   assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
   shows "\<theta><\<theta>'> = \<theta>'"
 using assms
-apply(induct \<theta>')
-apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
-done 
-
-
-abbreviation
-  "sub_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
-where
-  "xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"
+by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
 
 
 definition
-  generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<prec>\<prec> _")
+  generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
 where
-  " T \<prec>\<prec>\<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
+  "T \<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
 
 
 lemma lookup_fresh:
@@ -277,40 +223,34 @@
   assumes a: "atom X \<sharp> \<theta>"
   shows "lookup \<theta> X = Var X"
   using a
-  apply (induct \<theta>)
-  apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
-  done
+  by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
 
 lemma lookup_dom:
   fixes X::"name"
-  assumes a: "X |\<notin>| dom \<theta>"
+  assumes "X |\<notin>| dom \<theta>"
   shows "lookup \<theta> X = Var X"
-  using a
-  apply (induct \<theta>)
-  apply(auto)
-  done
+  using assms
+  by (induct \<theta>) (auto)
 
 lemma w1: 
-  "\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
-apply(induct \<theta>')
-apply(auto)
-done
+  shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"
+  by (induct \<theta>')(auto)
 
 lemma w2:
   assumes "name |\<in>| dom \<theta>'" 
   shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
 using assms
 apply(induct \<theta>')
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
 
 lemma w3:
   assumes "name |\<in>| dom \<theta>" 
-  shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
+  shows "lookup \<theta> name = lookup (\<theta>|p) (p \<bullet> name)"
 using assms
 apply(induct \<theta>)
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
 
 lemma fresh_lookup:
   fixes X Y::"name"
@@ -320,13 +260,13 @@
   using assms
   apply (induct \<theta>)
   apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
-done
+  done
 
 lemma test:
   fixes \<theta> \<theta>'::"Subst"
   and T::"ty"
   assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
-  shows "\<theta><\<theta>'<T>> = \<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'><\<theta><p \<bullet> T>>"
+  shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'|p><\<theta><p \<bullet> T>>"
 using assms
 apply(induct T rule: ty.induct)
 defer
@@ -341,7 +281,7 @@
 apply(simp add: w1)
 apply(simp add: w2)
 apply(subst w3[symmetric])
-apply(simp add:redundant3)
+apply(simp add: dom_subst)
 apply(simp)
 apply(perm_simp)
 apply(rotate_tac 2)
@@ -354,18 +294,17 @@
 apply(subst dom_fresh_ty)
 apply(auto)[1]
 apply(rule fresh_lookup)
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi)
 apply(perm_simp)
 apply(rotate_tac 2)
 apply(drule_tac p="p" in permute_boolI)
 apply(perm_simp)
 apply(simp add: fresh_at_base)
 apply (metis in_fset)
-apply(simp add: redundant3)
+apply(simp add: dom_subst)
 apply(simp add: dom_pi[symmetric])
 apply(perm_simp)
-apply metis
 apply(subst supp_perm_eq)
 apply(simp add: supp_at_base fresh_star_def)
 apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
@@ -373,8 +312,8 @@
 done
 
 lemma
-  shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
-unfolding generalises3_def
+  shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
+unfolding generalises_def
 apply(erule exE)+
 apply(erule conjE)+
 apply(rule_tac t="S" and s="All [Xs].T'" in subst)
@@ -401,17 +340,18 @@
 apply(subst substs.simps)
 apply(perm_simp)
 apply(simp)
-apply(rule_tac x="\<theta><map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>'>" in exI)
+apply(rule_tac x="\<theta><\<theta>'|p>" in exI)
 apply(rule_tac x="p \<bullet> Xs" in exI)
 apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
 apply(rule conjI)
 apply(simp)
 apply(rule conjI)
 defer
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi dom_eqvt[symmetric])
 apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
 apply(simp)
+apply(simp)
 apply(rule test)
 apply(perm_simp)
 apply(rotate_tac 2)
@@ -420,5 +360,19 @@
 apply(auto simp add: fresh_star_def)
 done
 
+lemma 
+  "T \<prec>\<prec>  All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> dom \<theta> = Xs)"
+apply(auto)
+defer
+unfolding generalises_def
+apply(auto)[1]
+apply(auto)[1]
+apply(drule sym)
+apply(simp add: Abs_eq_iff2)
+apply(simp add: alphas)
+apply(auto)
+apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)
+apply(auto)
+oops
 
 end




