src/ZF/pair.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 48891 c0eafbd55de3
child 51717 9e7d1c139569
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41777
1f7cbe39d425 more precise headers;
wenzelm
parents: 28952
diff changeset
     1
(*  Title:      ZF/pair.thy
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
     3
    Copyright   1992  University of Cambridge
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
     4
*)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
     5
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
     6
header{*Ordered Pairs*}
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14864
diff changeset
     8
theory pair imports upair
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
     9
begin
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    10
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46953
diff changeset
    11
ML_file "simpdata.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46953
diff changeset
    12
42795
66fcc9882784 clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents: 42794
diff changeset
    13
setup {*
45625
750c5a47400b modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45620
diff changeset
    14
  Simplifier.map_simpset_global
750c5a47400b modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45620
diff changeset
    15
    (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
750c5a47400b modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45620
diff changeset
    16
      #> Simplifier.add_cong @{thm if_weak_cong})
42794
07155da3b2f4 make ZF_cs snapshot after final setup;
wenzelm
parents: 42459
diff changeset
    17
*}
07155da3b2f4 make ZF_cs snapshot after final setup;
wenzelm
parents: 42459
diff changeset
    18
07155da3b2f4 make ZF_cs snapshot after final setup;
wenzelm
parents: 42459
diff changeset
    19
ML {* val ZF_ss = @{simpset} *}
07155da3b2f4 make ZF_cs snapshot after final setup;
wenzelm
parents: 42459
diff changeset
    20
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45625
diff changeset
    21
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    22
  let
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    23
    val unfold_bex_tac = unfold_tac @{thms Bex_def};
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    24
    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42456
diff changeset
    25
  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    26
*}
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    27
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45625
diff changeset
    28
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    29
  let
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    30
    val unfold_ball_tac = unfold_tac @{thms Ball_def};
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    31
    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42456
diff changeset
    32
  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    33
*}
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 41777
diff changeset
    34
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    35
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    36
(** Lemmas for showing that <a,b> uniquely determines a and b **)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    37
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    38
lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    39
by (rule extension [THEN iff_trans], blast)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    40
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    41
lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    42
by (rule extension [THEN iff_trans], blast)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    43
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    44
lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    45
by (simp add: Pair_def doubleton_eq_iff, blast)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    46
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    47
lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    48
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    49
lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    50
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    51
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45625
diff changeset
    52
lemma Pair_not_0: "<a,b> \<noteq> 0"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    53
apply (unfold Pair_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    54
apply (blast elim: equalityE)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    55
done
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    56
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    57
lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    58
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    59
declare sym [THEN Pair_neq_0, elim!]
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    60
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    61
lemma Pair_neq_fst: "<a,b>=a ==> P"
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    62
proof (unfold Pair_def)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    63
  assume eq: "{{a, a}, {a, b}} = a"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    64
  have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    65
  hence "{a, a} \<in> a" by (simp add: eq)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    66
  moreover have "a \<in> {a, a}" by (rule consI1)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    67
  ultimately show "P" by (rule mem_asym)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    68
qed
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    69
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    70
lemma Pair_neq_snd: "<a,b>=b ==> P"
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    71
proof (unfold Pair_def)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    72
  assume eq: "{{a, a}, {a, b}} = b"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    73
  have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    74
  hence "{a, b} \<in> b" by (simp add: eq)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    75
  moreover have "b \<in> {a, b}" by blast
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    76
  ultimately show "P" by (rule mem_asym)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
    77
qed
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    78
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    79
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
    80
subsection{*Sigma: Disjoint Union of a Family of Sets*}
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
    81
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
    82
text{*Generalizes Cartesian product*}
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    83
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    84
lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    85
by (simp add: Sigma_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    86
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    87
lemma SigmaI [TC,intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a,b> \<in> Sigma(A,B)"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    88
by simp
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    89
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    90
lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42795
diff changeset
    91
lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    92
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    93
(*The general elimination rule*)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    94
lemma SigmaE [elim!]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    95
    "[| c \<in> Sigma(A,B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    96
        !!x y.[| x \<in> A;  y \<in> B(x);  c=<x,y> |] ==> P
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    97
     |] ==> P"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
    98
by (unfold Sigma_def, blast)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
    99
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   100
lemma SigmaE2 [elim!]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   101
    "[| <a,b> \<in> Sigma(A,B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   102
        [| a \<in> A;  b \<in> B(a) |] ==> P
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   103
     |] ==> P"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   104
by (unfold Sigma_def, blast)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   105
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   106
lemma Sigma_cong:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   107
    "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   108
     Sigma(A,B) = Sigma(A',B')"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   109
by (simp add: Sigma_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   110
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   111
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   112
  flex-flex pairs and the "Check your prover" error.  Most
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   113
  Sigmas and Pis are abbreviated as * or -> *)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   114
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   115
lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   116
by blast
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   117
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   118
lemma Sigma_empty2 [simp]: "A*0 = 0"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   119
by blast
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   120
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   121
lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   122
by blast
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   123
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   124
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
   125
subsection{*Projections @{term fst} and @{term snd}*}
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   126
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   127
lemma fst_conv [simp]: "fst(<a,b>) = a"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   128
by (simp add: fst_def)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   129
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   130
lemma snd_conv [simp]: "snd(<a,b>) = b"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   131
by (simp add: snd_def)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   132
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   133
lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   134
by auto
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   135
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   136
lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   137
by auto
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   138
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   139
lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   140
by auto
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   141
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   142
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
   143
subsection{*The Eliminator, @{term split}*}
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   144
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   145
(*A META-equality, so that it applies to higher types as well...*)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   146
lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   147
by (simp add: split_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   148
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   149
lemma split_type [TC]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   150
    "[|  p \<in> Sigma(A,B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   151
         !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x,y>)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45625
diff changeset
   152
     |] ==> split(%x y. c(x,y), p) \<in> C(p)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   153
by (erule SigmaE, auto)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   154
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   155
lemma expand_split:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   156
  "u \<in> A*B ==>
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   157
        R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   158
by (auto simp add: split_def)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   159
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   160
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13240
diff changeset
   161
subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   162
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   163
lemma splitI: "R(a,b) ==> split(R, <a,b>)"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   164
by (simp add: split_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   165
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   166
lemma splitE:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   167
    "[| split(R,z);  z \<in> Sigma(A,B);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46841
diff changeset
   168
        !!x y. [| z = <x,y>;  R(x,y) |] ==> P
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   169
     |] ==> P"
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   170
by (auto simp add: split_def)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   171
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   172
lemma splitD: "split(R,<a,b>) ==> R(a,b)"
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   173
by (simp add: split_def)
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 11694
diff changeset
   174
14864
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   175
text {*
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   176
  \bigskip Complex rules for Sigma.
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   177
*}
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   178
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   179
lemma split_paired_Bex_Sigma [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   180
     "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
14864
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   181
by blast
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   182
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   183
lemma split_paired_Ball_Sigma [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   184
     "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
14864
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   185
by blast
419b45cdb400 new rules for simplifying quantifiers with Sigma
paulson
parents: 13544
diff changeset
   186
9570
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 2469
diff changeset
   187
end
124
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents:
diff changeset
   188
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
   189