# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289735199 0
# Node ID a59d8e1e3a17ce32d088be48f3c455dc515c450d
# Parent  6bf33236051019d35f485310593b3bc91d6e84b7
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example

diff -r 6bf332360510 -r a59d8e1e3a17 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Sun Nov 14 11:46:39 2010 +0000
@@ -66,7 +66,6 @@
 apply(clarify)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
-thm at_set_avoiding
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
@@ -90,85 +89,87 @@
 done
 
 
-text {* *}
-
-(*
-lemma strong_induct:
-  assumes a1: "\<And>name b. P b (Var name)"
-  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
-  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
-proof -
-  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
-    apply (rule ty_tys.induct)
-    apply (simp add: a1)
-    apply (simp)
-    apply (rule allI)+
-    apply (rule a2)
-    apply simp
-    apply simp
-    apply (rule allI)
-    apply (rule allI)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)")
-    apply clarify
-    apply(rule_tac t="p \<bullet> All fset ty" and 
-                   s="pa \<bullet> (p \<bullet> All fset ty)" in subst)
-    apply (rule supp_perm_eq)
-    apply assumption
-    apply (simp only: ty_tys.perm_simps)
-    apply (rule a3)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2)
-    apply (simp add: fin_fset)
-    apply (simp add: finite_supp)
-    apply (simp add: eqvts finite_supp)
-    apply (rule_tac p=" -p" in permute_boolE)
-    apply(simp add: eqvts)
-    apply(simp add: permute_fun_def atom_eqvt)
-    apply (simp add: fresh_star_def)
-    apply clarify
-    apply (simp add: fresh_def)
-    apply(auto)
-    apply (simp add: ty_tys.supp)
-    done
-  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
-  then show ?thesis by simp
-qed
+text {* Some Tests *}
 
 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(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)
   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)
+  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 eqvts supp_at_base)
+  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)
+  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 eqvts ty_tys.eq_iff supp_at_base)
+  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)
+  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
   apply(clarify)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
+  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
   apply auto
   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
diff -r 6bf332360510 -r a59d8e1e3a17 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Nov 14 11:46:39 2010 +0000
@@ -2,7 +2,6 @@
 imports 
   "../Nominal-General/Nominal2_Base" 
   "../Nominal-General/Nominal2_Eqvt" 
-  "Nominal2_FSet"
   "Abs"
 uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
diff -r 6bf332360510 -r a59d8e1e3a17 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sun Nov 14 11:05:22 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy	Sun Nov 14 11:46:39 2010 +0000
@@ -4,43 +4,6 @@
 begin
 
 
-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
 
 end