1.1 --- a/src/HOL/Tools/lin_arith.ML Thu Aug 13 17:19:54 2009 +0100
1.2 +++ b/src/HOL/Tools/lin_arith.ML Fri Aug 14 13:45:52 2009 +0100
1.3 @@ -67,7 +67,7 @@
1.4 and ct = cterm_of thy t
1.5 in instantiate ([], [(cn, ct)]) @{thm le0} end;
1.6
1.7 -end;
1.8 +end; (* LA_Logic *)
1.9
1.10
1.11 (* arith context data *)
1.12 @@ -279,7 +279,7 @@
1.13
1.14
1.15 (*---------------------------------------------------------------------------*)
1.16 -(* the following code performs splitting of certain constants (e.g. min, *)
1.17 +(* the following code performs splitting of certain constants (e.g., min, *)
1.18 (* max) in a linear arithmetic problem; similar to what split_tac later does *)
1.19 (* to the proof state *)
1.20 (*---------------------------------------------------------------------------*)
1.21 @@ -342,23 +342,30 @@
1.22 (* takes a list [t1, ..., tn] to the term *)
1.23 (* tn' --> ... --> t1' --> False , *)
1.24 (* where ti' = HOLogic.dest_Trueprop ti *)
1.25 - fun REPEAT_DETERM_etac_rev_mp terms' =
1.26 - fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
1.27 - val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
1.28 - val cmap = Splitter.cmap_of_split_thms split_thms
1.29 - val splits = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
1.30 + fun REPEAT_DETERM_etac_rev_mp tms =
1.31 + fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
1.32 + HOLogic.false_const
1.33 + val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
1.34 + val cmap = Splitter.cmap_of_split_thms split_thms
1.35 + val goal_tm = REPEAT_DETERM_etac_rev_mp terms
1.36 + val splits = Splitter.split_posns cmap thy Ts goal_tm
1.37 val split_limit = Config.get ctxt split_limit
1.38 in
1.39 - if length splits > split_limit then
1.40 - (tracing ("linarith_split_limit exceeded (current value is " ^
1.41 - string_of_int split_limit ^ ")"); NONE)
1.42 - else (
1.43 - case splits of [] =>
1.44 + if length splits > split_limit then (
1.45 + tracing ("linarith_split_limit exceeded (current value is " ^
1.46 + string_of_int split_limit ^ ")");
1.47 + NONE
1.48 + ) else case splits of
1.49 + [] =>
1.50 (* split_tac would fail: no possible split *)
1.51 NONE
1.52 - | ((_, _, _, split_type, split_term) :: _) => (
1.53 - (* ignore all but the first possible split *)
1.54 - case strip_comb split_term of
1.55 + | (_, _::_, _, _, _) :: _ =>
1.56 + (* disallow a split that involves non-locally bound variables (except *)
1.57 + (* when bound by outermost meta-quantifiers) *)
1.58 + NONE
1.59 + | (_, [], _, split_type, split_term) :: _ =>
1.60 + (* ignore all but the first possible split *)
1.61 + (case strip_comb split_term of
1.62 (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
1.63 (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
1.64 let
1.65 @@ -627,12 +634,11 @@
1.66 (* out *)
1.67 | (t, ts) => (
1.68 warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
1.69 - " (with " ^ string_of_int (length ts) ^
1.70 - " argument(s)) not implemented; proof reconstruction is likely to fail");
1.71 + " (with " ^ string_of_int (length ts) ^
1.72 + " argument(s)) not implemented; proof reconstruction is likely to fail");
1.73 NONE
1.74 ))
1.75 - )
1.76 -end;
1.77 +end; (* split_once_items *)
1.78
1.79 (* remove terms that do not satisfy 'p'; change the order of the remaining *)
1.80 (* terms in the same way as filter_prems_tac does *)
1.81 @@ -651,29 +657,32 @@
1.82
1.83 fun negated_term_occurs_positively (terms : term list) : bool =
1.84 List.exists
1.85 - (fn (Trueprop $ (Const ("Not", _) $ t)) => member Pattern.aeconv terms (Trueprop $ t)
1.86 - | _ => false)
1.87 + (fn (Trueprop $ (Const ("Not", _) $ t)) =>
1.88 + member Pattern.aeconv terms (Trueprop $ t)
1.89 + | _ => false)
1.90 terms;
1.91
1.92 fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
1.93 let
1.94 (* repeatedly split (including newly emerging subgoals) until no further *)
1.95 (* splitting is possible *)
1.96 - fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
1.97 - | split_loop (subgoal::subgoals) = (
1.98 - case split_once_items ctxt subgoal of
1.99 - SOME new_subgoals => split_loop (new_subgoals @ subgoals)
1.100 - | NONE => subgoal :: split_loop subgoals
1.101 - )
1.102 + fun split_loop ([] : (typ list * term list) list) =
1.103 + ([] : (typ list * term list) list)
1.104 + | split_loop (subgoal::subgoals) =
1.105 + (case split_once_items ctxt subgoal of
1.106 + SOME new_subgoals => split_loop (new_subgoals @ subgoals)
1.107 + | NONE => subgoal :: split_loop subgoals)
1.108 fun is_relevant t = isSome (decomp ctxt t)
1.109 (* filter_prems_tac is_relevant: *)
1.110 val relevant_terms = filter_prems_tac_items is_relevant terms
1.111 (* split_tac, NNF normalization: *)
1.112 val split_goals = split_loop [(Ts, relevant_terms)]
1.113 (* necessary because split_once_tac may normalize terms: *)
1.114 - val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
1.115 + val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
1.116 + split_goals
1.117 (* TRY (etac notE) THEN eq_assume_tac: *)
1.118 - val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
1.119 + val result = List.filter (not o negated_term_occurs_positively o snd)
1.120 + beta_eta_norm
1.121 in
1.122 result
1.123 end;
1.124 @@ -694,7 +703,8 @@
1.125 addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
1.126 not_all, not_ex, not_not]
1.127 fun prem_nnf_tac i st =
1.128 - full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
1.129 + full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset)
1.130 + i st
1.131 in
1.132
1.133 fun split_once_tac ctxt split_thms =
1.134 @@ -706,10 +716,15 @@
1.135 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
1.136 val cmap = Splitter.cmap_of_split_thms split_thms
1.137 val splits = Splitter.split_posns cmap thy Ts concl
1.138 - val split_limit = Config.get ctxt split_limit
1.139 in
1.140 - if length splits > split_limit then no_tac
1.141 - else split_tac split_thms i
1.142 + if null splits orelse length splits > Config.get ctxt split_limit then
1.143 + no_tac
1.144 + else if null (#2 (hd splits)) then
1.145 + split_tac split_thms i
1.146 + else
1.147 + (* disallow a split that involves non-locally bound variables *)
1.148 + (* (except when bound by outermost meta-quantifiers) *)
1.149 + no_tac
1.150 end)
1.151 in
1.152 EVERY' [
1.153 @@ -726,7 +741,7 @@
1.154 (* remove irrelevant premises, then split the i-th subgoal (and all new *)
1.155 (* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *)
1.156 (* subgoals and finally attempt to solve them by finding an immediate *)
1.157 -(* contradiction (i.e. a term and its negation) in their premises. *)
1.158 +(* contradiction (i.e., a term and its negation) in their premises. *)
1.159
1.160 fun pre_tac ctxt i =
1.161 let