1.1 --- a/doc-src/ZF/ZF_examples.thy Wed Aug 20 13:05:22 2003 +0200
1.2 +++ b/doc-src/ZF/ZF_examples.thy Wed Aug 20 13:34:17 2003 +0200
1.3 @@ -33,28 +33,93 @@
1.4 apply auto
1.5 done
1.6
1.7 -lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
1.8 +lemma Br_iff: "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'"
1.9 -- "Proving a freeness theorem."
1.10 by (blast elim!: bt.free_elims)
1.11
1.12 -inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
1.13 +inductive_cases Br_in_bt: "Br(a,l,r) \<in> bt(A)"
1.14 -- "An elimination rule, for type-checking."
1.15
1.16 text {*
1.17 -@{thm[display] BrE[no_vars]}
1.18 -\rulename{BrE}
1.19 +@{thm[display] Br_in_bt[no_vars]}
1.20 *};
1.21
1.22 +subsection{*Primitive recursion*}
1.23 +
1.24 +consts n_nodes :: "i => i"
1.25 +primrec
1.26 + "n_nodes(Lf) = 0"
1.27 + "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
1.28 +
1.29 +lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
1.30 + by (induct_tac t, auto)
1.31 +
1.32 +consts n_nodes_aux :: "i => i"
1.33 +primrec
1.34 + "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
1.35 + "n_nodes_aux(Br(a,l,r)) =
1.36 + (\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
1.37 +
1.38 +lemma n_nodes_aux_eq [rule_format]:
1.39 + "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
1.40 + by (induct_tac t, simp_all)
1.41 +
1.42 +constdefs n_nodes_tail :: "i => i"
1.43 + "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
1.44 +
1.45 +lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
1.46 + by (simp add: n_nodes_tail_def n_nodes_aux_eq)
1.47 +
1.48 +
1.49 +subsection {*Inductive definitions*}
1.50 +
1.51 +consts Fin :: "i=>i"
1.52 +inductive
1.53 + domains "Fin(A)" \<subseteq> "Pow(A)"
1.54 + intros
1.55 + emptyI: "0 \<in> Fin(A)"
1.56 + consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
1.57 + type_intros empty_subsetI cons_subsetI PowI
1.58 + type_elims PowD [THEN revcut_rl]
1.59 +
1.60 +
1.61 +consts acc :: "i => i"
1.62 +inductive
1.63 + domains "acc(r)" \<subseteq> "field(r)"
1.64 + intros
1.65 + vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
1.66 + monos Pow_mono
1.67 +
1.68 +
1.69 +consts
1.70 + llist :: "i=>i";
1.71 +
1.72 +codatatype
1.73 + "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
1.74 +
1.75 +
1.76 +(*Coinductive definition of equality*)
1.77 +consts
1.78 + lleq :: "i=>i"
1.79 +
1.80 +(*Previously used <*> in the domain and variant pairs as elements. But
1.81 + standard pairs work just as well. To use variant pairs, must change prefix
1.82 + a q/Q to the Sigma, Pair and converse rules.*)
1.83 +coinductive
1.84 + domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
1.85 + intros
1.86 + LNil: "<LNil, LNil> \<in> lleq(A)"
1.87 + LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |]
1.88 + ==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)"
1.89 + type_intros llist.intros
1.90 +
1.91 +
1.92 subsection{*Powerset example*}
1.93
1.94 -lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
1.95 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.96 +lemma Pow_mono: "A\<subseteq>B ==> Pow(A) \<subseteq> Pow(B)"
1.97 apply (rule subsetI)
1.98 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.99 apply (rule PowI)
1.100 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.101 apply (drule PowD)
1.102 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.103 apply (erule subset_trans, assumption)
1.104 done
1.105
1.106 @@ -76,7 +141,9 @@
1.107 --{* @{subgoals[display,indent=0,margin=65]} *}
1.108 apply (drule PowD)+
1.109 --{* @{subgoals[display,indent=0,margin=65]} *}
1.110 -apply (rule Int_greatest, assumption+)
1.111 +apply (rule Int_greatest)
1.112 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.113 +apply (assumption+)
1.114 done
1.115
1.116 text{*Trying again from the beginning in order to use @{text blast}*}
1.117 @@ -84,20 +151,24 @@
1.118 by blast
1.119
1.120
1.121 -lemma "C<=D ==> Union(C) <= Union(D)"
1.122 +lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
1.123 --{* @{subgoals[display,indent=0,margin=65]} *}
1.124 apply (rule subsetI)
1.125 --{* @{subgoals[display,indent=0,margin=65]} *}
1.126 apply (erule UnionE)
1.127 --{* @{subgoals[display,indent=0,margin=65]} *}
1.128 apply (rule UnionI)
1.129 -apply (erule subsetD, assumption, assumption)
1.130 --{* @{subgoals[display,indent=0,margin=65]} *}
1.131 +apply (erule subsetD)
1.132 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.133 +apply assumption
1.134 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.135 +apply assumption
1.136 done
1.137
1.138 -text{*Trying again from the beginning in order to prove from the definitions*}
1.139 +text{*A more abstract version of the same proof*}
1.140
1.141 -lemma "C<=D ==> Union(C) <= Union(D)"
1.142 +lemma "C\<subseteq>D ==> Union(C) \<subseteq> Union(D)"
1.143 --{* @{subgoals[display,indent=0,margin=65]} *}
1.144 apply (rule Union_least)
1.145 --{* @{subgoals[display,indent=0,margin=65]} *}
1.146 @@ -107,15 +178,25 @@
1.147 done
1.148
1.149
1.150 -lemma "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> (f Un g)`a = f`a"
1.151 +lemma "[| a \<in> A; f \<in> A->B; g \<in> C->D; A \<inter> C = 0 |] ==> (f \<union> g)`a = f`a"
1.152 --{* @{subgoals[display,indent=0,margin=65]} *}
1.153 apply (rule apply_equality)
1.154 --{* @{subgoals[display,indent=0,margin=65]} *}
1.155 apply (rule UnI1)
1.156 --{* @{subgoals[display,indent=0,margin=65]} *}
1.157 -apply (rule apply_Pair, assumption+)
1.158 +apply (rule apply_Pair)
1.159 --{* @{subgoals[display,indent=0,margin=65]} *}
1.160 -apply (rule fun_disjoint_Un, assumption+)
1.161 +apply assumption
1.162 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.163 +apply assumption
1.164 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.165 +apply (rule fun_disjoint_Un)
1.166 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.167 +apply assumption
1.168 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.169 +apply assumption
1.170 + --{* @{subgoals[display,indent=0,margin=65]} *}
1.171 +apply assumption
1.172 done
1.173
1.174 end