(* 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