author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 61942 | f02b26f7d39d |
permissions | -rw-r--r-- |
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47790
diff
changeset
|
1 |
(* Title: HOL/TPTP/THF_Arith.thy |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
2 |
Author: Jasmin Blanchette |
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47790
diff
changeset
|
3 |
Copyright 2011, 2012 |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
4 |
|
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47790
diff
changeset
|
5 |
Experimental setup for THF arithmetic. This is not connected with the TPTP |
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47790
diff
changeset
|
6 |
parser yet. |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
7 |
*) |
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
8 |
|
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47790
diff
changeset
|
9 |
theory THF_Arith |
43805 | 10 |
imports Complex_Main |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
11 |
begin |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
12 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
13 |
consts |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
14 |
is_int :: "'a \<Rightarrow> bool" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
15 |
is_rat :: "'a \<Rightarrow> bool" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
16 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
17 |
overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
18 |
begin |
61076 | 19 |
definition "rat_is_int (q::rat) \<longleftrightarrow> (\<exists>n::int. q = of_int n)" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
20 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
21 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
22 |
overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
23 |
begin |
61076 | 24 |
definition "real_is_int (x::real) \<longleftrightarrow> x \<in> \<int>" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
25 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
26 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
27 |
overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
28 |
begin |
61076 | 29 |
definition "real_is_rat (x::real) \<longleftrightarrow> x \<in> \<rat>" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
30 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
31 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
32 |
consts |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
33 |
to_int :: "'a \<Rightarrow> int" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
34 |
to_rat :: "'a \<Rightarrow> rat" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
35 |
to_real :: "'a \<Rightarrow> real" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
36 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
37 |
overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
38 |
begin |
61942 | 39 |
definition "rat_to_int (q::rat) = \<lfloor>q\<rfloor>" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
40 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
41 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
42 |
overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
43 |
begin |
61942 | 44 |
definition "real_to_int (x::real) = \<lfloor>x\<rfloor>" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
45 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
46 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
47 |
overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat" |
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset
|
48 |
begin |
61076 | 49 |
definition "int_to_rat (n::int) = (of_int n::rat)" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
50 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
51 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
52 |
overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
53 |
begin |
61076 | 54 |
definition "real_to_rat (x::real) = (inv of_rat x::rat)" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
55 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
56 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
57 |
overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
58 |
begin |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61076
diff
changeset
|
59 |
definition "int_to_real (n::int) = real_of_int n" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
60 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
61 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
62 |
overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real" |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
63 |
begin |
61076 | 64 |
definition "rat_to_real (x::rat) = (of_rat x::real)" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
65 |
end |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
66 |
|
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
67 |
declare |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
68 |
rat_is_int_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
69 |
real_is_int_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
70 |
real_is_rat_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
71 |
rat_to_int_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
72 |
real_to_int_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
73 |
int_to_rat_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
74 |
real_to_rat_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
75 |
int_to_real_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
76 |
rat_to_real_def [simp] |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
77 |
|
61076 | 78 |
lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n::int))" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
79 |
by (metis int_to_rat_def rat_is_int_def) |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
80 |
|
61076 | 81 |
lemma to_real_is_int [intro, simp]: "is_int (to_real (n::int))" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61076
diff
changeset
|
82 |
by (metis Ints_of_int int_to_real_def real_is_int_def) |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
83 |
|
61076 | 84 |
lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q::rat))" |
43806
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
85 |
by (metis Rats_of_rat rat_to_real_def real_is_rat_def) |
6b158ce2b5e2
added some arithmetic functions, for THF with arithmetic
blanchet
parents:
43805
diff
changeset
|
86 |
|
61076 | 87 |
lemma inj_of_rat [intro, simp]: "inj (of_rat::rat\<Rightarrow>real)" |
58042
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
47792
diff
changeset
|
88 |
by (metis injI of_rat_eq_iff) |
42063
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset
|
89 |
|
a2a69b32d899
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
blanchet
parents:
diff
changeset
|
90 |
end |