doc-src/ZF/ZF_examples.thy
author haftmann
Tue Oct 10 13:59:12 2006 +0200 (2006-10-10)
changeset 20950 981fa0ce23ed
parent 16417 9bc16273c2d4
child 35416 d8d7d1b785af
permissions -rw-r--r--
added IsarAdvanced material
     1 header{*Examples of Reasoning in ZF Set Theory*}
     2 
     3 theory ZF_examples imports Main_ZFC begin
     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 Br_in_bt: "Br(a,l,r) \<in> bt(A)"
    41   -- "An elimination rule, for type-checking."
    42 
    43 text {*
    44 @{thm[display] Br_in_bt[no_vars]}
    45 *};
    46 
    47 subsection{*Primitive recursion*}
    48 
    49 consts  n_nodes :: "i => i"
    50 primrec
    51   "n_nodes(Lf) = 0"
    52   "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
    53 
    54 lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
    55   by (induct_tac t, auto) 
    56 
    57 consts  n_nodes_aux :: "i => i"
    58 primrec
    59   "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
    60   "n_nodes_aux(Br(a,l,r)) = 
    61       (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"
    62 
    63 lemma n_nodes_aux_eq [rule_format]:
    64      "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
    65   by (induct_tac t, simp_all) 
    66 
    67 constdefs  n_nodes_tail :: "i => i"
    68    "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
    69 
    70 lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
    71  by (simp add: n_nodes_tail_def n_nodes_aux_eq) 
    72 
    73 
    74 subsection {*Inductive definitions*}
    75 
    76 consts  Fin       :: "i=>i"
    77 inductive
    78   domains   "Fin(A)" \<subseteq> "Pow(A)"
    79   intros
    80     emptyI:  "0 \<in> Fin(A)"
    81     consI:   "[| a \<in> A;  b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
    82   type_intros  empty_subsetI cons_subsetI PowI
    83   type_elims   PowD [THEN revcut_rl]
    84 
    85 
    86 consts  acc :: "i => i"
    87 inductive
    88   domains "acc(r)" \<subseteq> "field(r)"
    89   intros
    90     vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
    91   monos      Pow_mono
    92 
    93 
    94 consts
    95   llist  :: "i=>i";
    96 
    97 codatatype
    98   "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
    99 
   100 
   101 (*Coinductive definition of equality*)
   102 consts
   103   lleq :: "i=>i"
   104 
   105 (*Previously used <*> in the domain and variant pairs as elements.  But
   106   standard pairs work just as well.  To use variant pairs, must change prefix
   107   a q/Q to the Sigma, Pair and converse rules.*)
   108 coinductive
   109   domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
   110   intros
   111     LNil:  "<LNil, LNil> \<in> lleq(A)"
   112     LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] 
   113             ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
   114   type_intros  llist.intros
   115 
   116 
   117 subsection{*Powerset example*}
   118 
   119 lemma Pow_mono: "A\<subseteq>B  ==>  Pow(A) \<subseteq> Pow(B)"
   120 apply (rule subsetI)
   121 apply (rule PowI)
   122 apply (drule PowD)
   123 apply (erule subset_trans, assumption)
   124 done
   125 
   126 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
   127   --{* @{subgoals[display,indent=0,margin=65]} *}
   128 apply (rule equalityI)
   129   --{* @{subgoals[display,indent=0,margin=65]} *}
   130 apply (rule Int_greatest)
   131   --{* @{subgoals[display,indent=0,margin=65]} *}
   132 apply (rule Int_lower1 [THEN Pow_mono])
   133   --{* @{subgoals[display,indent=0,margin=65]} *}
   134 apply (rule Int_lower2 [THEN Pow_mono])
   135   --{* @{subgoals[display,indent=0,margin=65]} *}
   136 apply (rule subsetI)
   137   --{* @{subgoals[display,indent=0,margin=65]} *}
   138 apply (erule IntE)
   139   --{* @{subgoals[display,indent=0,margin=65]} *}
   140 apply (rule PowI)
   141   --{* @{subgoals[display,indent=0,margin=65]} *}
   142 apply (drule PowD)+
   143   --{* @{subgoals[display,indent=0,margin=65]} *}
   144 apply (rule Int_greatest)
   145   --{* @{subgoals[display,indent=0,margin=65]} *}
   146 apply (assumption+)
   147 done
   148 
   149 text{*Trying again from the beginning in order to use @{text blast}*}
   150 lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
   151 by blast
   152 
   153 
   154 lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
   155   --{* @{subgoals[display,indent=0,margin=65]} *}
   156 apply (rule subsetI)
   157   --{* @{subgoals[display,indent=0,margin=65]} *}
   158 apply (erule UnionE)
   159   --{* @{subgoals[display,indent=0,margin=65]} *}
   160 apply (rule UnionI)
   161   --{* @{subgoals[display,indent=0,margin=65]} *}
   162 apply (erule subsetD)
   163   --{* @{subgoals[display,indent=0,margin=65]} *}
   164 apply assumption 
   165   --{* @{subgoals[display,indent=0,margin=65]} *}
   166 apply assumption 
   167 done
   168 
   169 text{*A more abstract version of the same proof*}
   170 
   171 lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
   172   --{* @{subgoals[display,indent=0,margin=65]} *}
   173 apply (rule Union_least)
   174   --{* @{subgoals[display,indent=0,margin=65]} *}
   175 apply (rule Union_upper)
   176   --{* @{subgoals[display,indent=0,margin=65]} *}
   177 apply (erule subsetD, assumption)
   178 done
   179 
   180 
   181 lemma "[| a \<in> A;  f \<in> A->B;  g \<in> C->D;  A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
   182   --{* @{subgoals[display,indent=0,margin=65]} *}
   183 apply (rule apply_equality)
   184   --{* @{subgoals[display,indent=0,margin=65]} *}
   185 apply (rule UnI1)
   186   --{* @{subgoals[display,indent=0,margin=65]} *}
   187 apply (rule apply_Pair)
   188   --{* @{subgoals[display,indent=0,margin=65]} *}
   189 apply assumption 
   190   --{* @{subgoals[display,indent=0,margin=65]} *}
   191 apply assumption 
   192   --{* @{subgoals[display,indent=0,margin=65]} *}
   193 apply (rule fun_disjoint_Un)
   194   --{* @{subgoals[display,indent=0,margin=65]} *}
   195 apply assumption 
   196   --{* @{subgoals[display,indent=0,margin=65]} *}
   197 apply assumption 
   198   --{* @{subgoals[display,indent=0,margin=65]} *}
   199 apply assumption 
   200 done
   201 
   202 end