# HG changeset patch # User wenzelm # Date 899480139 -7200 # Node ID 1ce3cccfacdb508c74a2bd7715dafdc4bbb1e276 # Parent 97c1d5c7b701e0804be163a1d429a50a399e5844 stepping stones: Recdef, Main; String now part of main HOL; diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/IsaMakefile --- 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 \ diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ROOT.ML --- 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*) diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ex/ROOT.ML --- 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"; diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ex/Recdef.ML --- 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; diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ex/Recdef.thy --- 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 diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ex/Recdefs.ML --- /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; diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ex/Recdefs.thy --- /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