# 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",