--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 16:25:00 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 16:25:24 2010 +0200
@@ -2,6 +2,8 @@
 imports "../../../Nominal/FSet"
 begin
 
+(*sledgehammer[overlord,isar_proof,sorts]*)
+
 notation
   list_eq (infix "\<approx>" 50)
 
@@ -25,39 +27,47 @@
 qed
 
 lemma concat_rsp_pre:
-  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y; \<exists>x\<in>set x. xa \<in> set x\<rbrakk> \<Longrightarrow> 
-    \<exists>x\<in>set y. xa \<in> set x"
-  apply clarify
-  apply (frule list_rel_find_element[of _ "x"])
-  apply assumption
-  apply clarify
-  apply (subgoal_tac "ya \<in> set y'")
-  prefer 2
-  apply simp
-  apply (frule list_rel_find_element[of _ "y'"])
-  apply assumption
-  apply auto
-  done
+  assumes a: "list_rel op \<approx> x x'"
+  and     b: "x' \<approx> y'"
+  and     c: "list_rel op \<approx> y' y"
+  and     d: "\<exists>x\<in>set x. xa \<in> set x"
+  shows "\<exists>x\<in>set y. xa \<in> set x"
+proof -
+  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
+  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
+  have j: "ya \<in> set y'" using b h by simp
+  have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+  then show ?thesis using f i by auto
+qed
+
+lemma fun_relI [intro]:
+  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
+  shows "(P ===> Q) x y"
+  using assms by (simp add: fun_rel_def)
 
 lemma [quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-  apply (simp only: fun_rel_def)
-  apply clarify
-  apply (simp (no_asm))
-  apply rule
-  apply rule
-  apply (erule concat_rsp_pre)
-  apply assumption+
-  apply (rule concat_rsp_pre)
-  prefer 4
-  apply assumption
-  apply (rule list_rel_symp[OF list_eq_equivp])
-  apply assumption
-  apply (rule equivp_symp[OF list_eq_equivp])
-  apply assumption
-  apply (rule list_rel_symp[OF list_eq_equivp])
-  apply assumption
-  done
+proof (rule fun_relI, (erule pred_compE, erule pred_compE))
+  fix a b ba bb
+  assume a: "list_rel op \<approx> a ba"
+  assume b: "ba \<approx> bb"
+  assume c: "list_rel op \<approx> bb b"
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "concat a \<approx> concat b" by simp
+qed
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   by (metis nil_rsp list_rel.simps(1) pred_compI)
@@ -82,7 +92,7 @@
   apply (rule equivp_reflp[OF fset_equivp])
   apply (rule list_rel_refl)
   apply (metis equivp_def fset_equivp)
-  apply(rule)
+  apply (rule)
   apply rule
   apply (rule list_rel_refl)
   apply (metis equivp_def fset_equivp)
@@ -94,29 +104,27 @@
   apply (metis Quotient_rel[OF Quotient_fset])
   apply (auto simp only:)[1]
   apply (subgoal_tac "map abs_fset r = map abs_fset b")
-  prefer 2
+  apply (subgoal_tac "map abs_fset s = map abs_fset ba")
+  apply (simp only: map_rel_cong)
   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (subgoal_tac "map abs_fset s = map abs_fset ba")
-  prefer 2
   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (simp only: map_rel_cong)
   apply rule
   apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
   apply (rule list_rel_refl)
   apply (metis equivp_def fset_equivp)
   apply rule
+  apply (erule conjE)+
   prefer 2
   apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
   apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
   apply (rule list_rel_refl)
   apply (metis equivp_def fset_equivp)
-  apply (erule conjE)+
   apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
-  prefer 2
-  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
   apply (rule map_rel_cong)
   apply (assumption)
+  apply (subst Quotient_rel[OF Quotient_fset])
+  apply simp
   done
 
 lemma quotient_compose_list[quot_thm]:
@@ -139,12 +147,12 @@
   apply (rule quotient_compose_list_pre)
   done
 
+lemma nil_prs2[quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+  by simp
+
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-  apply(lifting concat.simps(1))
-  apply(cleaning)
-  apply(simp add: comp_def bot_fset_def)
-  done
+  by (lifting concat.simps(1))
 
 lemma insert_rsp2[quot_respect]:
   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
@@ -160,16 +168,32 @@
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (auto)
 
+lemma insert_prs2[quot_preserve]:
+  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+      abs_o_rep[OF Quotient_fset] map_id finsert_def)
+
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-  apply (lifting concat.simps(2))
-  apply (cleaning)
-  apply (simp add: finsert_def fconcat_def comp_def)
-  apply (cleaning)
-  done
+  by (lifting concat.simps(2))
+
+lemma append_prs2[quot_preserve]:
+  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+      abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
+
+lemma append_rsp2[quot_respect]:
+  "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
+  sorry
+
+lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+  by (lifting concat_append)
 
 (* TBD *)
 
+
+find_theorems concat
+
 text {* syntax for fset comprehensions (adapted from lists) *}
 
 nonterminals fsc_qual fsc_quals