Added trans_tac (see Provers/nat_transitive.ML)
authornipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 21159709f9188549
parent 2114 c6a7fd523a5a
child 2116 73bbf2cc7651
Added trans_tac (see Provers/nat_transitive.ML)
src/HOL/Nat.ML
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/Nat.ML	Mon Oct 21 09:49:41 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Oct 21 09:50:50 1996 +0200
     1.3 @@ -585,3 +585,74 @@
     1.4          Fast_tac 2,
     1.5          dtac Suc_mono 1,
     1.6          Fast_tac 1]);
     1.7 +
     1.8 +
     1.9 +(*** Instantiation of transitivity prover ***)
    1.10 +
    1.11 +structure Less_Arith =
    1.12 +struct
    1.13 +val nat_leI = leI;
    1.14 +val nat_leD = leD;
    1.15 +val lessI = lessI;
    1.16 +val zero_less_Suc = zero_less_Suc;
    1.17 +val less_reflE = less_irrefl;
    1.18 +val less_zeroE = less_zeroE;
    1.19 +val less_incr = Suc_mono;
    1.20 +val less_decr = Suc_less_SucD;
    1.21 +val less_incr_rhs = Suc_mono RS Suc_lessD;
    1.22 +val less_decr_lhs = Suc_lessD;
    1.23 +val less_trans_Suc = less_trans_Suc;
    1.24 +val leI = lessD RS (Suc_le_mono RS iffD1);
    1.25 +val not_lessI = leI RS leD
    1.26 +val not_leI = prove_goal Nat.thy "!!m::nat. n < m ==> ~ m <= n"
    1.27 +  (fn _ => [etac swap2 1, etac leD 1]);
    1.28 +val eqI = prove_goal Nat.thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
    1.29 +  (fn _ => [etac less_SucE 1,
    1.30 +            fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
    1.31 +                             addDs [less_trans_Suc]) 1,
    1.32 +            atac 1]);
    1.33 +val leD = le_eq_less_Suc RS iffD1;
    1.34 +val not_lessD = nat_leI RS leD;
    1.35 +val not_leD = not_leE
    1.36 +val eqD1 = prove_goal Nat.thy  "!!n. m = n ==> m < Suc n"
    1.37 + (fn _ => [etac subst 1, rtac lessI 1]);
    1.38 +val eqD2 = sym RS eqD1;
    1.39 +
    1.40 +fun is_zero(t) =  t = Const("0",Type("nat",[]));
    1.41 +
    1.42 +fun nnb T = T = Type("fun",[Type("nat",[]),
    1.43 +                            Type("fun",[Type("nat",[]),
    1.44 +                                        Type("bool",[])])])
    1.45 +
    1.46 +fun decomp_Suc(Const("Suc",_)$t) = let val (a,i) = decomp_Suc t in (a,i+1) end
    1.47 +  | decomp_Suc t = (t,0);
    1.48 +
    1.49 +fun decomp2(rel,T,lhs,rhs) =
    1.50 +  if not(nnb T) then None else
    1.51 +  let val (x,i) = decomp_Suc lhs
    1.52 +      val (y,j) = decomp_Suc rhs
    1.53 +  in case rel of
    1.54 +       "op <"  => Some(x,i,"<",y,j)
    1.55 +     | "op <=" => Some(x,i,"<=",y,j)
    1.56 +     | "op ="  => Some(x,i,"=",y,j)
    1.57 +     | _       => None
    1.58 +  end;
    1.59 +
    1.60 +fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
    1.61 +
    1.62 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
    1.63 +  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
    1.64 +      negate(decomp2(rel,T,lhs,rhs))
    1.65 +  | decomp _ = None
    1.66 +
    1.67 +end;
    1.68 +
    1.69 +structure Trans_Tac = Trans_Tac_Fun(Less_Arith);
    1.70 +
    1.71 +open Trans_Tac;
    1.72 +
    1.73 +(*** eliminates ~= in premises, which trans_tac cannot deal with ***)
    1.74 +qed_goal "nat_neqE" Nat.thy
    1.75 +  "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
    1.76 +  (fn major::prems => [cut_facts_tac [less_linear] 1,
    1.77 +                       REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
     2.1 --- a/src/HOL/ROOT.ML	Mon Oct 21 09:49:41 1996 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Mon Oct 21 09:50:50 1996 +0200
     2.3 @@ -19,6 +19,7 @@
     2.4  use "../Provers/splitter.ML";
     2.5  use "../Provers/hypsubst.ML";
     2.6  use "../Provers/classical.ML";
     2.7 +use "../Provers/nat_transitive.ML";
     2.8  
     2.9  
    2.10  use_thy "HOL";