1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ZF/ZF_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     1.3 @@ -0,0 +1,121 @@
     1.4 +header{*Examples of Reasoning in ZF Set Theory*}
     1.5 +
     1.6 +theory ZF_examples = Main_ZFC:
     1.7 +
     1.8 +subsection {* Binary Trees *}
     1.9 +
    1.10 +consts
    1.11 +  bt :: "i => i"
    1.12 +
    1.13 +datatype "bt(A)" =
    1.14 +  Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
    1.15 +
    1.16 +declare bt.intros [simp]
    1.17 +
    1.18 +text{*Induction via tactic emulation*}
    1.19 +lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
    1.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.21 +  apply (induct_tac l)
    1.22 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.23 +  apply auto
    1.24 +  done
    1.25 +
    1.26 +(*
    1.27 +  apply (Inductive.case_tac l)
    1.28 +  apply (tactic {*exhaust_tac "l" 1*})
    1.29 +*)
    1.30 +
    1.31 +text{*The new induction method, which I don't understand*}
    1.32 +lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
    1.33 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.34 +  apply (induct set: bt)
    1.35 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.36 +  apply auto
    1.37 +  done
    1.38 +
    1.39 +lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
    1.40 +  -- "Proving a freeness theorem."
    1.41 +  by (blast elim!: bt.free_elims)
    1.42 +
    1.43 +inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
    1.44 +  -- "An elimination rule, for type-checking."
    1.45 +
    1.46 +text {*
    1.47 +@{thm[display] BrE[no_vars]}
    1.48 +\rulename{BrE}
    1.49 +*};
    1.50 +
    1.51 +subsection{*Powerset example*}
    1.52 +
    1.53 +lemma Pow_mono: "A<=B  ==>  Pow(A) <= Pow(B)"
    1.54 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.55 +apply (rule subsetI)
    1.56 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.57 +apply (rule PowI)
    1.58 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.59 +apply (drule PowD)
    1.60 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.61 +apply (erule subset_trans, assumption)
    1.62 +done
    1.63 +
    1.64 +lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    1.65 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.66 +apply (rule equalityI)
    1.67 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.68 +apply (rule Int_greatest)
    1.69 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.70 +apply (rule Int_lower1 [THEN Pow_mono])
    1.71 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.72 +apply (rule Int_lower2 [THEN Pow_mono])
    1.73 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.74 +apply (rule subsetI)
    1.75 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.76 +apply (erule IntE)
    1.77 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.78 +apply (rule PowI)
    1.79 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.80 +apply (drule PowD)+
    1.81 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.82 +apply (rule Int_greatest, assumption+)
    1.83 +done
    1.84 +
    1.85 +text{*Trying again from the beginning in order to use @{text blast}*}
    1.86 +lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    1.87 +by blast
    1.88 +
    1.89 +
    1.90 +lemma "C<=D ==> Union(C) <= Union(D)"
    1.91 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.92 +apply (rule subsetI)
    1.93 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.94 +apply (erule UnionE)
    1.95 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.96 +apply (rule UnionI)
    1.97 +apply (erule subsetD, assumption, assumption)
    1.98 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.99 +done
   1.100 +
   1.101 +text{*Trying again from the beginning in order to prove from the definitions*}
   1.102 +
   1.103 +lemma "C<=D ==> Union(C) <= Union(D)"
   1.104 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.105 +apply (rule Union_least)
   1.106 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.107 +apply (rule Union_upper)
   1.108 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.109 +apply (erule subsetD, assumption)
   1.110 +done
   1.111 +
   1.112 +
   1.113 +lemma "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==> (f Un g)`a = f`a"
   1.114 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.115 +apply (rule apply_equality)
   1.116 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.117 +apply (rule UnI1)
   1.118 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.119 +apply (rule apply_Pair, assumption+)
   1.120 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   1.121 +apply (rule fun_disjoint_Un, assumption+)
   1.122 +done
   1.123 +
   1.124 +end