src/HOL/Tools/function_package/lexicographic_order.ML
author bulwahn
Wed Nov 01 08:46:54 2006 +0100 (2006-11-01)
changeset 21131 a447addc14af
child 21201 803bc7672d17
permissions -rw-r--r--
added lexicographic_order tactic
bulwahn@21131
     1
(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
bulwahn@21131
     2
    ID:
bulwahn@21131
     3
    Author:      Lukas Bulwahn, TU Muenchen
bulwahn@21131
     4
bulwahn@21131
     5
Method for termination proofs with lexicographic orderings.
bulwahn@21131
     6
*)
bulwahn@21131
     7
bulwahn@21131
     8
signature LEXICOGRAPHIC_ORDER =
bulwahn@21131
     9
sig
bulwahn@21131
    10
    val setup: theory -> theory
bulwahn@21131
    11
end
bulwahn@21131
    12
bulwahn@21131
    13
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
bulwahn@21131
    14
struct
bulwahn@21131
    15
bulwahn@21131
    16
(* Theory dependencies *)
bulwahn@21131
    17
val measures = "List.measures"
bulwahn@21131
    18
val wf_measures = thm "wf_measures"
bulwahn@21131
    19
val measures_less = thm "measures_less"
bulwahn@21131
    20
val measures_lesseq = thm "measures_lesseq"
bulwahn@21131
    21
bulwahn@21131
    22
fun del_index (n, []) = []
bulwahn@21131
    23
  | del_index (n, x :: xs) =
bulwahn@21131
    24
      if n>0 then x :: del_index (n - 1, xs) else xs 
bulwahn@21131
    25
bulwahn@21131
    26
fun transpose ([]::_) = []
bulwahn@21131
    27
  | transpose xss = map hd xss :: transpose (map tl xss)
bulwahn@21131
    28
bulwahn@21131
    29
fun mk_sum_case (f1, f2) =
bulwahn@21131
    30
    case (fastype_of f1, fastype_of f2) of
bulwahn@21131
    31
	(Type("fun", [A, B]), Type("fun", [C, D])) =>
bulwahn@21131
    32
	if (B = D) then
bulwahn@21131
    33
            Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
bulwahn@21131
    34
	else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
bulwahn@21131
    35
      | _ => raise TERM ("mk_sum_case", [f1, f2])
bulwahn@21131
    36
bulwahn@21131
    37
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
bulwahn@21131
    38
  | dest_wf t = raise TERM ("dest_wf", [t])
bulwahn@21131
    39
bulwahn@21131
    40
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
bulwahn@21131
    41
bulwahn@21131
    42
fun is_Less cell = case cell of (Less _) => true | _ => false  
bulwahn@21131
    43
bulwahn@21131
    44
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
bulwahn@21131
    45
bulwahn@21131
    46
fun thm_of_cell cell =
bulwahn@21131
    47
    case cell of 
bulwahn@21131
    48
	Less thm => thm
bulwahn@21131
    49
      | LessEq thm => thm
bulwahn@21131
    50
      | False thm => thm
bulwahn@21131
    51
      | None thm => thm
bulwahn@21131
    52
			   
bulwahn@21131
    53
fun mk_base_fun_bodys (t : term) (tt : typ) =
bulwahn@21131
    54
    case tt of
bulwahn@21131
    55
	Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
bulwahn@21131
    56
      | _ => [(t, tt)]
bulwahn@21131
    57
	     
bulwahn@21131
    58
fun mk_base_fun_header fulltyp (t, typ) =
bulwahn@21131
    59
    if typ = HOLogic.natT then
bulwahn@21131
    60
	Abs ("x", fulltyp, t)
bulwahn@21131
    61
    else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
bulwahn@21131
    62
	 	 
bulwahn@21131
    63
fun mk_base_funs (tt: typ) = 
bulwahn@21131
    64
    mk_base_fun_bodys (Bound 0) tt |>
bulwahn@21131
    65
		      map (mk_base_fun_header tt)
bulwahn@21131
    66
		   
bulwahn@21131
    67
fun mk_ext_base_funs (tt : typ) =
bulwahn@21131
    68
    case tt of
bulwahn@21131
    69
	Type("+", [ft, st]) =>
bulwahn@21131
    70
	product (mk_ext_base_funs ft) (mk_ext_base_funs st)
bulwahn@21131
    71
        |> map mk_sum_case
bulwahn@21131
    72
      | _ => mk_base_funs tt
bulwahn@21131
    73
bulwahn@21131
    74
fun dest_term (t : term) =
bulwahn@21131
    75
    let
bulwahn@21131
    76
	val (vars, prop) = (FundefLib.dest_all_all t)
bulwahn@21131
    77
	val prems = Logic.strip_imp_prems prop
