1.1 --- a/src/Tools/isac/CalcElements/ListC.thy	Thu Aug 29 10:59:57 2019 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/ListC.thy	Thu Aug 29 13:52:47 2019 +0200
     1.3 @@ -130,6 +130,10 @@
     1.4  remdups_Nil:	"remdups [] = []" and
     1.5  remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 
     1.6  
     1.7 +consts lastI :: "'a list \<Rightarrow> 'a"
     1.8 +axiomatization where
     1.9 +last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
    1.10 +
    1.11  ML\<open>(** rule set for evaluating listexpr in scripts, will be extended in several thys **)
    1.12  val list_rls = 
    1.13    Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

     2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 29 10:59:57 2019 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 29 13:52:47 2019 +0200
     2.3 @@ -2,4 +2,148 @@
     2.4    imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
     2.5                                                            (*  ^^^ for KEStore_Elems.add_thes *)
     2.6  begin
     2.7 +subsection \<open>theorems for Base_Tools\<close>
     2.8 +axiomatization where (*for evaluating the assumptions of conditional rules*)
     2.9 +
    2.10 +(*last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
    2.11 +  real_unari_minus:   "- a = (-1) * a" and
    2.12 +  radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
    2.13 +  (* should be in Rational.thy, but: 
    2.14 +   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
    2.15 +  rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
    2.16 +		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
    2.17 +  rat_leq2:	      "d ~= 0 ==>
    2.18 +		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
    2.19 +  rat_leq3:	      "b ~= 0 ==>
    2.20 +		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
    2.21 +
    2.22 +subsection \<open>setup for ML-functions\<close>
    2.23 +text \<open>required by "eval_binop" below\<close>
    2.24 +setup \<open>KEStore_Elems.add_calcs
    2.25 +  [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
    2.26 +    ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
    2.27 +    ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
    2.28 +    ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
    2.29 +    ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
    2.30 +    ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
    2.31 +    ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
    2.32 +    ("ident", ("Atools.ident", eval_ident "#ident_")),
    2.33 +    ("equal", ("HOL.eq", eval_equal "#equal_")),
    2.34 +    ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
    2.35 +    ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
    2.36 +    ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
    2.37 +    ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
    2.38 +    ("POWER",("Atools.pow", eval_binop "#power_")),
    2.39 +    ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
    2.40 +
    2.41 +subsection \<open>rewrite-order for rule-sets\<close>
    2.42 +ML \<open>
    2.43 +\<close> ML \<open>
    2.44 +local
    2.45 +  open Term;
    2.46 +in
    2.47 +  fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
    2.48 +  fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
    2.49 +end;
    2.50 +\<close> ML \<open>
    2.51 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
    2.52 +val tless_true = Rule.dummy_ord;
    2.53 +Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
    2.54 +			[("tless_true", tless_true),
    2.55 +			 ("e_rew_ord'", tless_true),
    2.56 +			 ("dummy_ord", Rule.dummy_ord)]);
    2.57 +\<close>
    2.58 +
    2.59 +subsection \<open>rule-sets\<close>
    2.60 +ML \<open>
    2.61 +\<close> ML \<open>
    2.62 +val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
    2.63 +  [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
    2.64 +    Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    2.65 +		(*"(~ True) = False"*)
    2.66 +		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    2.67 +		(*"(~ False) = True"*)
    2.68 +		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
    2.69 +		(*"(?a & True) = ?a"*)
    2.70 +		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
    2.71 +		(*"(?a & False) = False"*)
    2.72 +		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
    2.73 +		(*"(?a | True) = True"*)
    2.74 +		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
    2.75 +		(*"(?a | False) = ?a"*)
    2.76 +               
    2.77 +		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
    2.78 +		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
    2.79 +		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
    2.80 +      Rule.Thm ("refl", TermC.num_str @{thm refl}),
    2.81 +		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
    2.82 +		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
    2.83 +		
    2.84 +		Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
    2.85 +		Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
    2.86 +		
    2.87 +		Rule.Calc ("Atools.ident", eval_ident "#ident_"),    
    2.88 +		Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
    2.89 +		Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),    
    2.90 +		Rule.Calc ("Tools.matches", Tools.eval_matches "")];
    2.91 +\<close>
    2.92 +
    2.93 +ML \<open>
    2.94 +val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
    2.95 +  [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
    2.96 +    Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    2.97 +		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    2.98 +		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
    2.99 +		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
   2.100 +		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
   2.101 +		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
   2.102 +               
   2.103 +		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
   2.104 +		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
   2.105 +		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
   2.106 +		Rule.Thm ("refl", TermC.num_str @{thm refl}),
   2.107 +		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
   2.108 +		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
   2.109 +		
   2.110 +		Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
   2.111 +		Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
   2.112 +		
   2.113 +		Rule.Calc ("Atools.ident", eval_ident "#ident_"),    
   2.114 +		Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
   2.115 +		Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),    
   2.116 +		Rule.Calc ("Tools.matches", Tools.eval_matches "")];
   2.117 +\<close>
   2.118 +
   2.119 +subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
   2.120 +text \<open>requires "eval_binop" from above\<close>
   2.121 +ML \<open>
   2.122 +val list_rls = Rule.append_rls "list_rls" list_rls
   2.123 +	[ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
   2.124 +		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
   2.125 +		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
   2.126 +		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
   2.127 +		Rule.Calc ("Atools.ident",eval_ident "#ident_"),
   2.128 +		Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
   2.129 +       
   2.130 +		Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
   2.131 +		
   2.132 +		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
   2.133 +		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
   2.134 +
   2.135 +val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
   2.136 +	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
   2.137 +    erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
   2.138 +    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
   2.139 +    rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
   2.140 +      Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
   2.141 +      (*    ~~~~~~ for nth_Cons_*)],
   2.142 +    scr = Rule.EmptyScr},
   2.143 +    srls = Rule.Erls, calc = [], errpatts = [],
   2.144 +    rules = [], scr = Rule.EmptyScr})
   2.145 +  list_rls);
   2.146 +\<close>
   2.147 +subsection \<open>setup for extended rule-set\<close>
   2.148 +setup \<open>KEStore_Elems.add_rlss
   2.149 +  [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>
   2.150 +
   2.151  end
   2.152 \ No newline at end of file

     3.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Thu Aug 29 10:59:57 2019 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Thu Aug 29 13:52:47 2019 +0200
     3.3 @@ -47,8 +47,8 @@
     3.4  ccc
     3.5  \<close> ML \<open>
     3.6  case aaa of ("list_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 1";
     3.7 -case bbb of ("e_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 2";
     3.8 -case ccc of ("e_rrls", _) => () | _ => error "test/../thy-hierarchy CHANGED 3";
     3.9 +case bbb of ("e_rrls", _) => () | _ => error "test/../thy-hierarchy CHANGED 2";
    3.10 +case ccc of ("e_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 3";
    3.11  \<close> ML \<open>
    3.12  case ddd of
    3.13    ("rls111",

     4.1 --- a/src/Tools/isac/ProgLang/Atools.thy	Thu Aug 29 10:59:57 2019 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/Atools.thy	Thu Aug 29 13:52:47 2019 +0200
     4.3 @@ -21,6 +21,7 @@
     4.4  consts
     4.5    Arbfix           :: "real"
     4.6    Undef            :: "real"  (* WN190823 probably an outdated design for DiffApp *)
     4.7 +(*+ UniversalList from Tools.thy*)
     4.8  
     4.9    pow              :: "[real, real] => real"    (infixr "^^^" 80)
    4.10    (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
    4.11 @@ -53,22 +54,6 @@
    4.12    boollist2sum     :: "bool list => real"
    4.13    lastI            :: "'a list \<Rightarrow> 'a"
    4.14  
    4.15 -subsection \<open>theorems for Base_Tools\<close>
    4.16 -axiomatization where (*for evaluating the assumptions of conditional rules*)
    4.17 -
    4.18 -  last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
    4.19 -  real_unari_minus:   "- a = (-1) * a" and
    4.20 -  radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
    4.21 -  (* should be in Rational.thy, but: 
    4.22 -   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
    4.23 -  rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
    4.24 -		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
    4.25 -  rat_leq2:	      "d ~= 0 ==>
    4.26 -		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
    4.27 -  rat_leq3:	      "b ~= 0 ==>
    4.28 -		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
    4.29 -
    4.30 -
    4.31  axiomatization where (*..if replaced by "and" we get error:
    4.32  Type unification failed: No type arity bool :: zero ...*)
    4.33    rle_refl:           "(n::real) <= n" and
    4.34 @@ -539,148 +524,6 @@
    4.35    | eval_boollist2sum _ _ _ _ = NONE;
    4.36  \<close>
    4.37  
    4.38 -subsection \<open>setup for ML-functions\<close>
    4.39 -text \<open>required by "eval_binop" below\<close>
    4.40 -setup \<open>KEStore_Elems.add_calcs
    4.41 -  [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
    4.42 -    ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
    4.43 -    ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
    4.44 -    ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
    4.45 -    ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
    4.46 -    ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
    4.47 -    ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
    4.48 -    ("ident", ("Atools.ident", eval_ident "#ident_")),
    4.49 -    ("equal", ("HOL.eq", eval_equal "#equal_")),
    4.50 -    ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
    4.51 -    ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
    4.52 -    ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
    4.53 -    ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
    4.54 -    ("POWER",("Atools.pow", eval_binop "#power_")),
    4.55 -    ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
    4.56 -
    4.57 -subsection \<open>rewrite-order for rule-sets\<close>
    4.58 -ML \<open>
    4.59 -\<close> ML \<open>
    4.60 -local
    4.61 -  open Term;
    4.62 -in
    4.63 -  fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
    4.64 -  fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
    4.65 -end;
    4.66 -\<close>
    4.67 -
    4.68 -subsection \<open>rewrite-order for rule-sets\<close>
    4.69 -ML \<open>
    4.70 -(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
    4.71 -val tless_true = Rule.dummy_ord;
    4.72 -Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
    4.73 -			[("tless_true", tless_true),
    4.74 -			 ("e_rew_ord'", tless_true),
    4.75 -			 ("dummy_ord", Rule.dummy_ord)]);
    4.76 -\<close>
    4.77 -
    4.78 -subsection \<open>rule-sets\<close>
    4.79 -ML \<open>
    4.80 -val calculate_Base_Tools = Rule.append_rls "calculate_Atools" Rule.e_rls
    4.81 -  [ Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
    4.82 -		Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
    4.83 -		Rule.Calc ("HOL.eq", eval_equal "#equal_"),
    4.84 -
    4.85 -		Rule.Thm  ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
    4.86 -		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    4.87 -		Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
    4.88 -		Rule.Calc ("Groups.times_class.times", eval_binop "#mult_")
    4.89 -		];
    4.90 -
    4.91 -\<close> ML \<open>
    4.92 -val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
    4.93 -  [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
    4.94 -    Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    4.95 -		(*"(~ True) = False"*)
    4.96 -		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    4.97 -		(*"(~ False) = True"*)
    4.98 -		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
    4.99 -		(*"(?a & True) = ?a"*)
   4.100 -		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
   4.101 -		(*"(?a & False) = False"*)
   4.102 -		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
   4.103 -		(*"(?a | True) = True"*)
   4.104 -		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
   4.105 -		(*"(?a | False) = ?a"*)
   4.106 -               
   4.107 -		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
   4.108 -		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
   4.109 -		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
   4.110 -      Rule.Thm ("refl", TermC.num_str @{thm refl}),
   4.111 -		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
   4.112 -		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
   4.113 -		
   4.114 -		Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
   4.115 -		Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
   4.116 -		
   4.117 -		Rule.Calc ("Atools.ident", eval_ident "#ident_"),    
   4.118 -		Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
   4.119 -		Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),    
   4.120 -		Rule.Calc ("Tools.matches", Tools.eval_matches "")];
   4.121 -\<close>
   4.122 -
   4.123 -ML \<open>
   4.124 -val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
   4.125 -  [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
   4.126 -    Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
   4.127 -		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
   4.128 -		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
   4.129 -		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
   4.130 -		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
   4.131 -		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
   4.132 -               
   4.133 -		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
   4.134 -		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
   4.135 -		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
   4.136 -		Rule.Thm ("refl", TermC.num_str @{thm refl}),
   4.137 -		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
   4.138 -		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
   4.139 -		
   4.140 -		Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
   4.141 -		Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
   4.142 -		
   4.143 -		Rule.Calc ("Atools.ident", eval_ident "#ident_"),    
   4.144 -		Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
   4.145 -		Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),    
   4.146 -		Rule.Calc ("Tools.matches", Tools.eval_matches "")];
   4.147 -\<close>
   4.148 -
   4.149 -subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
   4.150 -text \<open>requires "eval_binop" from above\<close>
   4.151 -ML \<open>
   4.152 -val list_rls = Rule.append_rls "list_rls" list_rls
   4.153 -	[ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
   4.154 -		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), 
   4.155 -		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
   4.156 -		Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
   4.157 -		Rule.Calc ("Atools.ident",eval_ident "#ident_"),
   4.158 -		Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
   4.159 -       
   4.160 -		Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
   4.161 -		
   4.162 -		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
   4.163 -		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
   4.164 -
   4.165 -val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
   4.166 -	(Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
   4.167 -    erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
   4.168 -    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
   4.169 -    rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
   4.170 -      Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
   4.171 -      (*    ~~~~~~ for nth_Cons_*)],
   4.172 -    scr = Rule.EmptyScr},
   4.173 -    srls = Rule.Erls, calc = [], errpatts = [],
   4.174 -    rules = [], scr = Rule.EmptyScr})
   4.175 -  list_rls);
   4.176 -\<close>
   4.177 -subsection \<open>setup for extended rule-set\<close>
   4.178 -setup \<open>KEStore_Elems.add_rlss
   4.179 -  [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>
   4.180  
   4.181  ML \<open>
   4.182  \<close> ML \<open>

     5.1 --- a/src/Tools/isac/ProgLang/Program.thy	Thu Aug 29 10:59:57 2019 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/Program.thy	Thu Aug 29 13:52:47 2019 +0200
     5.3 @@ -5,44 +5,14 @@
     5.4  
     5.5  theory Program imports Tools begin
     5.6  
     5.7 -(* special formulas for frontend *)
     5.8 +section \<open>Consts for tacticals\<close>
     5.9  consts
    5.10 -  Problem      :: "[char list * char list list] => 'a"
    5.11 -  Subproblem   :: "(char list * char list list) => 'a" 
    5.12 -
    5.13 -(*script-expressions (tacticals)*)
    5.14    Seq      :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
    5.15    Try      :: "['a => 'a, 'a] => 'a"
    5.16    Repeat   :: "['a => 'a, 'a] => 'a" 
    5.17    Or       :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
    5.18    While    :: "[bool, 'a => 'a, 'a] => 'a"     ("((While (_) Do)//(_))" 9)
    5.19 -(*WN100723 because of "Error in syntax translation" below...
    5.20 -        (*'b => bool doesn't work with "contains_root _"*)
    5.21 -  Letpar   :: "['a, 'a => 'b] => 'b"
    5.22 -  (*--- defined in Isabelle/scr/HOL/HOL.thy:
    5.23 -  Let      :: "['a, 'a => 'b] => 'b"
    5.24 -  "_Let"   :: "[letbinds, 'a] => 'a"       ("(let (_)/ in (_))" 10)
    5.25 -  If       :: "[bool, 'a, 'a] => 'a"       ("(if (_)/ then (_)/ else (_))" 10)
    5.26 -  %x. P x  .. lambda is defined in Isabelles meta logic
    5.27 -  --- *)
    5.28 -*)
    5.29 -  failtac :: 'a
    5.30 -  idletac :: 'a
    5.31 -  (*... + RECORD IN 'screxpr' in Program.ML *)
    5.32  
    5.33 -(*Makarius 10.03
    5.34 -syntax
    5.35 -
    5.36 -  "_Letpar"     :: "[letbinds, 'a] => 'a"      ("(letpar (_)/ in (_))" 10)
    5.37 -
    5.38 -translations
    5.39 -
    5.40 -  "_Letpar (_binds b bs) e"  == "_Letpar b (_Letpar bs e)"
    5.41 -  "letpar x = a in e"        == "Letpar a (%x. e)"
    5.42 -*** Error in syntax translation rule: rhs contains extra variables
    5.43 -*** ("_Letpar" ("_bind" x a) e)  ->  (Letpar a ("_abs" x e))
    5.44 -*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Program").
    5.45 -*)
    5.46  ML \<open>
    5.47  \<close> ML \<open>
    5.48  \<close> ML \<open>

     6.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Thu Aug 29 10:59:57 2019 +0200
     6.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Thu Aug 29 13:52:47 2019 +0200
     6.3 @@ -21,7 +21,6 @@
     6.4  "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
     6.5  "----------- fun Thm.make_thm ------------------------------------";
     6.6  "----------- correct theIDs for e_rls ----------------------------";
     6.7 -"----------- correct theIDs for list_rls -------------------------";
     6.8  "----------- fun revert_sym --------------------------------------";
     6.9  "----------- fun thms_of_rlss ------------------------------------";
    6.10  "----------- repair thydata2xml for rls --------------------------";
    6.11 @@ -170,17 +169,6 @@
    6.12                                                  ["IsacScripts", "KEStore", "Rulesets", "e_rls"], 
    6.13    :*)
    6.14  
    6.15 -"----------- correct theIDs for list_rls -------------------------";
    6.16 -"----------- correct theIDs for list_rls -------------------------";
    6.17 -"----------- correct theIDs for list_rls -------------------------";
    6.18 -if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacScripts", "Atools") then ()
    6.19 -else error "thy_containing_rls list_rls changed";
    6.20 -show_thes ();
    6.21 -(*shows different assignment for "list_rls"...
    6.22 -  : 
    6.23 -                                                   ["IsacScripts", "Tools", "Rulesets", "list_rls"],
    6.24 -  :*)
    6.25 -
    6.26  "----------- fun revert_sym --------------------------------------";
    6.27  "----------- fun revert_sym --------------------------------------";
    6.28  "----------- fun revert_sym --------------------------------------";

     7.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Thu Aug 29 10:59:57 2019 +0200
     7.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Thu Aug 29 13:52:47 2019 +0200
     7.3 @@ -76,11 +76,7 @@
     7.4  else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
     7.5  ;
     7.6  if thy_containing_rls "Build_Thydata" "list_rls" = (*FIXME: handle redifinition in several thys*)
     7.7 -  ("IsacScripts", "Atools") then ()
     7.8 -else error ("thy_containing_rls changed for 'Biegelinie', 'list_rls'")
     7.9 -;
    7.10 -if thy_containing_rls "Biegelinie" "list_rls" =    (*FIXME: handle redifinition in several thys*)
    7.11 -  ("IsacScripts", "Atools") then ()
    7.12 +  ("IsacKnowledge", "Base_Tools") then ()
    7.13  else error ("thy_containing_rls changed for 'Biegelinie', 'list_rls'")
    7.14  
    7.15  "----------- fun thy_containing_cal ---------------------";