--- 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
--- 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 \<Rightarrow> nat"
+fun identity :: "nat \<Rightarrow> nat"
where
-"f n = n"
+"identity n = n"
-fun g :: "nat \<Rightarrow> nat"
+fun yaSuc :: "nat \<Rightarrow> 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) \<Rightarrow> nat"
+fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> 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) \<Rightarrow> nat"
+fun ack :: "(nat * nat) \<Rightarrow> 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 \<Rightarrow> '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) \<Rightarrow> 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) \<Rightarrow> 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) \<Rightarrow> 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 \<noteq> [] ==> 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 \<noteq> [] \<Longrightarrow> 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 *}