1.1 --- a/doc-src/ZF/Makefile Wed Aug 20 13:05:22 2003 +0200
1.2 +++ b/doc-src/ZF/Makefile Wed Aug 20 13:34:17 2003 +0200
1.3 @@ -12,7 +12,7 @@
1.4 include ../Makefile.in
1.5
1.6 NAME = logics-ZF
1.7 -FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex \
1.8 +FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty\
1.9 ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
1.10
1.11 dvi: $(NAME).dvi
2.1 --- a/doc-src/ZF/ZF_examples.thy Wed Aug 20 13:05:22 2003 +0200
2.2 +++ b/doc-src/ZF/ZF_examples.thy Wed Aug 20 13:34:17 2003 +0200
2.3 @@ -33,28 +33,93 @@
2.4 apply auto
2.5 done
2.6
2.7 -lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
2.8 +lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
2.9 -- "Proving a freeness theorem."
2.10 by (blast elim!: bt.free_elims)
2.11
2.12 -inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
2.13 +inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)"
2.14 -- "An elimination rule, for type-checking."
2.15
2.16 text {*
2.17 -@{thm[display] BrE[no_vars]}
2.18 -\rulename{BrE}
2.19 +@{thm[display] Br_in_bt[no_vars]}
2.20 *};
2.21
2.22 +subsection{*Primitive recursion*}
2.23 +
2.24 +consts n_nodes :: "i => i"
2.25 +primrec
2.26 + "n_nodes(Lf) = 0"
2.27 + "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
2.28 +
2.29 +lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
2.30 + by (induct_tac t, auto)
2.31 +
2.32 +consts n_nodes_aux :: "i => i"
2.33 +primrec
2.34 + "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
2.35 + "n_nodes_aux(Br(a,l,r)) =
2.36 + (\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
2.37 +
2.38 +lemma n_nodes_aux_eq [rule_format]:
2.39 + "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
2.40 + by (induct_tac t, simp_all)
2.41 +
2.42 +constdefs n_nodes_tail :: "i => i"
2.43 + "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
2.44 +
2.45 +lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
2.46 + by (simp add: n_nodes_tail_def n_nodes_aux_eq)
2.47 +
2.48 +
2.49 +subsection {*Inductive definitions*}
2.50 +
2.51 +consts Fin :: "i=>i"
2.52 +inductive
2.53 + domains "Fin(A)" \<subseteq> "Pow(A)"
2.54 + intros
2.55 + emptyI: "0 \<in> Fin(A)"
2.56 + consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
2.57 + type_intros empty_subsetI cons_subsetI PowI
2.58 + type_elims PowD [THEN revcut_rl]
2.59 +
2.60 +
2.61 +consts acc :: "i => i"
2.62 +inductive
2.63 + domains "acc(r)" \<subseteq> "field(r)"
2.64 + intros
2.65 + vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
2.66 + monos Pow_mono
2.67 +
2.68 +
2.69 +consts
2.70 + llist :: "i=>i";
2.71 +
2.72 +codatatype
2.73 + "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
2.74 +
2.75 +
2.76 +(*Coinductive definition of equality*)
2.77 +consts
2.78 + lleq :: "i=>i"
2.79 +
2.80 +(*Previously used <*> in the domain and variant pairs as elements. But
2.81 + standard pairs work just as well. To use variant pairs, must change prefix
2.82 + a q/Q to the Sigma, Pair and converse rules.*)
2.83 +coinductive
2.84 + domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
2.85 + intros
2.86 + LNil: "<LNil, LNil> \<in> lleq(A)"
2.87 + LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |]
2.88 + ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
2.89 + type_intros llist.intros
2.90 +
2.91 +
2.92 subsection{*Powerset example*}
2.93
2.94 -lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
2.95 - --{* @{subgoals[display,indent=0,margin=65]} *}
2.96 +lemma Pow_mono: "A\<subseteq>B ==> Pow(A) \<subseteq> Pow(B)"
2.97 apply (rule subsetI)
2.98 - --{* @{subgoals[display,indent=0,margin=65]} *}
2.99 apply (rule PowI)
2.100 - --{* @{subgoals[display,indent=0,margin=65]} *}
2.101 apply (drule PowD)
2.102 - --{* @{subgoals[display,indent=0,margin=65]} *}
2.103 apply (erule subset_trans, assumption)
2.104 done
2.105
2.106 @@ -76,7 +141,9 @@
2.107 --{* @{subgoals[display,indent=0,margin=65]} *}
2.108 apply (drule PowD)+
2.109 --{* @{subgoals[display,indent=0,margin=65]} *}
2.110 -apply (rule Int_greatest, assumption+)
2.111 +apply (rule Int_greatest)
2.112 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.113 +apply (assumption+)
2.114 done
2.115
2.116 text{*Trying again from the beginning in order to use @{text blast}*}
2.117 @@ -84,20 +151,24 @@
2.118 by blast
2.119
2.120
2.121 -lemma "C<=D ==> Union(C) <= Union(D)"
2.122 +lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
2.123 --{* @{subgoals[display,indent=0,margin=65]} *}
2.124 apply (rule subsetI)
2.125 --{* @{subgoals[display,indent=0,margin=65]} *}
2.126 apply (erule UnionE)
2.127 --{* @{subgoals[display,indent=0,margin=65]} *}
2.128 apply (rule UnionI)
2.129 -apply (erule subsetD, assumption, assumption)
2.130 --{* @{subgoals[display,indent=0,margin=65]} *}
2.131 +apply (erule subsetD)
2.132 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.133 +apply assumption
2.134 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.135 +apply assumption
2.136 done
2.137
2.138 -text{*Trying again from the beginning in order to prove from the definitions*}
2.139 +text{*A more abstract version of the same proof*}
2.140
2.141 -lemma "C<=D ==> Union(C) <= Union(D)"
2.142 +lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
2.143 --{* @{subgoals[display,indent=0,margin=65]} *}
2.144 apply (rule Union_least)
2.145 --{* @{subgoals[display,indent=0,margin=65]} *}
2.146 @@ -107,15 +178,25 @@
2.147 done
2.148
2.149
2.150 -lemma "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> (f Un g)`a = f`a"
2.151 +lemma "[| a \<in> A; f \<in> A->B; g \<in> C->D; A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
2.152 --{* @{subgoals[display,indent=0,margin=65]} *}
2.153 apply (rule apply_equality)
2.154 --{* @{subgoals[display,indent=0,margin=65]} *}
2.155 apply (rule UnI1)
2.156 --{* @{subgoals[display,indent=0,margin=65]} *}
2.157 -apply (rule apply_Pair, assumption+)
2.158 +apply (rule apply_Pair)
2.159 --{* @{subgoals[display,indent=0,margin=65]} *}
2.160 -apply (rule fun_disjoint_Un, assumption+)
2.161 +apply assumption
2.162 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.163 +apply assumption
2.164 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.165 +apply (rule fun_disjoint_Un)
2.166 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.167 +apply assumption
2.168 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.169 +apply assumption
2.170 + --{* @{subgoals[display,indent=0,margin=65]} *}
2.171 +apply assumption
2.172 done
2.173
2.174 end