Method "lexicographic_order" now takes the same arguments as "auto"
authorkrauss
Mon May 21 16:22:46 2007 +0200 (2007-05-21)
changeset 2305534158639dc12
parent 23054 d1bbe5afa279
child 23056 448827ccd9e9
Method "lexicographic_order" now takes the same arguments as "auto"
src/HOL/Tools/function_package/lexicographic_order.ML
     1.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 21 16:19:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 21 16:22:46 2007 +0200
     1.3 @@ -114,20 +114,20 @@
     1.4                           fold_rev FundefLib.mk_forall vars
     1.5      end
     1.6      
     1.7 -fun prove (thy: theory) (t: term) =
     1.8 +fun prove (thy: theory) solve_tac (t: term) =
     1.9      cterm_of thy t |> Goal.init 
    1.10 -    |> SINGLE (CLASIMPSET auto_tac) |> the
    1.11 +    |> SINGLE solve_tac |> the
    1.12      
    1.13 -fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
    1.14 +fun mk_cell (thy : theory) solve_tac (vars, prems) (lhs, rhs) = 
    1.15      let 
    1.16        val goals = mk_goal (vars, prems, lhs, rhs) 
    1.17 -      val less_thm = goals "Orderings.ord_class.less" |> prove thy
    1.18 +      val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
    1.19      in
    1.20        if Thm.no_prems less_thm then
    1.21          Less (Goal.finish less_thm)
    1.22        else
    1.23          let
    1.24 -          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy
    1.25 +          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
    1.26          in
    1.27            if Thm.no_prems lesseq_thm then
    1.28              LessEq (Goal.finish lesseq_thm)
    1.29 @@ -137,13 +137,13 @@
    1.30          end
    1.31      end
    1.32      
    1.33 -fun mk_row (thy: theory) measure_funs (t : term) =
    1.34 +fun mk_row (thy: theory) solve_tac measure_funs (t : term) =
    1.35      let
    1.36        val (vars, prems, lhs, rhs, _) = dest_term t
    1.37        val lhs_list = map (fn x => x $ lhs) measure_funs
    1.38        val rhs_list = map (fn x => x $ rhs) measure_funs
    1.39      in
    1.40 -      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
    1.41 +      map (mk_cell thy solve_tac (vars, prems)) (lhs_list ~~ rhs_list)
    1.42      end
    1.43      
    1.44  fun pr_cell cell = case cell of Less _ => " <  " 
    1.45 @@ -261,7 +261,7 @@
    1.46        
    1.47  (* the main function: create table, search table, create relation,
    1.48     and prove the subgoals *)  
    1.49 -fun lexicographic_order_tac ctxt (st: thm) = 
    1.50 +fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
    1.51      let
    1.52        val thy = theory_of_thm st
    1.53        val premlist = prems_of st
    1.54 @@ -274,7 +274,7 @@
    1.55      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
    1.56      val measure_funs = mk_all_measure_funs domT
    1.57      val _ = writeln "Creating table"
    1.58 -    val table = map (mk_row thy measure_funs) tl
    1.59 +    val table = map (mk_row thy solve_tac measure_funs) tl
    1.60      val _ = writeln "Searching for lexicographic order"
    1.61      (* val _ = pr_table table *)
    1.62      val possible_order = search_table table
    1.63 @@ -299,9 +299,10 @@
    1.64      end
    1.65  
    1.66  (* FIXME goal addressing ?? *)
    1.67 -val lexicographic_order = Method.SIMPLE_METHOD o (fn ctxt => FundefCommon.apply_termination_rule ctxt 1 
    1.68 -                                                              THEN lexicographic_order_tac ctxt)
    1.69 +fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1 
    1.70 +                                                         THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
    1.71  
    1.72 -val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
    1.73 +val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, 
    1.74 +                                 "termination prover for lexicographic orderings")]
    1.75  
    1.76  end