doc-src/ZF/ZF_examples.thy
author nipkow
Sun, 22 Feb 2009 17:25:28 +0100
changeset 30056 0a35bee25c20
parent 16417 9bc16273c2d4
child 35416 d8d7d1b785af
permissions -rw-r--r--
added lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     1
header{*Examples of Reasoning in ZF Set Theory*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     2
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14159
diff changeset
     3
theory ZF_examples imports Main_ZFC begin
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     4
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     5
subsection {* Binary Trees *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     6
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     7
consts
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     8
  bt :: "i => i"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     9
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    10
datatype "bt(A)" =
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    11
  Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    12
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    13
declare bt.intros [simp]
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    14
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    15
text{*Induction via tactic emulation*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    16
lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    17
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    18
  apply (induct_tac l)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    19
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    20
  apply auto
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    21
  done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    22
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    23
(*
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    24
  apply (Inductive.case_tac l)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    25
  apply (tactic {*exhaust_tac "l" 1*})
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    26
*)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    27
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    28
text{*The new induction method, which I don't understand*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    29
lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    30
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    31
  apply (induct set: bt)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    32
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    33
  apply auto
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    34
  done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    35
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    36
lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    37
  -- "Proving a freeness theorem."
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    38
  by (blast elim!: bt.free_elims)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    39
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    40
inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    41
  -- "An elimination rule, for type-checking."
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    42
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    43
text {*
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    44
@{thm[display] Br_in_bt[no_vars]}
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    45
*};
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    46
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    47
subsection{*Primitive recursion*}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    48
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    49
consts  n_nodes :: "i => i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    50
primrec
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    51
  "n_nodes(Lf) = 0"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    52
  "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    53
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    54
lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    55
  by (induct_tac t, auto) 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    56
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    57
consts  n_nodes_aux :: "i => i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    58
primrec
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    59
  "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    60
  "n_nodes_aux(Br(a,l,r)) = 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    61
      (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    62
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    63
lemma n_nodes_aux_eq [rule_format]:
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    64
     "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    65
  by (induct_tac t, simp_all) 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    66
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    67
constdefs  n_nodes_tail :: "i => i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    68
   "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    69
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    70
lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    71
 by (simp add: n_nodes_tail_def n_nodes_aux_eq) 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    72
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    73
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    74
subsection {*Inductive definitions*}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    75
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    76
consts  Fin       :: "i=>i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    77
inductive
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    78
  domains   "Fin(A)" \<subseteq> "Pow(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    79
  intros
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    80
    emptyI:  "0 \<in> Fin(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    81
    consI:   "[| a \<in> A;  b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    82
  type_intros  empty_subsetI cons_subsetI PowI
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    83
  type_elims   PowD [THEN revcut_rl]
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    84
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    85
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    86
consts  acc :: "i => i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    87
inductive
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    88
  domains "acc(r)" \<subseteq> "field(r)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    89
  intros
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    90
    vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    91
  monos      Pow_mono
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    92
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    93
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    94
consts
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    95
  llist  :: "i=>i";
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    96
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    97
codatatype
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    98
  "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
    99
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   100
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   101
(*Coinductive definition of equality*)
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   102
consts
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   103
  lleq :: "i=>i"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   104
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   105
(*Previously used <*> in the domain and variant pairs as elements.  But
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   106
  standard pairs work just as well.  To use variant pairs, must change prefix
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   107
  a q/Q to the Sigma, Pair and converse rules.*)
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   108
coinductive
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   109
  domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   110
  intros
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   111
    LNil:  "<LNil, LNil> \<in> lleq(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   112
    LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   113
            ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   114
  type_intros  llist.intros
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   115
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   116
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   117
subsection{*Powerset example*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   118
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   119
lemma Pow_mono: "A\<subseteq>B  ==>  Pow(A) \<subseteq> Pow(B)"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   120
apply (rule subsetI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   121
apply (rule PowI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   122
apply (drule PowD)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   123
apply (erule subset_trans, assumption)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   124
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   125
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   126
lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   127
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   128
apply (rule equalityI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   129
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   130
apply (rule Int_greatest)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   131
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   132
apply (rule Int_lower1 [THEN Pow_mono])
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   133
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   134
apply (rule Int_lower2 [THEN Pow_mono])
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   135
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   136
apply (rule subsetI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   137
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   138
apply (erule IntE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   139
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   140
apply (rule PowI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   141
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   142
apply (drule PowD)+
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   143
  --{* @{subgoals[display,indent=0,margin=65]} *}
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   144
apply (rule Int_greatest)
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   145
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   146
apply (assumption+)
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   147
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   148
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   149
text{*Trying again from the beginning in order to use @{text blast}*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   150
lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   151
by blast
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   153
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   154
lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   155
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   156
apply (rule subsetI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   157
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   158
apply (erule UnionE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   159
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   160
apply (rule UnionI)
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   161
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   162
apply (erule subsetD)
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   163
  --{* @{subgoals[display,indent=0,margin=65]} *}
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   164
apply assumption 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   165
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   166
apply assumption 
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   167
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   168
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   169
text{*A more abstract version of the same proof*}
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   170
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   171
lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   172
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   173
apply (rule Union_least)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   174
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   175
apply (rule Union_upper)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   176
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   177
apply (erule subsetD, assumption)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   178
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   179
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   180
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   181
lemma "[| a \<in> A;  f \<in> A->B;  g \<in> C->D;  A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   182
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   183
apply (rule apply_equality)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   184
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   185
apply (rule UnI1)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   186
  --{* @{subgoals[display,indent=0,margin=65]} *}
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   187
apply (rule apply_Pair)
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   188
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   189
apply assumption 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   190
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   191
apply assumption 
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   192
  --{* @{subgoals[display,indent=0,margin=65]} *}
14159
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   193
apply (rule fun_disjoint_Un)
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   194
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   195
apply assumption 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   196
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   197
apply assumption 
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   198
  --{* @{subgoals[display,indent=0,margin=65]} *}
e2eba24c8a2a final tweaks for Isar version
paulson
parents: 14152
diff changeset
   199
apply assumption 
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   200
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   201
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
   202
end