# HG changeset patch # User paulson # Date 952707196 -3600 # Node ID 852c630723345d951bb0dfac3424a7719157dd66 # Parent 5983668cac15e2cad413f4cdfbac371b63463cfb tidied diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Fib.ML --- 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"; diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/NatSum.ML --- 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"; diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Recdefs.ML --- 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; diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Recdefs.thy --- 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))" diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Sorting.ML --- 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]; + diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Sorting.thy --- 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