1.1 --- a/src/ZF/Coind/BCR.thy Fri Dec 28 10:10:55 2001 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,5 +0,0 @@
1.4 -(* Title: ZF/Coind/BCR.thy
1.5 - ID: $Id$
1.6 - Author: Jacob Frost, Cambridge University Computer Laboratory
1.7 - Copyright 1995 University of Cambridge
1.8 -*)
2.1 --- a/src/ZF/IMP/Com.ML Fri Dec 28 10:10:55 2001 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,47 +0,0 @@
2.4 -(* Title: ZF/IMP/Com.ML
2.5 - ID: $Id$
2.6 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
2.7 - Copyright 1994 TUM
2.8 -*)
2.9 -
2.10 -val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
2.11 - evalb.dom_subset RS subsetD,
2.12 - evalc.dom_subset RS subsetD];
2.13 -
2.14 -(********** type_intrs for evala **********)
2.15 -
2.16 -val evala_type_intrs =
2.17 - map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
2.18 - ["!!a.<a,sigma> -a-> n ==> a \\<in> aexp",
2.19 - "!!a.<a,sigma> -a-> n ==> sigma \\<in> loc->nat",
2.20 - "!!a.<a,sigma> -a-> n ==> n \\<in> nat"];
2.21 -
2.22 -
2.23 -(********** type_intrs for evalb **********)
2.24 -
2.25 -val evalb_type_intrs =
2.26 - map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
2.27 - ["!!b.<b,sigma> -b-> w ==> b \\<in> bexp",
2.28 - "!!b.<b,sigma> -b-> w ==> sigma \\<in> loc->nat",
2.29 - "!!b.<b,sigma> -b-> w ==> w \\<in> bool"];
2.30 -
2.31 -
2.32 -(********** type_intrs for evalb **********)
2.33 -
2.34 -val evalc_type_intrs =
2.35 - map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
2.36 - ["!!c.<c,sigma> -c-> sigma' ==> c \\<in> com",
2.37 - "!!c.<c,sigma> -c-> sigma' ==> sigma \\<in> loc->nat",
2.38 - "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
2.39 -
2.40 -
2.41 -val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs;
2.42 -
2.43 -
2.44 -val aexp_elim_cases =
2.45 - [
2.46 - evala.mk_cases "<N(n),sigma> -a-> i",
2.47 - evala.mk_cases "<X(x),sigma> -a-> i",
2.48 - evala.mk_cases "<Op1(f,e),sigma> -a-> i",
2.49 - evala.mk_cases "<Op2(f,a1,a2),sigma> -a-> i"
2.50 - ];
3.1 --- a/src/ZF/IMP/Com.thy Fri Dec 28 10:10:55 2001 +0100
3.2 +++ b/src/ZF/IMP/Com.thy Fri Dec 28 10:11:14 2001 +0100
3.3 @@ -8,34 +8,33 @@
3.4 And their Operational semantics
3.5 *)
3.6
3.7 -Com = Main +
3.8 +theory Com = Main:
3.9
3.10 (** Arithmetic expressions **)
3.11 consts loc :: i
3.12 aexp :: i
3.13
3.14 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
3.15 - "aexp" = N ("n \\<in> nat")
3.16 - | X ("x \\<in> loc")
3.17 - | Op1 ("f \\<in> nat -> nat", "a \\<in> aexp")
3.18 - | Op2 ("f \\<in> (nat*nat) -> nat", "a0 \\<in> aexp", "a1 \\<in> aexp")
3.19 + "aexp" = N ("n \<in> nat")
3.20 + | X ("x \<in> loc")
3.21 + | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
3.22 + | Op2 ("f \<in> (nat*nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
3.23
3.24
3.25 (** Evaluation of arithmetic expressions **)
3.26 -consts evala :: i
3.27 - "-a->" :: [i,i] => o (infixl 50)
3.28 +consts evala :: "i"
3.29 + "-a->" :: "[i,i] => o" (infixl 50)
3.30 translations
3.31 - "p -a-> n" == "<p,n> \\<in> evala"
3.32 + "p -a-> n" == "<p,n> \<in> evala"
3.33 inductive
3.34 domains "evala" <= "(aexp * (loc -> nat)) * nat"
3.35 - intrs
3.36 - N "[| n \\<in> nat; sigma \\<in> loc->nat |] ==> <N(n),sigma> -a-> n"
3.37 - X "[| x \\<in> loc; sigma \\<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
3.38 - Op1 "[| <e,sigma> -a-> n; f \\<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
3.39 - Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \\<in> (nat*nat) -> nat |]
3.40 - ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
3.41 -
3.42 - type_intrs "aexp.intrs@[apply_funtype]"
3.43 + intros
3.44 + N: "[| n \<in> nat; sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n"
3.45 + X: "[| x \<in> loc; sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
3.46 + Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
3.47 + Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat*nat) -> nat |]
3.48 + ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
3.49 + type_intros aexp.intros apply_funtype
3.50
3.51
3.52 (** Boolean expressions **)
3.53 @@ -44,35 +43,34 @@
3.54 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
3.55 "bexp" = true
3.56 | false
3.57 - | ROp ("f \\<in> (nat*nat)->bool", "a0 \\<in> aexp", "a1 \\<in> aexp")
3.58 - | noti ("b \\<in> bexp")
3.59 - | andi ("b0 \\<in> bexp", "b1 \\<in> bexp") (infixl 60)
3.60 - | ori ("b0 \\<in> bexp", "b1 \\<in> bexp") (infixl 60)
3.61 + | ROp ("f \<in> (nat*nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
3.62 + | noti ("b \<in> bexp")
3.63 + | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
3.64 + | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
3.65
3.66
3.67 (** Evaluation of boolean expressions **)
3.68 -consts evalb :: i
3.69 - "-b->" :: [i,i] => o (infixl 50)
3.70 +consts evalb :: "i"
3.71 + "-b->" :: "[i,i] => o" (infixl 50)
3.72
3.73 translations
3.74 - "p -b-> b" == "<p,b> \\<in> evalb"
3.75 + "p -b-> b" == "<p,b> \<in> evalb"
3.76
3.77 inductive
3.78 domains "evalb" <= "(bexp * (loc -> nat)) * bool"
3.79 - intrs (*avoid clash with ML constructors true, false*)
3.80 - tru "[| sigma \\<in> loc -> nat |] ==> <true,sigma> -b-> 1"
3.81 - fls "[| sigma \\<in> loc -> nat |] ==> <false,sigma> -b-> 0"
3.82 - ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \\<in> (nat*nat)->bool |]
3.83 + intros (*avoid clash with ML constructors true, false*)
3.84 + tru: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
3.85 + fls: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
3.86 + ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |]
3.87 ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
3.88 - noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
3.89 - andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
3.90 + noti: "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
3.91 + andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
3.92 ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
3.93 - ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
3.94 + ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
3.95 ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
3.96 -
3.97 - type_intrs "bexp.intrs @
3.98 - [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
3.99 - type_elims "[make_elim(evala.dom_subset RS subsetD)]"
3.100 + type_intros bexp.intros
3.101 + apply_funtype and_type or_type bool_1I bool_0I not_type
3.102 + type_elims evala.dom_subset [THEN subsetD, elim_format]
3.103
3.104
3.105 (** Commands **)
3.106 @@ -80,50 +78,83 @@
3.107
3.108 datatype
3.109 "com" = skip
3.110 - | asgt ("x \\<in> loc", "a \\<in> aexp") (infixl 60)
3.111 - | semic ("c0 \\<in> com", "c1 \\<in> com") ("_; _" [60, 60] 10)
3.112 - | while ("b \\<in> bexp", "c \\<in> com") ("while _ do _" 60)
3.113 - | ifc ("b \\<in> bexp", "c0 \\<in> com", "c1 \\<in> com") ("ifc _ then _ else _" 60)
3.114 + | asgt ("x \<in> loc", "a \<in> aexp") (infixl 60)
3.115 + | semic("c0 \<in> com", "c1 \<in> com") ("_; _" [60, 60] 10)
3.116 + | while("b \<in> bexp", "c \<in> com") ("while _ do _" 60)
3.117 + | ifc ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("ifc _ then _ else _" 60)
3.118
3.119 (*Constructor ";" has low precedence to avoid syntactic ambiguities
3.120 - with [| m \\<in> nat; x \\<in> loc; ... |] ==> ... It usually will need parentheses.*)
3.121 + with [| m \<in> nat; x \<in> loc; ... |] ==> ... It usually will need parentheses.*)
3.122
3.123 (** Execution of commands **)
3.124 -consts evalc :: i
3.125 - "-c->" :: [i,i] => o (infixl 50)
3.126 +consts evalc :: "i"
3.127 + "-c->" :: "[i,i] => o" (infixl 50)
3.128
3.129 translations
3.130 - "p -c-> s" == "<p,s> \\<in> evalc"
3.131 -
3.132 + "p -c-> s" == "<p,s> \<in> evalc"
3.133
3.134 inductive
3.135 domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
3.136 - intrs
3.137 - skip "[| sigma \\<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
3.138 + intros
3.139 + skip: "[| sigma \<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
3.140
3.141 - assign "[| m \\<in> nat; x \\<in> loc; <a,sigma> -a-> m |] ==>
3.142 - <x asgt a,sigma> -c-> sigma(x:=m)"
3.143 + assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |]
3.144 + ==> <x asgt a,sigma> -c-> sigma(x:=m)"
3.145
3.146 - semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==>
3.147 - <c0 ; c1, sigma> -c-> sigma1"
3.148 + semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |]
3.149 + ==> <c0 ; c1, sigma> -c-> sigma1"
3.150
3.151 - ifc1 "[| b \\<in> bexp; c1 \\<in> com; sigma \\<in> loc->nat;
3.152 - <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
3.153 - <ifc b then c0 else c1, sigma> -c-> sigma1"
3.154 + ifc1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;
3.155 + <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
3.156 + ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
3.157
3.158 - ifc0 "[| b \\<in> bexp; c0 \\<in> com; sigma \\<in> loc->nat;
3.159 - <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
3.160 - <ifc b then c0 else c1, sigma> -c-> sigma1"
3.161 + ifc0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;
3.162 + <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
3.163 + ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
3.164
3.165 - while0 "[| c \\<in> com; <b, sigma> -b-> 0 |] ==>
3.166 - <while b do c,sigma> -c-> sigma "
3.167 + while0: "[| c \<in> com; <b, sigma> -b-> 0 |]
3.168 + ==> <while b do c,sigma> -c-> sigma"
3.169
3.170 - while1 "[| c \\<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
3.171 - <while b do c, sigma2> -c-> sigma1 |] ==>
3.172 - <while b do c, sigma> -c-> sigma1 "
3.173 + while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
3.174 + <while b do c, sigma2> -c-> sigma1 |]
3.175 + ==> <while b do c, sigma> -c-> sigma1"
3.176
3.177 - type_intrs "com.intrs @ [update_type]"
3.178 - type_elims "[make_elim(evala.dom_subset RS subsetD),
3.179 - make_elim(evalb.dom_subset RS subsetD) ]"
3.180 + type_intros com.intros update_type
3.181 + type_elims evala.dom_subset [THEN subsetD, elim_format]
3.182 + evalb.dom_subset [THEN subsetD, elim_format]
3.183 +
3.184 +
3.185 +(*** type_intros for evala ***)
3.186 +
3.187 +lemmas evala_1 [simp] =
3.188 + evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
3.189 +lemmas evala_2 [simp] =
3.190 + evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
3.191 +lemmas evala_3 [simp] =
3.192 + evala.dom_subset [THEN subsetD, THEN SigmaD2]
3.193 +
3.194 +
3.195 +(*** type_intros for evalb ***)
3.196 +
3.197 +lemmas evalb_1 [simp] =
3.198 + evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
3.199 +lemmas evalb_2 [simp] =
3.200 + evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
3.201 +lemmas evalb_3 [simp] =
3.202 + evalb.dom_subset [THEN subsetD, THEN SigmaD2]
3.203 +
3.204 +(*** type_intros for evalc ***)
3.205 +
3.206 +lemmas evalc_1 [simp] =
3.207 + evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
3.208 +lemmas evalc_2 [simp] =
3.209 + evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
3.210 +lemmas evalc_3 [simp] =
3.211 + evalc.dom_subset [THEN subsetD, THEN SigmaD2]
3.212 +
3.213 +inductive_cases evala_N_E [elim!]: "<N(n),sigma> -a-> i"
3.214 +inductive_cases evala_X_E [elim!]: "<X(x),sigma> -a-> i"
3.215 +inductive_cases evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
3.216 +inductive_cases evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i"
3.217
3.218 end
4.1 --- a/src/ZF/IMP/Denotation.ML Fri Dec 28 10:10:55 2001 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,58 +0,0 @@
4.4 -(* Title: ZF/IMP/Denotation.ML
4.5 - ID: $Id$
4.6 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
4.7 - Copyright 1994 TUM
4.8 -*)
4.9 -
4.10 -(** Rewrite Rules for A,B,C **)
4.11 -Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
4.12 -Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def];
4.13 -Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def];
4.14 -
4.15 -(** Type_intr for A **)
4.16 -
4.17 -Goal "[|a \\<in> aexp; sigma \\<in> loc->nat|] ==> A(a,sigma):nat";
4.18 -by (etac aexp.induct 1);
4.19 -by (ALLGOALS Asm_simp_tac);
4.20 -by (ALLGOALS (fast_tac (claset() addSIs [apply_type])));
4.21 -qed "A_type";
4.22 -
4.23 -(** Type_intr for B **)
4.24 -
4.25 -Goal "[|b \\<in> bexp; sigma \\<in> loc->nat|] ==> B(b,sigma):bool";
4.26 -by (etac bexp.induct 1);
4.27 -by (ALLGOALS Asm_simp_tac);
4.28 -by (ALLGOALS (fast_tac (claset() addSIs [apply_type,A_type]@bool_typechecks)));
4.29 -qed "B_type";
4.30 -
4.31 -(** C_subset **)
4.32 -
4.33 -Goal "c \\<in> com ==> C(c) \\<subseteq> (loc->nat)*(loc->nat)";
4.34 -by (etac com.induct 1);
4.35 -by (ALLGOALS Asm_simp_tac);
4.36 -by (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])));
4.37 -qed "C_subset";
4.38 -
4.39 -(** Type_elims for C **)
4.40 -
4.41 -Goal "[| <x,y>:C(c); c \\<in> com |] ==> x \\<in> loc->nat & y \\<in> loc->nat";
4.42 -by (blast_tac (claset() addDs [C_subset RS subsetD]) 1);
4.43 -qed "C_type_D";
4.44 -
4.45 -Goal "[| x \\<in> C(c); c \\<in> com |] ==> fst(x):loc->nat";
4.46 -by (dtac (C_subset RS subsetD) 1);
4.47 -by (atac 1);
4.48 -by (etac SigmaE 1);
4.49 -by (Asm_simp_tac 1);
4.50 -qed "C_type_fst";
4.51 -
4.52 -AddDs [C_type_D, C_type_fst];
4.53 -
4.54 -(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
4.55 -
4.56 -Goalw [bnd_mono_def,Gamma_def]
4.57 - "c \\<in> com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))";
4.58 -by (Blast_tac 1);
4.59 -qed "Gamma_bnd_mono";
4.60 -
4.61 -(** End ***)
5.1 --- a/src/ZF/IMP/Denotation.thy Fri Dec 28 10:10:55 2001 +0100
5.2 +++ b/src/ZF/IMP/Denotation.thy Fri Dec 28 10:11:14 2001 +0100
5.3 @@ -6,41 +6,82 @@
5.4 Denotational semantics of expressions & commands
5.5 *)
5.6
5.7 -Denotation = Com +
5.8 +theory Denotation = Com:
5.9 +
5.10
5.11 consts
5.12 - A :: i => i => i
5.13 - B :: i => i => i
5.14 - C :: i => i
5.15 - Gamma :: [i,i,i] => i
5.16 + A :: "i => i => i"
5.17 + B :: "i => i => i"
5.18 + C :: "i => i"
5.19
5.20 -rules (*NOT definitional*)
5.21 - A_nat_def "A(N(n)) == (%sigma. n)"
5.22 - A_loc_def "A(X(x)) == (%sigma. sigma`x)"
5.23 - A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
5.24 - A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
5.25 +constdefs
5.26 + Gamma :: "[i,i,i] => i"
5.27 + "Gamma(b,cden) == (%phi.{io \<in> (phi O cden). B(b,fst(io))=1} Un
5.28 + {io \<in> id(loc->nat). B(b,fst(io))=0})"
5.29
5.30 +primrec
5.31 + "A(N(n), sigma) = n"
5.32 + "A(X(x), sigma) = sigma`x"
5.33 + "A(Op1(f,a), sigma) = f`A(a,sigma)"
5.34 + "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
5.35
5.36 - B_true_def "B(true) == (%sigma. 1)"
5.37 - B_false_def "B(false) == (%sigma. 0)"
5.38 - B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
5.39
5.40 +primrec
5.41 + "B(true, sigma) = 1"
5.42 + "B(false, sigma) = 0"
5.43 + "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
5.44 + "B(noti(b), sigma) = not(B(b,sigma))"
5.45 + "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
5.46 + "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
5.47
5.48 - B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
5.49 - B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
5.50 - B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
5.51
5.52 - C_skip_def "C(skip) == id(loc->nat)"
5.53 - C_assign_def "C(x asgt a) == {io:(loc->nat)*(loc->nat).
5.54 - snd(io) = fst(io)(x := A(a,fst(io)))}"
5.55 +primrec
5.56 + "C(skip) = id(loc->nat)"
5.57
5.58 - C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
5.59 - C_if_def "C(ifc b then c0 else c1) == {io \\<in> C(c0). B(b,fst(io))=1} Un
5.60 - {io \\<in> C(c1). B(b,fst(io))=0}"
5.61 + "C(x asgt a) = {io:(loc->nat)*(loc->nat).
5.62 + snd(io) = fst(io)(x := A(a,fst(io)))}"
5.63
5.64 - Gamma_def "Gamma(b,c) == (%phi.{io \\<in> (phi O C(c)). B(b,fst(io))=1} Un
5.65 - {io \\<in> id(loc->nat). B(b,fst(io))=0})"
5.66 + "C(c0 ; c1) = C(c1) O C(c0)"
5.67
5.68 - C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
5.69 + "C(ifc b then c0 else c1) = {io \<in> C(c0). B(b,fst(io))=1} Un
5.70 + {io \<in> C(c1). B(b,fst(io))=0}"
5.71 +
5.72 + "C(while b do c) = lfp((loc->nat)*(loc->nat), Gamma(b,C(c)))"
5.73 +
5.74 +
5.75 +(** Type_intr for A **)
5.76 +
5.77 +lemma A_type [TC]: "[|a \<in> aexp; sigma \<in> loc->nat|] ==> A(a,sigma) \<in> nat"
5.78 +by (erule aexp.induct, simp_all)
5.79 +
5.80 +
5.81 +(** Type_intr for B **)
5.82 +
5.83 +lemma B_type [TC]: "[|b \<in> bexp; sigma \<in> loc->nat|] ==> B(b,sigma) \<in> bool"
5.84 +by (erule bexp.induct, simp_all)
5.85 +
5.86 +(** C_subset **)
5.87 +
5.88 +lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat)*(loc->nat)"
5.89 +apply (erule com.induct)
5.90 +apply simp_all
5.91 +apply (blast dest: lfp_subset [THEN subsetD])+
5.92 +done
5.93 +
5.94 +(** Type_elims for C **)
5.95 +
5.96 +lemma C_type_D [dest]:
5.97 + "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
5.98 +by (blast dest: C_subset [THEN subsetD])
5.99 +
5.100 +lemma C_type_fst [dest]: "[| x \<in> C(c); c \<in> com |] ==> fst(x) \<in> loc->nat"
5.101 +by (auto dest!: C_subset [THEN subsetD])
5.102 +
5.103 +(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
5.104 +
5.105 +lemma Gamma_bnd_mono:
5.106 + "cden <= (loc->nat)*(loc->nat)
5.107 + ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,cden))"
5.108 +by (unfold bnd_mono_def Gamma_def, blast)
5.109
5.110 end
6.1 --- a/src/ZF/IMP/Equiv.ML Fri Dec 28 10:10:55 2001 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,98 +0,0 @@
6.4 -(* Title: ZF/IMP/Equiv.ML
6.5 - ID: $Id$
6.6 - Author: Heiko Loetzbeyer & Robert Sandner, TUM
6.7 - Copyright 1994 TUM
6.8 -*)
6.9 -
6.10 -Goal "[| a \\<in> aexp; sigma: loc -> nat |] ==> \
6.11 -\ <a,sigma> -a-> n <-> A(a,sigma) = n";
6.12 -by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
6.13 -by (etac aexp.induct 1);
6.14 -by (ALLGOALS (fast_tac (claset() addSIs evala.intrs
6.15 - addSEs aexp_elim_cases
6.16 - addss (simpset()))));
6.17 -qed "aexp_iff";
6.18 -
6.19 -
6.20 -val aexp1 = aexp_iff RS iffD1;
6.21 -val aexp2 = aexp_iff RS iffD2;
6.22 -
6.23 -
6.24 -val bexp_elim_cases =
6.25 - [
6.26 - evalb.mk_cases "<true,sigma> -b-> x",
6.27 - evalb.mk_cases "<false,sigma> -b-> x",
6.28 - evalb.mk_cases "<ROp(f,a0,a1),sigma> -b-> x",
6.29 - evalb.mk_cases "<noti(b),sigma> -b-> x",
6.30 - evalb.mk_cases "<b0 andi b1,sigma> -b-> x",
6.31 - evalb.mk_cases "<b0 ori b1,sigma> -b-> x"
6.32 - ];
6.33 -
6.34 -
6.35 -Goal "[| b \\<in> bexp; sigma: loc -> nat |] ==> \
6.36 -\ <b,sigma> -b-> w <-> B(b,sigma) = w";
6.37 -by (res_inst_tac [("x","w")] spec 1);
6.38 -by (etac bexp.induct 1);
6.39 -by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs
6.40 - addSEs bexp_elim_cases
6.41 - addss (simpset() addsimps [aexp_iff]))));
6.42 -qed "bexp_iff";
6.43 -
6.44 -val bexp1 = bexp_iff RS iffD1;
6.45 -val bexp2 = bexp_iff RS iffD2;
6.46 -
6.47 -
6.48 -Goal "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \\<in> C(c)";
6.49 -by (etac evalc.induct 1);
6.50 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
6.51 -(* skip *)
6.52 -by (Fast_tac 1);
6.53 -(* assign *)
6.54 -by (asm_full_simp_tac (simpset() addsimps
6.55 - [aexp1, update_type] @ op_type_intrs) 1);
6.56 -(* comp *)
6.57 -by (Fast_tac 1);
6.58 -(* while *)
6.59 -by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
6.60 -by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
6.61 -by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
6.62 -(* recursive case of while *)
6.63 -by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
6.64 -by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
6.65 -by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
6.66 -val com1 = result();
6.67 -
6.68 -
6.69 -AddSIs [aexp2,bexp2,B_type,A_type];
6.70 -AddIs evalc.intrs;
6.71 -
6.72 -
6.73 -Goal "c \\<in> com ==> \\<forall>x \\<in> C(c). <c,fst(x)> -c-> snd(x)";
6.74 -by (etac com.induct 1);
6.75 -(* comp *)
6.76 -by (Force_tac 3);
6.77 -(* assign *)
6.78 -by (Force_tac 2);
6.79 -(* skip *)
6.80 -by (Force_tac 1);
6.81 -(* while *)
6.82 -by Safe_tac;
6.83 -by (ALLGOALS Asm_full_simp_tac);
6.84 -by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]);
6.85 -by (rewtac Gamma_def);
6.86 -by Safe_tac;
6.87 -by (EVERY1 [dtac bspec, atac]);
6.88 -by (ALLGOALS Asm_full_simp_tac);
6.89 -(* while, if *)
6.90 -by (ALLGOALS Blast_tac);
6.91 -val com2 = result();
6.92 -
6.93 -
6.94 -(**** Proof of Equivalence ****)
6.95 -
6.96 -Goal "\\<forall>c \\<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
6.97 -by (fast_tac (claset() addIs [C_subset RS subsetD]
6.98 - addEs [com2 RS bspec]
6.99 - addDs [com1]
6.100 - addss (simpset())) 1);
6.101 -val com_equivalence = result();
7.1 --- a/src/ZF/IMP/Equiv.thy Fri Dec 28 10:10:55 2001 +0100
7.2 +++ b/src/ZF/IMP/Equiv.thy Fri Dec 28 10:11:14 2001 +0100
7.3 @@ -4,4 +4,84 @@
7.4 Copyright 1994 TUM
7.5 *)
7.6
7.7 -Equiv = Denotation + Com
7.8 +theory Equiv = Denotation + Com:
7.9 +
7.10 +lemma aexp_iff [rule_format]:
7.11 + "[| a \<in> aexp; sigma: loc -> nat |]
7.12 + ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
7.13 +apply (erule aexp.induct)
7.14 +apply (force intro!: evala.intros)+
7.15 +done
7.16 +
7.17 +declare aexp_iff [THEN iffD1, simp]
7.18 + aexp_iff [THEN iffD2, intro!]
7.19 +
7.20 +inductive_cases [elim!]: "<true,sigma> -b-> x"
7.21 +inductive_cases [elim!]: "<false,sigma> -b-> x"
7.22 +inductive_cases [elim!]: "<ROp(f,a0,a1),sigma> -b-> x"
7.23 +inductive_cases [elim!]: "<noti(b),sigma> -b-> x"
7.24 +inductive_cases [elim!]: "<b0 andi b1,sigma> -b-> x"
7.25 +inductive_cases [elim!]: "<b0 ori b1,sigma> -b-> x"
7.26 +
7.27 +
7.28 +lemma bexp_iff [rule_format]:
7.29 + "[| b \<in> bexp; sigma: loc -> nat |]
7.30 + ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
7.31 +apply (erule bexp.induct)
7.32 +apply (auto intro!: evalb.intros)
7.33 +done
7.34 +
7.35 +declare bexp_iff [THEN iffD1, simp]
7.36 + bexp_iff [THEN iffD2, intro!]
7.37 +
7.38 +lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
7.39 +apply (erule evalc.induct)
7.40 +apply simp_all
7.41 +(* skip *)
7.42 +apply fast
7.43 +(* assign *)
7.44 +apply (simp add: update_type)
7.45 +(* comp *)
7.46 +apply fast
7.47 +(* while *)
7.48 +apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
7.49 +apply (simp add: Gamma_def)
7.50 +apply (force )
7.51 +(* recursive case of while *)
7.52 +apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
7.53 +apply (simp add: Gamma_def)
7.54 +apply auto
7.55 +done
7.56 +
7.57 +
7.58 +declare B_type [intro!] A_type [intro!]
7.59 +declare evalc.intros [intro]
7.60 +
7.61 +
7.62 +lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
7.63 +apply (erule com.induct)
7.64 +(* skip *)
7.65 +apply force
7.66 +(* assign *)
7.67 +apply force
7.68 +(* comp *)
7.69 +apply force
7.70 +(* while *)
7.71 +apply safe
7.72 +apply simp_all
7.73 +apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
7.74 +apply (unfold Gamma_def)
7.75 +apply force
7.76 +(* if *)
7.77 +apply auto
7.78 +done
7.79 +
7.80 +
7.81 +(**** Proof of Equivalence ****)
7.82 +
7.83 +lemma com_equivalence:
7.84 + "\<forall>c \<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"
7.85 +by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
7.86 +
7.87 +end
7.88 +
8.1 --- a/src/ZF/IsaMakefile Fri Dec 28 10:10:55 2001 +0100
8.2 +++ b/src/ZF/IsaMakefile Fri Dec 28 10:11:14 2001 +0100
8.3 @@ -74,7 +74,7 @@
8.4
8.5 ZF-Coind: ZF $(LOG)/ZF-Coind.gz
8.6
8.7 -$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
8.8 +$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy \
8.9 Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
8.10 Coind/Static.thy Coind/Types.thy Coind/Values.thy
8.11 @$(ISATOOL) usedir $(OUT)/ZF Coind
8.12 @@ -84,8 +84,8 @@
8.13
8.14 ZF-IMP: ZF $(LOG)/ZF-IMP.gz
8.15
8.16 -$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
8.17 - IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
8.18 +$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy \
8.19 + IMP/Denotation.thy IMP/Equiv.thy IMP/ROOT.ML
8.20 @$(ISATOOL) usedir $(OUT)/ZF IMP
8.21
8.22
8.23 @@ -131,9 +131,9 @@
8.24 ZF-ex: ZF $(LOG)/ZF-ex.gz
8.25
8.26 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
8.27 - ex/BinEx.thy ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
8.28 - ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy ex/Primes.ML ex/Primes.thy \
8.29 - ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
8.30 + ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy \
8.31 + ex/Limit.ML ex/Limit.thy ex/LList.thy ex/Primes.thy \
8.32 + ex/NatSum.thy ex/Ramsey.thy ex/misc.thy
8.33 @$(ISATOOL) usedir $(OUT)/ZF ex
8.34
8.35
9.1 --- a/src/ZF/ex/Commutation.ML Fri Dec 28 10:10:55 2001 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,131 +0,0 @@
9.4 -(* Title: HOL/Lambda/Commutation.thy
9.5 - ID: $Id$
9.6 - Author: Tobias Nipkow & Sidi Ould Ehmety
9.7 - Copyright 1995 TU Muenchen
9.8 -
9.9 -Commutation theory for proving the Church Rosser theorem
9.10 - ported from Isabelle/HOL by Sidi Ould Ehmety
9.11 -*)
9.12 -
9.13 -Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
9.14 -by (Blast_tac 1);
9.15 -qed "square_sym";
9.16 -
9.17 -
9.18 -Goalw [square_def] "[| square(r,s,t,u); t \\<subseteq> t' |] ==> square(r,s,t',u)";
9.19 -by (Blast_tac 1);
9.20 -qed "square_subset";
9.21 -
9.22 -
9.23 -Goalw [square_def]
9.24 - "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
9.25 -by (Clarify_tac 1);
9.26 -by (etac rtrancl_induct 1);
9.27 -by (blast_tac (claset() addIs [rtrancl_refl]) 1);
9.28 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
9.29 -qed_spec_mp "square_rtrancl";
9.30 -
9.31 -(* A special case of square_rtrancl_on *)
9.32 -Goalw [diamond_def, commute_def, strip_def]
9.33 - "diamond(r) ==> strip(r)";
9.34 -by (rtac square_rtrancl 1);
9.35 -by (ALLGOALS(Asm_simp_tac));
9.36 -qed "diamond_strip";
9.37 -
9.38 -(*** commute ***)
9.39 -
9.40 -Goalw [commute_def]
9.41 - "commute(r,s) ==> commute(s,r)";
9.42 -by (blast_tac (claset() addIs [square_sym]) 1);
9.43 -qed "commute_sym";
9.44 -
9.45 -Goalw [commute_def]
9.46 -"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
9.47 -by (Clarify_tac 1);
9.48 -by (rtac square_rtrancl 1);
9.49 -by (rtac square_sym 2);
9.50 -by (rtac square_rtrancl 2);
9.51 -by (rtac square_sym 3);
9.52 -by (ALLGOALS(asm_simp_tac
9.53 - (simpset() addsimps [rtrancl_field])));
9.54 -qed_spec_mp "commute_rtrancl";
9.55 -
9.56 -
9.57 -Goalw [strip_def,confluent_def, diamond_def]
9.58 -"strip(r) ==> confluent(r)";
9.59 -by (dtac commute_rtrancl 1);
9.60 -by (ALLGOALS(asm_full_simp_tac (simpset()
9.61 - addsimps [rtrancl_field])));
9.62 -qed "strip_confluent";
9.63 -
9.64 -
9.65 -Goalw [commute_def,square_def]
9.66 - "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
9.67 -by (Blast_tac 1);
9.68 -qed "commute_Un";
9.69 -
9.70 -
9.71 -Goalw [diamond_def]
9.72 - "[| diamond(r); diamond(s); commute(r, s) |] \
9.73 -\ ==> diamond(r Un s)";
9.74 -by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
9.75 -qed "diamond_Un";
9.76 -
9.77 -
9.78 -Goalw [diamond_def,confluent_def]
9.79 - "diamond(r) ==> confluent(r)";
9.80 -by (etac commute_rtrancl 1);
9.81 -by (Simp_tac 1);
9.82 -qed "diamond_confluent";
9.83 -
9.84 -
9.85 -Goalw [confluent_def]
9.86 - "[| confluent(r); confluent(s); commute(r^*, s^*); \
9.87 -\ r \\<subseteq> Sigma(A,B); s \\<subseteq> Sigma(C,D) |] ==> confluent(r Un s)";
9.88 -by (rtac (rtrancl_Un_rtrancl RS subst) 1);
9.89 -by (blast_tac (claset() addDs [diamond_Un]
9.90 - addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
9.91 -by Auto_tac;
9.92 -qed "confluent_Un";
9.93 -
9.94 -
9.95 -Goal
9.96 - "[| diamond(r); s \\<subseteq> r; r<= s^* |] ==> confluent(s)";
9.97 -by (dresolve_tac [rtrancl_subset RS sym] 1);
9.98 -by (assume_tac 1);
9.99 -by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
9.100 -by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
9.101 -by (Asm_simp_tac 1);
9.102 -qed "diamond_to_confluence";
9.103 -
9.104 -(*** Church_Rosser ***)
9.105 -
9.106 -Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
9.107 - "Church_Rosser(r) ==> confluent(r)";
9.108 -by Auto_tac;
9.109 -by (dtac converseI 1);
9.110 -by (full_simp_tac (simpset()
9.111 - addsimps [rtrancl_converse RS sym]) 1);
9.112 -by (dres_inst_tac [("x", "b")] spec 1);
9.113 -by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
9.114 -by (res_inst_tac [("b", "a")] rtrancl_trans 1);
9.115 -by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
9.116 -qed "Church_Rosser1";
9.117 -
9.118 -
9.119 -Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
9.120 -"confluent(r) ==> Church_Rosser(r)";
9.121 -by Auto_tac;
9.122 -by (ftac fieldI1 1);
9.123 -by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
9.124 -by (etac rtrancl_induct 1);
9.125 -by (ALLGOALS(Clarify_tac));
9.126 -by (blast_tac (claset() addIs [rtrancl_refl]) 1);
9.127 -by (blast_tac (claset() delrules [rtrancl_refl]
9.128 - addIs [r_into_rtrancl, rtrancl_trans]) 1);
9.129 -qed "Church_Rosser2";
9.130 -
9.131 -
9.132 -Goal "Church_Rosser(r) <-> confluent(r)";
9.133 -by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
9.134 -qed "Church_Rosser";
9.135 \ No newline at end of file
10.1 --- a/src/ZF/ex/LList.ML Fri Dec 28 10:10:55 2001 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,195 +0,0 @@
10.4 -(* Title: ZF/ex/LList.ML
10.5 - ID: $Id$
10.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
10.7 - Copyright 1994 University of Cambridge
10.8 -
10.9 -Codatatype definition of Lazy Lists
10.10 -*)
10.11 -
10.12 -(*These commands cause classical reasoning to regard the subset relation
10.13 - as primitive, not reducing it to membership*)
10.14 -
10.15 -Delrules [subsetI, subsetCE];
10.16 -AddSIs [subset_refl, cons_subsetI, subset_consI,
10.17 - Union_least, UN_least, Un_least,
10.18 - Inter_greatest, Int_greatest, RepFun_subset,
10.19 - Un_upper1, Un_upper2, Int_lower1, Int_lower2];
10.20 -
10.21 -(*An elimination rule, for type-checking*)
10.22 -val LConsE = llist.mk_cases "LCons(a,l) \\<in> llist(A)";
10.23 -
10.24 -(*Proving freeness results*)
10.25 -val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
10.26 -val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
10.27 -
10.28 -Goal "llist(A) = {0} <+> (A <*> llist(A))";
10.29 -let open llist val rew = rewrite_rule con_defs in
10.30 -by (fast_tac (claset() addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
10.31 -end;
10.32 -qed "llist_unfold";
10.33 -
10.34 -(*** Lemmas to justify using "llist" in other recursive type definitions ***)
10.35 -
10.36 -Goalw llist.defs "A \\<subseteq> B ==> llist(A) \\<subseteq> llist(B)";
10.37 -by (rtac gfp_mono 1);
10.38 -by (REPEAT (rtac llist.bnd_mono 1));
10.39 -by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
10.40 -qed "llist_mono";
10.41 -
10.42 -(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **)
10.43 -
10.44 -AddSIs [QPair_Int_Vset_subset_UN RS subset_trans,
10.45 - QPair_subset_univ,
10.46 - empty_subsetI, one_in_quniv RS qunivD];
10.47 -AddSDs [qunivD];
10.48 -AddSEs [Ord_in_Ord];
10.49 -
10.50 -Goal "Ord(i) ==> \\<forall>l \\<in> llist(quniv(A)). l Int Vset(i) \\<subseteq> univ(eclose(A))";
10.51 -by (etac trans_induct 1);
10.52 -by (rtac ballI 1);
10.53 -by (etac llist.elim 1);
10.54 -by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
10.55 -(*LNil case*)
10.56 -by (Asm_simp_tac 1);
10.57 -(*LCons case*)
10.58 -by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
10.59 -qed "llist_quniv_lemma";
10.60 -
10.61 -Goal "llist(quniv(A)) \\<subseteq> quniv(A)";
10.62 -by (rtac (qunivI RS subsetI) 1);
10.63 -by (rtac Int_Vset_subset 1);
10.64 -by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
10.65 -qed "llist_quniv";
10.66 -
10.67 -bind_thm ("llist_subset_quniv",
10.68 - (llist_mono RS (llist_quniv RSN (2,subset_trans))));
10.69 -
10.70 -
10.71 -(*** Lazy List Equality: lleq ***)
10.72 -
10.73 -AddSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono];
10.74 -AddSEs [Ord_in_Ord, Pair_inject];
10.75 -
10.76 -(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
10.77 -Goal "Ord(i) ==> \\<forall>l l'. <l,l'> \\<in> lleq(A) --> l Int Vset(i) \\<subseteq> l'";
10.78 -by (etac trans_induct 1);
10.79 -by (REPEAT (resolve_tac [allI, impI] 1));
10.80 -by (etac lleq.elim 1);
10.81 -by (rewrite_goals_tac (QInr_def::llist.con_defs));
10.82 -by Safe_tac;
10.83 -by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
10.84 -qed "lleq_Int_Vset_subset_lemma";
10.85 -
10.86 -bind_thm ("lleq_Int_Vset_subset",
10.87 - (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
10.88 -
10.89 -
10.90 -(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
10.91 -val [prem] = goal LList.thy "<l,l'> \\<in> lleq(A) ==> <l',l> \\<in> lleq(A)";
10.92 -by (rtac (prem RS converseI RS lleq.coinduct) 1);
10.93 -by (rtac (lleq.dom_subset RS converse_type) 1);
10.94 -by Safe_tac;
10.95 -by (etac lleq.elim 1);
10.96 -by (ALLGOALS Fast_tac);
10.97 -qed "lleq_symmetric";
10.98 -
10.99 -Goal "<l,l'> \\<in> lleq(A) ==> l=l'";
10.100 -by (rtac equalityI 1);
10.101 -by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
10.102 - ORELSE etac lleq_symmetric 1));
10.103 -qed "lleq_implies_equal";
10.104 -
10.105 -val [eqprem,lprem] = goal LList.thy
10.106 - "[| l=l'; l \\<in> llist(A) |] ==> <l,l'> \\<in> lleq(A)";
10.107 -by (res_inst_tac [("X", "{<l,l>. l \\<in> llist(A)}")] lleq.coinduct 1);
10.108 -by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
10.109 -by Safe_tac;
10.110 -by (etac llist.elim 1);
10.111 -by (ALLGOALS Fast_tac);
10.112 -qed "equal_llist_implies_leq";
10.113 -
10.114 -
10.115 -(*** Lazy List Functions ***)
10.116 -
10.117 -(*Examples of coinduction for type-checking and to prove llist equations*)
10.118 -
10.119 -(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
10.120 -
10.121 -Goalw llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
10.122 -by (rtac bnd_monoI 1);
10.123 -by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
10.124 -by (REPEAT (ares_tac [subset_refl, A_subset_univ,
10.125 - QInr_subset_univ, QPair_subset_univ] 1));
10.126 -qed "lconst_fun_bnd_mono";
10.127 -
10.128 -(* lconst(a) = LCons(a,lconst(a)) *)
10.129 -bind_thm ("lconst",
10.130 - ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_unfold));
10.131 -
10.132 -val lconst_subset = lconst_def RS def_lfp_subset;
10.133 -
10.134 -bind_thm ("member_subset_Union_eclose", (arg_into_eclose RS Union_upper));
10.135 -
10.136 -Goal "a \\<in> A ==> lconst(a) \\<in> quniv(A)";
10.137 -by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
10.138 -by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
10.139 -qed "lconst_in_quniv";
10.140 -
10.141 -Goal "a \\<in> A ==> lconst(a): llist(A)";
10.142 -by (rtac (singletonI RS llist.coinduct) 1);
10.143 -by (etac (lconst_in_quniv RS singleton_subsetI) 1);
10.144 -by (fast_tac (claset() addSIs [lconst]) 1);
10.145 -qed "lconst_type";
10.146 -
10.147 -(*** flip --- equations merely assumed; certain consequences proved ***)
10.148 -
10.149 -Addsimps [flip_LNil, flip_LCons, not_type];
10.150 -
10.151 -goal QUniv.thy "!!b. b \\<in> bool ==> b Int X \\<subseteq> univ(eclose(A))";
10.152 -by (fast_tac (claset() addIs [Int_lower1 RS subset_trans] addSEs [boolE]) 1);
10.153 -qed "bool_Int_subset_univ";
10.154 -
10.155 -AddSIs [not_type];
10.156 -AddIs [bool_Int_subset_univ];
10.157 -
10.158 -(*Reasoning borrowed from lleq.ML; a similar proof works for all
10.159 - "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
10.160 -Goal "Ord(i) ==> \\<forall>l \\<in> llist(bool). flip(l) Int Vset(i) \\<subseteq> \
10.161 -\ univ(eclose(bool))";
10.162 -by (etac trans_induct 1);
10.163 -by (rtac ballI 1);
10.164 -by (etac llist.elim 1);
10.165 -by (ALLGOALS Asm_simp_tac);
10.166 -by (ALLGOALS
10.167 - (asm_simp_tac (simpset() addsimps [QInl_def,QInr_def] @ llist.con_defs)));
10.168 -(*LCons case*)
10.169 -by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
10.170 -qed "flip_llist_quniv_lemma";
10.171 -
10.172 -Goal "l \\<in> llist(bool) ==> flip(l) \\<in> quniv(bool)";
10.173 -by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
10.174 -by (REPEAT (assume_tac 1));
10.175 -qed "flip_in_quniv";
10.176 -
10.177 -val [prem] = goal LList.thy "l \\<in> llist(bool) ==> flip(l): llist(bool)";
10.178 -by (res_inst_tac [("X", "{flip(l) . l \\<in> llist(bool)}")]
10.179 - llist.coinduct 1);
10.180 -by (rtac (prem RS RepFunI) 1);
10.181 -by (fast_tac (claset() addSIs [flip_in_quniv]) 1);
10.182 -by (etac RepFunE 1);
10.183 -by (etac llist.elim 1);
10.184 -by (ALLGOALS Asm_simp_tac);
10.185 -by (Fast_tac 1);
10.186 -qed "flip_type";
10.187 -
10.188 -val [prem] = goal LList.thy
10.189 - "l \\<in> llist(bool) ==> flip(flip(l)) = l";
10.190 -by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l \\<in> llist(bool)}")]
10.191 - (lleq.coinduct RS lleq_implies_equal) 1);
10.192 -by (rtac (prem RS RepFunI) 1);
10.193 -by (fast_tac (claset() addSIs [flip_type]) 1);
10.194 -by (etac RepFunE 1);
10.195 -by (etac llist.elim 1);
10.196 -by (Asm_simp_tac 1);
10.197 -by (asm_full_simp_tac (simpset() addsimps [flip_type, not_not]) 1);
10.198 -qed "flip_flip";
11.1 --- a/src/ZF/ex/NatSum.ML Fri Dec 28 10:10:55 2001 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,64 +0,0 @@
11.4 -(* Title: HOL/ex/NatSum.ML
11.5 - ID: $Id$
11.6 - Author: Tobias Nipkow & Lawrence C Paulson
11.7 -
11.8 -Summing natural numbers, squares, cubes, etc.
11.9 -
11.10 -Originally demonstrated permutative rewriting, but add_ac is no longer needed
11.11 - thanks to new simprocs.
11.12 -
11.13 -Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
11.14 - http://www.research.att.com/~njas/sequences/
11.15 -*)
11.16 -
11.17 -Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2];
11.18 -Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
11.19 -
11.20 -(*The sum of the first n odd numbers equals n squared.*)
11.21 -Goal "n \\<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
11.22 -by (induct_tac "n" 1);
11.23 -by Auto_tac;
11.24 -qed "sum_of_odds";
11.25 -
11.26 -(*The sum of the first n odd squares*)
11.27 -Goal "n \\<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
11.28 -\ $#n $* (#4 $* $#n $* $#n $- #1)";
11.29 -by (induct_tac "n" 1);
11.30 -by Auto_tac;
11.31 -qed "sum_of_odd_squares";
11.32 -
11.33 -(*The sum of the first n odd cubes*)
11.34 -Goal "n \\<in> nat \
11.35 -\ ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
11.36 -\ $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
11.37 -by (induct_tac "n" 1);
11.38 -by Auto_tac;
11.39 -qed "sum_of_odd_cubes";
11.40 -
11.41 -(*The sum of the first n positive integers equals n(n+1)/2.*)
11.42 -Goal "n \\<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
11.43 -by (induct_tac "n" 1);
11.44 -by Auto_tac;
11.45 -qed "sum_of_naturals";
11.46 -
11.47 -Goal "n \\<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
11.48 -\ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
11.49 -by (induct_tac "n" 1);
11.50 -by Auto_tac;
11.51 -qed "sum_of_squares";
11.52 -
11.53 -Goal "n \\<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
11.54 -\ $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
11.55 -by (induct_tac "n" 1);
11.56 -by Auto_tac;
11.57 -qed "sum_of_cubes";
11.58 -
11.59 -(** Sum of fourth powers **)
11.60 -
11.61 -Goal "n \\<in> nat ==> \
11.62 -\ #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
11.63 -\ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
11.64 -\ (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";
11.65 -by (induct_tac "n" 1);
11.66 -by Auto_tac;
11.67 -qed "sum_of_fourth_powers";
12.1 --- a/src/ZF/ex/Primes.ML Fri Dec 28 10:10:55 2001 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,435 +0,0 @@
12.4 -(* Title: ZF/ex/Primes.ML
12.5 - ID: $Id$
12.6 - Author: Christophe Tabacznyj and Lawrence C Paulson
12.7 - Copyright 1996 University of Cambridge
12.8 -
12.9 -The "divides" relation, the greatest common divisor and Euclid's algorithm
12.10 -*)
12.11 -
12.12 -(************************************************)
12.13 -(** Divides Relation **)
12.14 -(************************************************)
12.15 -
12.16 -Goalw [dvd_def] "m dvd n ==> m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)";
12.17 -by (assume_tac 1);
12.18 -qed "dvdD";
12.19 -
12.20 -Goal "!!P. [|m dvd n; !!k. [|m \\<in> nat; n \\<in> nat; k \\<in> nat; n = m#*k|] ==> P|] \
12.21 -\ ==> P";
12.22 -by (blast_tac (claset() addSDs [dvdD]) 1);
12.23 -qed "dvdE";
12.24 -
12.25 -bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
12.26 -bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
12.27 -
12.28 -
12.29 -Goalw [dvd_def] "m \\<in> nat ==> m dvd 0";
12.30 -by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
12.31 -qed "dvd_0_right";
12.32 -Addsimps [dvd_0_right];
12.33 -
12.34 -Goalw [dvd_def] "0 dvd m ==> m = 0";
12.35 -by (fast_tac (claset() addss (simpset())) 1);
12.36 -qed "dvd_0_left";
12.37 -
12.38 -Goalw [dvd_def] "m \\<in> nat ==> m dvd m";
12.39 -by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
12.40 -qed "dvd_refl";
12.41 -Addsimps [dvd_refl];
12.42 -
12.43 -Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
12.44 -by (fast_tac (claset() addIs [mult_assoc, mult_type] ) 1);
12.45 -qed "dvd_trans";
12.46 -
12.47 -Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
12.48 -by (fast_tac (claset() addDs [mult_eq_self_implies_10]
12.49 - addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
12.50 -qed "dvd_anti_sym";
12.51 -
12.52 -Goalw [dvd_def] "[|(i#*j) dvd k; i \\<in> nat|] ==> i dvd k";
12.53 -by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
12.54 -by (Blast_tac 1);
12.55 -qed "dvd_mult_left";
12.56 -
12.57 -Goalw [dvd_def] "[|(i#*j) dvd k; j \\<in> nat|] ==> j dvd k";
12.58 -by (Clarify_tac 1);
12.59 -by (res_inst_tac [("x","i#*k")] bexI 1);
12.60 -by (simp_tac (simpset() addsimps mult_ac) 1);
12.61 -by (rtac mult_type 1);
12.62 -qed "dvd_mult_right";
12.63 -
12.64 -
12.65 -(************************************************)
12.66 -(** Greatest Common Divisor **)
12.67 -(************************************************)
12.68 -
12.69 -(* GCD by Euclid's Algorithm *)
12.70 -
12.71 -Goalw [gcd_def] "gcd(m,0) = natify(m)";
12.72 -by (stac transrec 1);
12.73 -by (Asm_simp_tac 1);
12.74 -qed "gcd_0";
12.75 -Addsimps [gcd_0];
12.76 -
12.77 -Goal "gcd(natify(m),n) = gcd(m,n)";
12.78 -by (simp_tac (simpset() addsimps [gcd_def]) 1);
12.79 -qed "gcd_natify1";
12.80 -
12.81 -Goal "gcd(m, natify(n)) = gcd(m,n)";
12.82 -by (simp_tac (simpset() addsimps [gcd_def]) 1);
12.83 -qed "gcd_natify2";
12.84 -Addsimps [gcd_natify1,gcd_natify2];
12.85 -
12.86 -Goalw [gcd_def]
12.87 - "[| 0<n; n \\<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)";
12.88 -by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
12.89 -by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
12.90 - mod_less_divisor RS ltD]) 1);
12.91 -qed "gcd_non_0_raw";
12.92 -
12.93 -Goal "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)";
12.94 -by (cut_inst_tac [("m","m"),("n","natify(n)")] gcd_non_0_raw 1);
12.95 -by Auto_tac;
12.96 -qed "gcd_non_0";
12.97 -
12.98 -Goal "gcd(m,1) = 1";
12.99 -by (asm_simp_tac (simpset() addsimps [gcd_non_0]) 1);
12.100 -qed "gcd_1";
12.101 -Addsimps [gcd_1];
12.102 -
12.103 -Goalw [dvd_def] "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
12.104 -by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
12.105 -qed "dvd_add";
12.106 -
12.107 -Goalw [dvd_def] "k dvd n ==> k dvd (m #* n)";
12.108 -by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
12.109 -qed "dvd_mult";
12.110 -
12.111 -Goal "k dvd m ==> k dvd (m #* n)";
12.112 -by (stac mult_commute 1);
12.113 -by (blast_tac (claset() addIs [dvd_mult]) 1);
12.114 -qed "dvd_mult2";
12.115 -
12.116 -(* k dvd (m*k) *)
12.117 -bind_thm ("dvdI1", dvd_refl RS dvd_mult);
12.118 -bind_thm ("dvdI2", dvd_refl RS dvd_mult2);
12.119 -Addsimps [dvdI1, dvdI2];
12.120 -
12.121 -Goal "[| a \\<in> nat; b \\<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a";
12.122 -by (div_undefined_case_tac "b=0" 1);
12.123 -by (blast_tac
12.124 - (claset() addIs [mod_div_equality RS subst]
12.125 - addEs [dvdE]
12.126 - addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 1);
12.127 -qed "dvd_mod_imp_dvd_raw";
12.128 -
12.129 -Goal "[| k dvd (a mod b); k dvd b; a \\<in> nat |] ==> k dvd a";
12.130 -by (cut_inst_tac [("b","natify(b)")] dvd_mod_imp_dvd_raw 1);
12.131 -by Auto_tac;
12.132 -by (asm_full_simp_tac (simpset() addsimps [dvd_def]) 1);
12.133 -qed "dvd_mod_imp_dvd";
12.134 -
12.135 -(*Imitating TFL*)
12.136 -Goal "[| n \\<in> nat; \
12.137 -\ \\<forall>m \\<in> nat. P(m,0); \
12.138 -\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |] \
12.139 -\ ==> \\<forall>m \\<in> nat. P (m,n)";
12.140 -by (eres_inst_tac [("i","n")] complete_induct 1);
12.141 -by (case_tac "x=0" 1);
12.142 -by (Asm_simp_tac 1);
12.143 -by (Clarify_tac 1);
12.144 -by (dres_inst_tac [("x1","m"),("x","x")] (bspec RS bspec) 1);
12.145 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_0_lt_iff])));
12.146 -by (blast_tac (claset() addIs [mod_less_divisor RS ltD]) 1);
12.147 -qed_spec_mp "gcd_induct_lemma";
12.148 -
12.149 -Goal "!!P. [| m \\<in> nat; n \\<in> nat; \
12.150 -\ !!m. m \\<in> nat ==> P(m,0); \
12.151 -\ !!m n. [|m \\<in> nat; n \\<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] \
12.152 -\ ==> P (m,n)";
12.153 -by (blast_tac (claset() addIs [gcd_induct_lemma]) 1);
12.154 -qed "gcd_induct";
12.155 -
12.156 -
12.157 -(* gcd type *)
12.158 -
12.159 -Goal "gcd(m, n) \\<in> nat";
12.160 -by (subgoal_tac "gcd(natify(m), natify(n)) \\<in> nat" 1);
12.161 -by (Asm_full_simp_tac 1);
12.162 -by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_induct 1);
12.163 -by Auto_tac;
12.164 -by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
12.165 -qed "gcd_type";
12.166 -Addsimps [gcd_type];
12.167 -
12.168 -(* Property 1: gcd(a,b) divides a and b *)
12.169 -
12.170 -Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n";
12.171 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
12.172 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
12.173 -by (blast_tac
12.174 - (claset() addIs [dvd_mod_imp_dvd_raw, nat_into_Ord RS Ord_0_lt]) 1);
12.175 -qed "gcd_dvd_both";
12.176 -
12.177 -Goal "m \\<in> nat ==> gcd(m,n) dvd m";
12.178 -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1);
12.179 -by Auto_tac;
12.180 -qed "gcd_dvd1";
12.181 -Addsimps [gcd_dvd1];
12.182 -
12.183 -Goal "n \\<in> nat ==> gcd(m,n) dvd n";
12.184 -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1);
12.185 -by Auto_tac;
12.186 -qed "gcd_dvd2";
12.187 -Addsimps [gcd_dvd2];
12.188 -
12.189 -(* if f divides a and b then f divides gcd(a,b) *)
12.190 -
12.191 -Goalw [dvd_def] "[| f dvd a; f dvd b |] ==> f dvd (a mod b)";
12.192 -by (div_undefined_case_tac "b=0" 1);
12.193 -by Auto_tac;
12.194 -by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);
12.195 -qed "dvd_mod";
12.196 -
12.197 -(* Property 2: for all a,b,f naturals,
12.198 - if f divides a and f divides b then f divides gcd(a,b)*)
12.199 -
12.200 -Goal "[| m \\<in> nat; n \\<in> nat; f \\<in> nat |] \
12.201 -\ ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
12.202 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
12.203 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_non_0, dvd_mod])));
12.204 -qed_spec_mp "gcd_greatest_raw";
12.205 -
12.206 -Goal "[| f dvd m; f dvd n; f \\<in> nat |] ==> f dvd gcd(m,n)";
12.207 -by (rtac gcd_greatest_raw 1);
12.208 -by (auto_tac (claset(), simpset() addsimps [dvd_def]));
12.209 -qed "gcd_greatest";
12.210 -
12.211 -Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
12.212 -\ ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)";
12.213 -by (blast_tac (claset() addSIs [gcd_greatest, gcd_dvd1, gcd_dvd2]
12.214 - addIs [dvd_trans]) 1);
12.215 -qed "gcd_greatest_iff";
12.216 -Addsimps [gcd_greatest_iff];
12.217 -
12.218 -(* GCD PROOF: GCD exists and gcd fits the definition *)
12.219 -
12.220 -Goalw [is_gcd_def] "[| m \\<in> nat; n \\<in> nat |] ==> is_gcd(gcd(m,n), m, n)";
12.221 -by (Asm_simp_tac 1);
12.222 -qed "is_gcd";
12.223 -
12.224 -(* GCD is unique *)
12.225 -
12.226 -Goalw [is_gcd_def] "[|is_gcd(m,a,b); is_gcd(n,a,b); m\\<in>nat; n\\<in>nat|] ==> m=n";
12.227 -by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
12.228 -qed "is_gcd_unique";
12.229 -
12.230 -Goalw [is_gcd_def] "is_gcd(k,m,n) <-> is_gcd(k,n,m)";
12.231 -by (Blast_tac 1);
12.232 -qed "is_gcd_commute";
12.233 -
12.234 -Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd(m,n) = gcd(n,m)";
12.235 -by (rtac is_gcd_unique 1);
12.236 -by (rtac is_gcd 1);
12.237 -by (rtac (is_gcd_commute RS iffD1) 3);
12.238 -by (rtac is_gcd 3);
12.239 -by Auto_tac;
12.240 -qed "gcd_commute_raw";
12.241 -
12.242 -Goal "gcd(m,n) = gcd(n,m)";
12.243 -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_commute_raw 1);
12.244 -by Auto_tac;
12.245 -qed "gcd_commute";
12.246 -
12.247 -Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
12.248 -\ ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
12.249 -by (rtac is_gcd_unique 1);
12.250 -by (rtac is_gcd 1);
12.251 -by (asm_full_simp_tac (simpset() addsimps [is_gcd_def]) 3);
12.252 -by (blast_tac (claset() addIs [gcd_dvd1, gcd_dvd2, gcd_type]
12.253 - addIs [dvd_trans]) 3);
12.254 -by Auto_tac;
12.255 -qed "gcd_assoc_raw";
12.256 -
12.257 -Goal "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
12.258 -by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")]
12.259 - gcd_assoc_raw 1);
12.260 -by Auto_tac;
12.261 -qed "gcd_assoc";
12.262 -
12.263 -Goal "gcd (0, m) = natify(m)";
12.264 -by (asm_simp_tac (simpset() addsimps [inst "m" "0" gcd_commute]) 1);
12.265 -qed "gcd_0_left";
12.266 -Addsimps [gcd_0_left];
12.267 -
12.268 -Goal "gcd (1, m) = 1";
12.269 -by (asm_simp_tac (simpset() addsimps [inst "m" "1" gcd_commute]) 1);
12.270 -qed "gcd_1_left";
12.271 -Addsimps [gcd_1_left];
12.272 -
12.273 -
12.274 -(* Multiplication laws *)
12.275 -
12.276 -Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
12.277 -\ ==> k #* gcd (m, n) = gcd (k #* m, k #* n)";
12.278 -by (eres_inst_tac [("m","m"),("n","n")] gcd_induct 1);
12.279 -by (assume_tac 1);
12.280 -by (Asm_simp_tac 1);
12.281 -by (case_tac "k = 0" 1);
12.282 -by (Asm_full_simp_tac 1);
12.283 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, gcd_non_0,
12.284 - mod_mult_distrib2, Ord_0_lt_iff]) 1);
12.285 -qed "gcd_mult_distrib2_raw";
12.286 -
12.287 -Goal "k #* gcd (m, n) = gcd (k #* m, k #* n)";
12.288 -by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")]
12.289 - gcd_mult_distrib2_raw 1);
12.290 -by Auto_tac;
12.291 -qed "gcd_mult_distrib2";
12.292 -
12.293 -Goal "gcd (k, k #* n) = natify(k)";
12.294 -by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
12.295 -by Auto_tac;
12.296 -qed "gcd_mult";
12.297 -Addsimps [gcd_mult];
12.298 -
12.299 -Goal "gcd (k, k) = natify(k)";
12.300 -by (cut_inst_tac [("k","k"),("n","1")] gcd_mult 1);
12.301 -by Auto_tac;
12.302 -qed "gcd_self";
12.303 -Addsimps [gcd_self];
12.304 -
12.305 -Goal "[| gcd (k,n) = 1; k dvd (m #* n); m \\<in> nat |] \
12.306 -\ ==> k dvd m";
12.307 -by (cut_inst_tac [("k","m"),("m","k"),("n","n")] gcd_mult_distrib2 1);
12.308 -by Auto_tac;
12.309 -by (eres_inst_tac [("b","m")] ssubst 1);
12.310 -by (asm_full_simp_tac (simpset() addsimps [dvd_imp_nat1]) 1);
12.311 -qed "relprime_dvd_mult";
12.312 -
12.313 -Goal "[| gcd (k,n) = 1; m \\<in> nat |] \
12.314 -\ ==> k dvd (m #* n) <-> k dvd m";
12.315 -by (blast_tac (claset() addIs [dvdI2, relprime_dvd_mult, dvd_trans]) 1);
12.316 -qed "relprime_dvd_mult_iff";
12.317 -
12.318 -Goalw [prime_def]
12.319 - "[| p \\<in> prime; ~ (p dvd n); n \\<in> nat |] ==> gcd (p, n) = 1";
12.320 -by (Clarify_tac 1);
12.321 -by (dres_inst_tac [("x","gcd(p,n)")] bspec 1);
12.322 -by Auto_tac;
12.323 -by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd2 1);
12.324 -by Auto_tac;
12.325 -qed "prime_imp_relprime";
12.326 -
12.327 -Goalw [prime_def] "p \\<in> prime ==> p \\<in> nat";
12.328 -by Auto_tac;
12.329 -qed "prime_into_nat";
12.330 -
12.331 -Goalw [prime_def] "p \\<in> prime \\<Longrightarrow> p\\<noteq>0";
12.332 -by Auto_tac;
12.333 -qed "prime_nonzero";
12.334 -
12.335 -
12.336 -(*This theorem leads immediately to a proof of the uniqueness of
12.337 - factorization. If p divides a product of primes then it is
12.338 - one of those primes.*)
12.339 -
12.340 -Goal "[|p dvd m #* n; p \\<in> prime; m \\<in> nat; n \\<in> nat |] ==> p dvd m \\<or> p dvd n";
12.341 -by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime,
12.342 - prime_into_nat]) 1);
12.343 -qed "prime_dvd_mult";
12.344 -
12.345 -
12.346 -(** Addition laws **)
12.347 -
12.348 -Goal "gcd (m #+ n, n) = gcd (m, n)";
12.349 -by (subgoal_tac "gcd (m #+ natify(n), natify(n)) = gcd (m, natify(n))" 1);
12.350 -by (Asm_full_simp_tac 1);
12.351 -by (case_tac "natify(n) = 0" 1);
12.352 -by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff, gcd_non_0]));
12.353 -qed "gcd_add1";
12.354 -Addsimps [gcd_add1];
12.355 -
12.356 -Goal "gcd (m, m #+ n) = gcd (m, n)";
12.357 -by (rtac (gcd_commute RS trans) 1);
12.358 -by (stac add_commute 1);
12.359 -by (Simp_tac 1);
12.360 -by (rtac gcd_commute 1);
12.361 -qed "gcd_add2";
12.362 -Addsimps [gcd_add2];
12.363 -
12.364 -Goal "gcd (m, n #+ m) = gcd (m, n)";
12.365 -by (stac add_commute 1);
12.366 -by (rtac gcd_add2 1);
12.367 -qed "gcd_add2'";
12.368 -Addsimps [gcd_add2'];
12.369 -
12.370 -Goal "k \\<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)";
12.371 -by (etac nat_induct 1);
12.372 -by (auto_tac (claset(), simpset() addsimps [gcd_add2, add_assoc]));
12.373 -qed "gcd_add_mult_raw";
12.374 -
12.375 -Goal "gcd (m, k #* m #+ n) = gcd (m, n)";
12.376 -by (cut_inst_tac [("k","natify(k)")] gcd_add_mult_raw 1);
12.377 -by Auto_tac;
12.378 -qed "gcd_add_mult";
12.379 -
12.380 -
12.381 -(* More multiplication laws *)
12.382 -
12.383 -Goal "[|gcd (k,n) = 1; m \\<in> nat; n \\<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)";
12.384 -by (rtac dvd_anti_sym 1);
12.385 - by (rtac gcd_greatest 1);
12.386 - by (rtac (inst "n" "k" relprime_dvd_mult) 1);
12.387 -by (asm_full_simp_tac (simpset() addsimps [gcd_assoc]) 1);
12.388 -by (asm_full_simp_tac (simpset() addsimps [gcd_commute]) 1);
12.389 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
12.390 -by (blast_tac (claset() addIs [dvdI1, gcd_dvd1, dvd_trans]) 1);
12.391 -qed "gcd_mult_cancel_raw";
12.392 -
12.393 -
12.394 -Goal "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)";
12.395 -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_mult_cancel_raw 1);
12.396 -by Auto_tac;
12.397 -qed "gcd_mult_cancel";
12.398 -
12.399 -
12.400 -(*** The square root of a prime is irrational: key lemma ***)
12.401 -
12.402 -Goal "\\<lbrakk>n#*n = p#*(k#*k); p \\<in> prime; n \\<in> nat\\<rbrakk> \\<Longrightarrow> p dvd n";
12.403 -by (subgoal_tac "p dvd n#*n" 1);
12.404 - by (blast_tac (claset() addDs [prime_dvd_mult]) 1);
12.405 -by (res_inst_tac [("j","k#*k")] dvd_mult_left 1);
12.406 - by (auto_tac (claset(), simpset() addsimps [prime_def]));
12.407 -qed "prime_dvd_other_side";
12.408 -
12.409 -Goal "\\<lbrakk>k#*k = p#*(j#*j); p \\<in> prime; 0 < k; j \\<in> nat; k \\<in> nat\\<rbrakk> \
12.410 -\ \\<Longrightarrow> k < p#*j & 0 < j";
12.411 -by (rtac ccontr 1);
12.412 -by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le, prime_into_nat]) 1);
12.413 -by (etac disjE 1);
12.414 - by (ftac mult_le_mono 1 THEN REPEAT (assume_tac 1));
12.415 -by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
12.416 -by (auto_tac (claset() addSDs [natify_eqE],
12.417 - simpset() addsimps [not_lt_iff_le, prime_into_nat,
12.418 - mult_le_cancel_le1]));
12.419 -by (asm_full_simp_tac (simpset() addsimps [prime_def]) 1);
12.420 -by (blast_tac (claset() addDs [lt_trans1]) 1);
12.421 -qed "reduction";
12.422 -
12.423 -
12.424 -Goal "j #* (p#*j) = k#*k \\<Longrightarrow> k#*k = p#*(j#*j)";
12.425 -by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
12.426 -qed "rearrange";
12.427 -
12.428 -Goal "\\<lbrakk>m \\<in> nat; p \\<in> prime\\<rbrakk> \\<Longrightarrow> \\<forall>k \\<in> nat. 0<k \\<longrightarrow> m#*m \\<noteq> p#*(k#*k)";
12.429 -by (etac complete_induct 1);
12.430 -by (Clarify_tac 1);
12.431 -by (ftac prime_dvd_other_side 1);
12.432 -by (assume_tac 1);
12.433 -by (assume_tac 1);
12.434 -by (etac dvdE 1);
12.435 -by (asm_full_simp_tac (simpset() addsimps [mult_assoc, mult_cancel1,
12.436 - prime_nonzero, prime_into_nat]) 1);
12.437 -by (blast_tac (claset() addDs [rearrange, reduction, ltD]) 1);
12.438 -qed "prime_not_square";
13.1 --- a/src/ZF/ex/Ramsey.ML Fri Dec 28 10:10:55 2001 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,204 +0,0 @@
13.4 -(* Title: ZF/ex/ramsey.ML
13.5 - ID: $Id$
13.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13.7 - Copyright 1992 University of Cambridge
13.8 -
13.9 -Ramsey's Theorem (finite exponent 2 version)
13.10 -
13.11 -Based upon the article
13.12 - D Basin and M Kaufmann,
13.13 - The Boyer-Moore Prover and Nuprl: An Experimental Comparison.
13.14 - In G Huet and G Plotkin, editors, Logical Frameworks.
13.15 - (CUP, 1991), pages 89--119
13.16 -
13.17 -See also
13.18 - M Kaufmann,
13.19 - An example in NQTHM: Ramsey's Theorem
13.20 - Internal Note, Computational Logic, Inc., Austin, Texas 78703
13.21 - Available from the author: kaufmann@cli.com
13.22 -*)
13.23 -
13.24 -(*** Cliques and Independent sets ***)
13.25 -
13.26 -Goalw [Clique_def] "Clique(0,V,E)";
13.27 -by (Fast_tac 1);
13.28 -qed "Clique0";
13.29 -
13.30 -Goalw [Clique_def] "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
13.31 -by (Fast_tac 1);
13.32 -qed "Clique_superset";
13.33 -
13.34 -Goalw [Indept_def] "Indept(0,V,E)";
13.35 -by (Fast_tac 1);
13.36 -qed "Indept0";
13.37 -
13.38 -Goalw [Indept_def] "[| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)";
13.39 -by (Fast_tac 1);
13.40 -qed "Indept_superset";
13.41 -
13.42 -(*** Atleast ***)
13.43 -
13.44 -Goalw [Atleast_def, inj_def, Pi_def, function_def] "Atleast(0,A)";
13.45 -by (Fast_tac 1);
13.46 -qed "Atleast0";
13.47 -
13.48 -Goalw [Atleast_def]
13.49 - "Atleast(succ(m),A) ==> \\<exists>x \\<in> A. Atleast(m, A-{x})";
13.50 -by (fast_tac (claset() addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
13.51 -qed "Atleast_succD";
13.52 -
13.53 -Goalw [Atleast_def]
13.54 - "[| Atleast(n,A); A \\<subseteq> B |] ==> Atleast(n,B)";
13.55 -by (fast_tac (claset() addEs [inj_weaken_type]) 1);
13.56 -qed "Atleast_superset";
13.57 -
13.58 -Goalw [Atleast_def,succ_def]
13.59 - "[| Atleast(m,B); b\\<notin> B |] ==> Atleast(succ(m), cons(b,B))";
13.60 -by (etac exE 1);
13.61 -by (rtac exI 1);
13.62 -by (etac inj_extend 1);
13.63 -by (rtac mem_not_refl 1);
13.64 -by (assume_tac 1);
13.65 -qed "Atleast_succI";
13.66 -
13.67 -Goal "[| Atleast(m, B-{x}); x \\<in> B |] ==> Atleast(succ(m), B)";
13.68 -by (etac (Atleast_succI RS Atleast_superset) 1);
13.69 -by (Fast_tac 1);
13.70 -by (Fast_tac 1);
13.71 -qed "Atleast_Diff_succI";
13.72 -
13.73 -(*** Main Cardinality Lemma ***)
13.74 -
13.75 -(*The #-succ(0) strengthens the original theorem statement, but precisely
13.76 - the same proof could be used!!*)
13.77 -Goal "m \\<in> nat ==> \
13.78 -\ \\<forall>n \\<in> nat. \\<forall>A B. Atleast((m#+n) #- succ(0), A Un B) --> \
13.79 -\ Atleast(m,A) | Atleast(n,B)";
13.80 -by (induct_tac "m" 1);
13.81 -by (fast_tac (claset() addSIs [Atleast0]) 1);
13.82 -by (Asm_simp_tac 1);
13.83 -by (rtac ballI 1);
13.84 -by (rename_tac "m' n" 1); (*simplifier does NOT preserve bound names!*)
13.85 -by (induct_tac "n" 1);
13.86 -by (fast_tac (claset() addSIs [Atleast0]) 1);
13.87 -by (Asm_simp_tac 1);
13.88 -by Safe_tac;
13.89 -by (etac (Atleast_succD RS bexE) 1);
13.90 -by (rename_tac "n' A B z" 1);
13.91 -by (etac UnE 1);
13.92 -(**case z \\<in> B. Instantiate the '\\<forall>A B' induction hypothesis. **)
13.93 -by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
13.94 -by (etac (mp RS disjE) 2);
13.95 -(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
13.96 -by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
13.97 -(*proving the condition*)
13.98 -by (etac Atleast_superset 2 THEN Fast_tac 2);
13.99 -(**case z \\<in> A. Instantiate the '\\<forall>n \\<in> nat. \\<forall>A B' induction hypothesis. **)
13.100 -by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")]
13.101 - (bspec RS spec RS spec) 1);
13.102 -by (etac nat_succI 1);
13.103 -by (etac (mp RS disjE) 1);
13.104 -(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
13.105 -by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
13.106 -(*proving the condition*)
13.107 -by (Asm_simp_tac 1);
13.108 -by (etac Atleast_superset 1 THEN Fast_tac 1);
13.109 -qed_spec_mp "pigeon2";
13.110 -
13.111 -
13.112 -(**** Ramsey's Theorem ****)
13.113 -
13.114 -(** Base cases of induction; they now admit ANY Ramsey number **)
13.115 -
13.116 -Goalw [Ramsey_def] "Ramsey(n,0,j)";
13.117 -by (fast_tac (claset() addIs [Clique0,Atleast0]) 1);
13.118 -qed "Ramsey0j";
13.119 -
13.120 -Goalw [Ramsey_def] "Ramsey(n,i,0)";
13.121 -by (fast_tac (claset() addIs [Indept0,Atleast0]) 1);
13.122 -qed "Ramseyi0";
13.123 -
13.124 -(** Lemmas for induction step **)
13.125 -
13.126 -(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of
13.127 - Ramsey_step_lemma.*)
13.128 -Goal "[| Atleast(m #+ n, A); m \\<in> nat; n \\<in> nat |] \
13.129 -\ ==> Atleast(succ(m), {x \\<in> A. ~P(x)}) | Atleast(n, {x \\<in> A. P(x)})";
13.130 -by (rtac (nat_succI RS pigeon2) 1);
13.131 -by (Asm_simp_tac 3);
13.132 -by (rtac Atleast_superset 3);
13.133 -by Auto_tac;
13.134 -qed "Atleast_partition";
13.135 -
13.136 -(*For the Atleast part, proves ~(a \\<in> I) from the second premise!*)
13.137 -Goalw [Symmetric_def,Indept_def]
13.138 - "[| Symmetric(E); Indept(I, {z \\<in> V-{a}. <a,z> \\<notin> E}, E); a \\<in> V; \
13.139 -\ Atleast(j,I) |] ==> \
13.140 -\ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
13.141 -by (blast_tac (claset() addSIs [Atleast_succI]) 1);
13.142 -qed "Indept_succ";
13.143 -
13.144 -Goalw [Symmetric_def,Clique_def]
13.145 - "[| Symmetric(E); Clique(C, {z \\<in> V-{a}. <a,z>:E}, E); a \\<in> V; \
13.146 -\ Atleast(j,C) |] ==> \
13.147 -\ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
13.148 -by (blast_tac (claset() addSIs [Atleast_succI]) 1);
13.149 -qed "Clique_succ";
13.150 -
13.151 -(** Induction step **)
13.152 -
13.153 -(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
13.154 -val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def]
13.155 - "[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); \
13.156 -\ m \\<in> nat; n \\<in> nat |] ==> \
13.157 -\ Ramsey(succ(m#+n), succ(i), succ(j))";
13.158 -by Safe_tac;
13.159 -by (etac (Atleast_succD RS bexE) 1);
13.160 -by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
13.161 -by (REPEAT (resolve_tac prems 1));
13.162 -(*case m*)
13.163 -by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
13.164 -by (Fast_tac 1);
13.165 -by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
13.166 -by Safe_tac;
13.167 -by (eresolve_tac (swapify [exI]) 1); (*ignore main \\<exists>quantifier*)
13.168 -by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*)
13.169 -(*case n*)
13.170 -by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
13.171 -by (Fast_tac 1);
13.172 -by Safe_tac;
13.173 -by (rtac exI 1);
13.174 -by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*)
13.175 -by (fast_tac (claset() addEs [Indept_superset]) 1); (*easy -- given an Indept*)
13.176 -qed "Ramsey_step_lemma";
13.177 -
13.178 -
13.179 -(** The actual proof **)
13.180 -
13.181 -(*Again, the induction requires Ramsey numbers to be positive.*)
13.182 -Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. \\<exists>n \\<in> nat. Ramsey(succ(n), i, j)";
13.183 -by (induct_tac "i" 1);
13.184 -by (fast_tac (claset() addSIs [Ramsey0j]) 1);
13.185 -by (rtac ballI 1);
13.186 -by (induct_tac "j" 1);
13.187 -by (fast_tac (claset() addSIs [Ramseyi0]) 1);
13.188 -by (fast_tac (claset() addSDs [bspec]
13.189 - addSIs [add_type,Ramsey_step_lemma]) 1);
13.190 -qed "ramsey_lemma";
13.191 -
13.192 -(*Final statement in a tidy form, without succ(...) *)
13.193 -Goal "[| i \\<in> nat; j \\<in> nat |] ==> \\<exists>n \\<in> nat. Ramsey(n,i,j)";
13.194 -by (best_tac (claset() addDs [ramsey_lemma]) 1);
13.195 -qed "ramsey";
13.196 -
13.197 -(*Compute Ramsey numbers according to proof above -- which, actually,
13.198 - does not constrain the base case values at all!*)
13.199 -fun ram 0 j = 1
13.200 - | ram i 0 = 1
13.201 - | ram i j = ram (i-1) j + ram i (j-1);
13.202 -
13.203 -(*Previous proof gave the following Ramsey numbers, which are smaller than
13.204 - those above by one!*)
13.205 -fun ram' 0 j = 0
13.206 - | ram' i 0 = 0
13.207 - | ram' i j = ram' (i-1) j + ram' i (j-1) + 1;