diff -r 09acd7e116e8 -r 5b5ade6bc889 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Dec 29 18:05:13 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,441 +0,0 @@
-theory TypeSchemes
-imports "../Nominal2"
-begin
-
-section {*** Type Schemes ***}
-
-atom_decl name 
-
-(* defined as a single nominal datatype *)
-
-nominal_datatype ty =
-  Var "name"
-| Fun "ty" "ty"
-and tys =
-  All xs::"name fset" ty::"ty" binds (set+) xs in ty
-
-ML {*
-get_all_info @{context}
-*}
-
-ML {*
-get_info @{context} "TypeSchemes.ty"
-*}
-
-ML {*
-#strong_exhaust (the_info @{context} "TypeSchemes.tys")
-*}
-
-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
-
-
-section {* defined as two separate nominal datatypes *}
-
-nominal_datatype ty2 =
-  Var2 "name"
-| Fun2 "ty2" "ty2"
-
-nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty
-
-thm tys2.distinct
-thm tys2.induct tys2.strong_induct
-thm tys2.exhaust tys2.strong_exhaust
-thm tys2.fv_defs
-thm tys2.bn_defs
-thm tys2.perm_simps
-thm tys2.eq_iff
-thm tys2.fv_bn_eqvt
-thm tys2.size_eqvt
-thm tys2.supports
-thm tys2.supp
-thm tys2.fresh
-
-fun
-  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
-where
-  "lookup2 [] Y = Var2 Y"
-| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
-
-lemma lookup2_eqvt[eqvt]:
-  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
-  by (induct Ts T rule: lookup2.induct) simp_all
-
-nominal_primrec
-  subst2  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
-where
-  "subst2 \<theta> (Var2 X) = lookup2 \<theta> X"
-| "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"
-  unfolding eqvt_def subst2_graph_def
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply(case_tac x)
-  apply(rule_tac y="b" in ty2.exhaust)
-  apply(blast)
-  apply(blast)
-  apply(simp_all add: ty2.distinct)
-  done
-
-termination (eqvt)
-  by lexicographic_order
-
-
-lemma supp_fun_app2_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 (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
-  apply (rule supp_fun_app2_eqvt)
-  unfolding eqvt_def by (simp add: eqvts_raw)
- 
-lemma fresh_star_inter1:
-  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
-  unfolding fresh_star_def by blast
-
-nominal_primrec
-  substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
-where
-  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"
-  unfolding eqvt_def substs2_graph_def
-  apply (rule, perm_simp, rule)
-  apply auto[2]
-  apply (rule_tac y="b" and c="a" in tys2.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: subst2.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 (subst2 \<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: ty_tys.eq_iff 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: ty_tys.eq_iff 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: ty_tys.eq_iff 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: ty_tys.eq_iff Abs_eq_iff)
-  apply(clarify)
-  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
-  apply auto
-  done
-
-
-
-
-end