aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2008-06-14 17:16:23 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2008-06-14 17:16:23 +0000
commit41fc4493a96c8a66971d293b557ba9903bf9c053 (patch)
tree574f9c8f375204cc2ef11e1c04e53f21cfae079d /etc
parentfaea8019ff496be6b5bf49f8257117fb1bddacef (diff)
obsolete;
Diffstat (limited to 'etc')
-rw-r--r--etc/isa/completed-proof.ML43
-rw-r--r--etc/isa/depends/Fib.ML106
-rw-r--r--etc/isa/depends/Fib.thy17
-rw-r--r--etc/isa/depends/Primes.ML197
-rw-r--r--etc/isa/depends/Primes.thy33
-rw-r--r--etc/isa/depends/Usedepends.ML3
-rw-r--r--etc/isa/depends/Usedepends.thy5
-rw-r--r--etc/isa/goal-matching.ML10
8 files changed, 0 insertions, 414 deletions
diff --git a/etc/isa/completed-proof.ML b/etc/isa/completed-proof.ML
deleted file mode 100644
index 70cc8e18..00000000
--- a/etc/isa/completed-proof.ML
+++ /dev/null
@@ -1,43 +0,0 @@
-(* Test of completed proof behaviour: even if qed command is missing,
- PG should close of the proof as a goalsave.
-
- Issue with Isabelle2002: Goals.disable_pr prevents
- proof-shell-proof-completed being set because "No Subgoals!" is not
- displayed. This means that processing file in one go here (or C-c
- C-RET at val_) does not work properly.
-*)
-
-(* default proof-completed-proof-behaviour for isa is 'closeany.
- Also should test this file with 'closegoal, 'extend.
-
- (setq proof-completed-proof-behaviour 'closeany)
- : close on any command after proof completed seen
- (setq proof-completed-proof-behaviour 'closegoal)
- : close when next goal is seen
- (setq proof-completed-proof-behaviour 'extend)
- : continually extend region after proof completed, until next goal.
-
- *)
-
-Goal "A & B --> B & A";
- by (rtac impI 1);
- by (etac conjE 1);
- by (rtac conjI 1);
- by (assume_tac 1);
- by (assume_tac 1);
- (* qed "and_comms"; *)
-
-val _ = ();
-val _ = ();
-
-Goal "A & B --> B & A";
- by (rtac impI 1);
- by (etac conjE 1);
- by (rtac conjI 1);
- by (assume_tac 1);
- by (assume_tac 1);
- qed "and_comms";
-
-
-
-
diff --git a/etc/isa/depends/Fib.ML b/etc/isa/depends/Fib.ML
deleted file mode 100644
index eba2f0e0..00000000
--- a/etc/isa/depends/Fib.ML
+++ /dev/null
@@ -1,106 +0,0 @@
-(* Title: HOL/ex/Fib
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1997 University of Cambridge
-
-Fibonacci numbers: proofs of laws taken from
-
- R. L. Graham, D. E. Knuth, O. Patashnik.
- Concrete Mathematics.
- (Addison-Wesley, 1989)
-*)
-
-
-(** The difficulty in these proofs is to ensure that the induction hypotheses
- are applied before the definition of "fib". Towards this end, the
- "fib" equations are not added to the simpset and are applied very
- selectively at first.
-**)
-
-Delsimps fib.Suc_Suc;
-
-val [fib_Suc_Suc] = fib.Suc_Suc;
-val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
-
-(*Concrete Mathematics, page 280*)
-Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
-by (res_inst_tac [("u","n")] fib.induct 1);
-(*Simplify the LHS just enough to apply the induction hypotheses*)
-by (asm_full_simp_tac
- (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps
- ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
-qed "fib_add";
-
-
-Goal "fib (Suc n) ~= 0";
-by (res_inst_tac [("u","n")] fib.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
-qed "fib_Suc_neq_0";
-
-(* Also add 0 < fib (Suc n) *)
-Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
-
-Goal "0<n ==> 0 < fib n";
-by (rtac (not0_implies_Suc RS exE) 1);
-by Auto_tac;
-qed "fib_gr_0";
-
-(*Concrete Mathematics, page 278: Cassini's identity.
- It is much easier to prove using integers!*)
-Goal "int (fib (Suc (Suc n)) * fib n) = \
-\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
-\ else int (fib(Suc n) * fib(Suc n)) + #1)";
-by (res_inst_tac [("u","n")] fib.induct 1);
-by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
-by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2,
- mod_Suc, zmult_int RS sym] @ zmult_ac) 1);
-qed "fib_Cassini";
-
-
-
-(** Towards Law 6.111 of Concrete Mathematics **)
-
-Goal "gcd(fib n, fib (Suc n)) = 1";
-by (res_inst_tac [("u","n")] fib.induct 1);
-by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
-by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
-qed "gcd_fib_Suc_eq_1";
-
-val gcd_fib_commute =
- read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
-
-Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
-by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
-by (case_tac "m=0" 1);
-by (Asm_simp_tac 1);
-by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
-by (simp_tac (simpset() addsimps [fib_add]) 1);
-by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1);
-by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
-qed "gcd_fib_add";
-
-Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
-by (rtac (gcd_fib_add RS sym RS trans) 1);
-by (Asm_simp_tac 1);
-qed "gcd_fib_diff";
-
-Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-by (res_inst_tac [("n","n")] less_induct 1);
-by (stac mod_if 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq,
- not_less_iff_le, diff_less]) 1);
-qed "gcd_fib_mod";
-
-(*Law 6.111*)
-Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
-by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
-qed "fib_gcd";
diff --git a/etc/isa/depends/Fib.thy b/etc/isa/depends/Fib.thy
deleted file mode 100644
index 9272ed8c..00000000
--- a/etc/isa/depends/Fib.thy
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Title: ex/Fib
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The Fibonacci function. Demonstrates the use of recdef.
-*)
-
-Fib = Usedepends + Divides + Primes +
-
-consts fib :: "nat => nat"
-recdef fib "less_than"
- zero "fib 0 = 0"
- one "fib 1 = 1"
- Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
-
-end
diff --git a/etc/isa/depends/Primes.ML b/etc/isa/depends/Primes.ML
deleted file mode 100644
index 102419da..00000000
--- a/etc/isa/depends/Primes.ML
+++ /dev/null
@@ -1,197 +0,0 @@
-(* Title: HOL/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
-
-See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)
-*)
-
-eta_contract:=false;
-
-(************************************************)
-(** Greatest Common Divisor **)
-(************************************************)
-
-(*** Euclid's Algorithm ***)
-
-
-val [gcd_eq] = gcd.simps;
-
-
-val prems = goal thy
- "[| !!m. P m 0; \
-\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \
-\ |] ==> P (m::nat) (n::nat)";
-by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
-by (case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps prems) 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps prems) 1);
-qed "gcd_induct";
-
-
-Goal "gcd(m,0) = m";
-by (Simp_tac 1);
-qed "gcd_0";
-Addsimps [gcd_0];
-
-Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
-by (Asm_simp_tac 1);
-qed "gcd_non_0";
-
-Delsimps gcd.simps;
-
-Goal "gcd(m,1) = 1";
-by (simp_tac (simpset() addsimps [gcd_non_0]) 1);
-qed "gcd_1";
-Addsimps [gcd_1];
-
-(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
-Goal "(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() addDs [dvd_mod_imp_dvd]) 1);
-qed "gcd_dvd_both";
-
-bind_thm ("gcd_dvd1", gcd_dvd_both RS conjunct1);
-bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2);
-
-
-(*Maximality: for all m,n,f naturals,
- if f divides m and f divides n then f divides gcd(m,n)*)
-Goal "(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_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod])));
-qed_spec_mp "gcd_greatest";
-
-(*Function gcd yields the Greatest Common Divisor*)
-Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n";
-by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1);
-qed "is_gcd";
-
-(*uniqueness of GCDs*)
-Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n";
-by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
-qed "is_gcd_unique";
-
-(*USED??*)
-Goalw [is_gcd_def]
- "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
-by (Blast_tac 1);
-qed "is_gcd_dvd";
-
-(** Commutativity **)
-
-Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m";
-by (Blast_tac 1);
-qed "is_gcd_commute";
-
-Goal "gcd(m,n) = gcd(n,m)";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 2);
-by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1);
-qed "gcd_commute";
-
-Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 2);
-by (rewtac is_gcd_def);
-by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2]
- addIs [gcd_greatest, dvd_trans]) 1);
-qed "gcd_assoc";
-
-Goal "gcd(0,m) = m";
-by (stac gcd_commute 1);
-by (rtac gcd_0 1);
-qed "gcd_0_left";
-
-Goal "gcd(1,m) = 1";
-by (stac gcd_commute 1);
-by (rtac gcd_1 1);
-qed "gcd_1_left";
-Addsimps [gcd_0_left, gcd_1_left];
-
-
-(** Multiplication laws **)
-
-(*Davenport, page 27*)
-Goal "k * gcd(m,n) = gcd(k*m, k*n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (Asm_full_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]) 1);
-qed "gcd_mult_distrib2";
-
-Goal "gcd(m,m) = m";
-by (cut_inst_tac [("k","m"),("m","1"),("n","1")] gcd_mult_distrib2 1);
-by (Asm_full_simp_tac 1);
-qed "gcd_self";
-Addsimps [gcd_self];
-
-Goal "gcd(k, k*n) = k";
-by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
-by (Asm_full_simp_tac 1);
-qed "gcd_mult";
-Addsimps [gcd_mult];
-
-Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
-by (subgoal_tac "m = gcd(m*k, m*n)" 1);
-by (etac ssubst 1 THEN rtac gcd_greatest 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
-qed "relprime_dvd_mult";
-
-Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1";
-by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
-by Auto_tac;
-qed "prime_imp_relprime";
-
-(*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: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
-by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
-qed "prime_dvd_mult";
-
-
-(** Addition laws **)
-
-Goal "gcd(m, m+n) = gcd(m,n)";
-by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1);
-by (rtac (gcd_eq RS trans) 1);
-by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1);
-by (stac gcd_commute 1);
-by (stac gcd_non_0 1);
-by Safe_tac;
-qed "gcd_add";
-
-Goal "gcd(m, n+m) = gcd(m,n)";
-by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1);
-qed "gcd_add2";
-
-Goal "gcd(m, k*m+n) = gcd(m,n)";
-by (induct_tac "k" 1);
-by (asm_simp_tac (simpset() addsimps [gcd_add, add_assoc]) 2);
-by (Simp_tac 1);
-qed "gcd_add_mult";
-
-
-(** More multiplication laws **)
-
-Goal "gcd(m,n) dvd gcd(k*m, n)";
-by (blast_tac (claset() addIs [gcd_greatest, dvd_trans,
- gcd_dvd1, gcd_dvd2]) 1);
-qed "gcd_dvd_gcd_mult";
-
-Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
-by (rtac dvd_anti_sym 1);
-by (rtac gcd_dvd_gcd_mult 2);
-by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1);
-by (stac mult_commute 2);
-by (rtac gcd_dvd1 2);
-by (stac gcd_commute 1);
-by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1);
-qed "gcd_mult_cancel";
diff --git a/etc/isa/depends/Primes.thy b/etc/isa/depends/Primes.thy
deleted file mode 100644
index fac39463..00000000
--- a/etc/isa/depends/Primes.thy
+++ /dev/null
@@ -1,33 +0,0 @@
-(* Title: HOL/ex/Primes.thy
- ID: $Id$
- Author: Christophe Tabacznyj and Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-The Greatest Common Divisor and Euclid's algorithm
-
-The "simpset" clause in the recdef declaration used to be necessary when the
-two lemmas where not part of the default simpset.
-*)
-
-Primes = Main +
-
-
-consts
- is_gcd :: [nat,nat,nat]=>bool (*gcd as a relation*)
- gcd :: "nat*nat=>nat" (*Euclid's algorithm *)
- coprime :: [nat,nat]=>bool
- prime :: nat set
-
-recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
-(* simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *)
- "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
-
-defs
- is_gcd_def "is_gcd p m n == p dvd m & p dvd n &
- (ALL d. d dvd m & d dvd n --> d dvd p)"
-
- coprime_def "coprime m n == gcd(m,n) = 1"
-
- prime_def "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
-
-end
diff --git a/etc/isa/depends/Usedepends.ML b/etc/isa/depends/Usedepends.ML
deleted file mode 100644
index 7557d6e8..00000000
--- a/etc/isa/depends/Usedepends.ML
+++ /dev/null
@@ -1,3 +0,0 @@
-use "~/ProofGeneral/isa/depends.ML";
-
-
diff --git a/etc/isa/depends/Usedepends.thy b/etc/isa/depends/Usedepends.thy
deleted file mode 100644
index 4f8eb516..00000000
--- a/etc/isa/depends/Usedepends.thy
+++ /dev/null
@@ -1,5 +0,0 @@
-(* dummy theory to load depends.ML *)
-theory Usedepends = Main:
-end
-
-
diff --git a/etc/isa/goal-matching.ML b/etc/isa/goal-matching.ML
deleted file mode 100644
index 843e2ca5..00000000
--- a/etc/isa/goal-matching.ML
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- Test case sent by David von Oheimb.
- Bug in matching case-insensitively meant that
- the SELECT_GOAL line was considered a goal.
-*)
-
-Goal "x";
-by (SELECT_GOAL all_tac 1);
-
-