nominal2: comparison Nominal/Ex/TypeSchemes1.thy

equal deleted inserted replaced

-:9a63d90d1752
+:f7c4b8e6918b
 theory TypeSchemes1
 imports "../Nominal2"
 begin
-section {*** Type Schemes defined as two separate nominal datatypes ***}
+section {* Type Schemes defined as two separate nominal datatypes *}
 atom_decl name
 nominal_datatype ty =
 Var "name"
 thm tys.size_eqvt
 thm tys.supports
 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
 Subst = "(name \<times> ty) list"
 "lookup [] Y = Var Y"
 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
 lemma lookup_eqvt[eqvt]:
 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
+by (induct Ts T rule: lookup.induct) (simp_all)
-apply(simp_all)
-done
 nominal_primrec
 subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
 where
 "\<theta><Var X> = lookup \<theta> X"
 done
 termination (eqvt)
 by (lexicographic_order)
-text {* Some Tests about Alpha-Equality *}
+subsection {* Generalisation of types and type-schemes*}
-lemma
-shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
+fun
-apply(simp add: Abs_eq_iff)
+subst_dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")
-apply(rule_tac x="0::perm" in exI)
+where
-apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+"[]|p = []"
-done
+| "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)"
-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
-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
 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 [] = {||}"
 | "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
 lemma dom_eqvt[eqvt]:
-shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
+shows "p \<bullet> (dom \<theta>) = dom (p \<bullet> \<theta>)"
-apply(induct \<theta> rule: dom.induct)
+by (induct \<theta>) (auto)
-apply(simp_all)
-done
+lemma dom_subst:
+fixes \<theta>1 \<theta>2::"Subst"
-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>)"
+shows "dom (\<theta>|p) = dom (p \<bullet> \<theta>)"
-apply(induct \<theta>)
+by (induct \<theta>) (auto)
-apply(auto)
-done
 lemma dom_fresh_lookup:
 fixes \<theta>::"Subst"
-assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
+assumes "\<forall>Y \<in> fset (dom \<theta>). atom Y \<sharp> X"
-shows "lookup \<theta> name = Var name"
+shows "lookup \<theta> X = Var X"
 using assms
-apply(induct \<theta>)
+by (induct \<theta>) (auto simp add: fresh_at_base)
-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)
+by (induct T rule: ty.induct) (auto simp add: ty.fresh dom_fresh_lookup)
-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>')
+by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
-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"
 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:
 fixes X::"name"
 assumes a: "atom X \<sharp> \<theta>"
 shows "lookup \<theta> X = Var X"
 using a
-apply (induct \<theta>)
+by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
-apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
-done
 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
+using assms
-apply (induct \<theta>)
+by (induct \<theta>) (auto)
-apply(auto)
-done
 lemma w1:
-"\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
+shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"
-apply(induct \<theta>')
+by (induct \<theta>')(auto)
-apply(auto)
-done
 lemma w2:
 assumes "name |\<in>| dom \<theta>'"
 shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
 using assms
 apply(induct \<theta>')
-apply(auto)
+apply(auto simp add: notin_empty_fset)
-by (metis 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)
+apply(auto simp add: notin_empty_fset)
-by (metis notin_empty_fset)
+done
 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 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
 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(auto simp add: fresh_star_def)[1]
 apply(simp)
 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)
 apply(drule_tac p="p" in permute_boolI)
 apply(perm_simp)
 apply(simp add: lookup_dom)
 apply(perm_simp)
 apply(subst dom_fresh_ty)
 apply(auto)[1]
 apply(rule fresh_lookup)
-apply(simp add: redundant3)
+apply(simp add: dom_subst)
-apply(simp add: dom_pi[symmetric])
+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)
 apply(simp)
 done
 lemma
-shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
+shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
-unfolding generalises3_def
+unfolding generalises_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(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="\<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_subst)
-apply(simp add: dom_pi[symmetric])
+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)
 apply(drule_tac p="p" in permute_boolI)
 apply(perm_simp)
 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

changeset 3104	f7c4b8e6918b
parent 3103	9a63d90d1752
child 3109	d79e936e30ea