--- a/src/HOL/IsaMakefile Fri Jul 03 17:34:55 1998 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 03 17:35:39 1998 +0200
@@ -42,11 +42,11 @@
Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
- Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
+ Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
- Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Record.thy RelPow.ML \
+ Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
- Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
+ String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
@@ -281,7 +281,7 @@
ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \
ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \
- ex/Recdef.ML ex/Recdef.thy ex/String.ML ex/String.thy ex/cla.ML \
+ ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML \
ex/meson.ML ex/mesontest.ML ex/set.ML \
ex/Group.ML ex/Group.thy ex/IntRing.ML ex/IntRing.thy \
ex/IntRingDefs.ML ex/IntRingDefs.thy \
--- a/src/HOL/ROOT.ML Fri Jul 03 17:34:55 1998 +0200
+++ b/src/HOL/ROOT.ML Fri Jul 03 17:35:39 1998 +0200
@@ -52,7 +52,7 @@
use_thy "RelPow";
use_thy "Finite";
use_thy "Sexp";
-use_thy "WF_Rel";
+use_thy "Recdef";
use_thy "Map";
use_thy "Update";
@@ -65,6 +65,9 @@
use "sys.sml";
cd "$ISABELLE_HOME/src/HOL";
+(*the all-in-one theory*)
+use_thy "Main";
+
print_depth 8;
val HOL_build_completed = (); (*indicate successful build*)
--- a/src/HOL/ex/ROOT.ML Fri Jul 03 17:34:55 1998 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Jul 03 17:35:39 1998 +0200
@@ -12,7 +12,7 @@
set proof_timing;
(**Some examples of recursive function definitions: the TFL package**)
-time_use_thy "Recdef";
+time_use_thy "Recdefs";
time_use_thy "Primes";
time_use_thy "Fib";
time_use_thy "Primrec";
@@ -22,7 +22,6 @@
time_use "meson.ML";
time_use "mesontest.ML";
(** time_use "mesontest2.ML"; ULTRA SLOW **)
-time_use_thy "String";
time_use_thy "BT";
time_use_thy "InSort";
time_use_thy "Qsort";
--- a/src/HOL/ex/Recdef.ML Fri Jul 03 17:34:55 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/ex/Recdef.ML
- ID: $Id$
- Author: Konrad Lawrence C Paulson
- Copyright 1997 University of Cambridge
-
-A few proofs to demonstrate the functions defined in Recdef.thy
-Lemma statements from Konrad Slind's Web site
-*)
-
-open Recdef;
-
-Addsimps qsort.rules;
-
-Goal "(x mem qsort (ord,l)) = (x mem l)";
-by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "qsort_mem_stable";
-
-
-(** The silly g function: example of nested recursion **)
-
-Addsimps g.rules;
-
-Goal "g x < Suc x";
-by (res_inst_tac [("u","x")] g.induct 1);
-by Auto_tac;
-by (trans_tac 1);
-qed "g_terminates";
-
-Goal "g x = 0";
-by (res_inst_tac [("u","x")] g.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
-qed "g_zero";
-
-(*** the contrived `mapf' ***)
-
-(* proving the termination condition: *)
-val [tc] = mapf.tcs;
-goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by (rtac allI 1);
-by (case_tac "n=0" 1);
-by (ALLGOALS Asm_simp_tac);
-val lemma = result();
-
-(* removing the termination condition from the generated thms: *)
-val [mapf_0,mapf_Suc] = mapf.rules;
-val mapf_Suc = lemma RS mapf_Suc;
-
-val mapf_induct = lemma RS mapf.induct;
--- a/src/HOL/ex/Recdef.thy Fri Jul 03 17:34:55 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(* Title: HOL/ex/Recdef.thy
- ID: $Id$
- Author: Konrad Slind and Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-Examples of recdef definitions. Most, but not all, are handled automatically.
-*)
-
-Recdef = WF_Rel + List +
-
-consts fact :: "nat => nat"
-recdef fact "less_than"
- "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
-
-consts Fact :: "nat => nat"
-recdef Fact "less_than"
- "Fact 0 = 1"
- "Fact (Suc x) = (Fact x * Suc x)"
-
-consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
-recdef map2 "measure(%(f,l1,l2).size l1)"
- "map2(f, [], []) = []"
- "map2(f, h#t, []) = []"
- "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
-
-consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
-recdef finiteRchain "measure (%(R,l).size l)"
- "finiteRchain(R, []) = True"
- "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 [le_eq_less_Suc RS sym, 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))"
- "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
-
-consts gcd :: "nat * nat => nat"
-recdef gcd "measure (%(x,y).x+y)"
- simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
- "gcd (0,y) = y"
- "gcd (Suc x, 0) = Suc x"
- "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)
- else gcd(Suc x, y - x))"
-
-(*Not handled automatically. In fact, g is the zero constant function.*)
-consts g :: "nat => nat"
-recdef g "less_than"
- "g 0 = 0"
- "g(Suc x) = g(g x)"
-
-consts Div :: "nat * nat => nat * nat"
-recdef Div "measure fst"
- "Div(0,x) = (0,0)"
- "Div(Suc x, y) =
- (let (q,r) = Div(x,y)
- in
- if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
-
-(*Not handled automatically. Should be the predecessor function, but there
- is an unnecessary "looping" recursive call in k(1) *)
-consts k :: "nat => nat"
-recdef k "less_than"
- "k 0 = 0"
- "k (Suc n) = (let x = k 1
- in if (0=1) then k (Suc 1) else n)"
-
-consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
-recdef part "measure (%(P,l,l1,l2).size l)"
- "part(P, [], l1,l2) = (l1,l2)"
- "part(P, h#rst, l1,l2) =
- (if P h then part(P,rst, h#l1, l2)
- else part(P,rst, l1, h#l2))"
-
-consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
-recdef fqsort "measure (size o snd)"
- "fqsort(ord,[]) = []"
- "fqsort(ord, x#rst) =
- (let (less,more) = part((%y. ord y x), rst, ([],[]))
- in
- fqsort(ord,less)@[x]@fqsort(ord,more))"
-
-(* silly example which demonstrates the occasional need for additional
- congruence rules (here: map_cong from List). If the congruence rule is
- removed, an unprovable termination condition is generated!
- Termination not proved automatically; see the ML file.
- TFL requires (%x.mapf x) instead of mapf.
-*)
-consts mapf :: nat => nat list
-recdef mapf "measure(%m. m)"
-congs "[map_cong]"
-"mapf 0 = []"
-"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Recdefs.ML Fri Jul 03 17:35:39 1998 +0200
@@ -0,0 +1,48 @@
+(* Title: HOL/ex/Recdefs.ML
+ ID: $Id$
+ Author: Konrad Lawrence C Paulson
+ Copyright 1997 University of Cambridge
+
+A few proofs to demonstrate the functions defined in Recdefs.thy
+Lemma statements from Konrad Slind's Web site
+*)
+
+Addsimps qsort.rules;
+
+Goal "(x mem qsort (ord,l)) = (x mem l)";
+by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed "qsort_mem_stable";
+
+
+(** The silly g function: example of nested recursion **)
+
+Addsimps g.rules;
+
+Goal "g x < Suc x";
+by (res_inst_tac [("u","x")] g.induct 1);
+by Auto_tac;
+by (trans_tac 1);
+qed "g_terminates";
+
+Goal "g x = 0";
+by (res_inst_tac [("u","x")] g.induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
+qed "g_zero";
+
+(*** the contrived `mapf' ***)
+
+(* proving the termination condition: *)
+val [tc] = mapf.tcs;
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+by (rtac allI 1);
+by (case_tac "n=0" 1);
+by (ALLGOALS Asm_simp_tac);
+val lemma = result();
+
+(* removing the termination condition from the generated thms: *)
+val [mapf_0,mapf_Suc] = mapf.rules;
+val mapf_Suc = lemma RS mapf_Suc;
+
+val mapf_induct = lemma RS mapf.induct;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Recdefs.thy Fri Jul 03 17:35:39 1998 +0200
@@ -0,0 +1,102 @@
+(* Title: HOL/ex/Recdef.thy
+ ID: $Id$
+ Author: Konrad Slind and Lawrence C Paulson
+ Copyright 1996 University of Cambridge
+
+Examples of recdef definitions. Most, but not all, are handled automatically.
+*)
+
+Recdefs = Recdef + List +
+
+consts fact :: "nat => nat"
+recdef fact "less_than"
+ "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
+
+consts Fact :: "nat => nat"
+recdef Fact "less_than"
+ "Fact 0 = 1"
+ "Fact (Suc x) = (Fact x * Suc x)"
+
+consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
+recdef map2 "measure(%(f,l1,l2).size l1)"
+ "map2(f, [], []) = []"
+ "map2(f, h#t, []) = []"
+ "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
+
+consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
+recdef finiteRchain "measure (%(R,l).size l)"
+ "finiteRchain(R, []) = True"
+ "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 [le_eq_less_Suc RS sym, 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))"
+ "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
+
+consts gcd :: "nat * nat => nat"
+recdef gcd "measure (%(x,y).x+y)"
+ simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
+ "gcd (0,y) = y"
+ "gcd (Suc x, 0) = Suc x"
+ "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)
+ else gcd(Suc x, y - x))"
+
+(*Not handled automatically. In fact, g is the zero constant function.*)
+consts g :: "nat => nat"
+recdef g "less_than"
+ "g 0 = 0"
+ "g(Suc x) = g(g x)"
+
+consts Div :: "nat * nat => nat * nat"
+recdef Div "measure fst"
+ "Div(0,x) = (0,0)"
+ "Div(Suc x, y) =
+ (let (q,r) = Div(x,y)
+ in
+ if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
+
+(*Not handled automatically. Should be the predecessor function, but there
+ is an unnecessary "looping" recursive call in k(1) *)
+consts k :: "nat => nat"
+recdef k "less_than"
+ "k 0 = 0"
+ "k (Suc n) = (let x = k 1
+ in if (0=1) then k (Suc 1) else n)"
+
+consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
+recdef part "measure (%(P,l,l1,l2).size l)"
+ "part(P, [], l1,l2) = (l1,l2)"
+ "part(P, h#rst, l1,l2) =
+ (if P h then part(P,rst, h#l1, l2)
+ else part(P,rst, l1, h#l2))"
+
+consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
+recdef fqsort "measure (size o snd)"
+ "fqsort(ord,[]) = []"
+ "fqsort(ord, x#rst) =
+ (let (less,more) = part((%y. ord y x), rst, ([],[]))
+ in
+ fqsort(ord,less)@[x]@fqsort(ord,more))"
+
+(* silly example which demonstrates the occasional need for additional
+ congruence rules (here: map_cong from List). If the congruence rule is
+ removed, an unprovable termination condition is generated!
+ Termination not proved automatically; see the ML file.
+ TFL requires (%x.mapf x) instead of mapf.
+*)
+consts mapf :: nat => nat list
+recdef mapf "measure(%m. m)"
+congs "[map_cong]"
+"mapf 0 = []"
+"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
+
+end