# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260306134 -3600
# Node ID fe2a37cfecd3c9e287cc6dfd2ec255d9d33b8182
# Parent  97a397ba57437df184ae3a63f19464eff5551745
proper formulation of all preservation theorems

diff -r 97a397ba5743 -r fe2a37cfecd3 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 20:55:55 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 22:02:14 2009 +0100
@@ -204,8 +204,8 @@
 
 lemma "foldl PLUS x [] = x"
 apply(lifting ho_tst)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -215,8 +215,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
@@ -226,10 +226,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
-(* TODO: does not work when this is added *)
-(* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
@@ -310,8 +308,8 @@
 apply(rule impI)
 apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac  @{context} 1 *})
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -344,9 +342,9 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
 apply(cleaning)
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])
 done
 
 end
diff -r 97a397ba5743 -r fe2a37cfecd3 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Dec 08 20:55:55 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 22:02:14 2009 +0100
@@ -92,12 +92,21 @@
   shows "list_rel R [] []"
 by simp
 
-lemma map_prs:
+lemma map_prs_aux:
   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_prs[quot_preserve]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
+by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b])
+   (simp)
+
+
 lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
@@ -110,18 +119,33 @@
 apply simp_all
 done
 
-lemma foldr_prs:
+lemma foldr_prs_aux:
   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:
+lemma foldr_prs[quot_respect]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
+by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b])
+   (simp)
+
+lemma foldl_prs_aux:
   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])
 
+
+lemma foldl_prs[quot_preserve]:
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
+by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b])
+   (simp)
+
 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0"
 by (induct b) (simp_all)