src/HOL/Tools/lin_arith.ML
changeset 66035 de6cd60b1226
parent 63950 cdc1e59aa513
child 66610 98b7ba7b1e9a
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 07 23:23:48 2017 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jun 08 23:37:01 2017 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
     1.5        if of_lin_arith_sort thy U then (true, member (op =) discrete D)
     1.6        else if member (op =) discrete D then (true, true) else (false, false)
     1.7 -  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
     1.8 +  | allows_lin_arith sg _ U = (of_lin_arith_sort sg U, false);
     1.9  
    1.10  fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option =
    1.11    case T of
    1.12 @@ -266,7 +266,7 @@
    1.13    | decomp_negation thy data
    1.14        ((Const (@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
    1.15        negate (decomp_typecheck thy data (T, (rel, lhs, rhs)))
    1.16 -  | decomp_negation thy data _ =
    1.17 +  | decomp_negation _ _ _ =
    1.18        NONE;
    1.19  
    1.20  fun decomp ctxt : term -> decomp option =
    1.21 @@ -280,6 +280,75 @@
    1.22    | domain_is_nat _ = false;
    1.23  
    1.24  
    1.25 +(* Abstraction of terms *)
    1.26 +
    1.27 +(*
    1.28 +  Abstract terms contain only arithmetic operators and relations.
    1.29 +
    1.30 +  When constructing an abstract term for an arbitrary term, non-arithmetic sub-terms
    1.31 +  are replaced by fresh variables which are declared in the context. Constructing
    1.32 +  an abstract term from an arbitrary term follows the strategy of decomp.
    1.33 +*)
    1.34 +
    1.35 +fun apply t u = t $ u
    1.36 +
    1.37 +fun with2 f c t u cx = f t cx ||>> f u |>> (fn (t, u) => c $ t $ u)
    1.38 +
    1.39 +fun abstract_atom (t as Free _) cx = (t, cx)
    1.40 +  | abstract_atom (t as Const _) cx = (t, cx)
    1.41 +  | abstract_atom t (cx as (terms, ctxt)) =
    1.42 +      (case AList.lookup Envir.aeconv terms t of
    1.43 +        SOME u => (u, cx)
    1.44 +      | NONE =>
    1.45 +          let
    1.46 +            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
    1.47 +            val u = Free (n, fastype_of t)
    1.48 +          in (u, ((t, u) :: terms, ctxt')) end)
    1.49 +
    1.50 +fun abstract_num t cx = if can HOLogic.dest_number t then (t, cx) else abstract_atom t cx
    1.51 +
    1.52 +fun is_field_sort (_, ctxt) T = of_field_sort (Proof_Context.theory_of ctxt) (domain_type T)
    1.53 +
    1.54 +fun is_inj_const (_, ctxt) f =
    1.55 +  let val {inj_consts, ...} = get_arith_data ctxt
    1.56 +  in member (op =) inj_consts f end
    1.57 +
    1.58 +fun abstract_arith ((c as Const (@{const_name Groups.plus}, _)) $ u1 $ u2) cx =
    1.59 +      with2 abstract_arith c u1 u2 cx
    1.60 +  | abstract_arith (t as (c as Const (@{const_name Groups.minus}, T)) $ u1 $ u2) cx =
    1.61 +      if nT T then abstract_atom t cx else with2 abstract_arith c u1 u2 cx
    1.62 +  | abstract_arith (t as (c as Const (@{const_name Groups.uminus}, T)) $ u) cx =
    1.63 +      if nT T then abstract_atom t cx else abstract_arith u cx |>> apply c
    1.64 +  | abstract_arith ((c as Const (@{const_name Suc}, _)) $ u) cx = abstract_arith u cx |>> apply c
    1.65 +  | abstract_arith ((c as Const (@{const_name Groups.times}, _)) $ u1 $ u2) cx =
    1.66 +      with2 abstract_arith c u1 u2 cx
    1.67 +  | abstract_arith (t as (c as Const (@{const_name Rings.divide}, T)) $ u1 $ u2) cx =
    1.68 +      if is_field_sort cx T then with2 abstract_arith c u1 u2 cx else abstract_atom t cx
    1.69 +  | abstract_arith (t as (c as Const f) $ u) cx =
    1.70 +      if is_inj_const cx f then abstract_arith u cx |>> apply c else abstract_num t cx
    1.71 +  | abstract_arith t cx = abstract_num t cx
    1.72 +
    1.73 +fun is_lin_arith_rel @{const_name Orderings.less} = true
    1.74 +  | is_lin_arith_rel @{const_name Orderings.less_eq} = true
    1.75 +  | is_lin_arith_rel @{const_name HOL.eq} = true
    1.76 +  | is_lin_arith_rel _ = false
    1.77 +
    1.78 +fun is_lin_arith_type (_, ctxt) T =
    1.79 +  let val {discrete, ...} = get_arith_data ctxt
    1.80 +  in fst (allows_lin_arith (Proof_Context.theory_of ctxt) discrete T) end
    1.81 +
    1.82 +fun abstract_rel (t as (r as Const (rel, Type ("fun", [U, _]))) $ lhs $ rhs) cx =
    1.83 +      if is_lin_arith_rel rel andalso is_lin_arith_type cx U then with2 abstract_arith r lhs rhs cx
    1.84 +      else abstract_atom t cx
    1.85 +  | abstract_rel t cx = abstract_atom t cx
    1.86 +
    1.87 +fun abstract_neg ((c as Const (@{const_name Not}, _)) $ t) cx = abstract_rel t cx |>> apply c
    1.88 +  | abstract_neg t cx = abstract_rel t cx
    1.89 +
    1.90 +fun abstract ((c as Const (@{const_name Trueprop}, _)) $ t) cx = abstract_neg t cx |>> apply c
    1.91 +  | abstract t cx = abstract_atom t cx
    1.92 +
    1.93 +
    1.94  (*---------------------------------------------------------------------------*)
    1.95  (* the following code performs splitting of certain constants (e.g., min,    *)
    1.96  (* max) in a linear arithmetic problem; similar to what split_tac later does *)