# HG changeset patch
# User wenzelm
# Date 1183826352 -7200
# Node ID f25b1566f7b5cf5d95d73c5b6cc4f84be4a24170
# Parent  a7df2990f12727d865ec9d6e4c071e31b972d6b7
pr_goals: adapted Display.pretty_goals_aux;
pr_goals/prterm: proper context;
tuned;

diff -r a7df2990f127 -r f25b1566f7b5 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Sat Jul 07 12:16:20 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Sat Jul 07 18:39:12 2007 +0200
@@ -29,7 +29,7 @@
 
 fun del_index n [] = []
   | del_index n (x :: xs) =
-    if n > 0 then x :: del_index (n - 1) xs else xs 
+    if n > 0 then x :: del_index (n - 1) xs else xs
 
 fun transpose ([]::_) = []
   | transpose xss = map hd xss :: transpose (map tl xss)
@@ -37,29 +37,29 @@
 (** Matrix cell datatype **)
 
 datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
-         
+
 fun is_Less (Less _) = true
   | is_Less _ = false
-                                                        
+
 fun is_LessEq (LessEq _) = true
   | is_LessEq _ = false
-                                                            
-fun thm_of_cell (Less thm) = thm 
-  | thm_of_cell (LessEq (thm, _)) = thm 
-  | thm_of_cell (False thm) = thm 
-  | thm_of_cell (None (thm, _)) = thm 
-                  
+
+fun thm_of_cell (Less thm) = thm
+  | thm_of_cell (LessEq (thm, _)) = thm
+  | thm_of_cell (False thm) = thm
+  | thm_of_cell (None (thm, _)) = thm
+
 fun pr_cell (Less _ ) = " < "
-  | pr_cell (LessEq _) = " <=" 
+  | pr_cell (LessEq _) = " <="
   | pr_cell (None _) = " ? "
   | pr_cell (False _) = " F "
 
 
 (** Generating Measure Functions **)
 
-fun mk_comp g f = 
-    let 
-      val fT = fastype_of f 
+fun mk_comp g f =
+    let
+      val fT = fastype_of f
       val gT as (Type ("fun", [xT, _])) = fastype_of g
       val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0))))
     in
@@ -77,19 +77,19 @@
 
 fun mk_sum_case f1 f2 =
     let
-      val Type ("fun", [fT, Q]) = fastype_of f1 
+      val Type ("fun", [fT, Q]) = fastype_of f1
       val Type ("fun", [sT, _]) = fastype_of f2
     in
       Const (@{const_name "Sum_Type.sum_case"}, (fT --> Q) --> (sT --> Q) --> Type("+", [fT, sT]) --> Q) $ f1 $ f2
     end
-                 
+
 fun constant_0 T = Abs ("x", T, HOLogic.zero)
 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
 
 fun mk_funorder_funs (Type ("+", [fT, sT])) =
       map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT)
     @ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT)
-  | mk_funorder_funs T = [ constant_1 T ] 
+  | mk_funorder_funs T = [ constant_1 T ]
 
 fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
     product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
@@ -102,34 +102,34 @@
 
 
 (** Proof attempts to build the matrix **)
-           
+
 fun dest_term (t : term) =
     let
       val (vars, prop) = FundefLib.dest_all_all t
       val prems = Logic.strip_imp_prems prop
       val (lhs, rhs) = Logic.strip_imp_concl prop
-                         |> HOLogic.dest_Trueprop 
+                         |> HOLogic.dest_Trueprop
                          |> HOLogic.dest_mem |> fst
-                         |> HOLogic.dest_prod 
+                         |> HOLogic.dest_prod
     in
       (vars, prems, lhs, rhs)
     end
-    
+
 fun mk_goal (vars, prems, lhs, rhs) rel =
-    let 
+    let
       val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
-    in  
-      Logic.list_implies (prems, concl) 
+    in
+      Logic.list_implies (prems, concl)
         |> fold_rev FundefLib.mk_forall vars
     end
-    
-fun prove (thy: theory) solve_tac (t: term) =
-    cterm_of thy t |> Goal.init 
+
+fun prove thy solve_tac t =
+    cterm_of thy t |> Goal.init
     |> SINGLE solve_tac |> the
-    
-fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = 
-    let 
-      val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 
+
+fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
+    let
+      val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
       val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
     in
       if Thm.no_prems less_thm then
