src/Doc/Logics_ZF/ZF_examples.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (23 months ago) changeset 66816 212a3334e7da parent 65449 c82e63b11b8b child 67406 23307fd33906 permissions -rw-r--r--
more fundamental definition of div and mod on int
```     1 section{*Examples of Reasoning in ZF Set Theory*}
```
```     2
```
```     3 theory ZF_examples imports 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 definition n_nodes_tail :: "i => i" where
```
```    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 [elim_format]
```
```    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
```