src/HOL/NumberTheory/BijectionRel.thy
changeset 13524 604d0f3622d6
parent 11549 e7265e70fd7c
child 13630 a013a9dd370f
     1.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -77,26 +77,27 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 -lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
     1.8 +lemma inj_func_bijR_aux1:
     1.9 +    "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
    1.10    apply (unfold inj_on_def)
    1.11    apply auto
    1.12    done
    1.13  
    1.14 -lemma aux:
    1.15 +lemma inj_func_bijR_aux2:
    1.16    "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
    1.17      ==> (F, f ` F) \<in> bijR P"
    1.18    apply (rule_tac F = F and A = A in aux_induct)
    1.19       apply (rule finite_subset)
    1.20        apply auto
    1.21    apply (rule bijR.insert)
    1.22 -     apply (rule_tac [3] aux)
    1.23 +     apply (rule_tac [3] inj_func_bijR_aux1)
    1.24          apply auto
    1.25    done
    1.26  
    1.27  lemma inj_func_bijR:
    1.28    "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
    1.29      ==> (A, f ` A) \<in> bijR P"
    1.30 -  apply (rule aux)
    1.31 +  apply (rule inj_func_bijR_aux2)
    1.32       apply auto
    1.33    done
    1.34  
    1.35 @@ -166,14 +167,14 @@
    1.36        apply auto
    1.37    done
    1.38  
    1.39 -lemma aux: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
    1.40 +lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
    1.41    apply auto
    1.42    done
    1.43  
    1.44  lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
    1.45    apply (unfold bijP_def)
    1.46    apply (rule iffI)
    1.47 -  apply (erule_tac [!] aux)
    1.48 +  apply (erule_tac [!] aux_foo)
    1.49        apply simp_all
    1.50    apply (rule iffD2)
    1.51     apply (rule_tac P = P in aux_sym)