# HG changeset patch # User bulwahn # Date 1171357761 -3600 # Node ID 87ec1ca65312fe5449fca3e07720eaff238b5fb5 # Parent 7901493455ca6403c907ca6cbce140c4bc3d0063 improved lexicographic order termination tactic diff -r 7901493455ca -r 87ec1ca65312 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Sat Feb 10 17:06:40 2007 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Tue Feb 13 10:09:21 2007 +0100 @@ -12,7 +12,7 @@ (* exported for use by size-change termination prototype. FIXME: provide a common interface later *) val mk_base_funs : typ -> term list - + (* exported for debugging *) val setup: theory -> theory end @@ -68,11 +68,19 @@ mk_base_fun_bodys (Bound 0) tt |> map (mk_base_fun_header tt) -fun mk_funorder_funs (tt : typ) = +fun mk_funorder_funs (tt : typ) (one : bool) : Term.term list = case tt of - Type("+", [ft, st]) => product (mk_funorder_funs ft) (mk_funorder_funs st) + Type("+", [ft, st]) => let + val ft_funs = mk_funorder_funs ft + val st_funs = mk_funorder_funs st + in + (if one then + (product (ft_funs true) (st_funs false)) @ (product (ft_funs false) (st_funs true)) + else + product (ft_funs false) (st_funs false)) |> map mk_sum_case - | _ => [Abs ("x", tt, HOLogic.zero), Abs ("x", tt, HOLogic.Suc_zero)] + end + | _ => if one then [Abs ("x", tt, HOLogic.Suc_zero)] else [Abs ("x", tt, HOLogic.zero)] fun mk_ext_base_funs (tt : typ) = case tt of @@ -83,7 +91,7 @@ fun mk_all_measure_funs (tt : typ) = case tt of - Type("+", _) => (mk_ext_base_funs tt) @ (mk_funorder_funs tt) + Type("+", _) => (mk_ext_base_funs tt) @ (mk_funorder_funs tt true) | _ => mk_base_funs tt fun dest_term (t : term) = @@ -137,29 +145,38 @@ in map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list) end + +fun pr_cell cell = case cell of Less _ => " < " + | LessEq _ => " <= " + | None _ => " N " + | False _ => " F " + +fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) + +fun check_col ls = (forall (fn c => is_Less c orelse is_LessEq c) ls) andalso not (forall (fn c => is_LessEq c) ls) + +fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) + +fun transform_order col order = map (fn x => if x>=col then x+1 else x) order (* simple depth-first search algorithm for the table *) - fun search_table table = case table of [] => SOME [] | _ => let - val check_col = forall (fn c => is_Less c orelse is_LessEq c) val col = find_index (check_col) (transpose table) in case col of ~1 => NONE | _ => let - val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table - val transform_order = (fn col => map (fn x => if x>=col then x+1 else x)) + val order_opt = (table, col) |-> transform_table |> search_table in case order_opt of NONE => NONE | SOME order =>SOME (col::(transform_order col order)) end end - (* find all positions of elements in a list *) fun find_index_list pred = let fun find _ [] = [] @@ -167,30 +184,30 @@ in find 0 end; (* simple breadth-first search algorithm for the table *) -(* -fun bfs_search_table tables = - case tables of +fun bfs_search_table nodes = + case nodes of [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)" - | (table::rtables) => let - val check_col = forall (fn c => is_Less c orelse is_LessEq c) - val cols = find_index_list (check_col) (transpose table) - val _ = print "table" - val _ = print table - val _ = print "possible columns:" - val _ = print cols - in case cols of - [] => NONE - | _ => let - val s = - map (fn f => f table) (map (fn col => filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col)) cols) - |> append rtables - val _ = print s - in SOME [1] - end + | (node::rnodes) => let + val (order, table) = node + in + case table of + [] => SOME (foldr (fn (c, order) => c::transform_order c order) [] (rev order)) + | _ => let + val cols = find_index_list (check_col) (transpose table) + in + case cols of + [] => NONE + | _ => let + val newtables = map (transform_table table) cols + val neworders = map (fn c => c::order) cols + val newnodes = neworders ~~ newtables + in + bfs_search_table (rnodes @ newnodes) + end + end end -fun search_table table = let val _ = bfs_search_table [table] in SOME [1] end -*) +fun nsearch_table table = bfs_search_table [([], table)] fun prove_row row (st : thm) = case row of @@ -227,11 +244,6 @@ fun pr_fun thy t i = (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t)) - -fun pr_cell cell = case cell of Less _ => " < " - | LessEq _ => " <= " - | None _ => " N " - | False _ => " F " (* fun pr_err: prints the table if tactic failed *) fun pr_err table thy tl measure_funs = @@ -266,6 +278,7 @@ val _ = writeln "Creating table" val table = map (mk_row thy measure_funs) tl val _ = writeln "Searching for lexicographic order" + (* val _ = pr_table table *) val possible_order = search_table table in case possible_order of diff -r 7901493455ca -r 87ec1ca65312 src/HOL/ex/LexOrds.thy --- a/src/HOL/ex/LexOrds.thy Sat Feb 10 17:06:40 2007 +0100 +++ b/src/HOL/ex/LexOrds.thy Tue Feb 13 10:09:21 2007 +0100 @@ -9,42 +9,16 @@ imports Main begin -use "~~/src/HOL/Tools/function_package/sum_tools.ML" -use "~~/src/HOL/Tools/function_package/fundef_common.ML" -use "~~/src/HOL/Tools/function_package/fundef_lib.ML" -use "~~/src/HOL/Tools/function_package/inductive_wrap.ML" -use "~~/src/HOL/Tools/function_package/context_tree.ML" -(* use "~~/src/HOL/Tools/function_package/fundef_tailrec.ML"*) -use "~~/src/HOL/Tools/function_package/fundef_prep.ML" -use "~~/src/HOL/Tools/function_package/fundef_proof.ML" -use "~~/src/HOL/Tools/function_package/termination.ML" -use "~~/src/HOL/Tools/function_package/mutual.ML" -use "~~/src/HOL/Tools/function_package/pattern_split.ML" -use "~~/src/HOL/Tools/function_package/auto_term.ML" -use "~~/src/HOL/Tools/function_package/fundef_package.ML" -use "~~/src/HOL/Tools/function_package/lexicographic_order.ML" -use "~~/src/HOL/Tools/function_package/fundef_datatype.ML" - - -setup FundefPackage.setup -setup LexicographicOrder.setup -setup FundefDatatype.setup - -lemmas [fundef_cong] = - let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong - map_cong - - subsection {* Trivial examples *} -fun f :: "nat \ nat" +fun identity :: "nat \ nat" where -"f n = n" +"identity n = n" -fun g :: "nat \ nat" +fun yaSuc :: "nat \ nat" where - "g 0 = 0" - "g (Suc n) = Suc (g n)" + "yaSuc 0 = 0" + "yaSuc (Suc n) = Suc (yaSuc n)" subsection {* Examples on natural numbers *} @@ -64,19 +38,14 @@ "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" -function h :: "(nat * nat) * (nat * nat) \ nat" +fun k :: "(nat * nat) * (nat * nat) \ nat" where - "h ((0,0),(0,0)) = 0" - "h ((Suc z, y), (u,v)) = h((z, y), (u, v))" (* z is descending *) - "h ((0, Suc y), (u,v)) = h((1, y), (u, v))" (* y is descending *) - "h ((0,0), (Suc u, v)) = h((1, 1), (u, v))" (* u is descending *) - "h ((0,0), (0, Suc v)) = h ((1,1), (1,v))" (* v is descending *) -by (pat_completeness, auto) + "k ((0,0),(0,0)) = 0" + "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *) + "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *) + "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *) + "k ((0,0), (0, Suc v)) = k((1,1), (1,v))" (* v is descending *) -termination by lexicographic_order - -lemma[simp]: "size x = x" -apply (induct x) apply simp_all done fun gcd2 :: "nat \ nat \ nat" where @@ -85,18 +54,43 @@ "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) else gcd2 (x - y) (Suc y))" -termination by lexicographic_order - - -function ack :: "(nat * nat) \ nat" +fun ack :: "(nat * nat) \ nat" where "ack (0, m) = Suc m" "ack (Suc n, 0) = ack(n, 1)" "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))" -by pat_completeness auto + -termination by lexicographic_order +fun greedy :: "nat * nat * nat * nat * nat => nat" +where + "greedy (Suc a, Suc b, Suc c, Suc d, Suc e) = + (if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else + (if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else + (if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else + (if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else + (if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else + (if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else + (if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else + (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else + (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else + greedy (Suc a, Suc b, Suc c, d, e))))))))))" + "greedy (a, b, c, d, e) = 0" + +fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat" +where + "blowup 0 0 0 0 0 0 0 0 0 = 0" + "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)" + "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)" + "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)" + "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)" + "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)" + "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)" + "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)" + "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)" + "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)" + + subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *} datatype tree = Node | Branch tree tree @@ -109,9 +103,6 @@ "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))" -termination by lexicographic_order - - fun acklist :: "'a list * 'a list \ 'a list" where "acklist ([], m) = ((hd m)#m)" @@ -125,55 +116,10 @@ where "evn 0 = True" | "od 0 = False" -| "evn (Suc n) = od n" +| "evn (Suc n) = od (Suc n)" | "od (Suc n) = evn n" -fun - evn2 od2 :: "(nat * nat) \ bool" -where - "evn2 (0, n) = True" - "evn2 (n, 0) = True" - "od2 (0, n) = False" - "od2 (n, 0) = False" - "evn2 (Suc n, Suc m) = od2 (Suc n, m)" - "od2 (Suc n, Suc m) = evn2 (n, Suc m)" - - -fun evn3 od3 :: "(nat * nat) \ nat" -where - "evn3 (0,n) = n" - "od3 (0,n) = n" - "evn3 (n,0) = n" - "od3 (n,0) = n" - "evn3 (Suc n, Suc m) = od3 (Suc m, n)" - "od3 (Suc n, Suc m) = evn3 (Suc m, n) + od3(n, m)" - - -fun div3r0 div3r1 div3r2 :: "(nat * nat) \ bool" -where - "div3r0 (0, 0) = True" - "div3r1 (0, 0) = False" - "div3r2 (0, 0) = False" - "div3r0 (0, Suc m) = div3r2 (0, m)" - "div3r1 (0, Suc m) = div3r0 (0, m)" - "div3r2 (0, Suc m) = div3r1 (0, m)" - "div3r0 (Suc n, 0) = div3r2 (n, 0)" - "div3r1 (Suc n, 0) = div3r0 (n, 0)" - "div3r2 (Suc n, 0) = div3r1 (n, 0)" - "div3r1 (Suc n, Suc m) = div3r2 (n, m)" - "div3r2 (Suc n, Suc m) = div3r0 (n, m)" - "div3r0 (Suc n, Suc m) = div3r1 (n, m)" -(* -lemma "i \ [] ==> sum_case (%x. size (fst x)) (%x. size (fst x)) (Inr (tl i, xa, i)) < sum_case (%x. size (fst x)) (%x. size (fst x)) ( Inl (i, xa))" -apply simp -done -*) - -lemma "i \ [] \ size (tl i) < size i" -apply simp -done - fun sizechange_f :: "'a list => 'a list => 'a list" and sizechange_g :: "'a list => 'a list => 'a list => 'a list" where @@ -183,15 +129,15 @@ fun prod :: "nat => nat => nat => nat" and -eprod :: "nat => nat => nat => nat" and -oprod :: "nat => nat => nat => nat" + eprod :: "nat => nat => nat => nat" and + oprod :: "nat => nat => nat => nat" where -"prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)" -"oprod x y z = eprod x (y - 1) (z+x)" -"eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)" + "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)" + "oprod x y z = eprod x (y - 1) (z+x)" + "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)" -function (sequential) +fun pedal :: "nat => nat => nat => nat" and coast :: "nat => nat => nat => nat" @@ -205,12 +151,14 @@ | "coast n m c = (if n < m then coast n (m - 1) (c + n) else pedal n m (c + n))" - by pat_completeness auto -lemma [simp]: "size (x::nat) = x" -by (induct x) auto - -termination apply lexicographic_order done +fun ack1 :: "nat => nat => nat" + and ack2 :: "nat => nat => nat" + where + "ack1 0 m = m+1" | + "ack1 (Suc n) m = ack2 n m" | + "ack2 n 0 = ack1 n 1" | + "ack2 n (Suc m) = ack1 n (ack2 n (Suc m))" subsection {*Examples for an unprovable termination *}