# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279780250 -7200
# Node ID 2f13fe48c87719c9b9d68cc88d66e8acd2ca7a32
# Parent  273f57049bd191929a058c86e60a47c221b00deb
updated to new Isabelle; made FSet more "quiet"

diff -r 273f57049bd1 -r 2f13fe48c877 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Tue Jul 20 06:14:16 2010 +0100
+++ b/Nominal-General/Nominal2_Base.thy	Thu Jul 22 08:30:50 2010 +0200
@@ -489,7 +489,7 @@
 
 subsection {* Permutations for products *}
 
-instantiation "*" :: (pt, pt) pt
+instantiation prod :: (pt, pt) pt
 begin
 
 primrec 
@@ -504,7 +504,7 @@
 
 subsection {* Permutations for sums *}
 
-instantiation "+" :: (pt, pt) pt
+instantiation sum :: (pt, pt) pt
 begin
 
 primrec 
@@ -603,10 +603,10 @@
 instance "fun" :: (pure, pure) pure
 by default (simp add: permute_fun_def permute_pure)
 
-instance "*" :: (pure, pure) pure
+instance prod :: (pure, pure) pure
 by default (induct_tac x, simp add: permute_pure)
 
-instance "+" :: (pure, pure) pure
+instance sum :: (pure, pure) pure
 by default (induct_tac x, simp_all add: permute_pure)
 
 instance list :: (pure) pure
@@ -987,7 +987,7 @@
   shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"
   by (simp add: fresh_def supp_Pair)
 
-instance "*" :: (fs, fs) fs
+instance prod :: (fs, fs) fs
 apply default
 apply (induct_tac x)
 apply (simp add: supp_Pair finite_supp)
@@ -1011,7 +1011,7 @@
   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"
   by (simp add: fresh_def supp_Inr)
 
-instance "+" :: (fs, fs) fs
+instance sum :: (fs, fs) fs
 apply default
 apply (induct_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
diff -r 273f57049bd1 -r 2f13fe48c877 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Jul 20 06:14:16 2010 +0100
+++ b/Nominal/FSet.thy	Thu Jul 22 08:30:50 2010 +0200
@@ -107,23 +107,6 @@
   unfolding list_eq.simps
   by (simp only: set_map set_in_eq)
 
-text {* Peter *}
-ML {* Quotient_Info.quotient_rules_get @{context} *}
-
-lemma 
-  assumes "Quotient R1 abs1 rep1"
-  and     "Quotient R2 abs2 rep2"
-  shows   "Quotient (R1 OOO R2) (abs1 o ab2) (rep1 o rep2)"
-using assms
-sorry
-
-lemma 
-  assumes "Quotient R1 abs1 rep1"
-  and     "Quotient R2 abs2 rep2"
-  shows   "Quotient (R3) (abs1 o ab2) (rep1 o rep2)"
-using assms
-sorry
-
 lemma quotient_compose_list[quot_thm]:
   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
@@ -740,7 +723,7 @@
 
 lemma singleton_list_eq:
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
-  by (simp add: id_simps) auto
+  by (simp add:) auto
 
 lemma sub_list_cons:
   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
@@ -764,7 +747,7 @@
   assumes a: "fcard_raw xs = Suc n"
   shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
   using a
-  by (induct xs) (auto simp add: memb_def split: if_splits)
+  by (induct xs) (auto simp add: memb_def split_ifs)
 
 lemma singleton_fcard_1:
   shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
@@ -965,7 +948,7 @@
   by (auto simp add: sub_list_set)
 
 lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
-  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint)
 
 lemma memb_set: "memb x xs = (x \<in> set xs)"
   by (simp only: memb_def)
@@ -982,7 +965,7 @@
 
 lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
   by (induct ys arbitrary: xs)
-     (simp_all add: fminus_raw.simps delete_raw_set, blast)
+     (simp_all add: delete_raw_set, blast)
 
 text {* Raw theorems of ffilter *}
 
@@ -1323,25 +1306,10 @@
   shows "fconcat {||} = {||}"
   by (lifting concat.simps(1))
 
-text {* Peter *}
-lemma test: "equivp R ==> a = b --> R a b"
-by (simp add: equivp_def)
-
-lemma 
-  shows "fconcat {||} = {||}"
-apply(lifting_setup concat.simps(1))
-apply(rule test)
-apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *})
-
-sorry
-
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
   by (lifting concat.simps(2))
 
-lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
-  by (lifting concat_append)
-
 text {* ffilter *}
 
 lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
@@ -1350,7 +1318,8 @@
 lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
 by (lifting list_eq_filter)
 
-lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+lemma subset_ffilter: 
+  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
 unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
 
 section {* lemmas transferred from Finite_Set theory *}
@@ -1449,7 +1418,7 @@
 lemma list_all2_refl:
   assumes q: "equivp R"
   shows "(list_all2 R) r r"
-  by (rule list_all2_refl) (metis equivp_def fset_equivp q)
+  by (rule list_all2_refl) (metis equivp_def q)
 
 lemma compose_list_refl2:
   assumes q: "equivp R"
diff -r 273f57049bd1 -r 2f13fe48c877 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Jul 20 06:14:16 2010 +0100
+++ b/Nominal/NewParser.thy	Thu Jul 22 08:30:50 2010 +0200
@@ -438,7 +438,7 @@
   val qtys = map #qtyp qty_infos
   
   (* defining of quotient term-constructors, binding functions, free vars functions *)
-  val _ = warning "Defining the quotient constnats"
+  val _ = warning "Defining the quotient constants"
   val qconstrs_descr = 
     flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
     |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs