# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295382418 -3600
# Node ID 028d5511c15fd42940ea1c48b187edf600c58041
# Parent  68ccf847507de50294a473e2d38f93854bc34bc5
some tryes about substitution over type-schemes

diff -r 68ccf847507d -r 028d5511c15f Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue Jan 18 19:27:30 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jan 18 21:26:58 2011 +0100
@@ -28,7 +28,8 @@
 thm ty_tys.supp
 thm ty_tys.fresh
 
-(* defined as two separate nominal datatypes *)
+
+section {* defined as two separate nominal datatypes *}
 
 nominal_datatype ty2 =
   Var2 "name"
@@ -50,17 +51,87 @@
 thm tys2.supp
 thm tys2.fresh
 
+fun
+  lookup :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
+where
+  "lookup [] Y = Var2 Y"
+| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
 
-text {* Some Tests *}
+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
+
+function
+  subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
+where
+  "subst \<theta> (Var2 X) = lookup \<theta> X"
+| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="b" in ty2.exhaust)
+apply(blast)
+apply(blast)
+apply(simp_all add: ty2.distinct)
+apply(simp add: ty2.eq_iff)
+apply(simp add: ty2.eq_iff)
+done
+
+termination
+  apply(relation "measure (size o snd)")
+  apply(simp_all add: ty2.size)
+  done
+
+lemma subst_eqvt[eqvt]:
+  shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
+apply(induct \<theta> T rule: subst.induct)
+apply(simp_all add: lookup_eqvt)
+done
+
+lemma j:
+  assumes "a \<sharp> Ts" " a \<sharp> X"
+  shows "a \<sharp> lookup Ts X"
+using assms
+apply(induct Ts X rule: lookup.induct)
+apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)
+done
+
+lemma i:
+  assumes "a \<sharp> t" " a \<sharp> \<theta>"
+  shows "a \<sharp> subst \<theta> t"
+using assms
+apply(induct \<theta> t rule: subst.induct)
+apply(auto simp add: ty2.fresh j)
+done 
+
+lemma k:
+  assumes "as \<sharp>* t" " as \<sharp>* \<theta>"
+  shows "as \<sharp>* subst \<theta> t"
+using assms
+by (simp add: fresh_star_def i)
+
+lemma h:
+  assumes "as \<subseteq> bs \<union> cs"
+  and " cs \<sharp>* x"
+  shows "(as - bs) \<sharp>* x"
+using assms
+by (auto simp add: fresh_star_def)
+
+nominal_primrec
+  substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
+where
+  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
+oops
+
+
+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)
-  apply(simp add: Abs_eq_iff)
+  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas)
-  apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
-  apply(simp add: ty_tys.supp supp_at_base)
+  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
   done
 
 lemma
@@ -88,165 +159,6 @@
   done
 
 
