# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1325174214 0 # Node ID 8779fb01d8b42c438857b7d490ae8c9b938821f5 # Parent 502b5f02edaf34b5cbec2fa5c1fd5530fa8a20fe separated the two versions of type schemes into two files diff -r 502b5f02edaf -r 8779fb01d8b4 Nominal/Ex/TypeSchemes1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/TypeSchemes1.thy Thu Dec 29 15:56:54 2011 +0000 @@ -0,0 +1,161 @@ +theory TypeSchemes1 +imports "../Nominal2" +begin + +section {*** Type Schemes defined as two separate nominal datatypes ***} + +atom_decl name + +nominal_datatype ty = + Var "name" +| Fun "ty" "ty" + +nominal_datatype tys = + All xs::"name fset" ty::"ty" binds (set+) xs in ty + +thm tys.distinct +thm tys.induct tys.strong_induct +thm tys.exhaust tys.strong_exhaust +thm tys.fv_defs +thm tys.bn_defs +thm tys.perm_simps +thm tys.eq_iff +thm tys.fv_bn_eqvt +thm tys.size_eqvt +thm tys.supports +thm tys.supp +thm tys.fresh + + +fun + lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty" +where + "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) +apply(simp_all) +done + + +nominal_primrec + subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" +where + "subst \<theta> (Var X) = lookup \<theta> X" +| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)" + unfolding eqvt_def subst_graph_def + apply (rule, perm_simp, rule) + apply(rule TrueI) + apply(case_tac x) + apply(rule_tac y="b" in ty.exhaust) + apply(blast) + apply(blast) + apply(simp_all) + done + +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" + using supp_fun_app_eqvt[OF e] supp_fun_app + by blast + +lemma supp_subst: + "supp (subst \<theta> t) \<subseteq> supp \<theta> \<union> supp t" + apply (rule supp_fun_app_eqvt) + 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" +where + "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)" + unfolding eqvt_def substs_graph_def + apply (rule, perm_simp, rule) + apply auto[2] + apply (rule_tac y="b" and c="a" in tys.strong_exhaust) + apply auto[1] + apply(simp) + apply(erule conjE) + apply (erule Abs_res_fcb) + apply (simp add: Abs_fresh_iff) + apply(simp add: fresh_def) + apply(simp add: supp_Abs) + apply(rule impI) + 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") + using supp_subst + apply(blast) + using supp_subst + apply(blast) + apply clarify + apply (simp add: subst.eqvt) + apply (subst Abs_eq_iff) + 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 blast + 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 (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) + apply (simp add: fresh_star_def fresh_def) + apply (drule subsetD[OF supp_subst]) + apply (simp add: supp_Pair) + apply (rule perm_supp_eq) + apply (simp add: fresh_def fresh_star_def) + apply blast + done + +text {* Some Tests about Alpha-Equality *} + +lemma + shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (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|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (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))" + 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|} (Fun (Var a) (Var b)) = All {|c|} (Fun (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 + + + + +end diff -r 502b5f02edaf -r 8779fb01d8b4 Nominal/Ex/TypeSchemes2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/TypeSchemes2.thy Thu Dec 29 15:56:54 2011 +0000 @@ -0,0 +1,313 @@ +theory TypeSchemes2 +imports "../Nominal2" +begin + +section {*** Type Schemes defined as a single nominal datatype ***} + +atom_decl name + +nominal_datatype ty = + Var "name" +| Fun "ty" "ty" +and tys = + All xs::"name fset" ty::"ty" binds (set+) xs in ty + +thm ty_tys.distinct +thm ty_tys.induct +thm ty_tys.inducts +thm ty_tys.exhaust +thm ty_tys.strong_exhaust +thm ty_tys.fv_defs +thm ty_tys.bn_defs +thm ty_tys.perm_simps +thm ty_tys.eq_iff +thm ty_tys.fv_bn_eqvt +thm ty_tys.size_eqvt +thm ty_tys.supports +thm ty_tys.supp +thm ty_tys.fresh + +fun + lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty" +where + "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) +apply(simp_all) +done + +lemma TEST1: + assumes "x = Inl y" + shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)" +using assms by simp + +lemma TEST2: + assumes "x = Inr y" + shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)" +using assms by simp + +lemma test: + assumes a: "\<exists>y. f x = Inl y" + shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" +using a +apply clarify +apply(frule_tac p="p" in permute_boolI) +apply(simp (no_asm_use) only: eqvts) +apply(subst (asm) permute_fun_app_eq) +back +apply(simp) +done + +lemma test2: + assumes a: "\<exists>y. f x = Inl y" + shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))" +using a +apply clarify +apply(frule_tac p="p" in permute_boolI) +apply(simp (no_asm_use) only: eqvts) +apply(subst (asm) permute_fun_app_eq) +back +apply(simp) +done + +nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") + subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" +and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" +where + "subst \<theta> (Var X) = lookup \<theta> X" +| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" +| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" +(*unfolding subst_substs_graph_def eqvt_def +apply rule +apply perm_simp +apply (subst test3) +defer +apply (subst test3) +defer +apply (subst test3) +defer +apply rule*) +thm subst_substs_graph.intros +apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") +apply(simp add: eqvt_def) +apply(rule allI) +apply(simp add: permute_fun_def permute_bool_def) +apply(rule ext) +apply(rule ext) +apply(rule iffI) +apply(drule_tac x="p" in meta_spec) +apply(drule_tac x="- p \<bullet> x" in meta_spec) +apply(drule_tac x="- p \<bullet> xa" in meta_spec) +apply(simp) +apply(drule_tac x="-p" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(simp) +--"Eqvt One way" +apply(erule subst_substs_graph.induct) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(erule subst_substs_graph.cases) +apply(simp (no_asm_use) only: eqvts) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(rotate_tac 1) +apply(erule subst_substs_graph.cases) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(assumption) +apply(assumption) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(assumption) +apply(assumption) +apply(simp) +--"A" +apply(simp (no_asm_use) only: eqvts) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(rotate_tac 1) +apply(erule subst_substs_graph.cases) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(assumption) +apply(assumption) +apply(subst test) +back +apply (rule exI) +apply(assumption) +apply(perm_simp) +apply(rule subst_substs_graph.intros) +apply(assumption) +apply(assumption) +apply(simp) +--"A" +apply(simp) +apply(erule subst_substs_graph.cases) +apply(simp (no_asm_use) only: eqvts) +apply(subst test) +back +back +apply (rule exI) +apply(assumption) +apply(rule subst_substs_graph.intros) +apply (simp add: eqvts) +apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)") +apply (simp add: image_eqvt eqvts_raw eqvts) +apply (simp add: fresh_star_permute_iff) +apply(perm_simp) +apply(assumption) +apply(simp (no_asm_use) only: eqvts) +apply(subst test) +back +back +apply (rule exI) +apply(assumption) +apply(rule subst_substs_graph.intros) +apply (simp add: eqvts) +apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)") +apply (simp add: image_eqvt eqvts_raw eqvts) +apply (simp add: fresh_star_permute_iff) +apply(perm_simp) +apply(assumption) +apply(simp) +--"Eqvt done" +apply(rule TrueI) +apply (case_tac x) +apply simp apply clarify +apply (rule_tac y="b" in ty_tys.exhaust(1)) +apply (auto)[1] +apply (auto)[1] +apply simp apply clarify +apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) +apply (auto)[1] +apply (auto)[5] +--"LAST GOAL" +apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) +apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") +apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") +apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))") +prefer 2 +apply (simp add: eqvt_at_def subst_def) +apply rule +apply (subst test2) +apply (simp add: subst_substs_sumC_def) +apply (simp add: THE_default_def) +apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))") +prefer 2 +apply simp +apply (simp add: the1_equality) +apply auto[1] +apply (erule_tac x="x" in allE) +apply simp +apply(cases rule: subst_substs_graph.cases) +apply assumption +apply (rule_tac x="lookup \<theta> X" in exI) +apply clarify +apply (rule the1_equality) +apply blast apply assumption +apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1)))) + (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) +apply clarify +apply (rule the1_equality) +apply blast apply assumption +apply clarify +apply simp +--"-" +apply clarify + apply (frule supp_eqvt_at) + apply (simp add: finite_supp) + apply (erule Abs_res_fcb) + apply (simp add: Abs_fresh_iff) + apply (simp add: Abs_fresh_iff) + apply auto[1] + apply (simp add: fresh_def fresh_star_def) + apply (erule contra_subsetD) + apply (simp add: supp_Pair) + apply blast + apply clarify + apply (simp) + apply (simp add: eqvt_at_def) + apply (subst Abs_eq_iff) + 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 blast + 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 (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) + apply (simp add: fresh_star_def fresh_def) + apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric]) + apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)") + apply (erule subsetD) + apply (simp add: supp_eqvt) + apply (metis le_eqvt permute_boolI) + apply (rule perm_supp_eq) + apply (simp add: fresh_def fresh_star_def) + apply blast + done + + +termination (eqvt) by lexicographic_order + +text {* Some Tests about Alpha-Equality *} + +lemma + shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (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_tys.supp supp_at_base) + done + +lemma + shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (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_tys.supp) + done + +lemma + shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (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_tys.supp supp_at_base) +done + +lemma + assumes a: "a \<noteq> b" + shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" + using a + apply(simp add: Abs_eq_iff) + apply(clarify) + apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base) + apply auto + done + + + + +end diff -r 502b5f02edaf -r 8779fb01d8b4 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Thu Dec 29 12:40:36 2011 +0000 +++ b/Nominal/ROOT.ML Thu Dec 29 15:56:54 2011 +0000 @@ -21,7 +21,8 @@ "Ex/SingleLet", "Ex/Shallow", "Ex/SystemFOmega", - "Ex/TypeSchemes", + "Ex/TypeSchemes1", + "Ex/TypeSchemes2", "Ex/TypeVarsTest", "Ex/Foo1", "Ex/Foo2",