26 axioms |
26 axioms |
27 (*stated as axioms, todo: prove as theorems |
27 (*stated as axioms, todo: prove as theorems |
28 'bdv' is a constant handled on the meta-level |
28 'bdv' is a constant handled on the meta-level |
29 specifically as a 'bound variable' *) |
29 specifically as a 'bound variable' *) |
30 |
30 |
31 commute_0_equality "(0 = a) = (a = 0)" |
31 commute_0_equality: "(0 = a) = (a = 0)" |
32 |
32 |
33 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
33 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
34 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
34 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
35 separate_bdvs_add |
35 separate_bdvs_add: |
36 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] |
36 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] |
37 ==> (a + b = c) = (b = c + -1*a)" |
37 ==> (a + b = c) = (b = c + -1*a)" |
38 separate_bdvs0 |
38 separate_bdvs0: |
39 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] |
39 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] |
40 ==> (a = b) = (a + -1*b = 0)" |
40 ==> (a = b) = (a + -1*b = 0)" |
41 separate_bdvs_add1 |
41 separate_bdvs_add1: |
42 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] |
42 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] |
43 ==> (a = b + c) = (a + -1*c = b)" |
43 ==> (a = b + c) = (a + -1*c = b)" |
44 separate_bdvs_add2 |
44 separate_bdvs_add2: |
45 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] |
45 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] |
46 ==> (a + b = c) = (b = -1*a + c)" |
46 ==> (a + b = c) = (b = -1*a + c)" |
47 |
47 |
48 |
48 |
49 |
49 |
50 separate_bdvs_mult |
50 separate_bdvs_mult: |
51 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] |
51 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] |
52 ==>(a * b = c) = (b = c / a)" |
52 ==>(a * b = c) = (b = c / a)" |
53 |
53 |
54 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
54 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
55 works for lists of any length, interestingly !?!*) |
55 works for lists of any length, interestingly !?!*) |
56 order_system_NxN "[a,b] = [b,a]" |
56 order_system_NxN: "[a,b] = [b,a]" |
57 |
57 |
58 ML {* |
58 ML {* |
59 val thy = @{theory}; |
59 val thy = @{theory}; |
60 |
60 |
61 (** eval functions **) |
61 (** eval functions **) |