1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Sat Aug 14 18:59:30 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Sat Aug 14 20:38:23 2021 +0200
     1.3 @@ -10,6 +10,17 @@
     1.4    dummy :: real
     1.5  
     1.6  (*for script Maximum_value*)
     1.7 +(*//------------------- causes error at\<^rule_thm>\<open>filterVar.simps(1)\<close> ------------------------\\* )
     1.8 +fun filterVar :: \<open>real \<Rightarrow> 'a  list \<Rightarrow> 'a  list\<close> where
     1.9 +  \<open>filterVar v [] = []\<close>
    1.10 +| \<open>filterVar v (x # xs) = (if (v : set (Vars x)) then x # (filterVar v xs) else filterVar v xs)\<close>  
    1.11 +
    1.12 +thm filterVar.simps
    1.13 +ML \<open>
    1.14 +  @{thm filterVar.simps(1)};
    1.15 +  @{thm filterVar.simps(2)};
    1.16 +\<close>
    1.17 +( *\\------------------- causes error at\<^rule_thm>\<open>filterVar.simps(1)\<close> ------------------------//*)
    1.18    filterVar :: "[real, 'a list] => 'a list"
    1.19  
    1.20  axiomatization where
    1.21 @@ -17,6 +28,7 @@
    1.22    filterVar_Const:	"filterVar v (x#xs) =                       
    1.23  			 (if (v : set (Vars x)) then x#(filterVar v xs)  
    1.24  			                    else filterVar v xs)   "
    1.25 +
    1.26  text \<open>WN.6.5.03: old decisions in this file partially are being changed
    1.27    in a quick-and-dirty way to make scripts run: Maximum_value,
    1.28    Make_fun_by_new_variable, Make_fun_by_explicit.
    1.29 @@ -184,7 +196,12 @@
    1.30      errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>
    1.31  
    1.32  ML \<open>
    1.33 +\<close> ML \<open>
    1.34  val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
    1.35 +(*//------------------- causes error at\<^rule_thm>\<open>filterVar.simps(1)\<close> ------------------------\\* )
    1.36 +   \<^rule_thm>\<open>filterVar.simps(1)\<close>,
    1.37 +   \<^rule_thm>\<open>filterVar.simps(2)\<close>];
    1.38 +( *\\------------------- causes error at\<^rule_thm>\<open>filterVar.simps(1)\<close> ------------------------//*)
    1.39     \<^rule_thm>\<open>filterVar_Const\<close>,
    1.40     \<^rule_thm>\<open>filterVar_Nil\<close>];
    1.41  \<close>

     2.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 18:59:30 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 20:38:23 2021 +0200
     2.3 @@ -8,8 +8,8 @@
     2.4  theory DiophantEq imports Base_Tools Equation Test
     2.5  begin
     2.6  
     2.7 -axiomatization where
     2.8 -  int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     2.9 +lemma int_isolate_add : "(bdv + a = b) = (bdv = b +  -1 * (a::int))"
    2.10 +  by auto
    2.11  
    2.12  text \<open>problemclass for the usecase\<close>
    2.13  

     3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 18:59:30 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 20:38:23 2021 +0200
     3.3 @@ -18,15 +18,17 @@
     3.4    (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
     3.5    solveSystem        :: "[bool list, real list] => bool list"
     3.6  
     3.7 +lemma commute_0_equality : \<open>(0 = a) = (a = 0)\<close>
     3.8 +  by auto
     3.9 +
    3.10  axiomatization where
    3.11 -(*stated as axioms, todo: prove as theorems
    3.12 -  'bdv' is a constant handled on the meta-level 
    3.13 -   specifically as a 'bound variable'            *)
    3.14 -
    3.15 -  commute_0_equality:  "(0 = a) = (a = 0)" and
    3.16 -
    3.17    (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
    3.18      [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
    3.19 +  (* these require lemmas about occur_exactly_in* )
    3.20 +  lemma xxx : 
    3.21 +    \<open>[| [] from [bdv_1, bdv_2, bdv_3, bdv_4] occur_exactly_in a |] ==> (a + b = c) = (b = c + -1 * a)\<close>
    3.22 +    by auto
    3.23 +  ( **)
    3.24    separate_bdvs_add:   
    3.25      "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] 
    3.26  		      			     ==> (a + b = c) = (b = c + -1*a)" and
    3.27 @@ -46,7 +48,8 @@
    3.28    ---  rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*)
    3.29    order_system_NxN:     "[a,b] = [b,a]"
    3.30    (*requires rew_ord for termination, eg. ord_simplify_Integral;
    3.31 -    works for lists of any length, interestingly !?!*)
    3.32 +    works for lists of any length, interestingly !?!
    3.33 +    CONTRADICTS PROPERTIES OF LIST: take set instead*)
    3.34  
    3.35  ML \<open>
    3.36  (** eval functions **)