replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
authorboehmes
Thu Jun 08 23:37:01 2017 +0200 (23 months ago)
changeset 66035de6cd60b1226
parent 66034 ded1c636aece
child 66045 f8c4442bb3a9
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
src/HOL/Int.thy
src/HOL/Tools/lin_arith.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Int.thy	Wed Jun 07 23:23:48 2017 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Jun 08 23:37:01 2017 +0200
     1.3 @@ -1713,11 +1713,7 @@
     1.4    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
     1.5    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
     1.6    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
     1.7 -          apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
     1.8 -        apply (simp_all only: algebra_simps minus_diff_eq)
     1.9 -  apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
    1.10 -  apply (simp_all only: minus_add add.assoc left_minus)
    1.11 -  done
    1.12 +  by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
    1.13  
    1.14  text \<open>Implementations.\<close>
    1.15  
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 07 23:23:48 2017 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jun 08 23:37:01 2017 +0200
     2.3 @@ -243,7 +243,7 @@
     2.4  fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
     2.5        if of_lin_arith_sort thy U then (true, member (op =) discrete D)
     2.6        else if member (op =) discrete D then (true, true) else (false, false)
     2.7 -  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
     2.8 +  | allows_lin_arith sg _ U = (of_lin_arith_sort sg U, false);
     2.9  
    2.10  fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option =
    2.11    case T of
    2.12 @@ -266,7 +266,7 @@
    2.13    | decomp_negation thy data
    2.14        ((Const (@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
    2.15        negate (decomp_typecheck thy data (T, (rel, lhs, rhs)))
    2.16 -  | decomp_negation thy data _ =
    2.17 +  | decomp_negation _ _ _ =
    2.18        NONE;
    2.19  
    2.20  fun decomp ctxt : term -> decomp option =
    2.21 @@ -280,6 +280,75 @@
    2.22    | domain_is_nat _ = false;
    2.23  
    2.24  
    2.25 +(* Abstraction of terms *)
    2.26 +
    2.27 +(*
    2.28 +  Abstract terms contain only arithmetic operators and relations.
    2.29 +
    2.30 +  When constructing an abstract term for an arbitrary term, non-arithmetic sub-terms
    2.31 +  are replaced by fresh variables which are declared in the context. Constructing
    2.32 +  an abstract term from an arbitrary term follows the strategy of decomp.
    2.33 +*)
    2.34 +
    2.35 +fun apply t u = t $ u
    2.36 +
    2.37 +fun with2 f c t u cx = f t cx ||>> f u |>> (fn (t, u) => c $ t $ u)
    2.38 +
    2.39 +fun abstract_atom (t as Free _) cx = (t, cx)
    2.40 +  | abstract_atom (t as Const _) cx = (t, cx)
    2.41 +  | abstract_atom t (cx as (terms, ctxt)) =
    2.42 +      (case AList.lookup Envir.aeconv terms t of
    2.43 +        SOME u => (u, cx)
    2.44 +      | NONE =>
    2.45 +          let
    2.46 +            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
    2.47 +            val u = Free (n, fastype_of t)
    2.48 +          in (u, ((t, u) :: terms, ctxt')) end)
    2.49 +
    2.50 +fun abstract_num t cx = if can HOLogic.dest_number t then (t, cx) else abstract_atom t cx
    2.51 +
    2.52 +fun is_field_sort (_, ctxt) T = of_field_sort (Proof_Context.theory_of ctxt) (domain_type T)
    2.53 +
    2.54 +fun is_inj_const (_, ctxt) f =
    2.55 +  let val {inj_consts, ...} = get_arith_data ctxt
    2.56 +  in member (op =) inj_consts f end
    2.57 +
    2.58 +fun abstract_arith ((c as Const (@{const_name Groups.plus}, _)) $ u1 $ u2) cx =
    2.59 +      with2 abstract_arith c u1 u2 cx
    2.60 +  | abstract_arith (t as (c as Const (@{const_name Groups.minus}, T)) $ u1 $ u2) cx =
    2.61 +      if nT T then abstract_atom t cx else with2 abstract_arith c u1 u2 cx
    2.62 +  | abstract_arith (t as (c as Const (@{const_name Groups.uminus}, T)) $ u) cx =
    2.63 +      if nT T then abstract_atom t cx else abstract_arith u cx |>> apply c
    2.64 +  | abstract_arith ((c as Const (@{const_name Suc}, _)) $ u) cx = abstract_arith u cx |>> apply c
    2.65 +  | abstract_arith ((c as Const (@{const_name Groups.times}, _)) $ u1 $ u2) cx =
    2.66 +      with2 abstract_arith c u1 u2 cx
    2.67 +  | abstract_arith (t as (c as Const (@{const_name Rings.divide}, T)) $ u1 $ u2) cx =
    2.68 +      if is_field_sort cx T then with2 abstract_arith c u1 u2 cx else abstract_atom t cx
    2.69 +  | abstract_arith (t as (c as Const f) $ u) cx =
    2.70 +      if is_inj_const cx f then abstract_arith u cx |>> apply c else abstract_num t cx
    2.71 +  | abstract_arith t cx = abstract_num t cx
    2.72 +
    2.73 +fun is_lin_arith_rel @{const_name Orderings.less} = true
    2.74 +  | is_lin_arith_rel @{const_name Orderings.less_eq} = true
    2.75 +  | is_lin_arith_rel @{const_name HOL.eq} = true
    2.76 +  | is_lin_arith_rel _ = false
    2.77 +
    2.78 +fun is_lin_arith_type (_, ctxt) T =
    2.79 +  let val {discrete, ...} = get_arith_data ctxt
    2.80 +  in fst (allows_lin_arith (Proof_Context.theory_of ctxt) discrete T) end
    2.81 +
    2.82 +fun abstract_rel (t as (r as Const (rel, Type ("fun", [U, _]))) $ lhs $ rhs) cx =
    2.83 +      if is_lin_arith_rel rel andalso is_lin_arith_type cx U then with2 abstract_arith r lhs rhs cx
    2.84 +      else abstract_atom t cx
    2.85 +  | abstract_rel t cx = abstract_atom t cx
    2.86 +
    2.87 +fun abstract_neg ((c as Const (@{const_name Not}, _)) $ t) cx = abstract_rel t cx |>> apply c
    2.88 +  | abstract_neg t cx = abstract_rel t cx
    2.89 +
    2.90 +fun abstract ((c as Const (@{const_name Trueprop}, _)) $ t) cx = abstract_neg t cx |>> apply c
    2.91 +  | abstract t cx = abstract_atom t cx
    2.92 +
    2.93 +
    2.94  (*---------------------------------------------------------------------------*)
    2.95  (* the following code performs splitting of certain constants (e.g., min,    *)
    2.96  (* max) in a linear arithmetic problem; similar to what split_tac later does *)
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 07 23:23:48 2017 +0200
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 08 23:37:01 2017 +0200
     3.3 @@ -49,6 +49,12 @@
     3.4    val decomp: Proof.context -> term -> decomp option
     3.5    val domain_is_nat: term -> bool
     3.6  
     3.7 +  (*abstraction for proof replay*)
     3.8 +  val abstract_arith: term -> (term * term) list * Proof.context ->
     3.9 +    term * ((term * term) list * Proof.context)
    3.10 +  val abstract: term -> (term * term) list * Proof.context ->
    3.11 +    term * ((term * term) list * Proof.context)
    3.12 +
    3.13    (*preprocessing, performed on a representation of subgoals as list of premises:*)
    3.14    val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list
    3.15  
    3.16 @@ -288,7 +294,7 @@
    3.17  fun extract_first p =
    3.18    let
    3.19      fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
    3.20 -      | extract xs [] = raise List.Empty
    3.21 +      | extract _ [] = raise List.Empty
    3.22    in extract [] end;
    3.23  
    3.24  fun print_ineqs ctxt ineqs =
    3.25 @@ -373,7 +379,7 @@
    3.26  with 0 <= n.
    3.27  *)
    3.28  local
    3.29 -  exception FalseE of thm
    3.30 +  exception FalseE of thm * (int * cterm) list * Proof.context
    3.31  in
    3.32  
    3.33  fun mkthm ctxt asms (just: injust) =
    3.34 @@ -439,29 +445,53 @@
    3.35                   | THM _ => mult_by_add n thm
    3.36            end);
    3.37  
    3.38 -    fun mult_thm (n, thm) =
    3.39 +    fun mult_thm n thm =
    3.40        if n = ~1 then thm RS LA_Logic.sym
    3.41        else if n < 0 then mult (~n) thm RS LA_Logic.sym
    3.42        else mult n thm;
    3.43  
    3.44 -    fun simp thm =
    3.45 +    fun simp thm (cx as (_, hyps, ctxt')) =
    3.46        let val thm' = trace_thm ctxt ["Simplified:"] (full_simplify simpset_ctxt thm)
    3.47 -      in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
    3.48 +      in if LA_Logic.is_False thm' then raise FalseE (thm', hyps, ctxt') else (thm', cx) end;
    3.49 +
    3.50 +    fun abs_thm i (cx as (terms, hyps, ctxt)) =
    3.51 +      (case AList.lookup (op =) hyps i of
    3.52 +        SOME ct => (Thm.assume ct, cx)
    3.53 +      | NONE =>
    3.54 +          let
    3.55 +            val thm = nth asms i
    3.56 +            val (t, (terms', ctxt')) = LA_Data.abstract (Thm.prop_of thm) (terms, ctxt)
    3.57 +            val ct = Thm.cterm_of ctxt' t
    3.58 +          in (Thm.assume ct, (terms', (i, ct) :: hyps, ctxt')) end);
    3.59 +
    3.60 +    fun nat_thm t (terms, hyps, ctxt) =
    3.61 +      let val (t', (terms', ctxt')) = LA_Data.abstract_arith t (terms, ctxt)
    3.62 +      in (LA_Logic.mk_nat_thm thy t', (terms', hyps, ctxt')) end;
    3.63  
    3.64 -    fun mk (Asm i) = trace_thm ctxt ["Asm " ^ string_of_int i] (nth asms i)
    3.65 -      | mk (Nat i) = trace_thm ctxt ["Nat " ^ string_of_int i] (LA_Logic.mk_nat_thm thy (nth atoms i))
    3.66 -      | mk (LessD j) = trace_thm ctxt ["L"] (hd ([mk j] RL lessD))
    3.67 -      | mk (NotLeD j) = trace_thm ctxt ["NLe"] (mk j RS LA_Logic.not_leD)
    3.68 -      | mk (NotLeDD j) = trace_thm ctxt ["NLeD"] (hd ([mk j RS LA_Logic.not_leD] RL lessD))
    3.69 -      | mk (NotLessD j) = trace_thm ctxt ["NL"] (mk j RS LA_Logic.not_lessD)
    3.70 -      | mk (Added (j1, j2)) = simp (trace_thm ctxt ["+"] (add_thms (mk j1) (mk j2)))
    3.71 -      | mk (Multiplied (n, j)) =
    3.72 -          (trace_msg ctxt ("*" ^ string_of_int n); trace_thm ctxt ["*"] (mult_thm (n, mk j)))
    3.73 +    fun step0 msg (thm, cx) = (trace_thm ctxt [msg] thm, cx)
    3.74 +    fun step1 msg j f cx = mk j cx |>> f |>> trace_thm ctxt [msg]
    3.75 +    and step2 msg j1 j2 f cx = mk j1 cx ||>> mk j2 |>> f |>> trace_thm ctxt [msg]
    3.76  
    3.77 +    and mk (Asm i) cx = step0 ("Asm " ^ string_of_int i) (abs_thm i cx)
    3.78 +      | mk (Nat i) cx = step0 ("Nat " ^ string_of_int i) (nat_thm (nth atoms i) cx)
    3.79 +      | mk (LessD j) cx = step1 "L" j (fn thm => hd ([thm] RL lessD)) cx
    3.80 +      | mk (NotLeD j) cx = step1 "NLe" j (fn thm => thm RS LA_Logic.not_leD) cx
    3.81 +      | mk (NotLeDD j) cx = step1 "NLeD" j (fn thm => hd ([thm RS LA_Logic.not_leD] RL lessD)) cx
    3.82 +      | mk (NotLessD j) cx = step1 "NL" j (fn thm => thm RS LA_Logic.not_lessD) cx
    3.83 +      | mk (Added (j1, j2)) cx = step2 "+" j1 j2 (uncurry add_thms) cx |-> simp
    3.84 +      | mk (Multiplied (n, j)) cx =
    3.85 +          (trace_msg ctxt ("*" ^ string_of_int n); step1 "*" j (mult_thm n) cx)
    3.86 +
    3.87 +    fun finish ctxt' hyps thm =
    3.88 +      thm
    3.89 +      |> fold_rev (Thm.implies_intr o snd) hyps
    3.90 +      |> singleton (Variable.export ctxt' ctxt)
    3.91 +      |> fold (fn (i, _) => fn thm => nth asms i RS thm) hyps
    3.92    in
    3.93      let
    3.94        val _ = trace_msg ctxt "mkthm";
    3.95 -      val thm = trace_thm ctxt ["Final thm:"] (mk just);
    3.96 +      val (thm, (_, hyps, ctxt')) = mk just ([], [], ctxt);
    3.97 +      val _ = trace_thm ctxt ["Final thm:"] thm;
    3.98        val fls = simplify simpset_ctxt thm;
    3.99        val _ = trace_thm ctxt ["After simplification:"] fls;
   3.100        val _ =
   3.101 @@ -472,8 +502,9 @@
   3.102              ["Proved:", Thm.string_of_thm ctxt fls, ""]));
   3.103            warning "Linear arithmetic should have refuted the assumptions.\n\
   3.104              \Please inform Tobias Nipkow.")
   3.105 -    in fls end
   3.106 -    handle FalseE thm => trace_thm ctxt ["False reached early:"] thm
   3.107 +    in finish ctxt' hyps fls end
   3.108 +    handle FalseE (thm, hyps, ctxt') =>
   3.109 +      trace_thm ctxt ["False reached early:"] (finish ctxt' hyps thm)
   3.110    end;
   3.111  
   3.112  end;
   3.113 @@ -555,7 +586,7 @@
   3.114    fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) :
   3.115                 (LA_Data.decomp option * bool) list list =
   3.116    let
   3.117 -    fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) :
   3.118 +    fun elim_neq' _ ([] : (LA_Data.decomp option * bool) list) :
   3.119                    (LA_Data.decomp option * bool) list list =
   3.120            [[]]
   3.121        | elim_neq' nat_only ((NONE, is_nat) :: ineqs) =