1(* Title: HOL/Tools/Function/lexicographic_order.ML 2 Author: Lukas Bulwahn, TU Muenchen 3 Author: Alexander Krauss, TU Muenchen 4 5Termination proofs with lexicographic orders. 6*) 7 8signature LEXICOGRAPHIC_ORDER = 9sig 10 val lex_order_tac : bool -> Proof.context -> tactic -> tactic 11 val lexicographic_order_tac : bool -> Proof.context -> tactic 12end 13 14structure Lexicographic_Order : LEXICOGRAPHIC_ORDER = 15struct 16 17open Function_Lib 18 19(** General stuff **) 20 21fun mk_measures domT mfuns = 22 let 23 val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) 24 val mlexT = (domT --> HOLogic.natT) --> relT --> relT 25 fun mk_ms [] = Const (\<^const_abbrev>\<open>Set.empty\<close>, relT) 26 | mk_ms (f::fs) = 27 Const (\<^const_name>\<open>mlex_prod\<close>, mlexT) $ f $ mk_ms fs 28 in 29 mk_ms mfuns 30 end 31 32fun del_index n [] = [] 33 | del_index n (x :: xs) = 34 if n > 0 then x :: del_index (n - 1) xs else xs 35 36fun transpose ([]::_) = [] 37 | transpose xss = map hd xss :: transpose (map tl xss) 38 39(** Matrix cell datatype **) 40 41datatype cell = 42 Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm; 43 44fun is_Less lcell = case Lazy.force lcell of Less _ => true | _ => false; 45fun is_LessEq lcell = case Lazy.force lcell of LessEq _ => true | _ => false; 46 47 48(** Proof attempts to build the matrix **) 49 50fun dest_term t = 51 let 52 val (vars, prop) = Function_Lib.dest_all_all t 53 val (prems, concl) = Logic.strip_horn prop 54 val (lhs, rhs) = concl 55 |> HOLogic.dest_Trueprop 56 |> HOLogic.dest_mem |> fst 57 |> HOLogic.dest_prod 58 in 59 (vars, prems, lhs, rhs) 60 end 61 62fun mk_goal (vars, prems, lhs, rhs) rel = 63 let 64 val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop 65 in 66 fold_rev Logic.all vars (Logic.list_implies (prems, concl)) 67 end 68 69fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ => 70 let 71 val goals = Thm.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 72 in 73 (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less\<close>) solve_tac of 74 Solved thm => Less thm 75 | Stuck thm => 76 (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less_eq\<close>) solve_tac of 77 Solved thm2 => LessEq (thm2, thm) 78 | Stuck thm2 => 79 if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] then False thm2 80 else None (thm2, thm) 81 | _ => raise Match) (* FIXME *) 82 | _ => raise Match) 83 end); 84 85 86(** Search algorithms **) 87 88fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall is_LessEq ls) 89 90fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col) 91 92fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order 93 94(* simple depth-first search algorithm for the table *) 95fun search_table [] = SOME [] 96 | search_table table = 97 case find_index check_col (transpose table) of 98 ~1 => NONE 99 | col => 100 (case (table, col) |-> transform_table |> search_table of 101 NONE => NONE 102 | SOME order => SOME (col :: transform_order col order)) 103 104 105(** Proof Reconstruction **) 106 107fun prove_row_tac ctxt (c :: cs) = 108 (case Lazy.force c of 109 Less thm => 110 resolve_tac ctxt @{thms mlex_less} 1 111 THEN PRIMITIVE (Thm.elim_implies thm) 112 | LessEq (thm, _) => 113 resolve_tac ctxt @{thms mlex_leq} 1 114 THEN PRIMITIVE (Thm.elim_implies thm) 115 THEN prove_row_tac ctxt cs 116 | _ => raise General.Fail "lexicographic_order") 117 | prove_row_tac _ [] = no_tac; 118 119 120(** Error reporting **) 121 122fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *) 123fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *) 124 125fun pr_unprovable_cell _ ((i,j), Less _) = [] 126 | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = 127 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ 128 Goal_Display.string_of_goal ctxt st] 129 | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = 130 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ 131 Goal_Display.string_of_goal ctxt st_less ^ 132 "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ 133 Goal_Display.string_of_goal ctxt st_leq] 134 | pr_unprovable_cell ctxt ((i,j), False st) = 135 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ 136 Goal_Display.string_of_goal ctxt st] 137 138fun pr_unprovable_subgoals ctxt table = 139 table 140 |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) 141 |> flat 142 |> maps (pr_unprovable_cell ctxt) 143 144fun pr_cell (Less _ ) = " < " 145 | pr_cell (LessEq _) = " <=" 146 | pr_cell (None _) = " ? " 147 | pr_cell (False _) = " F " 148 149fun no_order_msg ctxt ltable tl measure_funs = 150 let 151 val table = map (map Lazy.force) ltable 152 val prterm = Syntax.string_of_term ctxt 153 fun pr_fun t i = string_of_int i ^ ") " ^ prterm t 154 155 fun pr_goal t i = 156 let 157 val (_, _, lhs, rhs) = dest_term t 158 in (* also show prems? *) 159 i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs 160 end 161 162 val gc = map (fn i => chr (i + 96)) (1 upto length table) 163 val mc = 1 upto length measure_funs 164 val tstr = "Result matrix:" :: (" " ^ implode (map (enclose " " " " o string_of_int) mc)) 165 :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc 166 val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc 167 val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc 168 val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table 169 in 170 cat_lines (ustr @ gstr @ mstr @ tstr @ 171 ["", "Could not find lexicographic termination order."]) 172 end 173 174(** The Main Function **) 175 176fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ => 177 let 178 val ((_ $ (_ $ rel)) :: tl) = Thm.prems_of st 179 180 val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) 181 182 val measure_funs = (* 1: generate measures *) 183 Measure_Functions.get_measure_functions ctxt domT 184 185 val table = (* 2: create table *) 186 map (fn t => map (mk_cell ctxt solve_tac (dest_term t)) measure_funs) tl 187 in 188 fn st => 189 case search_table table of 190 NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs) 191 | SOME order => 192 let 193 val clean_table = map (fn x => map (nth x) order) table 194 val relation = mk_measures domT (map (nth measure_funs) order) 195 val _ = 196 if not quiet then 197 Pretty.writeln (Pretty.block 198 [Pretty.str "Found termination order:", Pretty.brk 1, 199 Pretty.quote (Syntax.pretty_term ctxt relation)]) 200 else () 201 202 in (* 4: proof reconstruction *) 203 st |> 204 (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)]) 205 THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1)) 206 THEN (resolve_tac ctxt @{thms wf_empty} 1) 207 THEN EVERY (map (prove_row_tac ctxt) clean_table)) 208 end 209 end) 1 st; 210 211fun lexicographic_order_tac quiet ctxt = 212 TRY (Function_Common.termination_rule_tac ctxt 1) THEN 213 lex_order_tac quiet ctxt 214 (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp}))) 215 216val _ = 217 Theory.setup 218 (Context.theory_map 219 (Function_Common.set_termination_prover lexicographic_order_tac)) 220 221end; 222