4 |
4 |
5 Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions. |
5 Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions. |
6 *) |
6 *) |
7 theory BaseDefinitions imports Know_Store |
7 theory BaseDefinitions imports Know_Store |
8 begin |
8 begin |
|
9 |
|
10 subsection \<open>Power re-defined for a specific type\<close> |
|
11 |
|
12 definition even_real :: "real \<Rightarrow> bool" |
|
13 where "even_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> even (inv real \<bar>x\<bar>)" |
|
14 definition odd_real :: "real \<Rightarrow> bool" |
|
15 where "odd_real x \<longleftrightarrow> \<bar>x\<bar> \<in> \<nat> \<and> odd (inv real \<bar>x\<bar>)" |
|
16 |
|
17 definition realpow :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80) |
|
18 where "x \<up> n = |
|
19 (if x \<ge> 0 then x powr n |
|
20 else if n \<ge> 0 \<and> even_real n then (- x) powr n |
|
21 else if n \<ge> 0 \<and> odd_real n then - ((- x) powr n) |
|
22 else if n < 0 \<and> even_real n then 1 / (- x) powr (- n) |
|
23 else if n < 0 \<and> odd_real n then - 1 / ((- x) powr (- n)) |
|
24 else undefined)" |
|
25 |
|
26 lemma realpow_simps [simp]: |
|
27 "0 \<up> a = 0" |
|
28 "1 \<up> a = 1" |
|
29 "numeral m \<up> numeral n = (numeral m ^ numeral n :: real)" |
|
30 "x > 0 \<Longrightarrow> x \<up> 0 = 1" |
|
31 "x \<ge> 0 \<Longrightarrow> x \<up> 1 = x" |
|
32 "x \<ge> 0 \<Longrightarrow> x \<up> numeral n = x ^ numeral n" |
|
33 "x > 0 \<Longrightarrow> x \<up> - numeral n = 1 / (x ^ numeral n)" |
|
34 by (simp_all add: realpow_def powr_neg_numeral) |
|
35 |
|
36 lemma inv_real_eq: |
|
37 "inv real 0 = 0" |
|
38 "inv real 1 = 1" |
|
39 "inv real (numeral n) = numeral n" |
|
40 by (simp_all add: inv_f_eq) |
|
41 |
|
42 lemma realpow_uminus_simps [simp]: |
|
43 "(- numeral m) \<up> 0 = 1" |
|
44 "(- numeral m) \<up> 1 = - numeral m" |
|
45 "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = numeral m ^ numeral n" |
|
46 "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = - (numeral m ^ numeral n)" |
|
47 "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = 1 / (numeral m ^ numeral n)" |
|
48 "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = - 1 / (numeral m ^ numeral n)" |
|
49 by (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq) |
|
50 |
|
51 |
9 ML_file termC.sml |
52 ML_file termC.sml |
10 ML_file substitution.sml |
53 ML_file substitution.sml |
11 ML_file contextC.sml |
54 ML_file contextC.sml |
12 ML_file environment.sml |
55 ML_file environment.sml |
13 |
56 |