diff -r 09acd7e116e8 -r 5b5ade6bc889 Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Thu Dec 29 18:05:13 2011 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon Jan 02 16:13:16 2012 +0000
@@ -8,10 +8,10 @@
 
 nominal_datatype ty =
   Var "name"
-| Fun "ty" "ty"
+| Fun "ty" "ty" ("_ \<rightarrow> _")
 
 nominal_datatype tys =
-  All xs::"name fset" ty::"ty" binds (set+) xs in ty
+  All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")
 
 thm tys.distinct
 thm tys.induct tys.strong_induct
@@ -26,9 +26,13 @@
 thm tys.supp
 thm tys.fresh
 
+subsection {* Substitution function for types and type schemes *}
+
+type_synonym 
+  Subst = "(name \<times> ty) list"
 
 fun
-  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+  lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"
 where
   "lookup [] Y = Var Y"
 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
@@ -41,10 +45,10 @@
 
 
 nominal_primrec
-  subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+  subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
 where
-  "subst \<theta> (Var X) = lookup \<theta> X"
-| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)"
+  "\<theta><Var X> = lookup \<theta> X"
+| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
@@ -58,7 +62,6 @@
 termination (eqvt)
   by lexicographic_order
 
-
 lemma supp_fun_app_eqvt:
   assumes e: "eqvt f"
   shows "supp (f a b) \<subseteq> supp a \<union> supp b"
@@ -71,14 +74,10 @@
   unfolding eqvt_def 
   by (simp add: permute_fun_def subst.eqvt)
  
-lemma fresh_star_inter1:
-  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
-  unfolding fresh_star_def by blast
-
 nominal_primrec
-  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
-  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+  "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
   unfolding eqvt_def substs_graph_def
   apply (rule, perm_simp, rule)
   apply auto[2]
@@ -94,7 +93,7 @@
   apply(subgoal_tac "x \<notin> supp \<theta>")
   prefer 2
   apply(auto simp add: fresh_star_def fresh_def)[1]
-  apply(subgoal_tac "x \<in> supp t")
+  apply(subgoal_tac "x \<in> supp T")
   using supp_subst
   apply(blast)
   using supp_subst
@@ -105,12 +104,12 @@
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
-  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")
   apply blast
-  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
+  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
   apply (simp add: supp_Pair eqvts eqvts_raw)
   apply auto[1]
-  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
+  apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")
   apply (simp add: fresh_star_def fresh_def)
   apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
   apply (simp add: eqvts eqvts_raw)
@@ -125,21 +124,21 @@
 text {* Some Tests about Alpha-Equality *}
 
 lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
+  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|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
+  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|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
+  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)
@@ -147,7 +146,7 @@
 
 lemma
   assumes a: "a \<noteq> b"
-  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+  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)
@@ -156,6 +155,215 @@
   done
 
 
