src/HOL/UNITY/Lift.ML
changeset 5410 5ed7547a7f74
parent 5357 6efb2b87610c
child 5424 771a68a468cc
equal deleted inserted replaced
5409:e97558ee8e76 5410:5ed7547a7f74
    58 val nat_exhaust_le_pred = 
    58 val nat_exhaust_le_pred = 
    59     read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
    59     read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
    60 
    60 
    61 val nat_exhaust_pred_le = 
    61 val nat_exhaust_pred_le = 
    62     read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
    62     read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
    63 
       
    64 Goal "0 < n ==> (m <= n-1) = (m<n)";
       
    65 by (exhaust_tac "n" 1);
       
    66 by Auto_tac;
       
    67 qed "le_pred_eq";
       
    68 
       
    69 Goal "0 < n ==> (m-1 < n) = (m<=n)";
       
    70 by (exhaust_tac "m" 1);
       
    71 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
       
    72 qed "less_pred_eq";
       
    73 
    63 
    74 Goal "m < n ==> m <= n-1";
    64 Goal "m < n ==> m <= n-1";
    75 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    65 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    76 qed "less_imp_le_pred";
    66 qed "less_imp_le_pred";
    77 
    67