--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 13:39:34 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 19:10:55 2010 +0200
@@ -2,14 +2,12 @@
 imports "../../../Nominal/FSet"
 begin
 
-(*sledgehammer[overlord,isar_proof,sorts]*)
-
 notation
   list_eq (infix "\<approx>" 50)
 
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (lifting list.exhaust)
+  by (lifting list.exhaust)
 
 lemma list_rel_find_element:
   assumes a: "x \<in> set a"
@@ -48,7 +46,7 @@
 
 lemma [quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-proof (rule fun_relI, (erule pred_compE, erule pred_compE))
+proof (rule fun_relI, elim pred_compE)
   fix a b ba bb
   assume a: "list_rel op \<approx> a ba"
   assume b: "ba \<approx> bb"
@@ -79,73 +77,74 @@
   unfolding list_eq.simps
   by (simp only: set_map set_in_eq)
 
-lemma quotient_compose_list_pre:
-  "(list_rel op \<approx> OOO op \<approx>) r s =
-  ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>
-  abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
-  apply rule
-  apply rule
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (rule)
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
-  apply (metis Quotient_rel[OF Quotient_fset])
-  apply (auto simp only:)[1]
-  apply (subgoal_tac "map abs_fset r = map abs_fset b")
-  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 (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  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 (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
-  apply (rule map_rel_cong)
-  apply (assumption)
-  apply (subst Quotient_rel[OF Quotient_fset])
-  apply simp
-  done
+lemma compose_list_refl:
+  shows "(list_rel op \<approx> OOO op \<approx>) r r"
+proof
+  show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp)
+  have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+  show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+qed
+
+lemma list_rel_refl:
+  shows "(list_rel op \<approx>) r r"
+  by (rule list_rel_refl)(metis equivp_def fset_equivp)
+
+lemma Quotient_fset_list:
+  shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
+  by (fact list_quotient[OF Quotient_fset])
 
 lemma quotient_compose_list[quot_thm]:
   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
-  apply (rule)+
-  apply (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
-  apply (rule)
-  apply (rule)
-  apply (rule)
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (rule)
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply rule
-  apply (rule quotient_compose_list_pre)
-  done
+proof (intro conjI allI)
+  fix a r s
+  show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
+    by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
+  have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+    by (rule list_rel_refl)
+  have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
+  show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+    by (rule, rule list_rel_refl) (rule c)
+  show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
+        (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+  proof (intro iffI conjI)
+    show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
+    show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
+  next
+    assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
+    then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+      fix b ba
+      assume c: "list_rel op \<approx> r b"
+      assume d: "b \<approx> ba"
+      assume e: "list_rel op \<approx> ba s"
+      have f: "map abs_fset r = map abs_fset b"
+        by (metis Quotient_rel[OF Quotient_fset_list] c)
+      have g: "map abs_fset s = map abs_fset ba"
+        by (metis Quotient_rel[OF Quotient_fset_list] e)
+      show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp
+    qed
+    then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+      by (metis Quotient_rel[OF Quotient_fset])
+  next
+    assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
+      \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+    then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
+    have d: "map abs_fset r \<approx> map abs_fset s"
+      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+    have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
+      by (rule map_rel_cong[OF d])
+    have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
+      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
+    have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
+      by (rule pred_compI) (rule b, rule y)
+    have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
+      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
+    then show "(list_rel op \<approx> OOO op \<approx>) r s"
+      using a c pred_compI by simp
+  qed
+qed
 
 lemma nil_prs2[quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
   by simp
@@ -182,18 +181,69 @@
   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
+lemma list_rel_app_l:
+  assumes a: "reflp R"
+  and b: "list_rel R l r"
+  shows "list_rel R (z @ l) (z @ r)"
+  by (induct z) (simp_all add: b, metis a reflp_def)
+
+lemma append_rsp2_pre0:
+  assumes a:"list_rel op \<approx> x x'"
+  shows "list_rel op \<approx> (x @ z) (x' @ z)"
+  using a apply (induct x x' rule: list_induct2')
+  apply simp_all
+  apply (rule list_rel_refl)
+  done
+
+lemma append_rsp2_pre1:
+  assumes a:"list_rel op \<approx> x x'"
+  shows "list_rel op \<approx> (z @ x) (z @ x')"
+  using a apply (induct x x' arbitrary: z rule: list_induct2')
+  apply (rule list_rel_refl)
+  apply (simp_all del: list_eq.simps)
+  apply (rule list_rel_app_l)
+  apply (simp_all add: reflp_def)
+  done
+
+lemma append_rsp2_pre:
+  assumes a:"list_rel op \<approx> x x'"
+  and     b: "list_rel op \<approx> z z'"
+  shows "list_rel op \<approx> (x @ z) (x' @ z')"
+  apply (rule list_rel_transp[OF fset_equivp])
+  apply (rule append_rsp2_pre0)
+  apply (rule a)
+  using b apply (induct z z' rule: list_induct2')
+  apply (simp_all only: append_Nil2)
+  apply (rule list_rel_refl)
+  apply simp_all
+  apply (rule append_rsp2_pre1)
+  apply simp
+  done
+
 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
+proof (intro fun_relI, elim pred_compE)
+  fix x y z w x' z' y' w' :: "'a list list"
+  assume a:"list_rel op \<approx> x x'"
+  and b:    "x' \<approx> y'"
+  and c:    "list_rel op \<approx> y' y"
+  assume aa: "list_rel op \<approx> z z'"
+  and bb:   "z' \<approx> w'"
+  and cc:   "list_rel op \<approx> w' w"
+  have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
+  have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
+  have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
+  have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
+    by (rule pred_compI) (rule b', rule c')
+  show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
+    by (rule pred_compI) (rule a', rule d')
+qed
 
 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
@@ -211,6 +261,8 @@
 syntax (HTML output)
 "_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
 
+ML {* Syntax.check_term @{context} (Const ("List.append", dummyT) $ @{term "[3::nat,4]"}) *}
+
 parse_translation (advanced) {*
 let
   val femptyC = Syntax.const @{const_name fempty};