author  wenzelm 
Thu, 17 Aug 2000 10:33:13 +0200  
changeset 9618  ff8238561394 
parent 9436  62bb04ab4b01 
permissions  rwrr 
923  1 
(* Title: HOL/Arith.thy 
2 
ID: $Id$ 

3 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

4 
Setup arithmetic proof procedures. 
923  5 
*) 
6 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

7 
theory Arith = Nat 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

8 
files "arith_data.ML": 
923  9 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

10 
setup arith_setup 
1796  11 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

12 
(*elimination of `' on nat*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

13 
lemma nat_diff_split: 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

14 
"P(a  b::nat) = (ALL d. (a<b > P 0) & (a = b + d > P d))" 
9618  15 
by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2]) 
2681
93ed51a91622
definitions of +,,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset

16 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

17 
ML {* val nat_diff_split = thm "nat_diff_split" *} 
4360  18 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8970
diff
changeset

19 
lemmas [arith_split] = nat_diff_split split_min split_max 
2681
93ed51a91622
definitions of +,,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset

20 

923  21 
end 