# HG changeset patch # User paulson # Date 1109754141 -3600 # Node ID f5f4f89a3b84d15d833ff1c433412a9c676da2d3 # Parent 2901b1f6ba64955ce4e04b3e729dfd484a3efbe7 new lemmas int_diff_cases diff -r 2901b1f6ba64 -r f5f4f89a3b84 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Wed Mar 02 00:56:41 2005 +0100 +++ b/src/HOL/Integ/IntDef.thy Wed Mar 02 10:02:21 2005 +0100 @@ -836,6 +836,13 @@ "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" by (cases z) auto +text{*Contributed by Brian Huffman*} +theorem int_diff_cases [case_names diff]: +assumes prem: "!!m n. z = int m - int n ==> P" shows "P" + apply (rule_tac z=z in int_cases) + apply (rule_tac m=n and n=0 in prem, simp) + apply (rule_tac m=0 and n="Suc n" in prem, simp) +done lemma of_nat_nat: "0 \ z ==> of_nat (nat z) = of_int z" apply (cases z)