1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 18:59:30 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 20:38:23 2021 +0200
     1.3 @@ -18,15 +18,17 @@
     1.4    (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
     1.5    solveSystem        :: "[bool list, real list] => bool list"
     1.6  
     1.7 +lemma commute_0_equality : \<open>(0 = a) = (a = 0)\<close>
     1.8 +  by auto
     1.9 +
    1.10  axiomatization where
    1.11 -(*stated as axioms, todo: prove as theorems
    1.12 -  'bdv' is a constant handled on the meta-level 
    1.13 -   specifically as a 'bound variable'            *)
    1.14 -
    1.15 -  commute_0_equality:  "(0 = a) = (a = 0)" and
    1.16 -
    1.17    (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
    1.18      [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
    1.19 +  (* these require lemmas about occur_exactly_in* )
    1.20 +  lemma xxx : 
    1.21 +    \<open>[| [] from [bdv_1, bdv_2, bdv_3, bdv_4] occur_exactly_in a |] ==> (a + b = c) = (b = c + -1 * a)\<close>
    1.22 +    by auto
    1.23 +  ( **)
    1.24    separate_bdvs_add:   
    1.25      "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] 
    1.26  		      			     ==> (a + b = c) = (b = c + -1*a)" and
    1.27 @@ -46,7 +48,8 @@
    1.28    ---  rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*)
    1.29    order_system_NxN:     "[a,b] = [b,a]"
    1.30    (*requires rew_ord for termination, eg. ord_simplify_Integral;
    1.31 -    works for lists of any length, interestingly !?!*)
    1.32 +    works for lists of any length, interestingly !?!
    1.33 +    CONTRADICTS PROPERTIES OF LIST: take set instead*)
    1.34  
    1.35  ML \<open>
    1.36  (** eval functions **)