# HG changeset patch # User bulwahn # Date 1170849928 -3600 # Node ID 0967b03844b5cca78f92bec50c8941d9f970689a # Parent 159bfab776e2aa472a71533a0ff4bd52b54efb70 changes in lexicographic_order termination tactic diff -r 159bfab776e2 -r 0967b03844b5 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Wed Feb 07 12:08:48 2007 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Wed Feb 07 13:05:28 2007 +0100 @@ -67,13 +67,24 @@ fun mk_base_funs (tt: typ) = mk_base_fun_bodys (Bound 0) tt |> map (mk_base_fun_header tt) - + +fun mk_funorder_funs (tt : typ) = + case tt of + Type("+", [ft, st]) => product (mk_funorder_funs ft) (mk_funorder_funs st) + |> map mk_sum_case + | _ => [Abs ("x", tt, HOLogic.zero), Abs ("x", tt, HOLogic.Suc_zero)] + fun mk_ext_base_funs (tt : typ) = case tt of Type("+", [ft, st]) => product (mk_ext_base_funs ft) (mk_ext_base_funs st) |> map mk_sum_case | _ => mk_base_funs tt + +fun mk_all_measure_funs (tt : typ) = + case tt of + Type("+", _) => (mk_ext_base_funs tt) @ (mk_funorder_funs tt) + | _ => mk_base_funs tt fun dest_term (t : term) = let @@ -118,16 +129,17 @@ end end -fun mk_row (thy: theory) base_funs (t : term) = +fun mk_row (thy: theory) measure_funs (t : term) = let val (vars, prems, lhs, rhs, _) = dest_term t - val lhs_list = map (fn x => x $ lhs) base_funs - val rhs_list = map (fn x => x $ rhs) base_funs + val lhs_list = map (fn x => x $ lhs) measure_funs + val rhs_list = map (fn x => x $ rhs) measure_funs in map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list) end (* simple depth-first search algorithm for the table *) + fun search_table table = case table of [] => SOME [] @@ -146,7 +158,40 @@ | 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 _ [] = [] + | find n (x :: xs) = if pred x then n::(find (n + 1) xs) else find (n + 1) xs; + in find 0 end; + +(* simple breadth-first search algorithm for the table *) +(* +fun bfs_search_table tables = + case tables 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 + end + +fun search_table table = let val _ = bfs_search_table [table] in SOME [1] end +*) + fun prove_row row (st : thm) = case row of [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" @@ -189,14 +234,14 @@ | False _ => " F " (* fun pr_err: prints the table if tactic failed *) -fun pr_err table thy tl base_funs = +fun pr_err table thy tl measure_funs = let val gc = map (fn i => chr (i + 96)) (1 upto (length table)) - val mc = 1 upto (length base_funs) + val mc = 1 upto (length measure_funs) val tstr = (" " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ " ") mc))) :: (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc) val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc)) - val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc)) + val mstr = ("Measures:"::(map2 (pr_fun thy) measure_funs mc)) val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table)) in tstr @ gstr @ mstr @ ustr @@ -217,17 +262,17 @@ val (var, prop) = FundefLib.dest_all wf val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of val crel = cterm_of thy rel - val base_funs = mk_ext_base_funs (fastype_of var) + val measure_funs = mk_all_measure_funs (fastype_of var) val _ = writeln "Creating table" - val table = map (mk_row thy base_funs) tl + val table = map (mk_row thy measure_funs) tl val _ = writeln "Searching for lexicographic order" val possible_order = search_table table in case possible_order of - NONE => error (cat_lines ("Could not find lexicographic termination order:"::(pr_err table thy tl base_funs))) + NONE => error (cat_lines ("Could not find lexicographic termination order:"::(pr_err table thy tl measure_funs))) | SOME order => let val clean_table = map (fn x => map (nth x) order) table - val funs = map (nth base_funs) order + val funs = map (nth measure_funs) order val list = HOLogic.mk_list (fastype_of var --> HOLogic.natT) funs val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list) val crelterm = cterm_of thy relterm diff -r 159bfab776e2 -r 0967b03844b5 src/HOL/ex/LexOrds.thy --- a/src/HOL/ex/LexOrds.thy Wed Feb 07 12:08:48 2007 +0100 +++ b/src/HOL/ex/LexOrds.thy Wed Feb 07 13:05:28 2007 +0100 @@ -9,22 +9,43 @@ 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" where "f n = n" -termination by lexicographic_order - - fun g :: "nat \ nat" where "g 0 = 0" "g (Suc n) = Suc (g n)" -termination by lexicographic_order - subsection {* Examples on natural numbers *} @@ -35,8 +56,6 @@ "bin (0, Suc m) = 0" "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)" -termination by lexicographic_order - fun t :: "(nat * nat) \ nat" where @@ -44,7 +63,6 @@ "t (n,0) = 0" "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" -termination by lexicographic_order function h :: "(nat * nat) * (nat * nat) \ nat" where @@ -57,12 +75,14 @@ termination by lexicographic_order +lemma[simp]: "size x = x" +apply (induct x) apply simp_all done fun gcd2 :: "nat \ nat \ nat" where "gcd2 x 0 = x" -| "gcd2 0 y = y" -| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) + "gcd2 0 y = y" + "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) else gcd2 (x - y) (Suc y))" termination by lexicographic_order @@ -98,8 +118,6 @@ | "acklist (n#ns, []) = acklist (ns, [n])" | "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))" -termination by lexicographic_order - subsection {* Examples with mutual recursion *} @@ -110,8 +128,6 @@ | "evn (Suc n) = od n" | "od (Suc n) = evn n" -termination by lexicographic_order - fun evn2 od2 :: "(nat * nat) \ bool" @@ -123,8 +139,6 @@ "evn2 (Suc n, Suc m) = od2 (Suc n, m)" "od2 (Suc n, Suc m) = evn2 (n, Suc m)" -termination by lexicographic_order - fun evn3 od3 :: "(nat * nat) \ nat" where @@ -135,8 +149,6 @@ "evn3 (Suc n, Suc m) = od3 (Suc m, n)" "od3 (Suc n, Suc m) = evn3 (Suc m, n) + od3(n, m)" -termination by lexicographic_order - fun div3r0 div3r1 div3r2 :: "(nat * nat) \ bool" where @@ -152,34 +164,79 @@ "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 +*) -termination by lexicographic_order +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 +"sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)" +"sizechange_g a b c = sizechange_f a (b @ c)" + + +fun + prod :: "nat => nat => nat => nat" and +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)" + + +function (sequential) + pedal :: "nat => nat => nat => nat" +and + coast :: "nat => nat => nat => nat" +where + "pedal 0 m c = c" +| "pedal n 0 c = c" +| "pedal n m c = + (if n < m then coast (n - 1) (m - 1) (c + m) + else pedal (n - 1) m (c + m))" + +| "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 subsection {*Examples for an unprovable termination *} text {* If termination cannot be proven, the tactic gives further information about unprovable subgoals on the arguments *} -fun noterm :: "(nat * nat) \ nat" +function noterm :: "(nat * nat) \ nat" where "noterm (a,b) = noterm(b,a)" - +by pat_completeness auto (* termination by apply lexicographic_order*) -fun term_but_no_prove :: "nat * nat \ nat" +function term_but_no_prove :: "nat * nat \ nat" where "term_but_no_prove (0,0) = 1" "term_but_no_prove (0, Suc b) = 0" "term_but_no_prove (Suc a, 0) = 0" "term_but_no_prove (Suc a, Suc b) = term_but_no_prove (b, a)" - +by pat_completeness auto (* termination by lexicographic_order *) text{* The tactic distinguishes between N = not provable AND F = False *} -fun no_proof :: "nat \ nat" +function no_proof :: "nat \ nat" where "no_proof m = no_proof (Suc m)" - +by pat_completeness auto (* termination by lexicographic_order *) end \ No newline at end of file