doc-src/ZF/ZF_examples.thy
author paulson
Tue Aug 19 13:53:58 2003 +0200 (2003-08-19)
changeset 14152 12f6f18e7afc
child 14159 e2eba24c8a2a
permissions -rw-r--r--
For the Isar version of the ZF logics manual
     1 header{*Examples of Reasoning in ZF Set Theory*}
     2 
     3 theory ZF_examples = Main_ZFC:
     4 
     5 subsection {* Binary Trees *}
     6 
     7 consts
     8   bt :: "i => i"
     9 
    10 datatype "bt(A)" =
    11   Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
    12 
    13 declare bt.intros [simp]
    14 
    15 text{*Induction via tactic emulation*}
    16 lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
    17   --{* @{subgoals[display,indent=0,margin=65]} *}
    18   apply (induct_tac l)
    19   --{* @{subgoals[display,indent=0,margin=65]} *}
    20   apply auto
    21   done
    22 
    23 (*
    24   apply (Inductive.case_tac l)
    25   apply (tactic {*exhaust_tac "l" 1*})
    26 *)
    27 
    28 text{*The new induction method, which I don't understand*}
    29 lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
    30   --{* @{subgoals[display,indent=0,margin=65]} *}
    31   apply (induct set: bt)
    32   --{* @{subgoals[display,indent=0,margin=65]} *}
    33   apply auto
    34   done
    35 
    36 lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
    37   -- "Proving a freeness theorem."
    38   by (blast elim!: bt.free_elims)
    39 
    40 inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
    41   -- "An elimination rule, for type-checking."
    42 
    43 text {*
    44 @{thm[display] BrE[no_vars]}
    45 \rulename{BrE}
    46 *};
    47 
    48 subsection{*Powerset example*}
    49 
    50 lemma Pow_mono: "A<=B  ==>  Pow(A) <= Pow(B)"
    51   --{* @{subgoals[display,indent=0,margin=65]} *}
    52 apply (rule subsetI)
    53   --{* @{subgoals[display,indent=0,margin=65]} *}
    54 apply (rule PowI)
    55   --{* @{subgoals[display,indent=0,margin=65]} *}
    56 apply (drule PowD)
    57   --{* @{subgoals[display,indent=0,margin=65]} *}
    58 apply (erule subset_trans, assumption)
    59 done
    60 
    61 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    62   --{* @{subgoals[display,indent=0,margin=65]} *}
    63 apply (rule equalityI)
    64   --{* @{subgoals[display,indent=0,margin=65]} *}
    65 apply (rule Int_greatest)
    66   --{* @{subgoals[display,indent=0,margin=65]} *}
    67 apply (rule Int_lower1 [THEN Pow_mono])
    68   --{* @{subgoals[display,indent=0,margin=65]} *}
    69 apply (rule Int_lower2 [THEN Pow_mono])
    70   --{* @{subgoals[display,indent=0,margin=65]} *}
    71 apply (rule subsetI)
    72   --{* @{subgoals[display,indent=0,margin=65]} *}
    73 apply (erule IntE)
    74   --{* @{subgoals[display,indent=0,margin=65]} *}
    75 apply (rule PowI)
    76   --{* @{subgoals[display,indent=0,margin=65]} *}
    77 apply (drule PowD)+
    78   --{* @{subgoals[display,indent=0,margin=65]} *}
    79 apply (rule Int_greatest, assumption+)
    80 done
    81 
    82 text{*Trying again from the beginning in order to use @{text blast}*}
    83 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    84 by blast
    85 
    86 
    87 lemma "C<=D ==> Union(C) <= Union(D)"
    88   --{* @{subgoals[display,indent=0,margin=65]} *}
    89 apply (rule subsetI)
    90   --{* @{subgoals[display,indent=0,margin=65]} *}
    91 apply (erule UnionE)
    92   --{* @{subgoals[display,indent=0,margin=65]} *}
    93 apply (rule UnionI)
    94 apply (erule subsetD, assumption, assumption)
    95   --{* @{subgoals[display,indent=0,margin=65]} *}
    96 done
    97 
    98 text{*Trying again from the beginning in order to prove from the definitions*}
    99 
   100 lemma "C<=D ==> Union(C) <= Union(D)"
   101   --{* @{subgoals[display,indent=0,margin=65]} *}
   102 apply (rule Union_least)
   103   --{* @{subgoals[display,indent=0,margin=65]} *}
   104 apply (rule Union_upper)
   105   --{* @{subgoals[display,indent=0,margin=65]} *}
   106 apply (erule subsetD, assumption)
   107 done
   108 
   109 
   110 lemma "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==> (f Un g)`a = f`a"
   111   --{* @{subgoals[display,indent=0,margin=65]} *}
   112 apply (rule apply_equality)
   113   --{* @{subgoals[display,indent=0,margin=65]} *}
   114 apply (rule UnI1)
   115   --{* @{subgoals[display,indent=0,margin=65]} *}
   116 apply (rule apply_Pair, assumption+)
   117   --{* @{subgoals[display,indent=0,margin=65]} *}
   118 apply (rule fun_disjoint_Un, assumption+)
   119 done
   120 
   121 end