Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/ZF/ZF_examples.thy
author paulson
Tue, 19 Aug 2003 13:53:58 +0200
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
wneuper/isa