# HG changeset patch
# User bulwahn
# Date 1162367214 -3600
# Node ID a447addc14af9847ee511ab3cad418cc7cce00d3
# Parent  c725181f5117d6645421368de042fc3497366ff3
added lexicographic_order tactic

diff -r c725181f5117 -r a447addc14af src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 31 14:59:27 2006 +0100
+++ b/src/HOL/List.thy	Wed Nov 01 08:46:54 2006 +0100
@@ -2428,7 +2428,8 @@
 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
   by auto
 
-
+use "Tools/function_package/lexicographic_order.ML"
+setup {* LexicographicOrder.setup *}
 
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 
diff -r c725181f5117 -r a447addc14af src/HOL/Tools/function_package/lexicographic_order.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Nov 01 08:46:54 2006 +0100
@@ -0,0 +1,243 @@
+(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
+    ID:
+    Author:      Lukas Bulwahn, TU Muenchen
+
+Method for termination proofs with lexicographic orderings.
+*)
+
+signature LEXICOGRAPHIC_ORDER =
+sig
+    val setup: theory -> theory
+end
+
+structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
+struct
+
+(* Theory dependencies *)
+val measures = "List.measures"
+val wf_measures = thm "wf_measures"
+val measures_less = thm "measures_less"
+val measures_lesseq = thm "measures_lesseq"
+
+fun del_index (n, []) = []
+  | del_index (n, x :: xs) =
+      if n>0 then x :: del_index (n - 1, xs) else xs 
+
+fun transpose ([]::_) = []
+  | transpose xss = map hd xss :: transpose (map tl xss)
+
+fun mk_sum_case (f1, f2) =
+    case (fastype_of f1, fastype_of f2) of
+	(Type("fun", [A, B]), Type("fun", [C, D])) =>
+	if (B = D) then
+            Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
+	else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
+      | _ => raise TERM ("mk_sum_case", [f1, f2])
+
+fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
+  | dest_wf t = raise TERM ("dest_wf", [t])
+
+datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
+
+fun is_Less cell = case cell of (Less _) => true | _ => false  
+
+fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
+
+fun thm_of_cell cell =
+    case cell of 
+	Less thm => thm
+      | LessEq thm => thm
+      | False thm => thm
+      | None thm => thm
+			   
+fun mk_base_fun_bodys (t : term) (tt : typ) =
+    case tt of
+	Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
+      | _ => [(t, tt)]
+	     
+fun mk_base_fun_header fulltyp (t, typ) =
+    if typ = HOLogic.natT then
+	Abs ("x", fulltyp, t)
+    else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
+	 	 
+fun mk_base_funs (tt: typ) = 
+    mk_base_fun_bodys (Bound 0) tt |>
+		      map (mk_base_fun_header tt)
+		   
+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 dest_term (t : term) =
+    let
+	val (vars, prop) = (FundefLib.dest_all_all t)
+	val prems = Logic.strip_imp_prems prop
+	val (tuple, rel) = Logic.strip_imp_concl prop
+                           |> HOLogic.dest_Trueprop 
+                           |> HOLogic.dest_mem
+	val (lhs, rhs) = HOLogic.dest_prod tuple
+    in
+	(vars, prems, lhs, rhs, rel)
+    end
+
+fun mk_goal (vars, prems, lhs, rhs) rel =
+    let 
+	val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
+    in	
+	Logic.list_implies (prems, concl) |>
+	fold_rev FundefLib.mk_forall vars
+    end
+
+fun prove (thy: theory) (t: term) =
+    cterm_of thy t |> Goal.init 
+    |> SINGLE (CLASIMPSET auto_tac) |> the
+
+fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
+    let	
+	val goals = mk_goal (vars, prems, lhs, rhs) 
+	val less_thm = goals "Orderings.less" |> prove thy
+    in
+	if Thm.no_prems less_thm then
+	    Less (Goal.finish less_thm)
+	else
+	    let
+		val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+	    in
+		if Thm.no_prems lesseq_thm then
+		    LessEq (Goal.finish lesseq_thm)
+		else 
+		    if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
+		    else None lesseq_thm
+	    end
+    end
+
+fun mk_row (thy: theory) base_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
+    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 []
+      | _ =>
+	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))
+               in case order_opt of
+		      NONE => NONE
+		    | SOME order =>SOME (col::(transform_order col order))
+	       end
+	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)" 
+      | cell::tail =>
+	case cell of
+	    Less less_thm =>
+	    let
+		val next_thm = st |> SINGLE (rtac measures_less 1) |> the
+	    in
+		implies_elim next_thm less_thm
+	    end
+	  | LessEq lesseq_thm =>
+	    let
+		val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
+	    in
+		implies_elim next_thm lesseq_thm |>
+                prove_row tail
+	    end
+          | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
+
+fun pr_unprovable_subgoals table =
+    filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
+	   |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
+
+fun pr_goal thy t i = 
+    let
+	val (_, prems, lhs, rhs, _) = dest_term t 
+	val prterm = string_of_cterm o (cterm_of thy)
+    in
+	(* also show prems? *)
+        i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
+    end
+
+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 base_funs =  
+    let 
+	val gc = map (fn i => chr (i + 96)) (1 upto (length table))
+	val mc = 1 upto (length base_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 ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
+    in
+	tstr @ gstr @ mstr @ ustr
+    end
+
+(* the main function: create table, search table, create relation,
+   and prove the subgoals *)
+fun lexicographic_order_tac (st: thm) = 
+    let
+	val thy = theory_of_thm st
+        val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
+	val next_st = SINGLE (rtac termination_thm 1) st |> the
+        val premlist = prems_of next_st
+    in
+        case premlist of 
+            [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
+          | (wf::tl) => let
+		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 _ = writeln "Creating table"
+		val table = map (mk_row thy base_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 prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+		  | SOME order  => let
+			val clean_table = map (fn x => map (nth x) order) table
+			val funs = map (nth base_funs) order
+			val list = HOLogic.mk_list (fn x => x) (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
+			val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
+			val _ = writeln "Proving subgoals"
+		    in
+			next_st |> cterm_instantiate [(crel, crelterm)]
+				|> SINGLE (rtac wf_measures 1) |> the
+				|> fold prove_row clean_table
+				|> Seq.single
+                    end
+            end
+    end
+
+val setup = Method.add_methods [("lexicographic_order", Method.no_args (Method.SIMPLE_METHOD lexicographic_order_tac), "termination prover for lexicographic orderings")]
+
+end
\ No newline at end of file
diff -r c725181f5117 -r a447addc14af src/HOL/ex/LexOrds.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/LexOrds.thy	Wed Nov 01 08:46:54 2006 +0100
@@ -0,0 +1,185 @@
+(* Title:       HOL/ex/LexOrds.thy
+   ID:
+   Author:      Lukas Bulwahn, TU Muenchen
+
+Examples for functions whose termination is proven by lexicographic order.
+*)
+ 
+theory LexOrds
+imports Main
+begin
+
+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 *}
+
+fun bin :: "(nat * nat) \<Rightarrow> nat"
+where
+  "bin (0, 0) = 1"
+  "bin (Suc n, 0) = 0"
+  "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
+  "t (0,n) = 0"
+  "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
+  "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)
+
+termination by lexicographic_order
+
+
+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)
+                                    else gcd2 (x - y) (Suc y))"
+
+termination by lexicographic_order
+
+
+function 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
+
+subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
+
+datatype tree = Node | Branch tree tree
+
+fun g_tree :: "tree * tree \<Rightarrow> tree"
+where
+  "g_tree (Node, Node) = Node"
+  "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
+  "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
+  "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)"
+|  "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 *}
+
+fun evn od :: "nat \<Rightarrow> bool"
+where
+  "evn 0 = True"
+| "od 0 = False"
+| "evn (Suc n) = od n"
+| "od (Suc n) = evn n"
+
+termination by lexicographic_order
+
+
+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)"
+
+termination by lexicographic_order
+
+
+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)"
+
+termination by lexicographic_order
+
+
+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)"
+
+termination by lexicographic_order
+
+
+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"
+where
+  "noterm (a,b) = noterm(b,a)"
+
+(* termination by apply lexicographic_order*)
+
+fun 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)"
+
+(* termination by lexicographic_order *)
+
+text{* The tactic distinguishes between N = not provable AND F = False *}
+fun no_proof :: "nat \<Rightarrow> nat"
+where
+  "no_proof m = no_proof (Suc m)"
+
+(* termination by lexicographic_order *)
+
+end
\ No newline at end of file