-text {* Some lemmas about fsets *}
-
-lemma atom_map_fset_cong:
-  shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
-  apply(rule inj_map_fset_cong)
-  apply(simp add: inj_on_def)
-  done
-
-lemma supp_map_fset_atom:
-  shows "supp (map_fset atom S) = supp S"
-  unfolding supp_def
-  apply(perm_simp)
-  apply(simp add: atom_map_fset_cong)
-  done
-
-lemma supp_at_fset:
-  fixes S::"('a::at_base) fset"
-  shows "supp S = fset (map_fset atom S)"
-  apply (induct S)
-  apply (simp add: supp_empty_fset)
-  apply (simp add: supp_insert_fset)
-  apply (simp add: supp_at_base)
-  done
-
-lemma fresh_star_atom:
-  fixes a::"'a::at_base"
-  shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
-  apply (induct S)
-  apply (simp add: fresh_set_empty)
-  apply simp
-  apply (unfold fresh_def)
-  apply (simp add: supp_of_finite_insert)
-  apply (rule conjI)
-  apply (unfold fresh_star_def)
-  apply simp
-  apply (unfold fresh_def)
-  apply (simp add: supp_at_base supp_atom)
-  apply clarify
-  apply auto
-  done
-
-
-
-(*
-fun
-  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
-where
-  "lookup [] n = Var n"
-| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"
-
-locale subst_loc =
-fixes
-    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
-and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
-assumes
-    s1: "subst \<theta> (Var n) = lookup \<theta> n"
-and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"
-and s3: "fset (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
-begin
-
-lemma subst_ty:
-  assumes x: "atom x \<sharp> t"
-  shows "subst [(x, S)] t = t"
-  using x
-  apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
-  by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)
-
-lemma subst_tyS:
-  shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"
-  apply (rule strong_induct[of
-    "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])
-  apply clarify
-  apply (subst s3)
-  apply (simp add: fresh_star_def fresh_Cons fresh_Nil)
-  apply (subst subst_ty)
-  apply (simp_all add: fresh_star_prod_elim)
-  apply (drule fresh_star_atom)
-  apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
-  apply (subgoal_tac "atom a \<notin> fset (fmap atom fset)")
-  apply blast
-  apply (metis supp_finite_atom_set finite_fset)
-  done
-
-lemma subst_lemma_pre:
-  "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"
-  apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
-  apply (simp add: s1)
-  apply (auto simp add: fresh_Pair)
-  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]
-  apply (simp add: s2)
-  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
-  done
-
-lemma substs_lemma_pre:
-  "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"
-  apply (rule strong_induct[of
-    "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified])
-  apply clarify
-  apply (subst s3)
-  apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)
-  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
-  apply clarify
-  apply (drule fresh_star_atom)
-  apply (drule fresh_star_atom)
-  apply (simp add: fresh_def)
-  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
-  apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")
-  apply blast
-  apply (subgoal_tac "atom a \<notin> supp t")
-  apply (fold fresh_def)[1]
-  apply (rule mp[OF subst_lemma_pre])
-  apply (simp add: fresh_Pair)
-  apply (subgoal_tac "atom a \<notin> (fset (fmap atom fset))")
-  apply blast
-  apply (metis supp_finite_atom_set finite_fset)
-  done
-
-lemma subst_lemma:
-  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
-    subst [(y, L)] (subst [(x, N)] M) =
-    subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"
-  apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
-  apply (simp_all add: s1 s2)
-  apply clarify
-  apply (subst (2) subst_ty)
-  apply simp_all
-  done
-
-lemma substs_lemma:
-  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
-    substs [(y, L)] (substs [(x, N)] M) =
-    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"
-  apply (rule strong_induct[of
-    "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
-    substs [(y, L)] (substs [(x, N)] M) =
-    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])
-  apply clarify
-  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
-  apply (subst s3)
-  apply (unfold fresh_star_def)[1]
-  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
-  apply (subst s3)
-  apply (unfold fresh_star_def)[1]
-  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
-  apply (subst s3)
-  apply (unfold fresh_star_def)[1]
-  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
-  apply (subst s3)
-  apply (unfold fresh_star_def)[1]
-  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
-  apply (rule ballI)
-  apply (rule mp[OF subst_lemma_pre])
-  apply (simp add: fresh_Pair)
-  apply (subst subst_lemma)
-  apply simp_all
-  done
-
-end
-*)
 
 
 end
diff -r 68ccf847507d -r 028d5511c15f Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 19:27:30 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 21:26:58 2011 +0100
@@ -33,7 +33,8 @@
   swap_eqvt flip_eqvt
 
   (* datatypes *)
-  Pair_eqvt permute_list.simps permute_option.simps
+  Pair_eqvt permute_list.simps permute_option.simps 
+  permute_sum.simps
 
   (* sets *)
   mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
diff -r 68ccf847507d -r 028d5511c15f Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Jan 18 19:27:30 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jan 18 21:26:58 2011 +0100
@@ -531,6 +531,7 @@
       if eqvt_flag = false then NONE
       else 
         let
+          val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) 
           val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
         in
           SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})