Restructured lin.arith.package.
authornipkow
Thu Sep 23 09:04:36 1999 +0200 (1999-09-23 ago)
changeset 75822650c9c2ab7f
parent 7581 18070ae7a84c
child 7583 d1b40e0464b1
Restructured lin.arith.package.
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Sep 22 21:49:37 1999 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Sep 23 09:04:36 1999 +0200
     1.3 @@ -890,29 +890,18 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
     1.8 -struct
     1.9 -
    1.10 -val lessD = [Suc_leI];
    1.11 -
    1.12 -(* reduce contradictory <= to False.
    1.13 -   Most of the work is done by the cancel tactics.
    1.14 -*)
    1.15 -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
    1.16 +signature LIN_ARITH_DATA2 =
    1.17 +sig
    1.18 +  include LIN_ARITH_DATA
    1.19 +  val discrete: (string * bool)list ref
    1.20 +end;
    1.21  
    1.22 -val cancel_sums_ss = HOL_basic_ss addsimps add_rules
    1.23 -                                  addsimprocs nat_cancel_sums_add;
    1.24 -
    1.25 -val simp = simplify cancel_sums_ss;
    1.26 -
    1.27 -val add_mono_thms = map (fn s => prove_goal Arith.thy s
    1.28 - (fn prems => [cut_facts_tac prems 1,
    1.29 -               blast_tac (claset() addIs [add_le_mono]) 1]))
    1.30 -["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
    1.31 - "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
    1.32 - "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
    1.33 - "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
    1.34 -];
    1.35 +structure LA_Data_Ref: LIN_ARITH_DATA2 =
    1.36 +struct
    1.37 +  val add_mono_thms = ref ([]:thm list);
    1.38 +  val lessD = ref ([]:thm list);
    1.39 +  val ss_ref = ref HOL_basic_ss;
    1.40 +  val discrete = ref ([]:(string*bool)list);
    1.41  
    1.42  (* Decomposition of terms *)
    1.43  
    1.44 @@ -953,31 +942,44 @@
    1.45  fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
    1.46    | negate None = None;
    1.47  
    1.48 -fun decomp1 tab (T,xxx) =
    1.49 +fun decomp1 (T,xxx) =
    1.50    (case T of
    1.51       Type("fun",[Type(D,[]),_]) =>
    1.52 -       (case assoc(!tab,D) of
    1.53 +       (case assoc(!discrete,D) of
    1.54            None => None
    1.55          | Some d => (case decomp2 xxx of
    1.56                         None => None
    1.57                       | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
    1.58     | _ => None);
    1.59  
    1.60 -(* tab: (string * bool)list ref  contains the discreteneness flag *)
    1.61 -fun decomp tab (_$(Const(rel,T)$lhs$rhs)) = decomp1 tab (T,(rel,lhs,rhs))
    1.62 -  | decomp tab (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    1.63 -      negate(decomp1 tab (T,(rel,lhs,rhs)))
    1.64 -  | decomp _ _ = None
    1.65 -
    1.66 +fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs))
    1.67 +  | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    1.68 +      negate(decomp1 (T,(rel,lhs,rhs)))
    1.69 +  | decomp _ = None
    1.70  end;
    1.71  
    1.72 -structure LA_Data_Ref =
    1.73 -struct
    1.74 -  val add_mono_thms = ref Nat_LA_Data.add_mono_thms
    1.75 -  val lessD = ref Nat_LA_Data.lessD
    1.76 -  val simp = ref Nat_LA_Data.simp
    1.77 -  val discrete = ref [("nat",true)]
    1.78 -  val decomp = Nat_LA_Data.decomp discrete
    1.79 +let
    1.80 +
    1.81 +(* reduce contradictory <= to False.
    1.82 +   Most of the work is done by the cancel tactics.
    1.83 +*)
    1.84 +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
    1.85 +
    1.86 +val add_mono_thms = map (fn s => prove_goal Arith.thy s
    1.87 + (fn prems => [cut_facts_tac prems 1,
    1.88 +               blast_tac (claset() addIs [add_le_mono]) 1]))
    1.89 +["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
    1.90 + "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
    1.91 + "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
    1.92 + "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
    1.93 +];
    1.94 +
    1.95 +in
    1.96 +LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
    1.97 +LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI];
    1.98 +LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
    1.99 +                      addsimprocs nat_cancel_sums_add;
   1.100 +LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)]
   1.101  end;
   1.102  
   1.103  structure Fast_Arith =
   1.104 @@ -985,14 +987,16 @@
   1.105  
   1.106  val fast_arith_tac = Fast_Arith.lin_arith_tac;
   1.107  
   1.108 +let
   1.109  val nat_arith_simproc_pats =
   1.110    map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
   1.111        ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
   1.112  
   1.113 -val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
   1.114 -                                        Fast_Arith.lin_arith_prover;
   1.115 -
   1.116 -Addsimprocs [fast_nat_arith_simproc];
   1.117 +val fast_nat_arith_simproc = mk_simproc
   1.118 +  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
   1.119 +in
   1.120 +Addsimprocs [fast_nat_arith_simproc]
   1.121 +end;
   1.122  
   1.123  (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   1.124  useful to detect inconsistencies among the premises for subgoals which are
   1.125 @@ -1017,9 +1021,10 @@
   1.126     (max m n + k <= r) = (m+k <= r & n+k <= r)
   1.127     (l <= min m n + k) = (l <= m+k & l <= n+k)
   1.128  *)
   1.129 -val arith_tac =
   1.130 -  refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
   1.131 -             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
   1.132 +val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max];
   1.133 +fun arith_tac i =
   1.134 +  refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms))
   1.135 +             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i;
   1.136  
   1.137  
   1.138  (* proof method setup *)
     2.1 --- a/src/HOL/Integ/Bin.ML	Wed Sep 22 21:49:37 1999 +0200
     2.2 +++ b/src/HOL/Integ/Bin.ML	Thu Sep 23 09:04:36 1999 +0200
     2.3 @@ -480,22 +480,17 @@
     2.4  (The latter option is very inefficient!)
     2.5  *)
     2.6  
     2.7 -structure Int_LA_Data(*: LIN_ARITH_DATA*) =
     2.8 -struct
     2.9 -
    2.10 -val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
    2.11 +(* Update parameters of arithmetic prover *)
    2.12 +let
    2.13  
    2.14  (* reduce contradictory <= to False *)
    2.15  val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
    2.16                  [int_0,zmult_0,zmult_0_right];
    2.17  
    2.18 -val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
    2.19 -          addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
    2.20 -                       Int_CC.sum_conv, Int_CC.rel_conv];
    2.21 +val simprocs = [Int_Cancel.sum_conv, Int_Cancel.rel_conv,
    2.22 +                Int_CC.sum_conv, Int_CC.rel_conv];
    2.23  
    2.24 -val simp = simplify cancel_sums_ss;
    2.25 -
    2.26 -val add_mono_thms = Nat_LA_Data.add_mono_thms @
    2.27 +val add_mono_thms =
    2.28    map (fn s => prove_goal Int.thy s
    2.29                   (fn prems => [cut_facts_tac prems 1,
    2.30                        asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
    2.31 @@ -505,31 +500,24 @@
    2.32       "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
    2.33      ];
    2.34  
    2.35 +in
    2.36 +LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
    2.37 +LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
    2.38 +LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
    2.39 +                      addsimprocs simprocs;
    2.40 +LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
    2.41  end;
    2.42  
    2.43 -(* Update parameters of arithmetic prover *)
    2.44 -LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
    2.45 -LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
    2.46 -LA_Data_Ref.simp :=          Int_LA_Data.simp;
    2.47 -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)];
    2.48 -
    2.49 -
    2.50 +let
    2.51  val int_arith_simproc_pats =
    2.52    map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
    2.53        ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
    2.54  
    2.55 -val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
    2.56 -                                        Fast_Arith.lin_arith_prover;
    2.57 -
    2.58 -Addsimprocs [fast_int_arith_simproc];
    2.59 -
    2.60 -(* FIXME: K true should be replaced by a sensible test to speed things up
    2.61 -   in case there are lots of irrelevant terms involved.
    2.62 -
    2.63 -val arith_tac =
    2.64 -  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
    2.65 -             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
    2.66 -*)
    2.67 +val fast_int_arith_simproc = mk_simproc
    2.68 +  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
    2.69 +in
    2.70 +Addsimprocs [fast_int_arith_simproc]
    2.71 +end;
    2.72  
    2.73  (* Some test data
    2.74  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Sep 22 21:49:37 1999 +0200
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Sep 23 09:04:36 1999 +0200
     3.3 @@ -17,6 +17,8 @@
     3.4  (in)equations. lin_arith_prover tries to prove or disprove the term.
     3.5  *)
     3.6  
     3.7 +(* Debugging: (*? -> (*?*), !*) -> (*!*) *)
     3.8 +
     3.9  (*** Data needed for setting up the linear arithmetic package ***)
    3.10  
    3.11  signature LIN_ARITH_LOGIC =
    3.12 @@ -54,9 +56,8 @@
    3.13                              (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *)
    3.14    val lessD:            thm list ref (* m < n ==> m+1 <= n *)
    3.15    val decomp:
    3.16 -    term ->
    3.17 -      ((term * int)list * int * string * (term * int)list * int * bool)option
    3.18 -  val simp: (thm -> thm) ref
    3.19 +    term -> ((term*int)list * int * string * (term*int)list * int * bool)option
    3.20 +  val ss_ref: simpset ref
    3.21  end;
    3.22  (*
    3.23  decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
    3.24 @@ -65,7 +66,7 @@
    3.25           of summand * multiplicity pairs and a constant summand and
    3.26           d indicates if the domain is discrete.
    3.27  
    3.28 -simp must reduce contradictory <= to False.
    3.29 +ss_ref must reduce contradictory <= to False.
    3.30     It should also cancel common summands to keep <= reduced;
    3.31     otherwise <= can grow to massive proportions.
    3.32  *)
    3.33 @@ -202,7 +203,7 @@
    3.34  
    3.35  
    3.36  fun elim ineqs =
    3.37 -  let (*val dummy = print_ineqs ineqs;*)
    3.38 +  let (*?val dummy = print_ineqs ineqs;!*)
    3.39        val (triv,nontriv) = partition is_trivial ineqs in
    3.40    if not(null triv)
    3.41    then case find_first is_answer triv of
    3.42 @@ -268,19 +269,20 @@
    3.43          in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
    3.44  
    3.45        fun simp thm =
    3.46 -        let val thm' = !LA_Data.simp thm
    3.47 +        let val thm' = simplify (!LA_Data.ss_ref) thm
    3.48          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
    3.49  
    3.50 -      fun mk(Asm i) = ((*writeln"Asm";prth*)(nth_elem(i,asms)))
    3.51 -        | mk(Nat(i)) = ((*writeln"N";*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
    3.52 -        | mk(LessD(j)) = ((*writeln"L";prth*)(hd([mk j] RL !LA_Data.lessD)))
    3.53 -        | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
    3.54 -        | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
    3.55 -        | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
    3.56 -        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2)))))
    3.57 -        | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j))
    3.58 +      fun mk(Asm i) = ((*?writeln"Asm";prth!*)(nth_elem(i,asms)))
    3.59 +        | mk(Nat(i)) = ((*?writeln"Nat";!*)LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)))
    3.60 +        | mk(LessD(j)) = ((*?writeln"L";prth!*)(hd([mk j] RL !LA_Data.lessD)))
    3.61 +        | mk(NotLeD(j)) = ((*?writeln"NLe";prth!*)(mk j RS LA_Logic.not_leD))
    3.62 +        | mk(NotLeDD(j)) = ((*?writeln"NLeD";prth!*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
    3.63 +        | mk(NotLessD(j)) = ((*?writeln"NL";prth!*)(mk j RS LA_Logic.not_lessD))
    3.64 +        | mk(Added(j1,j2)) = ((*?writeln"+";prth!*)(simp((*?prth!*)(addthms (mk j1) (mk j2)))))
    3.65 +        | mk(Multiplied(n,j)) = ((*?writeln"*";!*)multn(n,mk j))
    3.66  
    3.67 -  in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
    3.68 +  in (*?writeln"mkthm";!*)
    3.69 +     simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end
    3.70  end;
    3.71  
    3.72  fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i;