+text {* HERE *}
+
+fun 
+  compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
+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
+
+fun
+  dom :: "Subst \<Rightarrow> name fset"
+where
+  "dom [] = {||}"
+| "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
+
+nominal_primrec
+  ftv  :: "ty \<Rightarrow> name fset"
+where
+  "ftv (Var X) = {|X|}"
+| "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"
+  unfolding eqvt_def ftv_graph_def
+  apply (rule, perm_simp, rule)
+  apply(auto)[2]
+  apply(rule_tac y="x" in ty.exhaust)
+  apply(blast)
+  apply(blast)
+  apply(simp_all)
+  done
+
+termination (eqvt)
+  by lexicographic_order
+
+lemma s1:
+  fixes T::"ty"
+  shows "(X \<leftrightarrow> Y) \<bullet> T = [(X, Var Y),(Y, Var X)]<T>"
+apply(induct T rule: ty.induct)
+apply(simp_all)
+done
+
+lemma s2:
+  fixes T::"ty"
+  shows "[]<T> = T"
+apply(induct T rule: ty.induct)
+apply(simp_all)
+done
+
+lemma perm_struct_induct_name[case_names pure zero swap]:
+  assumes pure: "supp p \<subseteq> atom ` (UNIV::name set)"
+  and     zero: "P 0"
+  and     swap: "\<And>p a b::name. \<lbrakk>P p; a \<noteq> b\<rbrakk> \<Longrightarrow> P ((a \<leftrightarrow> b) + p)"
+  shows "P p"
+apply(rule_tac S="supp p \<inter> atom ` (UNIV::name set)" in perm_struct_induct)
+using pure
+apply(auto)[1]
+apply(rule zero)
+apply(auto)
+apply(simp add: flip_def[symmetric])
+apply(rule swap)
+apply(auto)
+done
+
+lemma s3:
+  fixes T::"ty"
+  assumes "supp p \<subseteq> atom ` (UNIV::name set)"
+  shows "\<exists>\<theta>. p \<bullet> T = \<theta><T>"
+apply(induct p rule: perm_struct_induct_name)
+apply(rule assms)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp add: s2)
+apply(clarify)
+apply(simp) 
+apply(rule_tac x="[(a, Var b),(b, Var a)] \<circ> \<theta>" in exI)
+apply(simp add: compose_ty[symmetric])
+apply(simp add: s1)
+done
+
+lemma s4:
+  fixes x::"'a::fs"
+  assumes "supp x \<subseteq> atom ` (UNIV::name set)"
+  shows "\<exists>q. p \<bullet> x = q \<bullet> x \<and> supp q \<subseteq> atom ` (UNIV::name set)"
+apply(induct p rule: perm_simple_struct_induct)
+apply(rule_tac x="0" in exI)
+apply(auto)[1]
+apply(simp add: supp_zero_perm)
+apply(auto)[1]
+apply(case_tac "supp (a \<rightleftharpoons> b) \<subseteq> range atom")
+apply(rule_tac x="(a \<rightleftharpoons> b) + q" in exI)
+apply(simp)
+apply(rule subset_trans)
+apply(rule supp_plus_perm)
+apply(simp)
+apply(rule_tac x="q" in exI)
+apply(simp)
+apply(rule swap_fresh_fresh)
+apply(simp add: fresh_permute_left)
+apply(subst perm_supp_eq)
+apply(simp add: supp_swap)
+apply(simp add: supp_minus_perm)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_atom)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: supp_swap)
+using assms
+apply(simp add: fresh_def)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: fresh_permute_left)
+apply(subst perm_supp_eq)
+apply(simp add: supp_swap)
+apply(simp add: supp_minus_perm)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_atom)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: supp_swap)
+using assms
+apply(simp add: fresh_def)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+done
+
+lemma s5:
+  fixes T::"ty"
+  shows "supp T \<subseteq> atom ` (UNIV::name set)"
+apply(induct T rule: ty.induct)
+apply(auto simp add: ty.supp supp_at_base)
+done
+
+function
+  generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
+where
+  "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. \<theta><T'> = T)"
+  apply auto[1]
+  apply (rule_tac y="b" in tys.exhaust)
+  apply auto[1]
+  apply(simp)
+  apply(clarify)
+  apply(rule iffI)
+  apply(clarify)
+  apply(drule sym)
+  apply(simp add: Abs_eq_iff2)
+  apply(simp add: alphas)
+  apply(clarify)
+  using s4[OF s5]
+  apply -
+  apply(drule_tac x="p" in meta_spec)
+  apply(drule_tac x="T'a" in meta_spec)
+  apply(clarify)
+  apply(simp)
+  using s3
+  apply -
+  apply(drule_tac x="q" in meta_spec)
+  apply(drule_tac x="T'a" in meta_spec)
+  apply(drule meta_mp)
+  apply(simp)
+  apply(clarify)
+  apply(simp)
+  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)
+  apply(simp add: compose_ty)
+  apply(auto)
+  apply(simp add: Abs_eq_iff2)
+  apply(simp add: alphas)
+  apply(clarify)
+  apply(drule_tac x="p" in meta_spec)
+  apply(drule_tac x="T'" in meta_spec)
+  apply(clarify)
+  apply(simp)
+  apply(drule_tac x="q" in meta_spec)
+  apply(drule_tac x="T'" in meta_spec)
+  apply(drule meta_mp)
+  apply(simp)
+  apply(clarify)
+  apply(simp)
+  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)
+  apply(simp add: compose_ty)
+  done
+
+
+
+
 
 
 end