stepping stones: Recdef, Main;
authorwenzelm
Fri Jul 03 17:35:39 1998 +0200 (1998-07-03)
changeset 51241ce3cccfacdb
parent 5123 97c1d5c7b701
child 5125 463a0e9df5b5
stepping stones: Recdef, Main;
String now part of main HOL;
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/Recdef.ML
src/HOL/ex/Recdef.thy
src/HOL/ex/Recdefs.ML
src/HOL/ex/Recdefs.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 03 17:34:55 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 03 17:35:39 1998 +0200
     1.3 @@ -42,11 +42,11 @@
     1.4    Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
     1.5    Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
     1.6    Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
     1.7 -  Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
     1.8 +  Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
     1.9    Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    1.10 -  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Record.thy RelPow.ML \
    1.11 +  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    1.12    RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    1.13 -  Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
    1.14 +  String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
    1.15    Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.16    Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
    1.17    WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
    1.18 @@ -281,7 +281,7 @@
    1.19    ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
    1.20    ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \
    1.21    ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \
    1.22 -  ex/Recdef.ML ex/Recdef.thy ex/String.ML ex/String.thy ex/cla.ML \
    1.23 +  ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML \
    1.24    ex/meson.ML ex/mesontest.ML ex/set.ML \
    1.25    ex/Group.ML ex/Group.thy  ex/IntRing.ML ex/IntRing.thy \
    1.26    ex/IntRingDefs.ML ex/IntRingDefs.thy \
     2.1 --- a/src/HOL/ROOT.ML	Fri Jul 03 17:34:55 1998 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Jul 03 17:35:39 1998 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4  use_thy "RelPow";
     2.5  use_thy "Finite";
     2.6  use_thy "Sexp";
     2.7 -use_thy "WF_Rel";
     2.8 +use_thy "Recdef";
     2.9  use_thy "Map";
    2.10  use_thy "Update";
    2.11  
    2.12 @@ -65,6 +65,9 @@
    2.13  use "sys.sml";
    2.14  cd "$ISABELLE_HOME/src/HOL";
    2.15  
    2.16 +(*the all-in-one theory*)
    2.17 +use_thy "Main";
    2.18 +
    2.19  print_depth 8;
    2.20  
    2.21  val HOL_build_completed = ();   (*indicate successful build*)
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Jul 03 17:34:55 1998 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Jul 03 17:35:39 1998 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  set proof_timing;
     3.5  
     3.6  (**Some examples of recursive function definitions: the TFL package**)
     3.7 -time_use_thy "Recdef";
     3.8 +time_use_thy "Recdefs";
     3.9  time_use_thy "Primes";
    3.10  time_use_thy "Fib";
    3.11  time_use_thy "Primrec";
    3.12 @@ -22,7 +22,6 @@
    3.13  time_use     "meson.ML";
    3.14  time_use     "mesontest.ML";
    3.15  (** time_use "mesontest2.ML";  ULTRA SLOW **)
    3.16 -time_use_thy "String";
    3.17  time_use_thy "BT";
    3.18  time_use_thy "InSort";
    3.19  time_use_thy "Qsort";
     4.1 --- a/src/HOL/ex/Recdef.ML	Fri Jul 03 17:34:55 1998 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,50 +0,0 @@
     4.4 -(*  Title:      HOL/ex/Recdef.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Konrad Lawrence C Paulson
     4.7 -    Copyright   1997  University of Cambridge
     4.8 -
     4.9 -A few proofs to demonstrate the functions defined in Recdef.thy
    4.10 -Lemma statements from Konrad Slind's Web site
    4.11 -*)
    4.12 -
    4.13 -open Recdef;
    4.14 -
    4.15 -Addsimps qsort.rules;
    4.16 -
    4.17 -Goal "(x mem qsort (ord,l)) = (x mem l)";
    4.18 -by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    4.19 -by (ALLGOALS Asm_simp_tac);
    4.20 -by (Blast_tac 1);
    4.21 -qed "qsort_mem_stable";
    4.22 -
    4.23 -
    4.24 -(** The silly g function: example of nested recursion **)
    4.25 -
    4.26 -Addsimps g.rules;
    4.27 -
    4.28 -Goal "g x < Suc x";
    4.29 -by (res_inst_tac [("u","x")] g.induct 1);
    4.30 -by Auto_tac;
    4.31 -by (trans_tac 1);
    4.32 -qed "g_terminates";
    4.33 -
    4.34 -Goal "g x = 0";
    4.35 -by (res_inst_tac [("u","x")] g.induct 1);
    4.36 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
    4.37 -qed "g_zero";
    4.38 -
    4.39 -(*** the contrived `mapf' ***)
    4.40 -
    4.41 -(* proving the termination condition: *)
    4.42 -val [tc] = mapf.tcs;
    4.43 -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
    4.44 -by (rtac allI 1);
    4.45 -by (case_tac "n=0" 1);
    4.46 -by (ALLGOALS Asm_simp_tac);
    4.47 -val lemma = result();
    4.48 -
    4.49 -(* removing the termination condition from the generated thms: *)
    4.50 -val [mapf_0,mapf_Suc] = mapf.rules;
    4.51 -val mapf_Suc = lemma RS mapf_Suc;
    4.52 -
    4.53 -val mapf_induct = lemma RS mapf.induct;
     5.1 --- a/src/HOL/ex/Recdef.thy	Fri Jul 03 17:34:55 1998 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,102 +0,0 @@
     5.4 -(*  Title:      HOL/ex/Recdef.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Konrad Slind and Lawrence C Paulson
     5.7 -    Copyright   1996  University of Cambridge
     5.8 -
     5.9 -Examples of recdef definitions.  Most, but not all, are handled automatically.
    5.10 -*)
    5.11 -
    5.12 -Recdef = WF_Rel + List +
    5.13 -
    5.14 -consts fact :: "nat => nat"
    5.15 -recdef fact "less_than"
    5.16 -    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
    5.17 -
    5.18 -consts Fact :: "nat => nat"
    5.19 -recdef Fact "less_than"
    5.20 -    "Fact 0 = 1"
    5.21 -    "Fact (Suc x) = (Fact x * Suc x)"
    5.22 -
    5.23 -consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
    5.24 -recdef map2 "measure(%(f,l1,l2).size l1)"
    5.25 -    "map2(f, [], [])  = []"
    5.26 -    "map2(f, h#t, []) = []"
    5.27 -    "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
    5.28 -
    5.29 -consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
    5.30 -recdef finiteRchain "measure (%(R,l).size l)"
    5.31 -    "finiteRchain(R,  []) = True"
    5.32 -    "finiteRchain(R, [x]) = True"
    5.33 -    "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
    5.34 -
    5.35 -consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
    5.36 -recdef qsort "measure (size o snd)"
    5.37 -    simpset "simpset() addsimps [le_eq_less_Suc RS sym, length_filter]"
    5.38 -    "qsort(ord, [])    = []"
    5.39 -    "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)  
    5.40 -                         @ [x] @   
    5.41 -                         qsort(ord, filter(ord x) rst)"
    5.42 -
    5.43 -(*Not handled automatically: too complicated.*)
    5.44 -consts variant :: "nat * nat list => nat"
    5.45 -recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
    5.46 -    "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
    5.47 -
    5.48 -consts gcd :: "nat * nat => nat"
    5.49 -recdef gcd "measure (%(x,y).x+y)"
    5.50 -    simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
    5.51 -    "gcd (0,y)          = y"
    5.52 -    "gcd (Suc x, 0)     = Suc x"
    5.53 -    "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)  
    5.54 -                                       else gcd(Suc x, y - x))"
    5.55 -
    5.56 -(*Not handled automatically.  In fact, g is the zero constant function.*)
    5.57 -consts g   :: "nat => nat"
    5.58 -recdef g "less_than"
    5.59 -    "g 0 = 0"
    5.60 -    "g(Suc x) = g(g x)"
    5.61 -
    5.62 -consts Div :: "nat * nat => nat * nat"
    5.63 -recdef Div "measure fst"
    5.64 -    "Div(0,x)      = (0,0)"
    5.65 -    "Div(Suc x, y) =      
    5.66 -         (let (q,r) = Div(x,y)
    5.67 -          in                      
    5.68 -          if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
    5.69 -
    5.70 -(*Not handled automatically.  Should be the predecessor function, but there
    5.71 -  is an unnecessary "looping" recursive call in k(1) *)
    5.72 -consts k   :: "nat => nat"
    5.73 -recdef k "less_than"
    5.74 -    "k 0 = 0"
    5.75 -    "k (Suc n) = (let x = k 1  
    5.76 -                  in if (0=1) then k (Suc 1) else n)"
    5.77 -
    5.78 -consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
    5.79 -recdef part "measure (%(P,l,l1,l2).size l)"
    5.80 -    "part(P, [], l1,l2) = (l1,l2)"
    5.81 -    "part(P, h#rst, l1,l2) =  
    5.82 -        (if P h then part(P,rst, h#l1,  l2)  
    5.83 -                else part(P,rst,  l1,  h#l2))"
    5.84 -
    5.85 -consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
    5.86 -recdef fqsort "measure (size o snd)"
    5.87 -    "fqsort(ord,[]) = []"
    5.88 -    "fqsort(ord, x#rst) =    
    5.89 -     (let (less,more) = part((%y. ord y x), rst, ([],[]))
    5.90 -      in  
    5.91 -      fqsort(ord,less)@[x]@fqsort(ord,more))"
    5.92 -
    5.93 -(* silly example which demonstrates the occasional need for additional
    5.94 -   congruence rules (here: map_cong from List). If the congruence rule is
    5.95 -   removed, an unprovable termination condition is generated!
    5.96 -   Termination not proved automatically; see the ML file.
    5.97 -   TFL requires (%x.mapf x) instead of mapf.
    5.98 -*)
    5.99 -consts mapf :: nat => nat list
   5.100 -recdef mapf "measure(%m. m)"
   5.101 -congs "[map_cong]"
   5.102 -"mapf 0 = []"
   5.103 -"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
   5.104 -
   5.105 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/Recdefs.ML	Fri Jul 03 17:35:39 1998 +0200
     6.3 @@ -0,0 +1,48 @@
     6.4 +(*  Title:      HOL/ex/Recdefs.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Konrad Lawrence C Paulson
     6.7 +    Copyright   1997  University of Cambridge
     6.8 +
     6.9 +A few proofs to demonstrate the functions defined in Recdefs.thy
    6.10 +Lemma statements from Konrad Slind's Web site
    6.11 +*)
    6.12 +
    6.13 +Addsimps qsort.rules;
    6.14 +
    6.15 +Goal "(x mem qsort (ord,l)) = (x mem l)";
    6.16 +by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    6.17 +by (ALLGOALS Asm_simp_tac);
    6.18 +by (Blast_tac 1);
    6.19 +qed "qsort_mem_stable";
    6.20 +
    6.21 +
    6.22 +(** The silly g function: example of nested recursion **)
    6.23 +
    6.24 +Addsimps g.rules;
    6.25 +
    6.26 +Goal "g x < Suc x";
    6.27 +by (res_inst_tac [("u","x")] g.induct 1);
    6.28 +by Auto_tac;
    6.29 +by (trans_tac 1);
    6.30 +qed "g_terminates";
    6.31 +
    6.32 +Goal "g x = 0";
    6.33 +by (res_inst_tac [("u","x")] g.induct 1);
    6.34 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
    6.35 +qed "g_zero";
    6.36 +
    6.37 +(*** the contrived `mapf' ***)
    6.38 +
    6.39 +(* proving the termination condition: *)
    6.40 +val [tc] = mapf.tcs;
    6.41 +goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
    6.42 +by (rtac allI 1);
    6.43 +by (case_tac "n=0" 1);
    6.44 +by (ALLGOALS Asm_simp_tac);
    6.45 +val lemma = result();
    6.46 +
    6.47 +(* removing the termination condition from the generated thms: *)
    6.48 +val [mapf_0,mapf_Suc] = mapf.rules;
    6.49 +val mapf_Suc = lemma RS mapf_Suc;
    6.50 +
    6.51 +val mapf_induct = lemma RS mapf.induct;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ex/Recdefs.thy	Fri Jul 03 17:35:39 1998 +0200
     7.3 @@ -0,0 +1,102 @@
     7.4 +(*  Title:      HOL/ex/Recdef.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Konrad Slind and Lawrence C Paulson
     7.7 +    Copyright   1996  University of Cambridge
     7.8 +
     7.9 +Examples of recdef definitions.  Most, but not all, are handled automatically.
    7.10 +*)
    7.11 +
    7.12 +Recdefs = Recdef + List +
    7.13 +
    7.14 +consts fact :: "nat => nat"
    7.15 +recdef fact "less_than"
    7.16 +    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
    7.17 +
    7.18 +consts Fact :: "nat => nat"
    7.19 +recdef Fact "less_than"
    7.20 +    "Fact 0 = 1"
    7.21 +    "Fact (Suc x) = (Fact x * Suc x)"
    7.22 +
    7.23 +consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
    7.24 +recdef map2 "measure(%(f,l1,l2).size l1)"
    7.25 +    "map2(f, [], [])  = []"
    7.26 +    "map2(f, h#t, []) = []"
    7.27 +    "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
    7.28 +
    7.29 +consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
    7.30 +recdef finiteRchain "measure (%(R,l).size l)"
    7.31 +    "finiteRchain(R,  []) = True"
    7.32 +    "finiteRchain(R, [x]) = True"
    7.33 +    "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
    7.34 +
    7.35 +consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
    7.36 +recdef qsort "measure (size o snd)"
    7.37 +    simpset "simpset() addsimps [le_eq_less_Suc RS sym, length_filter]"
    7.38 +    "qsort(ord, [])    = []"
    7.39 +    "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)  
    7.40 +                         @ [x] @   
    7.41 +                         qsort(ord, filter(ord x) rst)"
    7.42 +
    7.43 +(*Not handled automatically: too complicated.*)
    7.44 +consts variant :: "nat * nat list => nat"
    7.45 +recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
    7.46 +    "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
    7.47 +
    7.48 +consts gcd :: "nat * nat => nat"
    7.49 +recdef gcd "measure (%(x,y).x+y)"
    7.50 +    simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
    7.51 +    "gcd (0,y)          = y"
    7.52 +    "gcd (Suc x, 0)     = Suc x"
    7.53 +    "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)  
    7.54 +                                       else gcd(Suc x, y - x))"
    7.55 +
    7.56 +(*Not handled automatically.  In fact, g is the zero constant function.*)
    7.57 +consts g   :: "nat => nat"
    7.58 +recdef g "less_than"
    7.59 +    "g 0 = 0"
    7.60 +    "g(Suc x) = g(g x)"
    7.61 +
    7.62 +consts Div :: "nat * nat => nat * nat"
    7.63 +recdef Div "measure fst"
    7.64 +    "Div(0,x)      = (0,0)"
    7.65 +    "Div(Suc x, y) =      
    7.66 +         (let (q,r) = Div(x,y)
    7.67 +          in                      
    7.68 +          if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
    7.69 +
    7.70 +(*Not handled automatically.  Should be the predecessor function, but there
    7.71 +  is an unnecessary "looping" recursive call in k(1) *)
    7.72 +consts k   :: "nat => nat"
    7.73 +recdef k "less_than"
    7.74 +    "k 0 = 0"
    7.75 +    "k (Suc n) = (let x = k 1  
    7.76 +                  in if (0=1) then k (Suc 1) else n)"
    7.77 +
    7.78 +consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
    7.79 +recdef part "measure (%(P,l,l1,l2).size l)"
    7.80 +    "part(P, [], l1,l2) = (l1,l2)"
    7.81 +    "part(P, h#rst, l1,l2) =  
    7.82 +        (if P h then part(P,rst, h#l1,  l2)  
    7.83 +                else part(P,rst,  l1,  h#l2))"
    7.84 +
    7.85 +consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
    7.86 +recdef fqsort "measure (size o snd)"
    7.87 +    "fqsort(ord,[]) = []"
    7.88 +    "fqsort(ord, x#rst) =    
    7.89 +     (let (less,more) = part((%y. ord y x), rst, ([],[]))
    7.90 +      in  
    7.91 +      fqsort(ord,less)@[x]@fqsort(ord,more))"
    7.92 +
    7.93 +(* silly example which demonstrates the occasional need for additional
    7.94 +   congruence rules (here: map_cong from List). If the congruence rule is
    7.95 +   removed, an unprovable termination condition is generated!
    7.96 +   Termination not proved automatically; see the ML file.
    7.97 +   TFL requires (%x.mapf x) instead of mapf.
    7.98 +*)
    7.99 +consts mapf :: nat => nat list
   7.100 +recdef mapf "measure(%m. m)"
   7.101 +congs "[map_cong]"
   7.102 +"mapf 0 = []"
   7.103 +"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
   7.104 +
   7.105 +end