# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1325554930 0
# Node ID 9a63d90d1752eda4b81a02a1cdca2e6a114c6828
# Parent  5b5ade6bc88912d693dba1654414dbd177c8fc8d
proved that generalisation is closed under substitution

diff -r 5b5ade6bc889 -r 9a63d90d1752 Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Mon Jan 02 16:13:16 2012 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Tue Jan 03 01:42:10 2012 +0000
@@ -121,6 +121,9 @@
   apply blast
   done
 
+termination (eqvt)
+  by (lexicographic_order)
+
 text {* Some Tests about Alpha-Equality *}
 
 lemma
@@ -186,6 +189,18 @@
 qed
 
 fun
+  subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>"  [100,60] 120)
+where
+  "\<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
   "dom [] = {||}"
@@ -197,173 +212,213 @@
 apply(simp_all)
 done
 
-nominal_primrec
-  ftv  :: "ty \<Rightarrow> name fset"
+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"
+  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
+
+lemma dom_fresh_lookup:
+  fixes \<theta>::"Subst"
+  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
+  shows "lookup \<theta> name = Var name"
+using assms
+apply(induct \<theta>)
+apply(auto simp add: fresh_at_base)
+done 
+
+lemma dom_fresh_ty:
+  fixes \<theta>::"Subst"
+  and   T::"ty"
+  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 
+
+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
-  "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)
+  "xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"
+
+
+definition
+  generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<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)"
+
+
+lemma lookup_fresh:
+  fixes X::"name"
+  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
 
-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 lookup_dom:
+  fixes X::"name"
+  assumes a: "X |\<notin>| dom \<theta>"
+  shows "lookup \<theta> X = Var X"
+  using a
+  apply (induct \<theta>)
+  apply(auto)
+  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)
+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
 
-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)
+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)
+
+lemma w3:
+  assumes "name |\<in>| dom \<theta>" 
+  shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
+using assms
+apply(induct \<theta>)
+apply(auto)
+by (metis notin_empty_fset)
+
+lemma fresh_lookup:
+  fixes X Y::"name"
+  and   \<theta>::"Subst"
+  assumes asms: "atom X \<sharp> Y" "atom X \<sharp> \<theta>"
+  shows "atom X \<sharp> (lookup \<theta> Y)"
+  using assms
+  apply (induct \<theta>)
+  apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
 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)
+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>>"
+using assms
+apply(induct T rule: ty.induct)
+defer
+apply(auto simp add: tys.supp ty.supp fresh_star_def)[1]
+apply(auto simp add: tys.supp ty.supp fresh_star_def supp_at_base)[1]
+apply(case_tac "name |\<in>| dom \<theta>'")
+apply(subgoal_tac "atom (p \<bullet> name) \<sharp> \<theta>")
+apply(subst (2) lookup_fresh)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
 apply(simp)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp)
-apply(rule_tac x="q" in exI)
+apply(simp add: w1)
+apply(simp add: w2)
+apply(subst w3[symmetric])
+apply(simp add:redundant3)
 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(perm_simp)
+apply(rotate_tac 2)
+apply(drule_tac p="p" in permute_boolI)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(metis notin_fset)
+apply(simp add: lookup_dom)
+apply(perm_simp)
+apply(subst dom_fresh_ty)
 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)
+apply(rule fresh_lookup)
+apply(simp add: redundant3)
+apply(simp add: dom_pi[symmetric])
+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_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)
+apply(simp)
 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
-
-
-
-
+lemma
+  shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
+unfolding generalises3_def
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac t="S" and s="All [Xs].T'" in subst)
+apply(simp)
+using at_set_avoiding3
+apply -
+apply(drule_tac x="fset (map_fset atom Xs)" in meta_spec)
+apply(drule_tac x="\<theta>" in meta_spec)
+apply(drule_tac x="All [Xs].T'" in meta_spec)
+apply(drule meta_mp)
+apply(simp)
+apply(drule meta_mp)
+apply(simp add: finite_supp)
+apply(drule meta_mp)
+apply(simp add: finite_supp)
+apply(drule meta_mp)
+apply(simp add: tys.fresh fresh_star_def)
+apply(erule exE)
+apply(erule conjE)+
+apply(rule_tac t="All[Xs].T'" and s="p \<bullet> (All [Xs].T')" in subst)
+apply(rule supp_perm_eq)
+apply(assumption)
+apply(perm_simp)
+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="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(rule_tac t="T" and s="\<theta>'<T'>" in subst)
+apply(simp)
+apply(rule test)
+apply(perm_simp)
+apply(rotate_tac 2)
+apply(drule_tac p="p" in permute_boolI)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)
+done
 
 
 end