--- a/src/ZF/Coind/BCR.thy Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(* Title: ZF/Coind/BCR.thy
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
--- a/src/ZF/IMP/Com.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: ZF/IMP/Com.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
-*)
-
-val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
- evalb.dom_subset RS subsetD,
- evalc.dom_subset RS subsetD];
-
-(********** type_intrs for evala **********)
-
-val evala_type_intrs =
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!a.<a,sigma> -a-> n ==> a \\<in> aexp",
- "!!a.<a,sigma> -a-> n ==> sigma \\<in> loc->nat",
- "!!a.<a,sigma> -a-> n ==> n \\<in> nat"];
-
-
-(********** type_intrs for evalb **********)
-
-val evalb_type_intrs =
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!b.<b,sigma> -b-> w ==> b \\<in> bexp",
- "!!b.<b,sigma> -b-> w ==> sigma \\<in> loc->nat",
- "!!b.<b,sigma> -b-> w ==> w \\<in> bool"];
-
-
-(********** type_intrs for evalb **********)
-
-val evalc_type_intrs =
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!c.<c,sigma> -c-> sigma' ==> c \\<in> com",
- "!!c.<c,sigma> -c-> sigma' ==> sigma \\<in> loc->nat",
- "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
-
-
-val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs;
-
-
-val aexp_elim_cases =
- [
- evala.mk_cases "<N(n),sigma> -a-> i",
- evala.mk_cases "<X(x),sigma> -a-> i",
- evala.mk_cases "<Op1(f,e),sigma> -a-> i",
- evala.mk_cases "<Op2(f,a1,a2),sigma> -a-> i"
- ];
--- a/src/ZF/IMP/Com.thy Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Com.thy Fri Dec 28 10:11:14 2001 +0100
@@ -8,34 +8,33 @@
And their Operational semantics
*)
-Com = Main +
+theory Com = Main:
(** Arithmetic expressions **)
consts loc :: i
aexp :: i
datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
- "aexp" = N ("n \\<in> nat")
- | X ("x \\<in> loc")
- | Op1 ("f \\<in> nat -> nat", "a \\<in> aexp")
- | Op2 ("f \\<in> (nat*nat) -> nat", "a0 \\<in> aexp", "a1 \\<in> aexp")
+ "aexp" = N ("n \<in> nat")
+ | X ("x \<in> loc")
+ | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
+ | Op2 ("f \<in> (nat*nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
(** Evaluation of arithmetic expressions **)
-consts evala :: i
- "-a->" :: [i,i] => o (infixl 50)
+consts evala :: "i"
+ "-a->" :: "[i,i] => o" (infixl 50)
translations
- "p -a-> n" == "<p,n> \\<in> evala"
+ "p -a-> n" == "<p,n> \<in> evala"
inductive
domains "evala" <= "(aexp * (loc -> nat)) * nat"
- intrs
- N "[| n \\<in> nat; sigma \\<in> loc->nat |] ==> <N(n),sigma> -a-> n"
- X "[| x \\<in> loc; sigma \\<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
- Op1 "[| <e,sigma> -a-> n; f \\<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
- Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \\<in> (nat*nat) -> nat |]
- ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
-
- type_intrs "aexp.intrs@[apply_funtype]"
+ intros
+ N: "[| n \<in> nat; sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n"
+ X: "[| x \<in> loc; sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
+ Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
+ Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat*nat) -> nat |]
+ ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
+ type_intros aexp.intros apply_funtype
(** Boolean expressions **)
@@ -44,35 +43,34 @@
datatype <= "univ(aexp Un ((nat*nat)->bool) )"
"bexp" = true
| false
- | ROp ("f \\<in> (nat*nat)->bool", "a0 \\<in> aexp", "a1 \\<in> aexp")
- | noti ("b \\<in> bexp")
- | andi ("b0 \\<in> bexp", "b1 \\<in> bexp") (infixl 60)
- | ori ("b0 \\<in> bexp", "b1 \\<in> bexp") (infixl 60)
+ | ROp ("f \<in> (nat*nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
+ | noti ("b \<in> bexp")
+ | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
+ | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl 60)
(** Evaluation of boolean expressions **)
-consts evalb :: i
- "-b->" :: [i,i] => o (infixl 50)
+consts evalb :: "i"
+ "-b->" :: "[i,i] => o" (infixl 50)
translations
- "p -b-> b" == "<p,b> \\<in> evalb"
+ "p -b-> b" == "<p,b> \<in> evalb"
inductive
domains "evalb" <= "(bexp * (loc -> nat)) * bool"
- intrs (*avoid clash with ML constructors true, false*)
- tru "[| sigma \\<in> loc -> nat |] ==> <true,sigma> -b-> 1"
- fls "[| sigma \\<in> loc -> nat |] ==> <false,sigma> -b-> 0"
- ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \\<in> (nat*nat)->bool |]
+ intros (*avoid clash with ML constructors true, false*)
+ tru: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
+ fls: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
+ ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |]
==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
- noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
- andi "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ noti: "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
+ andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
==> <b0 andi b1,sigma> -b-> (w0 and w1)"
- ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
+ ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |]
==> <b0 ori b1,sigma> -b-> (w0 or w1)"
-
- type_intrs "bexp.intrs @
- [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
- type_elims "[make_elim(evala.dom_subset RS subsetD)]"
+ type_intros bexp.intros
+ apply_funtype and_type or_type bool_1I bool_0I not_type
+ type_elims evala.dom_subset [THEN subsetD, elim_format]
(** Commands **)
@@ -80,50 +78,83 @@
datatype
"com" = skip
- | asgt ("x \\<in> loc", "a \\<in> aexp") (infixl 60)
- | semic ("c0 \\<in> com", "c1 \\<in> com") ("_; _" [60, 60] 10)
- | while ("b \\<in> bexp", "c \\<in> com") ("while _ do _" 60)
- | ifc ("b \\<in> bexp", "c0 \\<in> com", "c1 \\<in> com") ("ifc _ then _ else _" 60)
+ | asgt ("x \<in> loc", "a \<in> aexp") (infixl 60)
+ | semic("c0 \<in> com", "c1 \<in> com") ("_; _" [60, 60] 10)
+ | while("b \<in> bexp", "c \<in> com") ("while _ do _" 60)
+ | ifc ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("ifc _ then _ else _" 60)
(*Constructor ";" has low precedence to avoid syntactic ambiguities
- with [| m \\<in> nat; x \\<in> loc; ... |] ==> ... It usually will need parentheses.*)
+ with [| m \<in> nat; x \<in> loc; ... |] ==> ... It usually will need parentheses.*)
(** Execution of commands **)
-consts evalc :: i
- "-c->" :: [i,i] => o (infixl 50)
+consts evalc :: "i"
+ "-c->" :: "[i,i] => o" (infixl 50)
translations
- "p -c-> s" == "<p,s> \\<in> evalc"
-
+ "p -c-> s" == "<p,s> \<in> evalc"
inductive
domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
- intrs
- skip "[| sigma \\<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
+ intros
+ skip: "[| sigma \<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
+
+ assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |]
+ ==> <x asgt a,sigma> -c-> sigma(x:=m)"
- assign "[| m \\<in> nat; x \\<in> loc; <a,sigma> -a-> m |] ==>
- <x asgt a,sigma> -c-> sigma(x:=m)"
+ semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |]
+ ==> <c0 ; c1, sigma> -c-> sigma1"
+
+ ifc1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;
+ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |]
+ ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
- semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==>
- <c0 ; c1, sigma> -c-> sigma1"
+ ifc0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;
+ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |]
+ ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
+
+ while0: "[| c \<in> com; <b, sigma> -b-> 0 |]
+ ==> <while b do c,sigma> -c-> sigma"
- ifc1 "[| b \\<in> bexp; c1 \\<in> com; sigma \\<in> loc->nat;
- <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==>
- <ifc b then c0 else c1, sigma> -c-> sigma1"
+ while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
+ <while b do c, sigma2> -c-> sigma1 |]
+ ==> <while b do c, sigma> -c-> sigma1"
+
+ type_intros com.intros update_type
+ type_elims evala.dom_subset [THEN subsetD, elim_format]
+ evalb.dom_subset [THEN subsetD, elim_format]
+
+
+(*** type_intros for evala ***)
- ifc0 "[| b \\<in> bexp; c0 \\<in> com; sigma \\<in> loc->nat;
- <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==>
- <ifc b then c0 else c1, sigma> -c-> sigma1"
+lemmas evala_1 [simp] =
+ evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evala_2 [simp] =
+ evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evala_3 [simp] =
+ evala.dom_subset [THEN subsetD, THEN SigmaD2]
- while0 "[| c \\<in> com; <b, sigma> -b-> 0 |] ==>
- <while b do c,sigma> -c-> sigma "
+
+(*** type_intros for evalb ***)
- while1 "[| c \\<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2;
- <while b do c, sigma2> -c-> sigma1 |] ==>
- <while b do c, sigma> -c-> sigma1 "
+lemmas evalb_1 [simp] =
+ evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evalb_2 [simp] =
+ evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evalb_3 [simp] =
+ evalb.dom_subset [THEN subsetD, THEN SigmaD2]
+
+(*** type_intros for evalc ***)
- type_intrs "com.intrs @ [update_type]"
- type_elims "[make_elim(evala.dom_subset RS subsetD),
- make_elim(evalb.dom_subset RS subsetD) ]"
+lemmas evalc_1 [simp] =
+ evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evalc_2 [simp] =
+ evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evalc_3 [simp] =
+ evalc.dom_subset [THEN subsetD, THEN SigmaD2]
+
+inductive_cases evala_N_E [elim!]: "<N(n),sigma> -a-> i"
+inductive_cases evala_X_E [elim!]: "<X(x),sigma> -a-> i"
+inductive_cases evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
+inductive_cases evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i"
end
--- a/src/ZF/IMP/Denotation.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: ZF/IMP/Denotation.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
-*)
-
-(** Rewrite Rules for A,B,C **)
-Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
-Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def];
-Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def];
-
-(** Type_intr for A **)
-
-Goal "[|a \\<in> aexp; sigma \\<in> loc->nat|] ==> A(a,sigma):nat";
-by (etac aexp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addSIs [apply_type])));
-qed "A_type";
-
-(** Type_intr for B **)
-
-Goal "[|b \\<in> bexp; sigma \\<in> loc->nat|] ==> B(b,sigma):bool";
-by (etac bexp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addSIs [apply_type,A_type]@bool_typechecks)));
-qed "B_type";
-
-(** C_subset **)
-
-Goal "c \\<in> com ==> C(c) \\<subseteq> (loc->nat)*(loc->nat)";
-by (etac com.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])));
-qed "C_subset";
-
-(** Type_elims for C **)
-
-Goal "[| <x,y>:C(c); c \\<in> com |] ==> x \\<in> loc->nat & y \\<in> loc->nat";
-by (blast_tac (claset() addDs [C_subset RS subsetD]) 1);
-qed "C_type_D";
-
-Goal "[| x \\<in> C(c); c \\<in> com |] ==> fst(x):loc->nat";
-by (dtac (C_subset RS subsetD) 1);
-by (atac 1);
-by (etac SigmaE 1);
-by (Asm_simp_tac 1);
-qed "C_type_fst";
-
-AddDs [C_type_D, C_type_fst];
-
-(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
-
-Goalw [bnd_mono_def,Gamma_def]
- "c \\<in> com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))";
-by (Blast_tac 1);
-qed "Gamma_bnd_mono";
-
-(** End ***)
--- a/src/ZF/IMP/Denotation.thy Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Denotation.thy Fri Dec 28 10:11:14 2001 +0100
@@ -6,41 +6,82 @@
Denotational semantics of expressions & commands
*)
-Denotation = Com +
+theory Denotation = Com:
+
consts
- A :: i => i => i
- B :: i => i => i
- C :: i => i
- Gamma :: [i,i,i] => i
+ A :: "i => i => i"
+ B :: "i => i => i"
+ C :: "i => i"
+
+constdefs
+ Gamma :: "[i,i,i] => i"
+ "Gamma(b,cden) == (%phi.{io \<in> (phi O cden). B(b,fst(io))=1} Un
+ {io \<in> id(loc->nat). B(b,fst(io))=0})"
-rules (*NOT definitional*)
- A_nat_def "A(N(n)) == (%sigma. n)"
- A_loc_def "A(X(x)) == (%sigma. sigma`x)"
- A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
- A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+primrec
+ "A(N(n), sigma) = n"
+ "A(X(x), sigma) = sigma`x"
+ "A(Op1(f,a), sigma) = f`A(a,sigma)"
+ "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
+
+
+primrec
+ "B(true, sigma) = 1"
+ "B(false, sigma) = 0"
+ "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
+ "B(noti(b), sigma) = not(B(b,sigma))"
+ "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
+ "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
- B_true_def "B(true) == (%sigma. 1)"
- B_false_def "B(false) == (%sigma. 0)"
- B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+primrec
+ "C(skip) = id(loc->nat)"
+
+ "C(x asgt a) = {io:(loc->nat)*(loc->nat).
+ snd(io) = fst(io)(x := A(a,fst(io)))}"
+
+ "C(c0 ; c1) = C(c1) O C(c0)"
+
+ "C(ifc b then c0 else c1) = {io \<in> C(c0). B(b,fst(io))=1} Un
+ {io \<in> C(c1). B(b,fst(io))=0}"
+
+ "C(while b do c) = lfp((loc->nat)*(loc->nat), Gamma(b,C(c)))"
+
+
+(** Type_intr for A **)
+
+lemma A_type [TC]: "[|a \<in> aexp; sigma \<in> loc->nat|] ==> A(a,sigma) \<in> nat"
+by (erule aexp.induct, simp_all)
- B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))"
- B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
- B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+(** Type_intr for B **)
+
+lemma B_type [TC]: "[|b \<in> bexp; sigma \<in> loc->nat|] ==> B(b,sigma) \<in> bool"
+by (erule bexp.induct, simp_all)
- C_skip_def "C(skip) == id(loc->nat)"
- C_assign_def "C(x asgt a) == {io:(loc->nat)*(loc->nat).
- snd(io) = fst(io)(x := A(a,fst(io)))}"
+(** C_subset **)
+
+lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat)*(loc->nat)"
+apply (erule com.induct)
+apply simp_all
+apply (blast dest: lfp_subset [THEN subsetD])+
+done
- C_comp_def "C(c0 ; c1) == C(c1) O C(c0)"
- C_if_def "C(ifc b then c0 else c1) == {io \\<in> C(c0). B(b,fst(io))=1} Un
- {io \\<in> C(c1). B(b,fst(io))=0}"
+(** Type_elims for C **)
+
+lemma C_type_D [dest]:
+ "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
+by (blast dest: C_subset [THEN subsetD])
- Gamma_def "Gamma(b,c) == (%phi.{io \\<in> (phi O C(c)). B(b,fst(io))=1} Un
- {io \\<in> id(loc->nat). B(b,fst(io))=0})"
+lemma C_type_fst [dest]: "[| x \<in> C(c); c \<in> com |] ==> fst(x) \<in> loc->nat"
+by (auto dest!: C_subset [THEN subsetD])
+
+(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
- C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
+lemma Gamma_bnd_mono:
+ "cden <= (loc->nat)*(loc->nat)
+ ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,cden))"
+by (unfold bnd_mono_def Gamma_def, blast)
end
--- a/src/ZF/IMP/Equiv.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(* Title: ZF/IMP/Equiv.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
-*)
-
-Goal "[| a \\<in> aexp; sigma: loc -> nat |] ==> \
-\ <a,sigma> -a-> n <-> A(a,sigma) = n";
-by (res_inst_tac [("x","n")] spec 1); (* quantify n *)
-by (etac aexp.induct 1);
-by (ALLGOALS (fast_tac (claset() addSIs evala.intrs
- addSEs aexp_elim_cases
- addss (simpset()))));
-qed "aexp_iff";
-
-
-val aexp1 = aexp_iff RS iffD1;
-val aexp2 = aexp_iff RS iffD2;
-
-
-val bexp_elim_cases =
- [
- evalb.mk_cases "<true,sigma> -b-> x",
- evalb.mk_cases "<false,sigma> -b-> x",
- evalb.mk_cases "<ROp(f,a0,a1),sigma> -b-> x",
- evalb.mk_cases "<noti(b),sigma> -b-> x",
- evalb.mk_cases "<b0 andi b1,sigma> -b-> x",
- evalb.mk_cases "<b0 ori b1,sigma> -b-> x"
- ];
-
-
-Goal "[| b \\<in> bexp; sigma: loc -> nat |] ==> \
-\ <b,sigma> -b-> w <-> B(b,sigma) = w";
-by (res_inst_tac [("x","w")] spec 1);
-by (etac bexp.induct 1);
-by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs
- addSEs bexp_elim_cases
- addss (simpset() addsimps [aexp_iff]))));
-qed "bexp_iff";
-
-val bexp1 = bexp_iff RS iffD1;
-val bexp2 = bexp_iff RS iffD2;
-
-
-Goal "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \\<in> C(c)";
-by (etac evalc.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
-(* skip *)
-by (Fast_tac 1);
-(* assign *)
-by (asm_full_simp_tac (simpset() addsimps
- [aexp1, update_type] @ op_type_intrs) 1);
-(* comp *)
-by (Fast_tac 1);
-(* while *)
-by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
-by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
-(* recursive case of while *)
-by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
-by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
-by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
-val com1 = result();
-
-
-AddSIs [aexp2,bexp2,B_type,A_type];
-AddIs evalc.intrs;
-
-
-Goal "c \\<in> com ==> \\<forall>x \\<in> C(c). <c,fst(x)> -c-> snd(x)";
-by (etac com.induct 1);
-(* comp *)
-by (Force_tac 3);
-(* assign *)
-by (Force_tac 2);
-(* skip *)
-by (Force_tac 1);
-(* while *)
-by Safe_tac;
-by (ALLGOALS Asm_full_simp_tac);
-by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]);
-by (rewtac Gamma_def);
-by Safe_tac;
-by (EVERY1 [dtac bspec, atac]);
-by (ALLGOALS Asm_full_simp_tac);
-(* while, if *)
-by (ALLGOALS Blast_tac);
-val com2 = result();
-
-
-(**** Proof of Equivalence ****)
-
-Goal "\\<forall>c \\<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
-by (fast_tac (claset() addIs [C_subset RS subsetD]
- addEs [com2 RS bspec]
- addDs [com1]
- addss (simpset())) 1);
-val com_equivalence = result();
--- a/src/ZF/IMP/Equiv.thy Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Equiv.thy Fri Dec 28 10:11:14 2001 +0100
@@ -4,4 +4,84 @@
Copyright 1994 TUM
*)
-Equiv = Denotation + Com
+theory Equiv = Denotation + Com:
+
+lemma aexp_iff [rule_format]:
+ "[| a \<in> aexp; sigma: loc -> nat |]
+ ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
+apply (erule aexp.induct)
+apply (force intro!: evala.intros)+
+done
+
+declare aexp_iff [THEN iffD1, simp]
+ aexp_iff [THEN iffD2, intro!]
+
+inductive_cases [elim!]: "<true,sigma> -b-> x"
+inductive_cases [elim!]: "<false,sigma> -b-> x"
+inductive_cases [elim!]: "<ROp(f,a0,a1),sigma> -b-> x"
+inductive_cases [elim!]: "<noti(b),sigma> -b-> x"
+inductive_cases [elim!]: "<b0 andi b1,sigma> -b-> x"
+inductive_cases [elim!]: "<b0 ori b1,sigma> -b-> x"
+
+
+lemma bexp_iff [rule_format]:
+ "[| b \<in> bexp; sigma: loc -> nat |]
+ ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
+apply (erule bexp.induct)
+apply (auto intro!: evalb.intros)
+done
+
+declare bexp_iff [THEN iffD1, simp]
+ bexp_iff [THEN iffD2, intro!]
+
+lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
+apply (erule evalc.induct)
+apply simp_all
+(* skip *)
+apply fast
+(* assign *)
+apply (simp add: update_type)
+(* comp *)
+apply fast
+(* while *)
+apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+apply (simp add: Gamma_def)
+apply (force )
+(* recursive case of while *)
+apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+apply (simp add: Gamma_def)
+apply auto
+done
+
+
+declare B_type [intro!] A_type [intro!]
+declare evalc.intros [intro]
+
+
+lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
+apply (erule com.induct)
+(* skip *)
+apply force
+(* assign *)
+apply force
+(* comp *)
+apply force
+(* while *)
+apply safe
+apply simp_all
+apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
+apply (unfold Gamma_def)
+apply force
+(* if *)
+apply auto
+done
+
+
+(**** Proof of Equivalence ****)
+
+lemma com_equivalence:
+ "\<forall>c \<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"
+by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
+
+end
+
--- a/src/ZF/IsaMakefile Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IsaMakefile Fri Dec 28 10:11:14 2001 +0100
@@ -74,7 +74,7 @@
ZF-Coind: ZF $(LOG)/ZF-Coind.gz
-$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
+$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy \
Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
Coind/Static.thy Coind/Types.thy Coind/Values.thy
@$(ISATOOL) usedir $(OUT)/ZF Coind
@@ -84,8 +84,8 @@
ZF-IMP: ZF $(LOG)/ZF-IMP.gz
-$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
- IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
+$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy \
+ IMP/Denotation.thy IMP/Equiv.thy IMP/ROOT.ML
@$(ISATOOL) usedir $(OUT)/ZF IMP
@@ -131,9 +131,9 @@
ZF-ex: ZF $(LOG)/ZF-ex.gz
$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
- ex/BinEx.thy ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
- ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy ex/Primes.ML ex/Primes.thy \
- ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
+ ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy \
+ ex/Limit.ML ex/Limit.thy ex/LList.thy ex/Primes.thy \
+ ex/NatSum.thy ex/Ramsey.thy ex/misc.thy
@$(ISATOOL) usedir $(OUT)/ZF ex
--- a/src/ZF/ex/Commutation.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(* Title: HOL/Lambda/Commutation.thy
- ID: $Id$
- Author: Tobias Nipkow & Sidi Ould Ehmety
- Copyright 1995 TU Muenchen
-
-Commutation theory for proving the Church Rosser theorem
- ported from Isabelle/HOL by Sidi Ould Ehmety
-*)
-
-Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
-by (Blast_tac 1);
-qed "square_sym";
-
-
-Goalw [square_def] "[| square(r,s,t,u); t \\<subseteq> t' |] ==> square(r,s,t',u)";
-by (Blast_tac 1);
-qed "square_subset";
-
-
-Goalw [square_def]
- "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
-by (Clarify_tac 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-qed_spec_mp "square_rtrancl";
-
-(* A special case of square_rtrancl_on *)
-Goalw [diamond_def, commute_def, strip_def]
- "diamond(r) ==> strip(r)";
-by (rtac square_rtrancl 1);
-by (ALLGOALS(Asm_simp_tac));
-qed "diamond_strip";
-
-(*** commute ***)
-
-Goalw [commute_def]
- "commute(r,s) ==> commute(s,r)";
-by (blast_tac (claset() addIs [square_sym]) 1);
-qed "commute_sym";
-
-Goalw [commute_def]
-"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
-by (Clarify_tac 1);
-by (rtac square_rtrancl 1);
-by (rtac square_sym 2);
-by (rtac square_rtrancl 2);
-by (rtac square_sym 3);
-by (ALLGOALS(asm_simp_tac
- (simpset() addsimps [rtrancl_field])));
-qed_spec_mp "commute_rtrancl";
-
-
-Goalw [strip_def,confluent_def, diamond_def]
-"strip(r) ==> confluent(r)";
-by (dtac commute_rtrancl 1);
-by (ALLGOALS(asm_full_simp_tac (simpset()
- addsimps [rtrancl_field])));
-qed "strip_confluent";
-
-
-Goalw [commute_def,square_def]
- "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
-by (Blast_tac 1);
-qed "commute_Un";
-
-
-Goalw [diamond_def]
- "[| diamond(r); diamond(s); commute(r, s) |] \
-\ ==> diamond(r Un s)";
-by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
-qed "diamond_Un";
-
-
-Goalw [diamond_def,confluent_def]
- "diamond(r) ==> confluent(r)";
-by (etac commute_rtrancl 1);
-by (Simp_tac 1);
-qed "diamond_confluent";
-
-
-Goalw [confluent_def]
- "[| confluent(r); confluent(s); commute(r^*, s^*); \
-\ r \\<subseteq> Sigma(A,B); s \\<subseteq> Sigma(C,D) |] ==> confluent(r Un s)";
-by (rtac (rtrancl_Un_rtrancl RS subst) 1);
-by (blast_tac (claset() addDs [diamond_Un]
- addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
-by Auto_tac;
-qed "confluent_Un";
-
-
-Goal
- "[| diamond(r); s \\<subseteq> r; r<= s^* |] ==> confluent(s)";
-by (dresolve_tac [rtrancl_subset RS sym] 1);
-by (assume_tac 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
-by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
-by (Asm_simp_tac 1);
-qed "diamond_to_confluence";
-
-(*** Church_Rosser ***)
-
-Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
- "Church_Rosser(r) ==> confluent(r)";
-by Auto_tac;
-by (dtac converseI 1);
-by (full_simp_tac (simpset()
- addsimps [rtrancl_converse RS sym]) 1);
-by (dres_inst_tac [("x", "b")] spec 1);
-by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
-by (res_inst_tac [("b", "a")] rtrancl_trans 1);
-by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
-qed "Church_Rosser1";
-
-
-Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
-"confluent(r) ==> Church_Rosser(r)";
-by Auto_tac;
-by (ftac fieldI1 1);
-by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
-by (etac rtrancl_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (blast_tac (claset() addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() delrules [rtrancl_refl]
- addIs [r_into_rtrancl, rtrancl_trans]) 1);
-qed "Church_Rosser2";
-
-
-Goal "Church_Rosser(r) <-> confluent(r)";
-by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
-qed "Church_Rosser";
\ No newline at end of file
--- a/src/ZF/ex/LList.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(* Title: ZF/ex/LList.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Codatatype definition of Lazy Lists
-*)
-
-(*These commands cause classical reasoning to regard the subset relation
- as primitive, not reducing it to membership*)
-
-Delrules [subsetI, subsetCE];
-AddSIs [subset_refl, cons_subsetI, subset_consI,
- Union_least, UN_least, Un_least,
- Inter_greatest, Int_greatest, RepFun_subset,
- Un_upper1, Un_upper2, Int_lower1, Int_lower2];
-
-(*An elimination rule, for type-checking*)
-val LConsE = llist.mk_cases "LCons(a,l) \\<in> llist(A)";
-
-(*Proving freeness results*)
-val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
-val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
-
-Goal "llist(A) = {0} <+> (A <*> llist(A))";
-let open llist val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
-end;
-qed "llist_unfold";
-
-(*** Lemmas to justify using "llist" in other recursive type definitions ***)
-
-Goalw llist.defs "A \\<subseteq> B ==> llist(A) \\<subseteq> llist(B)";
-by (rtac gfp_mono 1);
-by (REPEAT (rtac llist.bnd_mono 1));
-by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
-qed "llist_mono";
-
-(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **)
-
-AddSIs [QPair_Int_Vset_subset_UN RS subset_trans,
- QPair_subset_univ,
- empty_subsetI, one_in_quniv RS qunivD];
-AddSDs [qunivD];
-AddSEs [Ord_in_Ord];
-
-Goal "Ord(i) ==> \\<forall>l \\<in> llist(quniv(A)). l Int Vset(i) \\<subseteq> univ(eclose(A))";
-by (etac trans_induct 1);
-by (rtac ballI 1);
-by (etac llist.elim 1);
-by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
-(*LNil case*)
-by (Asm_simp_tac 1);
-(*LCons case*)
-by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
-qed "llist_quniv_lemma";
-
-Goal "llist(quniv(A)) \\<subseteq> quniv(A)";
-by (rtac (qunivI RS subsetI) 1);
-by (rtac Int_Vset_subset 1);
-by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
-qed "llist_quniv";
-
-bind_thm ("llist_subset_quniv",
- (llist_mono RS (llist_quniv RSN (2,subset_trans))));
-
-
-(*** Lazy List Equality: lleq ***)
-
-AddSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono];
-AddSEs [Ord_in_Ord, Pair_inject];
-
-(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
-Goal "Ord(i) ==> \\<forall>l l'. <l,l'> \\<in> lleq(A) --> l Int Vset(i) \\<subseteq> l'";
-by (etac trans_induct 1);
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (etac lleq.elim 1);
-by (rewrite_goals_tac (QInr_def::llist.con_defs));
-by Safe_tac;
-by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
-qed "lleq_Int_Vset_subset_lemma";
-
-bind_thm ("lleq_Int_Vset_subset",
- (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
-
-
-(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList.thy "<l,l'> \\<in> lleq(A) ==> <l',l> \\<in> lleq(A)";
-by (rtac (prem RS converseI RS lleq.coinduct) 1);
-by (rtac (lleq.dom_subset RS converse_type) 1);
-by Safe_tac;
-by (etac lleq.elim 1);
-by (ALLGOALS Fast_tac);
-qed "lleq_symmetric";
-
-Goal "<l,l'> \\<in> lleq(A) ==> l=l'";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
- ORELSE etac lleq_symmetric 1));
-qed "lleq_implies_equal";
-
-val [eqprem,lprem] = goal LList.thy
- "[| l=l'; l \\<in> llist(A) |] ==> <l,l'> \\<in> lleq(A)";
-by (res_inst_tac [("X", "{<l,l>. l \\<in> llist(A)}")] lleq.coinduct 1);
-by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Fast_tac);
-qed "equal_llist_implies_leq";
-
-
-(*** Lazy List Functions ***)
-
-(*Examples of coinduction for type-checking and to prove llist equations*)
-
-(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
-
-Goalw llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
-by (REPEAT (ares_tac [subset_refl, A_subset_univ,
- QInr_subset_univ, QPair_subset_univ] 1));
-qed "lconst_fun_bnd_mono";
-
-(* lconst(a) = LCons(a,lconst(a)) *)
-bind_thm ("lconst",
- ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_unfold));
-
-val lconst_subset = lconst_def RS def_lfp_subset;
-
-bind_thm ("member_subset_Union_eclose", (arg_into_eclose RS Union_upper));
-
-Goal "a \\<in> A ==> lconst(a) \\<in> quniv(A)";
-by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
-by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
-qed "lconst_in_quniv";
-
-Goal "a \\<in> A ==> lconst(a): llist(A)";
-by (rtac (singletonI RS llist.coinduct) 1);
-by (etac (lconst_in_quniv RS singleton_subsetI) 1);
-by (fast_tac (claset() addSIs [lconst]) 1);
-qed "lconst_type";
-
-(*** flip --- equations merely assumed; certain consequences proved ***)
-
-Addsimps [flip_LNil, flip_LCons, not_type];
-
-goal QUniv.thy "!!b. b \\<in> bool ==> b Int X \\<subseteq> univ(eclose(A))";
-by (fast_tac (claset() addIs [Int_lower1 RS subset_trans] addSEs [boolE]) 1);
-qed "bool_Int_subset_univ";
-
-AddSIs [not_type];
-AddIs [bool_Int_subset_univ];
-
-(*Reasoning borrowed from lleq.ML; a similar proof works for all
- "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-Goal "Ord(i) ==> \\<forall>l \\<in> llist(bool). flip(l) Int Vset(i) \\<subseteq> \
-\ univ(eclose(bool))";
-by (etac trans_induct 1);
-by (rtac ballI 1);
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [QInl_def,QInr_def] @ llist.con_defs)));
-(*LCons case*)
-by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
-qed "flip_llist_quniv_lemma";
-
-Goal "l \\<in> llist(bool) ==> flip(l) \\<in> quniv(bool)";
-by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
-by (REPEAT (assume_tac 1));
-qed "flip_in_quniv";
-
-val [prem] = goal LList.thy "l \\<in> llist(bool) ==> flip(l): llist(bool)";
-by (res_inst_tac [("X", "{flip(l) . l \\<in> llist(bool)}")]
- llist.coinduct 1);
-by (rtac (prem RS RepFunI) 1);
-by (fast_tac (claset() addSIs [flip_in_quniv]) 1);
-by (etac RepFunE 1);
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "flip_type";
-
-val [prem] = goal LList.thy
- "l \\<in> llist(bool) ==> flip(flip(l)) = l";
-by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l \\<in> llist(bool)}")]
- (lleq.coinduct RS lleq_implies_equal) 1);
-by (rtac (prem RS RepFunI) 1);
-by (fast_tac (claset() addSIs [flip_type]) 1);
-by (etac RepFunE 1);
-by (etac llist.elim 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [flip_type, not_not]) 1);
-qed "flip_flip";
--- a/src/ZF/ex/NatSum.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* Title: HOL/ex/NatSum.ML
- ID: $Id$
- Author: Tobias Nipkow & Lawrence C Paulson
-
-Summing natural numbers, squares, cubes, etc.
-
-Originally demonstrated permutative rewriting, but add_ac is no longer needed
- thanks to new simprocs.
-
-Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
- http://www.research.att.com/~njas/sequences/
-*)
-
-Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2];
-Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
-
-(*The sum of the first n odd numbers equals n squared.*)
-Goal "n \\<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_odds";
-
-(*The sum of the first n odd squares*)
-Goal "n \\<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
-\ $#n $* (#4 $* $#n $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_odd_squares";
-
-(*The sum of the first n odd cubes*)
-Goal "n \\<in> nat \
-\ ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
-\ $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_odd_cubes";
-
-(*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "n \\<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_naturals";
-
-Goal "n \\<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
-\ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_squares";
-
-Goal "n \\<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
-\ $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_cubes";
-
-(** Sum of fourth powers **)
-
-Goal "n \\<in> nat ==> \
-\ #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
-\ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
-\ (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_fourth_powers";
--- a/src/ZF/ex/Primes.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,435 +0,0 @@
-(* Title: ZF/ex/Primes.ML
- ID: $Id$
- Author: Christophe Tabacznyj and Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-The "divides" relation, the greatest common divisor and Euclid's algorithm
-*)
-
-(************************************************)
-(** Divides Relation **)
-(************************************************)
-
-Goalw [dvd_def] "m dvd n ==> m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)";
-by (assume_tac 1);
-qed "dvdD";
-
-Goal "!!P. [|m dvd n; !!k. [|m \\<in> nat; n \\<in> nat; k \\<in> nat; n = m#*k|] ==> P|] \
-\ ==> P";
-by (blast_tac (claset() addSDs [dvdD]) 1);
-qed "dvdE";
-
-bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
-bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
-
-
-Goalw [dvd_def] "m \\<in> nat ==> m dvd 0";
-by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
-qed "dvd_0_right";
-Addsimps [dvd_0_right];
-
-Goalw [dvd_def] "0 dvd m ==> m = 0";
-by (fast_tac (claset() addss (simpset())) 1);
-qed "dvd_0_left";
-
-Goalw [dvd_def] "m \\<in> nat ==> m dvd m";
-by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
-qed "dvd_refl";
-Addsimps [dvd_refl];
-
-Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
-by (fast_tac (claset() addIs [mult_assoc, mult_type] ) 1);
-qed "dvd_trans";
-
-Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
-by (fast_tac (claset() addDs [mult_eq_self_implies_10]
- addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
-qed "dvd_anti_sym";
-
-Goalw [dvd_def] "[|(i#*j) dvd k; i \\<in> nat|] ==> i dvd k";
-by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
-by (Blast_tac 1);
-qed "dvd_mult_left";
-
-Goalw [dvd_def] "[|(i#*j) dvd k; j \\<in> nat|] ==> j dvd k";
-by (Clarify_tac 1);
-by (res_inst_tac [("x","i#*k")] bexI 1);
-by (simp_tac (simpset() addsimps mult_ac) 1);
-by (rtac mult_type 1);
-qed "dvd_mult_right";
-
-
-(************************************************)
-(** Greatest Common Divisor **)
-(************************************************)
-
-(* GCD by Euclid's Algorithm *)
-
-Goalw [gcd_def] "gcd(m,0) = natify(m)";
-by (stac transrec 1);
-by (Asm_simp_tac 1);
-qed "gcd_0";
-Addsimps [gcd_0];
-
-Goal "gcd(natify(m),n) = gcd(m,n)";
-by (simp_tac (simpset() addsimps [gcd_def]) 1);
-qed "gcd_natify1";
-
-Goal "gcd(m, natify(n)) = gcd(m,n)";
-by (simp_tac (simpset() addsimps [gcd_def]) 1);
-qed "gcd_natify2";
-Addsimps [gcd_natify1,gcd_natify2];
-
-Goalw [gcd_def]
- "[| 0<n; n \\<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)";
-by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
- mod_less_divisor RS ltD]) 1);
-qed "gcd_non_0_raw";
-
-Goal "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)";
-by (cut_inst_tac [("m","m"),("n","natify(n)")] gcd_non_0_raw 1);
-by Auto_tac;
-qed "gcd_non_0";
-
-Goal "gcd(m,1) = 1";
-by (asm_simp_tac (simpset() addsimps [gcd_non_0]) 1);
-qed "gcd_1";
-Addsimps [gcd_1];
-
-Goalw [dvd_def] "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
-by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
-qed "dvd_add";
-
-Goalw [dvd_def] "k dvd n ==> k dvd (m #* n)";
-by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
-qed "dvd_mult";
-
-Goal "k dvd m ==> k dvd (m #* n)";
-by (stac mult_commute 1);
-by (blast_tac (claset() addIs [dvd_mult]) 1);
-qed "dvd_mult2";
-
-(* k dvd (m*k) *)
-bind_thm ("dvdI1", dvd_refl RS dvd_mult);
-bind_thm ("dvdI2", dvd_refl RS dvd_mult2);
-Addsimps [dvdI1, dvdI2];
-
-Goal "[| a \\<in> nat; b \\<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a";
-by (div_undefined_case_tac "b=0" 1);
-by (blast_tac
- (claset() addIs [mod_div_equality RS subst]
- addEs [dvdE]
- addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 1);
-qed "dvd_mod_imp_dvd_raw";
-
-Goal "[| k dvd (a mod b); k dvd b; a \\<in> nat |] ==> k dvd a";
-by (cut_inst_tac [("b","natify(b)")] dvd_mod_imp_dvd_raw 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [dvd_def]) 1);
-qed "dvd_mod_imp_dvd";
-
-(*Imitating TFL*)
-Goal "[| n \\<in> nat; \
-\ \\<forall>m \\<in> nat. P(m,0); \
-\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |] \
-\ ==> \\<forall>m \\<in> nat. P (m,n)";
-by (eres_inst_tac [("i","n")] complete_induct 1);
-by (case_tac "x=0" 1);
-by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("x1","m"),("x","x")] (bspec RS bspec) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_0_lt_iff])));
-by (blast_tac (claset() addIs [mod_less_divisor RS ltD]) 1);
-qed_spec_mp "gcd_induct_lemma";
-
-Goal "!!P. [| m \\<in> nat; n \\<in> nat; \
-\ !!m. m \\<in> nat ==> P(m,0); \
-\ !!m n. [|m \\<in> nat; n \\<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] \
-\ ==> P (m,n)";
-by (blast_tac (claset() addIs [gcd_induct_lemma]) 1);
-qed "gcd_induct";
-
-
-(* gcd type *)
-
-Goal "gcd(m, n) \\<in> nat";
-by (subgoal_tac "gcd(natify(m), natify(n)) \\<in> nat" 1);
-by (Asm_full_simp_tac 1);
-by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_induct 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
-qed "gcd_type";
-Addsimps [gcd_type];
-
-(* Property 1: gcd(a,b) divides a and b *)
-
-Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
-by (blast_tac
- (claset() addIs [dvd_mod_imp_dvd_raw, nat_into_Ord RS Ord_0_lt]) 1);
-qed "gcd_dvd_both";
-
-Goal "m \\<in> nat ==> gcd(m,n) dvd m";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1);
-by Auto_tac;
-qed "gcd_dvd1";
-Addsimps [gcd_dvd1];
-
-Goal "n \\<in> nat ==> gcd(m,n) dvd n";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1);
-by Auto_tac;
-qed "gcd_dvd2";
-Addsimps [gcd_dvd2];
-
-(* if f divides a and b then f divides gcd(a,b) *)
-
-Goalw [dvd_def] "[| f dvd a; f dvd b |] ==> f dvd (a mod b)";
-by (div_undefined_case_tac "b=0" 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);
-qed "dvd_mod";
-
-(* Property 2: for all a,b,f naturals,
- if f divides a and f divides b then f divides gcd(a,b)*)
-
-Goal "[| m \\<in> nat; n \\<in> nat; f \\<in> nat |] \
-\ ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_non_0, dvd_mod])));
-qed_spec_mp "gcd_greatest_raw";
-
-Goal "[| f dvd m; f dvd n; f \\<in> nat |] ==> f dvd gcd(m,n)";
-by (rtac gcd_greatest_raw 1);
-by (auto_tac (claset(), simpset() addsimps [dvd_def]));
-qed "gcd_greatest";
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\ ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)";
-by (blast_tac (claset() addSIs [gcd_greatest, gcd_dvd1, gcd_dvd2]
- addIs [dvd_trans]) 1);
-qed "gcd_greatest_iff";
-Addsimps [gcd_greatest_iff];
-
-(* GCD PROOF: GCD exists and gcd fits the definition *)
-
-Goalw [is_gcd_def] "[| m \\<in> nat; n \\<in> nat |] ==> is_gcd(gcd(m,n), m, n)";
-by (Asm_simp_tac 1);
-qed "is_gcd";
-
-(* GCD is unique *)
-
-Goalw [is_gcd_def] "[|is_gcd(m,a,b); is_gcd(n,a,b); m\\<in>nat; n\\<in>nat|] ==> m=n";
-by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
-qed "is_gcd_unique";
-
-Goalw [is_gcd_def] "is_gcd(k,m,n) <-> is_gcd(k,n,m)";
-by (Blast_tac 1);
-qed "is_gcd_commute";
-
-Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd(m,n) = gcd(n,m)";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 1);
-by (rtac (is_gcd_commute RS iffD1) 3);
-by (rtac is_gcd 3);
-by Auto_tac;
-qed "gcd_commute_raw";
-
-Goal "gcd(m,n) = gcd(n,m)";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_commute_raw 1);
-by Auto_tac;
-qed "gcd_commute";
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\ ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 1);
-by (asm_full_simp_tac (simpset() addsimps [is_gcd_def]) 3);
-by (blast_tac (claset() addIs [gcd_dvd1, gcd_dvd2, gcd_type]
- addIs [dvd_trans]) 3);
-by Auto_tac;
-qed "gcd_assoc_raw";
-
-Goal "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
-by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")]
- gcd_assoc_raw 1);
-by Auto_tac;
-qed "gcd_assoc";
-
-Goal "gcd (0, m) = natify(m)";
-by (asm_simp_tac (simpset() addsimps [inst "m" "0" gcd_commute]) 1);
-qed "gcd_0_left";
-Addsimps [gcd_0_left];
-
-Goal "gcd (1, m) = 1";
-by (asm_simp_tac (simpset() addsimps [inst "m" "1" gcd_commute]) 1);
-qed "gcd_1_left";
-Addsimps [gcd_1_left];
-
-
-(* Multiplication laws *)
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\ ==> k #* gcd (m, n) = gcd (k #* m, k #* n)";
-by (eres_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (case_tac "k = 0" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, gcd_non_0,
- mod_mult_distrib2, Ord_0_lt_iff]) 1);
-qed "gcd_mult_distrib2_raw";
-
-Goal "k #* gcd (m, n) = gcd (k #* m, k #* n)";
-by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")]
- gcd_mult_distrib2_raw 1);
-by Auto_tac;
-qed "gcd_mult_distrib2";
-
-Goal "gcd (k, k #* n) = natify(k)";
-by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
-by Auto_tac;
-qed "gcd_mult";
-Addsimps [gcd_mult];
-
-Goal "gcd (k, k) = natify(k)";
-by (cut_inst_tac [("k","k"),("n","1")] gcd_mult 1);
-by Auto_tac;
-qed "gcd_self";
-Addsimps [gcd_self];
-
-Goal "[| gcd (k,n) = 1; k dvd (m #* n); m \\<in> nat |] \
-\ ==> k dvd m";
-by (cut_inst_tac [("k","m"),("m","k"),("n","n")] gcd_mult_distrib2 1);
-by Auto_tac;
-by (eres_inst_tac [("b","m")] ssubst 1);
-by (asm_full_simp_tac (simpset() addsimps [dvd_imp_nat1]) 1);
-qed "relprime_dvd_mult";
-
-Goal "[| gcd (k,n) = 1; m \\<in> nat |] \
-\ ==> k dvd (m #* n) <-> k dvd m";
-by (blast_tac (claset() addIs [dvdI2, relprime_dvd_mult, dvd_trans]) 1);
-qed "relprime_dvd_mult_iff";
-
-Goalw [prime_def]
- "[| p \\<in> prime; ~ (p dvd n); n \\<in> nat |] ==> gcd (p, n) = 1";
-by (Clarify_tac 1);
-by (dres_inst_tac [("x","gcd(p,n)")] bspec 1);
-by Auto_tac;
-by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd2 1);
-by Auto_tac;
-qed "prime_imp_relprime";
-
-Goalw [prime_def] "p \\<in> prime ==> p \\<in> nat";
-by Auto_tac;
-qed "prime_into_nat";
-
-Goalw [prime_def] "p \\<in> prime \\<Longrightarrow> p\\<noteq>0";
-by Auto_tac;
-qed "prime_nonzero";
-
-
-(*This theorem leads immediately to a proof of the uniqueness of
- factorization. If p divides a product of primes then it is
- one of those primes.*)
-
-Goal "[|p dvd m #* n; p \\<in> prime; m \\<in> nat; n \\<in> nat |] ==> p dvd m \\<or> p dvd n";
-by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime,
- prime_into_nat]) 1);
-qed "prime_dvd_mult";
-
-
-(** Addition laws **)
-
-Goal "gcd (m #+ n, n) = gcd (m, n)";
-by (subgoal_tac "gcd (m #+ natify(n), natify(n)) = gcd (m, natify(n))" 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "natify(n) = 0" 1);
-by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff, gcd_non_0]));
-qed "gcd_add1";
-Addsimps [gcd_add1];
-
-Goal "gcd (m, m #+ n) = gcd (m, n)";
-by (rtac (gcd_commute RS trans) 1);
-by (stac add_commute 1);
-by (Simp_tac 1);
-by (rtac gcd_commute 1);
-qed "gcd_add2";
-Addsimps [gcd_add2];
-
-Goal "gcd (m, n #+ m) = gcd (m, n)";
-by (stac add_commute 1);
-by (rtac gcd_add2 1);
-qed "gcd_add2'";
-Addsimps [gcd_add2'];
-
-Goal "k \\<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)";
-by (etac nat_induct 1);
-by (auto_tac (claset(), simpset() addsimps [gcd_add2, add_assoc]));
-qed "gcd_add_mult_raw";
-
-Goal "gcd (m, k #* m #+ n) = gcd (m, n)";
-by (cut_inst_tac [("k","natify(k)")] gcd_add_mult_raw 1);
-by Auto_tac;
-qed "gcd_add_mult";
-
-
-(* More multiplication laws *)
-
-Goal "[|gcd (k,n) = 1; m \\<in> nat; n \\<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)";
-by (rtac dvd_anti_sym 1);
- by (rtac gcd_greatest 1);
- by (rtac (inst "n" "k" relprime_dvd_mult) 1);
-by (asm_full_simp_tac (simpset() addsimps [gcd_assoc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [gcd_commute]) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
-by (blast_tac (claset() addIs [dvdI1, gcd_dvd1, dvd_trans]) 1);
-qed "gcd_mult_cancel_raw";
-
-
-Goal "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_mult_cancel_raw 1);
-by Auto_tac;
-qed "gcd_mult_cancel";
-
-
-(*** The square root of a prime is irrational: key lemma ***)
-
-Goal "\\<lbrakk>n#*n = p#*(k#*k); p \\<in> prime; n \\<in> nat\\<rbrakk> \\<Longrightarrow> p dvd n";
-by (subgoal_tac "p dvd n#*n" 1);
- by (blast_tac (claset() addDs [prime_dvd_mult]) 1);
-by (res_inst_tac [("j","k#*k")] dvd_mult_left 1);
- by (auto_tac (claset(), simpset() addsimps [prime_def]));
-qed "prime_dvd_other_side";
-
-Goal "\\<lbrakk>k#*k = p#*(j#*j); p \\<in> prime; 0 < k; j \\<in> nat; k \\<in> nat\\<rbrakk> \
-\ \\<Longrightarrow> k < p#*j & 0 < j";
-by (rtac ccontr 1);
-by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le, prime_into_nat]) 1);
-by (etac disjE 1);
- by (ftac mult_le_mono 1 THEN REPEAT (assume_tac 1));
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
-by (auto_tac (claset() addSDs [natify_eqE],
- simpset() addsimps [not_lt_iff_le, prime_into_nat,
- mult_le_cancel_le1]));
-by (asm_full_simp_tac (simpset() addsimps [prime_def]) 1);
-by (blast_tac (claset() addDs [lt_trans1]) 1);
-qed "reduction";
-
-
-Goal "j #* (p#*j) = k#*k \\<Longrightarrow> k#*k = p#*(j#*j)";
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
-qed "rearrange";
-
-Goal "\\<lbrakk>m \\<in> nat; p \\<in> prime\\<rbrakk> \\<Longrightarrow> \\<forall>k \\<in> nat. 0<k \\<longrightarrow> m#*m \\<noteq> p#*(k#*k)";
-by (etac complete_induct 1);
-by (Clarify_tac 1);
-by (ftac prime_dvd_other_side 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (etac dvdE 1);
-by (asm_full_simp_tac (simpset() addsimps [mult_assoc, mult_cancel1,
- prime_nonzero, prime_into_nat]) 1);
-by (blast_tac (claset() addDs [rearrange, reduction, ltD]) 1);
-qed "prime_not_square";
--- a/src/ZF/ex/Ramsey.ML Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-(* Title: ZF/ex/ramsey.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Ramsey's Theorem (finite exponent 2 version)
-
-Based upon the article
- D Basin and M Kaufmann,
- The Boyer-Moore Prover and Nuprl: An Experimental Comparison.
- In G Huet and G Plotkin, editors, Logical Frameworks.
- (CUP, 1991), pages 89--119
-
-See also
- M Kaufmann,
- An example in NQTHM: Ramsey's Theorem
- Internal Note, Computational Logic, Inc., Austin, Texas 78703
- Available from the author: kaufmann@cli.com
-*)
-
-(*** Cliques and Independent sets ***)
-
-Goalw [Clique_def] "Clique(0,V,E)";
-by (Fast_tac 1);
-qed "Clique0";
-
-Goalw [Clique_def] "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
-by (Fast_tac 1);
-qed "Clique_superset";
-
-Goalw [Indept_def] "Indept(0,V,E)";
-by (Fast_tac 1);
-qed "Indept0";
-
-Goalw [Indept_def] "[| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)";
-by (Fast_tac 1);
-qed "Indept_superset";
-
-(*** Atleast ***)
-
-Goalw [Atleast_def, inj_def, Pi_def, function_def] "Atleast(0,A)";
-by (Fast_tac 1);
-qed "Atleast0";
-
-Goalw [Atleast_def]
- "Atleast(succ(m),A) ==> \\<exists>x \\<in> A. Atleast(m, A-{x})";
-by (fast_tac (claset() addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
-qed "Atleast_succD";
-
-Goalw [Atleast_def]
- "[| Atleast(n,A); A \\<subseteq> B |] ==> Atleast(n,B)";
-by (fast_tac (claset() addEs [inj_weaken_type]) 1);
-qed "Atleast_superset";
-
-Goalw [Atleast_def,succ_def]
- "[| Atleast(m,B); b\\<notin> B |] ==> Atleast(succ(m), cons(b,B))";
-by (etac exE 1);
-by (rtac exI 1);
-by (etac inj_extend 1);
-by (rtac mem_not_refl 1);
-by (assume_tac 1);
-qed "Atleast_succI";
-
-Goal "[| Atleast(m, B-{x}); x \\<in> B |] ==> Atleast(succ(m), B)";
-by (etac (Atleast_succI RS Atleast_superset) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
-qed "Atleast_Diff_succI";
-
-(*** Main Cardinality Lemma ***)
-
-(*The #-succ(0) strengthens the original theorem statement, but precisely
- the same proof could be used!!*)
-Goal "m \\<in> nat ==> \
-\ \\<forall>n \\<in> nat. \\<forall>A B. Atleast((m#+n) #- succ(0), A Un B) --> \
-\ Atleast(m,A) | Atleast(n,B)";
-by (induct_tac "m" 1);
-by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (Asm_simp_tac 1);
-by (rtac ballI 1);
-by (rename_tac "m' n" 1); (*simplifier does NOT preserve bound names!*)
-by (induct_tac "n" 1);
-by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (Asm_simp_tac 1);
-by Safe_tac;
-by (etac (Atleast_succD RS bexE) 1);
-by (rename_tac "n' A B z" 1);
-by (etac UnE 1);
-(**case z \\<in> B. Instantiate the '\\<forall>A B' induction hypothesis. **)
-by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
-by (etac (mp RS disjE) 2);
-(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
-by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
-(*proving the condition*)
-by (etac Atleast_superset 2 THEN Fast_tac 2);
-(**case z \\<in> A. Instantiate the '\\<forall>n \\<in> nat. \\<forall>A B' induction hypothesis. **)
-by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")]
- (bspec RS spec RS spec) 1);
-by (etac nat_succI 1);
-by (etac (mp RS disjE) 1);
-(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
-by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
-(*proving the condition*)
-by (Asm_simp_tac 1);
-by (etac Atleast_superset 1 THEN Fast_tac 1);
-qed_spec_mp "pigeon2";
-
-
-(**** Ramsey's Theorem ****)
-
-(** Base cases of induction; they now admit ANY Ramsey number **)
-
-Goalw [Ramsey_def] "Ramsey(n,0,j)";
-by (fast_tac (claset() addIs [Clique0,Atleast0]) 1);
-qed "Ramsey0j";
-
-Goalw [Ramsey_def] "Ramsey(n,i,0)";
-by (fast_tac (claset() addIs [Indept0,Atleast0]) 1);
-qed "Ramseyi0";
-
-(** Lemmas for induction step **)
-
-(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of
- Ramsey_step_lemma.*)
-Goal "[| Atleast(m #+ n, A); m \\<in> nat; n \\<in> nat |] \
-\ ==> Atleast(succ(m), {x \\<in> A. ~P(x)}) | Atleast(n, {x \\<in> A. P(x)})";
-by (rtac (nat_succI RS pigeon2) 1);
-by (Asm_simp_tac 3);
-by (rtac Atleast_superset 3);
-by Auto_tac;
-qed "Atleast_partition";
-
-(*For the Atleast part, proves ~(a \\<in> I) from the second premise!*)
-Goalw [Symmetric_def,Indept_def]
- "[| Symmetric(E); Indept(I, {z \\<in> V-{a}. <a,z> \\<notin> E}, E); a \\<in> V; \
-\ Atleast(j,I) |] ==> \
-\ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
-by (blast_tac (claset() addSIs [Atleast_succI]) 1);
-qed "Indept_succ";
-
-Goalw [Symmetric_def,Clique_def]
- "[| Symmetric(E); Clique(C, {z \\<in> V-{a}. <a,z>:E}, E); a \\<in> V; \
-\ Atleast(j,C) |] ==> \
-\ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
-by (blast_tac (claset() addSIs [Atleast_succI]) 1);
-qed "Clique_succ";
-
-(** Induction step **)
-
-(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
-val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def]
- "[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); \
-\ m \\<in> nat; n \\<in> nat |] ==> \
-\ Ramsey(succ(m#+n), succ(i), succ(j))";
-by Safe_tac;
-by (etac (Atleast_succD RS bexE) 1);
-by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
-by (REPEAT (resolve_tac prems 1));
-(*case m*)
-by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
-by Safe_tac;
-by (eresolve_tac (swapify [exI]) 1); (*ignore main \\<exists>quantifier*)
-by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*)
-(*case n*)
-by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (rtac exI 1);
-by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*)
-by (fast_tac (claset() addEs [Indept_superset]) 1); (*easy -- given an Indept*)
-qed "Ramsey_step_lemma";
-
-
-(** The actual proof **)
-
-(*Again, the induction requires Ramsey numbers to be positive.*)
-Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. \\<exists>n \\<in> nat. Ramsey(succ(n), i, j)";
-by (induct_tac "i" 1);
-by (fast_tac (claset() addSIs [Ramsey0j]) 1);
-by (rtac ballI 1);
-by (induct_tac "j" 1);
-by (fast_tac (claset() addSIs [Ramseyi0]) 1);
-by (fast_tac (claset() addSDs [bspec]
- addSIs [add_type,Ramsey_step_lemma]) 1);
-qed "ramsey_lemma";
-
-(*Final statement in a tidy form, without succ(...) *)
-Goal "[| i \\<in> nat; j \\<in> nat |] ==> \\<exists>n \\<in> nat. Ramsey(n,i,j)";
-by (best_tac (claset() addDs [ramsey_lemma]) 1);
-qed "ramsey";
-
-(*Compute Ramsey numbers according to proof above -- which, actually,
- does not constrain the base case values at all!*)
-fun ram 0 j = 1
- | ram i 0 = 1
- | ram i j = ram (i-1) j + ram i (j-1);
-
-(*Previous proof gave the following Ramsey numbers, which are smaller than
- those above by one!*)
-fun ram' 0 j = 0
- | ram' i 0 = 0
- | ram' i j = ram' (i-1) j + ram' i (j-1) + 1;