--- 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
--- 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 \<Rightarrow> nat"
where
"f n = n"
-termination by lexicographic_order
-
-
fun g :: "nat \<Rightarrow> 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) \<Rightarrow> 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) \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> 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) \<Rightarrow> 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) \<Rightarrow> 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) \<Rightarrow> 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 \<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
+*)
-termination by lexicographic_order
+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
+"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) \<Rightarrow> nat"
+function noterm :: "(nat * nat) \<Rightarrow> nat"
where
"noterm (a,b) = noterm(b,a)"
-
+by pat_completeness auto
(* termination by apply lexicographic_order*)
-fun term_but_no_prove :: "nat * nat \<Rightarrow> nat"
+function term_but_no_prove :: "nat * nat \<Rightarrow> 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 \<Rightarrow> nat"
+function no_proof :: "nat \<Rightarrow> nat"
where
"no_proof m = no_proof (Suc m)"
-
+by pat_completeness auto
(* termination by lexicographic_order *)
end
\ No newline at end of file