(* Title:  "BaseDefinitions/BaseDefinitions.thy"

    Author: Walther Neuper 190823

    (c) due to copyright terms

 Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions.

 *)

 theory BaseDefinitions imports Know_Store

 begin

 subsection \<open>Power re-defined for a specific type\<close>

 definition even_real :: "real \<Rightarrow> bool"

   where "even_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> even (inv real \<bar>x\<bar>)"

 definition odd_real :: "real \<Rightarrow> bool"

   where "odd_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> odd (inv real \<bar>x\<bar>)"

 definition realpow :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)

   where "x \<up> n =

     (if x \<ge> 0 then x powr n

      else if n \<ge> 0 \<and> even_real n then (- x) powr n

      else if n \<ge> 0 \<and> odd_real n then - ((- x) powr n)

      else if n < 0 \<and> even_real n then 1 / (- x) powr (- n)

      else if n < 0 \<and> odd_real n then - 1 / ((- x) powr (- n))

      else undefined)"

 lemma realpow_simps [simp]:

   "0 \<up> a = 0"

   "1 \<up> a = 1"

   "numeral m \<up> numeral n = (numeral m ^ numeral n :: real)"

   "x > 0 \<Longrightarrow> x \<up> 0 = 1"

   "x \<ge> 0 \<Longrightarrow> x \<up> 1 = x"

   "x \<ge> 0 \<Longrightarrow> x \<up> numeral n = x ^ numeral n"

   "x > 0 \<Longrightarrow> x \<up> - numeral n = 1 / (x ^ numeral n)"

   by (simp_all add: realpow_def powr_neg_numeral)

 lemma inv_real_eq:

   "inv real 0 = 0"

   "inv real 1 = 1"

   "inv real (numeral n) = numeral n"

   by (simp_all add: inv_f_eq)

 lemma realpow_uminus_simps [simp]:

   "(- 1) \<up> 0 = 1"

   "(- 1) \<up> 1 = - 1"

   "x \<up> (- 1) = 1 / x"

   "(- numeral m) \<up> 0 = 1"

   "(- numeral m) \<up> 1 = - numeral m"

   "even (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (numeral n) = 1"

   "odd (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (numeral n) = - 1"

   "even (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (- numeral n) = 1"

   "odd (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (- numeral n) = - 1"

   "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = - (numeral m ^ numeral n)"

   "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = numeral m ^ numeral n"

   "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = 1 / (numeral m ^ numeral n)"

   "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = - 1 / (numeral m ^ numeral n)"

   apply (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)

   by (simp add: powr_minus_divide)

 ML_file termC.sml

 ML_file substitution.sml

 ML_file contextC.sml

 ML_file environment.sml

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end