bulwahn@21131
    78
	val (tuple, rel) = Logic.strip_imp_concl prop
bulwahn@21131
    79
                           |> HOLogic.dest_Trueprop 
bulwahn@21131
    80
                           |> HOLogic.dest_mem
bulwahn@21131
    81
	val (lhs, rhs) = HOLogic.dest_prod tuple
bulwahn@21131
    82
    in
bulwahn@21131
    83
	(vars, prems, lhs, rhs, rel)
bulwahn@21131
    84
    end
bulwahn@21131
    85
bulwahn@21131
    86
fun mk_goal (vars, prems, lhs, rhs) rel =
bulwahn@21131
    87
    let 
bulwahn@21131
    88
	val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
bulwahn@21131
    89
    in	
bulwahn@21131
    90
	Logic.list_implies (prems, concl) |>
bulwahn@21131
    91
	fold_rev FundefLib.mk_forall vars
bulwahn@21131
    92
    end
bulwahn@21131
    93
bulwahn@21131
    94
fun prove (thy: theory) (t: term) =
bulwahn@21131
    95
    cterm_of thy t |> Goal.init 
bulwahn@21131
    96
    |> SINGLE (CLASIMPSET auto_tac) |> the
bulwahn@21131
    97
bulwahn@21131
    98
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
bulwahn@21131
    99
    let	
bulwahn@21131
   100
	val goals = mk_goal (vars, prems, lhs, rhs) 
bulwahn@21131
   101
	val less_thm = goals "Orderings.less" |> prove thy
bulwahn@21131
   102
    in
bulwahn@21131
   103
	if Thm.no_prems less_thm then
bulwahn@21131
   104
	    Less (Goal.finish less_thm)
bulwahn@21131
   105
	else
bulwahn@21131
   106
	    let
bulwahn@21131
   107
		val lesseq_thm = goals "Orderings.less_eq" |> prove thy
bulwahn@21131
   108
	    in
bulwahn@21131
   109
		if Thm.no_prems lesseq_thm then
bulwahn@21131
   110
		    LessEq (Goal.finish lesseq_thm)
bulwahn@21131
   111
		else 
bulwahn@21131
   112
		    if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
bulwahn@21131
   113
		    else None lesseq_thm
bulwahn@21131
   114
	    end
bulwahn@21131
   115
    end
bulwahn@21131
   116
bulwahn@21131
   117
fun mk_row (thy: theory) base_funs (t : term) =
bulwahn@21131
   118
    let
bulwahn@21131
   119
	val (vars, prems, lhs, rhs, _) = dest_term t
bulwahn@21131
   120
	val lhs_list = map (fn x => x $ lhs) base_funs
bulwahn@21131
   121
	val rhs_list = map (fn x => x $ rhs) base_funs
bulwahn@21131
   122
    in
bulwahn@21131
   123
	map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
bulwahn@21131
   124
    end
bulwahn@21131
   125
bulwahn@21131
   126
(* simple depth-first search algorithm for the table *)
bulwahn@21131
   127
fun search_table table =
bulwahn@21131
   128
    case table of
bulwahn@21131
   129
	[] => SOME []
bulwahn@21131
   130
      | _ =>
bulwahn@21131
   131
	let
bulwahn@21131
   132
	    val check_col = forall (fn c => is_Less c orelse is_LessEq c)
bulwahn@21131
   133
            val col = find_index (check_col) (transpose table)
bulwahn@21131
   134
	in case col of
bulwahn@21131
   135
	       ~1 => NONE 
bulwahn@21131
   136
             | _ =>
bulwahn@21131
   137
               let
bulwahn@21131
   138
		   val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
bulwahn@21131
   139
		   val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
bulwahn@21131
   140
               in case order_opt of
bulwahn@21131
   141
		      NONE => NONE
bulwahn@21131
   142
		    | SOME order =>SOME (col::(transform_order col order))
bulwahn@21131
   143
	       end
bulwahn@21131
   144
	end
bulwahn@21131
   145
bulwahn@21131
   146
fun prove_row row (st : thm) =
bulwahn@21131
   147
    case row of
