respectfullness and preservation of map for identity quotients
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue Apr 20 14:56:58 2010 +0200 (2010-04-20)
changeset 362168fb6cc6f3b94
parent 36215 88ff48884d26
child 36217 3ff993695175
respectfullness and preservation of map for identity quotients
src/HOL/Library/Quotient_List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Tue Apr 20 14:56:20 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Apr 20 14:56:58 2010 +0200
     1.3 @@ -130,24 +130,24 @@
     1.4    by (induct l)
     1.5       (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
     1.6  
     1.7 -
     1.8  lemma map_prs[quot_preserve]:
     1.9    assumes a: "Quotient R1 abs1 rep1"
    1.10    and     b: "Quotient R2 abs2 rep2"
    1.11    shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
    1.12 -  by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
    1.13 -     (simp)
    1.14 -
    1.15 +  and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
    1.16 +  by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
    1.17 +     (simp_all add: Quotient_abs_rep[OF a])
    1.18  
    1.19  lemma map_rsp[quot_respect]:
    1.20    assumes q1: "Quotient R1 Abs1 Rep1"
    1.21    and     q2: "Quotient R2 Abs2 Rep2"
    1.22    shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
    1.23 -  apply(simp)
    1.24 -  apply(rule allI)+
    1.25 -  apply(rule impI)
    1.26 -  apply(rule allI)+
    1.27 -  apply (induct_tac xa ya rule: list_induct2')
    1.28 +  and   "((R1 ===> op =) ===> (list_rel R1) ===> op =) map map"
    1.29 +  apply simp_all
    1.30 +  apply(rule_tac [!] allI)+
    1.31 +  apply(rule_tac [!] impI)
    1.32 +  apply(rule_tac [!] allI)+
    1.33 +  apply (induct_tac [!] xa ya rule: list_induct2')
    1.34    apply simp_all
    1.35    done
    1.36