# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259941223 -3600
# Node ID c0b13fb70d6d7a49c7e0f6e780382eb834874162
# Parent  8287fb5b8d7a61429a7b84c758df1edf069bf859
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList

diff -r 8287fb5b8d7a -r c0b13fb70d6d IntEx.thy
--- a/IntEx.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -196,48 +196,9 @@
 done
 
 
-lemma foldr_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
-apply (induct l)
-apply (simp add: Quotient_ABS_REP[OF b])
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
-
-lemma foldl_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
-apply (induct l arbitrary:e)
-apply (simp add: Quotient_ABS_REP[OF a])
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
-
-lemma map_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  and     b: "Quotient R2 abs2 rep2"
-  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
-apply (induct l)
-apply (simp)
-apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
-done
 
 
-(* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *)
-lemma nil_prs:
-  shows "map abs1 [] = []"
-by simp
 
-lemma cons_prs:
-  assumes a: "Quotient R1 abs1 rep1"
-  shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
-  apply (induct t)
-by (simp_all add: Quotient_ABS_REP[OF a])
-
-lemma cons_rsp[quotient_rsp]:
-  "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #"
-by simp
 
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
@@ -255,16 +216,14 @@
 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
-lemma nil_listrel_rsp[quotient_rsp]:
-  "(list_rel R) [] []"
-by simp
-
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(rule nil_rsp)
+apply(tactic {* quotient_tac @{context} 1*})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: nil_prs)
+apply(simp only: nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -275,6 +234,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(rule cons_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
diff -r 8287fb5b8d7a -r c0b13fb70d6d QuotList.thy
--- a/QuotList.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -46,7 +46,7 @@
   apply(rule allI)
   apply(induct_tac a)
   apply(simp)
-  apply(simp add: Quotient_ABS_REP[OF q])
+  apply(simp add: Quotient_abs_rep[OF q])
   apply(rule conjI)
   apply(rule allI)
   apply(induct_tac a)
@@ -58,53 +58,62 @@
   done
 
 
-
-
-
+lemma cons_prs:
+  assumes q: "Quotient R Abs Rep"
+  shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
+by (induct t) (simp_all add: Quotient_abs_rep[OF q])
 
-(* Rest is not used *)
-
-
-lemma CONS_PRS:
+lemma cons_rsp:
   assumes q: "Quotient R Abs Rep"
-  shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
-by (induct t) (simp_all add: Quotient_ABS_REP[OF q])
+  shows "(R ===> list_rel R ===> list_rel R) op # op #"
+by (auto)
 
-lemma CONS_RSP:
+lemma nil_prs:
   assumes q: "Quotient R Abs Rep"
-  and     a: "R h1 h2" "list_rel R t1 t2"
-  shows "list_rel R (h1#t1) (h2#t2)"
-using a by (auto)
-
-lemma NIL_PRS:
-  assumes q: "Quotient R Abs Rep"
-  shows "[] = (map Abs [])"
+  shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma NIL_RSP:
+lemma nil_rsp:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
 
-lemma MAP_PRS:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
-by (induct l)
-   (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2])
+lemma map_prs:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
+by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma MAP_RSP:
+(* We need an ho version *)
+lemma map_rsp:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     a: "(R1 ===> R2) f1 f2"
   and     b: "list_rel R1 l1 l2"
   shows "list_rel R2 (map f1 l1) (map f2 l2)"
 using b a
-by (induct l1 l2 rule: list_induct2')
-   (simp_all)
+by (induct l1 l2 rule: list_induct2') (simp_all)
+
+lemma foldr_prs:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
+by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+
+lemma foldl_prs:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
+by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
 
 
+
+
+
+
+(* TODO: Rest are unused *)
+
 lemma LIST_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
diff -r 8287fb5b8d7a -r c0b13fb70d6d QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -1081,7 +1081,7 @@
     val thy = ProofContext.theory_of lthy;
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
+    val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
diff -r 8287fb5b8d7a -r c0b13fb70d6d QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -41,7 +41,7 @@
                         (\<forall>a. E (Rep a) (Rep a)) \<and> 
                         (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
-lemma Quotient_ABS_REP:
+lemma Quotient_abs_rep:
   assumes a: "Quotient E Abs Rep"
   shows "Abs (Rep a) = a" 
 using a unfolding Quotient_def
@@ -77,7 +77,7 @@
 using a unfolding Quotient_def
 by metis
 
-lemma Quotient_REP_ABS:
+lemma Quotient_rep_abs:
   assumes a: "Quotient R Abs Rep"
   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
 using a unfolding Quotient_def
@@ -283,7 +283,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 lemma lambda_prs1:
@@ -291,7 +291,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 (* Not used since applic_prs proves a version for an arbitrary number of arguments *)
@@ -300,7 +300,7 @@
   and     q2: "Quotient R2 abs2 rep2"
   shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
 unfolding expand_fun_eq
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
@@ -328,14 +328,14 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
 
 (* Not used *)
 lemma REP_ABS_RSP_LEFT:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
@@ -347,7 +347,7 @@
 lemma IF_PRS:
   assumes q: "Quotient R Abs Rep"
   shows "If a b c = Abs (If a (Rep b) (Rep c))"
-using Quotient_ABS_REP[OF q] by auto
+using Quotient_abs_rep[OF q] by auto
 
 (* ask peter: no use of q *)
 lemma IF_RSP:
@@ -360,7 +360,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
 
 lemma LET_RSP:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -384,7 +384,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
 
 (* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
@@ -408,7 +408,7 @@
 lemma I_PRS:
   assumes q: "Quotient R Abs Rep"
   shows "id e = Abs (id (Rep e))"
-using Quotient_ABS_REP[OF q] by auto
+using Quotient_abs_rep[OF q] by auto
 
 lemma I_RSP:
   assumes q: "Quotient R Abs Rep"
@@ -421,7 +421,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   and     q3: "Quotient R3 Abs3 Rep3"
   shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
-using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3]
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
 unfolding o_def expand_fun_eq
 by simp