16 solution :: "bool list => toreall" |
16 solution :: "bool list => toreall" |
17 |
17 |
18 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*) |
18 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*) |
19 solveSystem :: "[bool list, real list] => bool list" |
19 solveSystem :: "[bool list, real list] => bool list" |
20 |
20 |
|
21 lemma commute_0_equality : \<open>(0 = a) = (a = 0)\<close> |
|
22 by auto |
|
23 |
21 axiomatization where |
24 axiomatization where |
22 (*stated as axioms, todo: prove as theorems |
|
23 'bdv' is a constant handled on the meta-level |
|
24 specifically as a 'bound variable' *) |
|
25 |
|
26 commute_0_equality: "(0 = a) = (a = 0)" and |
|
27 |
|
28 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
25 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) |
29 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
26 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) |
|
27 (* these require lemmas about occur_exactly_in* ) |
|
28 lemma xxx : |
|
29 \<open>[| [] from [bdv_1, bdv_2, bdv_3, bdv_4] occur_exactly_in a |] ==> (a + b = c) = (b = c + -1 * a)\<close> |
|
30 by auto |
|
31 ( **) |
30 separate_bdvs_add: |
32 separate_bdvs_add: |
31 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] |
33 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] |
32 ==> (a + b = c) = (b = c + -1*a)" and |
34 ==> (a + b = c) = (b = c + -1*a)" and |
33 separate_bdvs0: |
35 separate_bdvs0: |
34 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] |
36 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] |
44 ==>(a * b = c) = (b = c / a)" |
46 ==>(a * b = c) = (b = c / a)" |
45 axiomatization where (*..if replaced by "and" we get an error in |
47 axiomatization where (*..if replaced by "and" we get an error in |
46 --- rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*) |
48 --- rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*) |
47 order_system_NxN: "[a,b] = [b,a]" |
49 order_system_NxN: "[a,b] = [b,a]" |
48 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
50 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
49 works for lists of any length, interestingly !?!*) |
51 works for lists of any length, interestingly !?! |
|
52 CONTRADICTS PROPERTIES OF LIST: take set instead*) |
50 |
53 |
51 ML \<open> |
54 ML \<open> |
52 (** eval functions **) |
55 (** eval functions **) |
53 |
56 |
54 (*certain variables of a given list occur _all_ in a term |
57 (*certain variables of a given list occur _all_ in a term |