--- a/src/HOL/ex/Fib.ML Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Fib.ML Fri Mar 10 17:53:16 2000 +0100
@@ -29,11 +29,10 @@
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 [read_instantiate[("x","Suc(?m+?n)")] fib_Suc_Suc]) 3);
+ (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps
- ([] @ add_ac @ mult_ac @
- [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
+ ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
qed "fib_add";
--- a/src/HOL/ex/NatSum.ML Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/NatSum.ML Fri Mar 10 17:53:16 2000 +0100
@@ -4,10 +4,11 @@
Copyright 1994 TU Muenchen
Summing natural numbers, squares and cubes. Could be continued...
-Demonstrates permutative rewriting.
+
+Originally demonstrated permutative rewriting, but add_ac is no longer needed
+ thanks to new simprocs.
*)
-Addsimps add_ac;
Addsimps [add_mult_distrib, add_mult_distrib2];
(*The sum of the first n positive integers equals n(n+1)/2.*)
@@ -16,12 +17,12 @@
by Auto_tac;
qed "sum_of_naturals";
-Goal "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
+Goal "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)";
by (induct_tac "n" 1);
by Auto_tac;
qed "sum_of_squares";
-Goal "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
+Goal "Suc(Suc 2) * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)";
by (induct_tac "n" 1);
by Auto_tac;
qed "sum_of_cubes";
@@ -29,7 +30,6 @@
(*The sum of the first n odd numbers equals n squared.*)
Goal "sum (%i. Suc(i+i)) n = n*n";
by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
qed "sum_of_odds";
--- a/src/HOL/ex/Recdefs.ML Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Recdefs.ML Fri Mar 10 17:53:16 2000 +0100
@@ -7,14 +7,6 @@
Lemma statements from Konrad Slind's Web site
*)
-Addsimps qsort.rules;
-
-Goal "(x: set (qsort (ord,l))) = (x: set l)";
-by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by Auto_tac;
-qed "qsort_mem_stable";
-
-
(** The silly g function: example of nested recursion **)
Addsimps g.rules;
--- a/src/HOL/ex/Recdefs.thy Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Recdefs.thy Fri Mar 10 17:53:16 2000 +0100
@@ -29,14 +29,6 @@
"finiteRchain(R, [x]) = True"
"finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
-consts qsort ::"('a => 'a => bool) * 'a list => 'a list"
-recdef qsort "measure (size o snd)"
- simpset "simpset() addsimps [less_Suc_eq_le, length_filter]"
- "qsort(ord, []) = []"
- "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)
- @ [x] @
- qsort(ord, filter(ord x) rst)"
-
(*Not handled automatically: too complicated.*)
consts variant :: "nat * nat list => nat"
recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
--- a/src/HOL/ex/Sorting.ML Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Sorting.ML Fri Mar 10 17:53:16 2000 +0100
@@ -6,31 +6,36 @@
Some general lemmas
*)
-Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
+Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mset_append";
+by Auto_tac;
+qed "multiset_append";
-Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
-\ mset xs x";
+Goal "multiset [x:xs. ~p(x)] x + multiset [x:xs. p(x)] x = multiset xs x";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mset_compl_add";
+by Auto_tac;
+qed "multiset_compl_add";
-Addsimps [mset_append, mset_compl_add];
+Addsimps [multiset_append, multiset_compl_add];
-Goal "set xs = {x. mset xs x ~= 0}";
+Goal "set xs = {x. multiset xs x ~= 0}";
by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "set_via_mset";
+by Auto_tac;
+qed "set_via_multiset";
(* Equivalence of two definitions of `sorted' *)
-val prems = goalw Sorting.thy [transf_def]
- "transf(le) ==> sorted1 le xs = sorted le xs";
+Goal "transf(le) ==> sorted1 le xs = sorted le xs";
by (induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
-by (cut_facts_tac prems 1);
-by (Fast_tac 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
+by (rewrite_goals_tac [transf_def]);
+by (Blast_tac 1);
qed "sorted1_is_sorted";
+
+Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
+\ (ALL x:set xs. ALL y:set ys. le x y))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "sorted_append";
+Addsimps [sorted_append];
+
--- a/src/HOL/ex/Sorting.thy Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Sorting.thy Fri Mar 10 17:53:16 2000 +0100
@@ -6,13 +6,11 @@
Specification of sorting
*)
-Sorting = List +
+Sorting = Main +
consts
sorted1:: [['a,'a] => bool, 'a list] => bool
sorted :: [['a,'a] => bool, 'a list] => bool
- mset :: 'a list => ('a => nat)
- total :: (['a,'a] => bool) => bool
- transf :: (['a,'a] => bool) => bool
+ multiset :: 'a list => ('a => nat)
primrec
"sorted1 le [] = True"
@@ -24,10 +22,14 @@
"sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
primrec
- "mset [] y = 0"
- "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
+ "multiset [] y = 0"
+ "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
-defs
-total_def "total r == (!x y. r x y | r y x)"
-transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
+constdefs
+ total :: (['a,'a] => bool) => bool
+ "total r == (ALL x y. r x y | r y x)"
+
+ transf :: (['a,'a] => bool) => bool
+ "transf f == (ALL x y z. f x y & f y z --> f x z)"
+
end