# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260411942 -3600
# Node ID 8aa67d037b3cd14c8e040156449baaf0e000b3d6
# Parent  3c6419a5a7fc9f8780313fbd85358b36f53175fa# Parent  fe64784b38c3c8f4d84f15631913a1886f591877
merged

diff -r fe64784b38c3 -r 8aa67d037b3c Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 02:42:09 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 03:25:42 2009 +0100
@@ -151,7 +151,7 @@
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
@@ -161,62 +161,26 @@
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
-lemma append_rsp_fst:
-  assumes a : "l1 \<approx> l2"
-  shows "(l1 @ s) \<approx> (l2 @ s)"
-  using a
-  by (induct) (auto intro: list_eq.intros list_eq_refl)
-
-lemma append_end:
-  shows "(e # l) \<approx> (l @ [e])"
-  apply (induct l)
-  apply (auto intro: list_eq.intros list_eq_refl)
-  done
-
-lemma rev_rsp:
-  shows "a \<approx> rev a"
-  apply (induct a)
-  apply simp
-  apply (rule list_eq_refl)
-  apply simp_all
-  apply (rule list_eq.intros(6))
-  prefer 2
-  apply (rule append_rsp_fst)
-  apply assumption
-  apply (rule append_end)
-  done
+lemma append_rsp_aux1:
+  assumes a : "l2 \<approx> r2 "
+  shows "(h @ l2) \<approx> (h @ r2)"
+using a
+apply(induct h)
+apply(auto intro: list_eq.intros(5))
+done
 
-lemma append_sym_rsp:
-  shows "(a @ b) \<approx> (b @ a)"
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  apply (rule rev_rsp)
-  apply (rule list_eq.intros(6))
-  apply (rule rev_rsp)
-  apply (simp)
-  apply (rule append_rsp_fst)
-  apply (rule list_eq.intros(3))
-  apply (rule rev_rsp)
-  done
+lemma append_rsp_aux2:
+  assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
+  shows "(l1 @ l2) \<approx> (r1 @ r2)"
+using a
+apply(induct arbitrary: l2 r2)
+apply(simp_all)
+apply(blast intro: list_eq.intros append_rsp_aux1)+
+done
 
-lemma append_rsp:
-  assumes a : "l1 \<approx> r1"
-  assumes b : "l2 \<approx> r2 "
-  shows "(l1 @ l2) \<approx> (r1 @ r2)"
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  using a apply (assumption)
-  apply (rule list_eq.intros(6))
-  apply (rule append_sym_rsp)
-  apply (rule list_eq.intros(6))
-  apply (rule append_rsp_fst)
-  using b apply (assumption)
-  apply (rule append_sym_rsp)
-  done
-
-lemma ho_append_rsp[quot_respect]:
+lemma append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by (simp add: append_rsp)
+  by (auto simp add: append_rsp_aux2)
 
 lemma map_rsp:
   assumes a: "a \<approx> b"
diff -r fe64784b38c3 -r 8aa67d037b3c Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 02:42:09 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 03:25:42 2009 +0100
@@ -218,12 +218,15 @@
 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
 done
 
-definition int_of_nat_raw: "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+definition int_of_nat_raw: 
+  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_def
-  int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" where "int_of_nat_raw"
+  int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" 
+where "int_of_nat_raw"
 
-lemma[quot_respect]: "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+lemma[quot_respect]: 
+  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
 by (simp add: equivp_reflp[OF int_equivp])
 
 lemma int_def:
@@ -326,7 +329,7 @@
 
 lemma zero_le_imp_eq_int_raw:
   fixes k::"(nat \<times> nat)"
-  shows "less_raw (0,0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+  shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
 apply(cases k)
 apply(simp add:int_of_nat_raw)
 apply(auto)
@@ -337,14 +340,17 @@
 lemma zero_le_imp_eq_int:
   fixes k::int
   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n"
-unfolding less_int_def by (lifting zero_le_imp_eq_int_raw)
+  unfolding less_int_def 
+  by (lifting zero_le_imp_eq_int_raw)
 
 lemma zmult_zless_mono2: 
   fixes i j k::int
   assumes a: "i < j" "0 < k"
   shows "k * i < k * j"
 using a
+using a
 apply(drule_tac zero_le_imp_eq_int)
+apply(fold int_def)
 apply(auto simp add: zmult_zless_mono2_lemma)
 done