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) \ (Var b)) = All [{|b, a|}]. ((Var a) \ (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) \ (Var b)) = All [{|a, b|}].((Var b) \ (Var a))" + apply(simp add: Abs_eq_iff) + apply(rule_tac x="(atom a \ 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) \ (Var b)) = All [{|a, b|}].((Var a) \ (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 \ b" + shows "\(All [{|a, b|}].((Var a) \ (Var b)) = All [{|c|}].((Var c) \ (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 \ lookup Ts T) = lookup (p \ Ts) (p \ 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 \ ty \ 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) \ (Var b)) = All [{|b, a|}]. ((Var a) \ (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) \ (Var b)) = All [{|a, b|}].((Var b) \ (Var a))" - apply(simp add: Abs_eq_iff) - apply(rule_tac x="(atom a \ 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) \ (Var b)) = All [{|a, b|}].((Var a) \ (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 \ b" - shows "\(All [{|a, b|}].((Var a) \ (Var b)) = All [{|c|}].((Var c) \ (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 \ Subst \ Subst" ("_ \ _" [100,100] 100) +fun + subst_dom_pi :: "Subst \ perm \ Subst" ("_|_") where - "\\<^isub>1 \ [] = \\<^isub>1" -| "\\<^isub>1 \ ((X,T)#\\<^isub>2) = (X,\\<^isub>1)#(\\<^isub>1 \ \\<^isub>2)" - -lemma compose_eqvt: - fixes \1 \2::"Subst" - shows "(p \ (\1 \ \2)) = ((p \ \1) \ (p \ \2))" -apply(induct \2) -apply(auto simp add: subst.eqvt) -done - -lemma compose_ty: - fixes \1 :: "Subst" - and \2 :: "Subst" - and T :: "ty" - shows "\1<\2> = (\1\\2)" -proof (induct T rule: ty.induct) - case (Var X) - have "\12 X> = lookup (\1\\2) X" - by (induct \2) (auto) - then show ?case by simp -next - case (Fun T1 T2) - then show ?case by simp -qed + "[]|p = []" +| "((X,T)#\)|p = (p \ X, T)#(\|p)" fun subst_subst :: "Subst \ Subst \ Subst" ("_<_>" [100,60] 120) @@ -194,12 +170,6 @@ "\<[]> = []" | "\ <((X,T)#\')> = (X,\)#(\<\'>)" -lemma redundant1: - fixes \1::"Subst" - and \2::"Subst" - shows "\1 \ \2 = (\1<\2>)@\1" -by (induct \2) (auto) - fun dom :: "Subst \ name fset" where @@ -207,38 +177,24 @@ | "dom ((X,T)#\) = {|X|} |\| dom \" lemma dom_eqvt[eqvt]: - shows "(p \ dom \) = dom (p \ \)" -apply(induct \ rule: dom.induct) -apply(simp_all) -done + shows "p \ (dom \) = dom (p \ \)" +by (induct \) (auto) -lemma dom_compose: - shows "dom (\1 \ \2) = dom \1 |\| dom \2" -apply(induct rule: dom.induct) -apply(simp) -apply(simp) -by (metis sup_commute union_insert_fset) - -lemma redundant3: - fixes \1::"Subst" - and \2::"Subst" +lemma dom_subst: + fixes \1 \2::"Subst" shows "dom (\2<\1>) = (dom \1)" by (induct \1) (auto) lemma dom_pi: - shows "(p \ (dom \)) = dom (map (\(X, T). (p \ X, T)) \)" -apply(induct \) -apply(auto) -done + shows "dom (\|p) = dom (p \ \)" +by (induct \) (auto) lemma dom_fresh_lookup: fixes \::"Subst" - assumes "\X \ fset (dom \). atom X \ name" - shows "lookup \ name = Var name" + assumes "\Y \ fset (dom \). atom Y \ X" + shows "lookup \ X = Var X" using assms -apply(induct \) -apply(auto simp add: fresh_at_base) -done +by (induct \) (auto simp add: fresh_at_base) lemma dom_fresh_ty: fixes \::"Subst" @@ -246,30 +202,20 @@ assumes "\X \ fset (dom \). atom X \ T" shows "\ = 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 \ \'::"Subst" assumes "\X \ fset (dom \). atom X \ \'" shows "\<\'> = \'" using assms -apply(induct \') -apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty) -done - - -abbreviation - "sub_list" :: "'a list \ 'a list \ bool" ("_ \ _" [60,60] 60) -where - "xs\<^isub>1 \ xs\<^isub>2 \ \x. x \ set xs\<^isub>1 \ x \ set xs\<^isub>2" +by (induct \') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty) definition - generalises3 :: "ty \ tys \ bool" ("_ \\\\ _") + generalises :: "ty \ tys \ bool" ("_ \\ _") where - " T \\\\ S \ (\\ Xs T'. S = All [Xs].T'\ T = \ \ dom \ = Xs)" + "T \\ S \ (\\ Xs T'. S = All [Xs].T'\ T = \ \ dom \ = Xs)" lemma lookup_fresh: @@ -277,40 +223,34 @@ assumes a: "atom X \ \" shows "lookup \ X = Var X" using a - apply (induct \) - apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base) - done + by (induct \) (auto simp add: fresh_Cons fresh_Pair fresh_at_base) lemma lookup_dom: fixes X::"name" - assumes a: "X |\| dom \" + assumes "X |\| dom \" shows "lookup \ X = Var X" - using a - apply (induct \) - apply(auto) - done + using assms + by (induct \) (auto) lemma w1: - "\(X, y). (p \ X, y)) \'> = map (\(X, y). (p \ X, y)) (\<\'>)" -apply(induct \') -apply(auto) -done + shows "\<\'|p> = (\<\'>)|p" + by (induct \')(auto) lemma w2: assumes "name |\| dom \'" shows "\' name> = lookup (\<\'>) name" using assms apply(induct \') -apply(auto) -by (metis notin_empty_fset) +apply(auto simp add: notin_empty_fset) +done lemma w3: assumes "name |\| dom \" - shows "lookup \ name = lookup (map (\(X, y). (p \ X, y)) \) (p \ name)" + shows "lookup \ name = lookup (\|p) (p \ name)" using assms apply(induct \) -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 \) apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh) -done + done lemma test: fixes \ \'::"Subst" and T::"ty" assumes "(p \ atom ` fset (dom \')) \* \" "supp All [dom \'].T \* p" - shows "\<\'> = \(X, y). (p \ X, y)) \'><\

T>>" + shows "\<\'> = \<\'|p><\

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 \\\\ S \ \ \\\\ \" -unfolding generalises3_def + shows "T \\ 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="\(X, T). (p \ X, T)) \'>" in exI) +apply(rule_tac x="\<\'|p>" in exI) apply(rule_tac x="p \ Xs" in exI) apply(rule_tac x="\

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="\'" 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 \\ All [Xs].T' \ (\\. T = \ \ dom \ = 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 (\(X, T). (p \ X, T)) \" in exI) +apply(auto) +oops end