(* Title:  collecting all knowledge for Root and Rational

   Author: Richard Lang 02.10 last change by: rlang date: 02.10.20

   (c) due to copyright terms

*)

theory RootRat imports Root Rational begin

ML \<open>

val thy = @{theory};

val rootrat_erls = 

  Rule_Set.merge "rootrat_erls" Root_erls

    (Rule_Set.merge "" rational_erls

      (Rule_Set.append_rules "" Rule_Set.empty []));

(*.calculate numeral groundterms.*)

val calculate_RootRat = 

  Rule_Set.append_rules "calculate_RootRat" calculate_Rational

	    [\<^rule_thm>\<open>distrib_left\<close>,

		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)

		     \<^rule_thm>\<open>mult_1_left\<close>,

		      (* 1 * z = z *)

		      Rule.Thm ("real_mult_minus1_sym",  (@{thm real_mult_minus1_sym})),

	        (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)

		     Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")

		     ];

val prep_rls' = Auto_Prog.prep_rls @{theory};

\<close>

rule_set_knowledge

  rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and

  calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end