# HG changeset patch # User haftmann # Date 1274448505 -7200 # Node ID 609ad88a94fca9dae8c3f57b000f44cf5424b92d # Parent ca1c293e521ea3a5a5eb82ca278a7effa6a09335# Parent a89b47a94b19d80068ce4db8bf4f98b2b0d4d892 merged diff -r a89b47a94b19 -r 609ad88a94fc src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Fri May 21 15:22:37 2010 +0200 +++ b/src/HOL/Quotient.thy Fri May 21 15:28:25 2010 +0200 @@ -618,15 +618,13 @@ lemma let_prs: assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" - shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f" - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto + shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + by (auto simp add: expand_fun_eq) lemma let_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - and a1: "(R1 ===> R2) f g" - and a2: "R1 x y" - shows "R2 ((Let x f)::'c) ((Let y g)::'c)" - using apply_rsp[OF q1 a1] a2 by auto + shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" + by auto locale quot_type = fixes R :: "'a \ 'a \ bool" @@ -716,8 +714,8 @@ declare [[map "fun" = (fun_map, fun_rel)]] lemmas [quot_thm] = fun_quotient -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp -lemmas [quot_preserve] = if_prs o_prs +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp +lemmas [quot_preserve] = if_prs o_prs let_prs lemmas [quot_equiv] = identity_equivp