@@ -140,7 +140,7 @@
         in
           if Thm.no_prems lesseq_thm then
             LessEq (Goal.finish lesseq_thm, less_thm)
-          else 
+          else
             if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
             else None (lesseq_thm, less_thm)
         end
@@ -154,7 +154,7 @@
 fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (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
@@ -163,7 +163,7 @@
       let
         val col = find_index (check_col) (transpose table)
       in case col of
-           ~1 => NONE 
+           ~1 => NONE
          | _ =>
            let
              val order_opt = (table, col) |-> transform_table |> search_table
@@ -173,37 +173,37 @@
            end
       end
 
-(* find all positions of elements in a list *) 
+(* find all positions of elements in a list *)
 fun find_index_list P =
     let fun find _ [] = []
           | find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs
     in find 0 end
 
-(* simple breadth-first search algorithm for the table *) 
+(* simple breadth-first search algorithm for the table *)
 fun bfs_search_table nodes =
     case nodes of
-      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)" 
+      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)"
     | (node::rnodes) => let
-	val (order, table) = node
+        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)
+            val cols = find_index_list (check_col) (transpose table)
           in
             case cols of
-	      [] => NONE
-            | _ => let 
-              val newtables = map (transform_table table) cols 
+              [] => 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
       end
 
-fun nsearch_table table = bfs_search_table [([], table)] 	       
+fun nsearch_table table = bfs_search_table [([], table)]
 
 (** Proof Reconstruction **)
 
@@ -221,37 +221,38 @@
 (** Error reporting **)
 
 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
-       
-fun my_pr_goals st  =
-    Display.pretty_goals_aux (Sign.pp (Thm.theory_of_thm st)) "" (true, false) (Thm.nprems_of st) st
+
+fun pr_goals ctxt st =
+    Display.pretty_goals_aux (ProofContext.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
      |> Pretty.chunks
      |> Pretty.string_of
 
 fun row_index i = chr (i + 97)
 fun col_index j = string_of_int (j + 1)
 
-fun pr_unprovable_cell ((i,j), Less _) = ""
-  | pr_unprovable_cell ((i,j), LessEq (_, st)) = "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st
-  | pr_unprovable_cell ((i,j), None (st_less, st_leq)) = 
-    "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st_less
-    ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ my_pr_goals st_leq
-  | pr_unprovable_cell ((i,j), False st) = 
-    "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st
+fun pr_unprovable_cell _ ((i,j), Less _) = ""
+  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
+      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
+  | pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) =
+      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
+      ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
+  | pr_unprovable_cell ctxt ((i,j), False st) =
+      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
 
-fun pr_unprovable_subgoals table =
+fun pr_unprovable_subgoals ctxt table =
     table
      |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
      |> flat
-     |> map pr_unprovable_cell
+     |> map (pr_unprovable_cell ctxt)
 
-fun no_order_msg table thy tl measure_funs =  
-    let 
-      fun pr_fun t i = string_of_int i ^ ") " ^ string_of_cterm (cterm_of thy t)
+fun no_order_msg ctxt table tl measure_funs =
+    let
+      val prterm = ProofContext.string_of_term ctxt
+      fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
 
-      fun pr_goal t i = 
+      fun pr_goal t i =
           let
-            val (_, _, lhs, rhs) = dest_term t 
-            val prterm = string_of_cterm o (cterm_of thy)
+            val (_, _, lhs, rhs) = dest_term t
           in (* also show prems? *)
                i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
           end
@@ -262,13 +263,13 @@
                  :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
       val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
       val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
-      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals table
+      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
     in
       cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
     end
-      
+
 (** The Main Function **)
-fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
+fun lexicographic_order_tac ctxt solve_tac (st: thm) =
     let
       val thy = theory_of_thm st
       val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
@@ -276,12 +277,12 @@
       val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
 
       val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *)
-                         
+
       (* 2: create table *)
       val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
 
       val order = the (search_table table) (* 3: search table *)
-          handle Option => error (no_order_msg table thy tl measure_funs)
+          handle Option => error (no_order_msg ctxt table tl measure_funs)
 
       val clean_table = map (fn x => map (nth x) order) table
 
@@ -294,10 +295,10 @@
               THEN EVERY (map prove_row clean_table))
     end
 
-fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1 
+fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
                                                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
 
-val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, 
+val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
                                  "termination prover for lexicographic orderings")]
 
 end