bulwahn@21131
   148
        [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
bulwahn@21131
   149
      | cell::tail =>
bulwahn@21131
   150
	case cell of
bulwahn@21131
   151
	    Less less_thm =>
bulwahn@21131
   152
	    let
bulwahn@21131
   153
		val next_thm = st |> SINGLE (rtac measures_less 1) |> the
bulwahn@21131
   154
	    in
bulwahn@21131
   155
		implies_elim next_thm less_thm
bulwahn@21131
   156
	    end
bulwahn@21131
   157
	  | LessEq lesseq_thm =>
bulwahn@21131
   158
	    let
bulwahn@21131
   159
		val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
bulwahn@21131
   160
	    in
bulwahn@21131
   161
		implies_elim next_thm lesseq_thm |>
bulwahn@21131
   162
                prove_row tail
bulwahn@21131
   163
	    end
bulwahn@21131
   164
          | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
bulwahn@21131
   165
bulwahn@21131
   166
fun pr_unprovable_subgoals table =
bulwahn@21131
   167
    filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
bulwahn@21131
   168
	   |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
bulwahn@21131
   169
bulwahn@21131
   170
fun pr_goal thy t i = 
bulwahn@21131
   171
    let
bulwahn@21131
   172
	val (_, prems, lhs, rhs, _) = dest_term t 
bulwahn@21131
   173
	val prterm = string_of_cterm o (cterm_of thy)
bulwahn@21131
   174
    in
bulwahn@21131
   175
	(* also show prems? *)
bulwahn@21131
   176
        i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
bulwahn@21131
   177
    end
bulwahn@21131
   178
bulwahn@21131
   179
fun pr_fun thy t i =
bulwahn@21131
   180
    (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
bulwahn@21131
   181
bulwahn@21131
   182
fun pr_cell cell = case cell of Less _ => " <  " 
bulwahn@21131
   183
				| LessEq _ => " <= " 
bulwahn@21131
   184
				| None _ => " N  "
bulwahn@21131
   185
				| False _ => " F  "
bulwahn@21131
   186
       
bulwahn@21131
   187
(* fun pr_err: prints the table if tactic failed *)
bulwahn@21131
   188
fun pr_err table thy tl base_funs =  
bulwahn@21131
   189
    let 
bulwahn@21131
   190
	val gc = map (fn i => chr (i + 96)) (1 upto (length table))
bulwahn@21131
   191
	val mc = 1 upto (length base_funs)
bulwahn@21131
   192
	val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
bulwahn@21131
   193
		   (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
bulwahn@21131
   194
	val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
bulwahn@21131
   195
	val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
bulwahn@21131
   196
	val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
bulwahn@21131
   197
    in
bulwahn@21131
   198
	tstr @ gstr @ mstr @ ustr
bulwahn@21131
   199
    end
bulwahn@21131
   200
bulwahn@21131
   201
(* the main function: create table, search table, create relation,
bulwahn@21131
   202
   and prove the subgoals *)
bulwahn@21131
   203
fun lexicographic_order_tac (st: thm) = 
bulwahn@21131
   204
    let
bulwahn@21131
   205
	val thy = theory_of_thm st
bulwahn@21131
   206
        val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
bulwahn@21131
   207
	val next_st = SINGLE (rtac termination_thm 1) st |> the
bulwahn@21131
   208
        val premlist = prems_of next_st
bulwahn@21131
   209
    in
bulwahn@21131
   210
        case premlist of 
bulwahn@21131
   211
            [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
bulwahn@21131
   212
          | (wf::tl) => let
bulwahn@21131
   213
		val (var, prop) = FundefLib.dest_all wf
bulwahn@21131
   214
		val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
bulwahn@21131
   215
		val crel = cterm_of thy rel
bulwahn@21131
   216
		val base_funs = mk_ext_base_funs (fastype_of var)
bulwahn@21131
   217
		val _ = writeln "Creating table"
bulwahn@21131
   218
		val table = map (mk_row thy base_funs) tl
bulwahn@21131
   219
		val _ = writeln "Searching for lexicographic order"
bulwahn@21131
   220
		val possible_order = search_table table
bulwahn@21131
   221
	    in
bulwahn@21131
   222
		case possible_order of 
bulwahn@21131
   223
		    NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
bulwahn@21131
   224
		  | SOME order  => let
bulwahn@21131
   225
			val clean_table = map (fn x => map (nth x) order) table
bulwahn@21131
   226
			val funs = map (nth base_funs) order
bulwahn@21131
   227
			val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
bulwahn@21131
   228
			val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
bulwahn@21131
   229
			val crelterm = cterm_of thy relterm
bulwahn@21131
   230
			val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
bulwahn@21131
   231
			val _ = writeln "Proving subgoals"
bulwahn@21131
   232
		    in
bulwahn@21131
   233
			next_st |> cterm_instantiate [(crel, crelterm)]
bulwahn@21131
   234
				|> SINGLE (rtac wf_measures 1) |> the
bulwahn@21131
   235
				|> fold prove_row clean_table
bulwahn@21131
   236
				|> Seq.single
bulwahn@21131
   237
                    end
bulwahn@21131
   238
            end
bulwahn@21131
   239
    end
bulwahn@21131
   240
bulwahn@21131
   241
val setup = Method.add_methods [("lexicographic_order", Method.no_args (Method.SIMPLE_METHOD lexicographic_order_tac), "termination prover for lexicographic orderings")]
bulwahn@21131
   242
bulwahn@21131
   243
end