deleted duplicate lemma
authorChristian Urban <urbanc@in.tum.de>
Wed Aug 11 13:30:24 2010 +0800 (2010-08-11)
changeset 38317cb8e2ac6397b
parent 38316 88e774d09fbc
child 38320 ac3080d48b01
deleted duplicate lemma
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     1.1 --- a/src/HOL/Quotient.thy	Tue Aug 10 22:26:23 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Aug 11 13:30:24 2010 +0800
     1.3 @@ -136,16 +136,6 @@
     1.4    shows "((op =) ===> (op =)) = (op =)"
     1.5    by (simp add: expand_fun_eq)
     1.6  
     1.7 -lemma fun_rel_id:
     1.8 -  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
     1.9 -  shows "(R1 ===> R2) f g"
    1.10 -  using a by simp
    1.11 -
    1.12 -lemma fun_rel_id_asm:
    1.13 -  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
    1.14 -  shows "A \<longrightarrow> (R1 ===> R2) f g"
    1.15 -  using a by auto
    1.16 -
    1.17  
    1.18  subsection {* Quotient Predicate *}
    1.19  
    1.20 @@ -597,7 +587,7 @@
    1.21  lemma quot_rel_rsp:
    1.22    assumes a: "Quotient R Abs Rep"
    1.23    shows "(R ===> R ===> op =) R R"
    1.24 -  apply(rule fun_rel_id)+
    1.25 +  apply(rule fun_relI)+
    1.26    apply(rule equals_rsp[OF a])
    1.27    apply(assumption)+
    1.28    done
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Aug 10 22:26:23 2010 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 11 13:30:24 2010 +0800
     2.3 @@ -316,7 +316,7 @@
     2.4     The deterministic part:
     2.5      - remove lambdas from both sides
     2.6      - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
     2.7 -    - prove Ball/Bex relations unfolding fun_rel_id
     2.8 +    - prove Ball/Bex relations using fun_relI
     2.9      - reflexivity of equality
    2.10      - prove equality of relations using equals_rsp
    2.11      - use user-supplied RSP theorems
    2.12 @@ -335,7 +335,7 @@
    2.13  (case (bare_concl goal) of
    2.14      (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
    2.15    (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
    2.16 -      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
    2.17 +      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
    2.18  
    2.19      (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
    2.20  | (Const (@{const_name "op ="},_) $
    2.21 @@ -347,7 +347,7 @@
    2.22  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
    2.23      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
    2.24      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
    2.25 -      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
    2.26 +      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
    2.27  
    2.28      (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
    2.29  | Const (@{const_name "op ="},_) $
    2.30 @@ -359,7 +359,7 @@
    2.31  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
    2.32      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
    2.33      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
    2.34 -      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
    2.35 +      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
    2.36  
    2.37  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
    2.38      (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)