author | haftmann |
Fri, 13 Oct 2006 12:32:44 +0200 | |
changeset 21009 | 0eae3fb48936 |
parent 20634 | 45fe31e72391 |
child 22917 | 3c56b12fd946 |
permissions | -rw-r--r-- |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
1 |
(* |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
3 |
Author: Amine Chaieb, TU Muenchen |
20634 | 4 |
*) |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
5 |
|
20634 | 6 |
header {* Ferrante and Rackoff Algorithm: LCF-proof-synthesis version. *} |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
7 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
8 |
theory Ferrante_Rackoff |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
9 |
imports RealPow |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
10 |
uses ("ferrante_rackoff_proof.ML") ("ferrante_rackoff.ML") |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
11 |
begin |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
12 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
13 |
(* Synthesis of \<exists>z. \<forall>x<z. P x = P1 *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
14 |
lemma minf: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
15 |
"\<exists>(z::real) . \<forall>x<z. x < t = True " "\<exists>(z::real) . \<forall>x<z. x > t = False " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
16 |
"\<exists>(z::real) . \<forall>x<z. x \<le> t = True " "\<exists>(z::real) . \<forall>x<z. x \<ge> t = False " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
17 |
"\<exists>(z::real) . \<forall>x<z. (x = t) = False " "\<exists>(z::real) . \<forall>x<z. (x \<noteq> t) = True " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
18 |
"\<exists>z. \<forall>(x::real)<z. (P::bool) = P" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
19 |
"\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
20 |
\<exists>z. \<forall>x<z. (P1 x \<and> P2 x) = (P1' \<and> P2')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
21 |
"\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
22 |
\<exists>z. \<forall>x<z. (P1 x \<or> P2 x) = (P1' \<or> P2')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
23 |
by (rule_tac x="t" in exI,simp)+ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
24 |
(clarsimp,rule_tac x="min z1 z2" in exI,simp)+ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
25 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
26 |
lemma minf_ex: "\<lbrakk>\<exists>z. \<forall>x<z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
27 |
by clarsimp (rule_tac x="z - 1" in exI, auto) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
28 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
29 |
(* Synthesis of \<exists>z. \<forall>x>z. P x = P1 *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
30 |
lemma pinf: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
31 |
"\<exists>(z::real) . \<forall>x>z. x < t = False " "\<exists>(z::real) . \<forall>x>z. x > t = True " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
32 |
"\<exists>(z::real) . \<forall>x>z. x \<le> t = False " "\<exists>(z::real) . \<forall>x>z. x \<ge> t = True " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
33 |
"\<exists>(z::real) . \<forall>x>z. (x = t) = False " "\<exists>(z::real) . \<forall>x>z. (x \<noteq> t) = True " |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
34 |
"\<exists>z. \<forall>(x::real)>z. (P::bool) = P" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
35 |
"\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
36 |
\<exists>z. \<forall>x>z. (P1 x \<and> P2 x) = (P1' \<and> P2')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
37 |
"\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
38 |
\<exists>z. \<forall>x>z. (P1 x \<or> P2 x) = (P1' \<or> P2')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
39 |
by (rule_tac x="t" in exI,simp)+ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
40 |
(clarsimp,rule_tac x="max z1 z2" in exI,simp)+ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
41 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
42 |
lemma pinf_ex: "\<lbrakk>\<exists>z. \<forall>x>z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
43 |
by clarsimp (rule_tac x="z+1" in exI, auto) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
44 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
45 |
(* The ~P1 \<and> ~P2 \<and> P x \<longrightarrow> \<exists> u,u' \<in> U. u \<le> x \<le> u'*) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
46 |
lemma nmilbnd: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
47 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
48 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) > t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
49 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
50 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) \<ge> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
51 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
52 |
"t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
53 |
"\<forall> (x::real). ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
54 |
"\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ; |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
55 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
56 |
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
57 |
"\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ; |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
58 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
59 |
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
60 |
by auto (rule_tac x="t" in bexI,simp,simp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
61 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
62 |
lemma npiubnd: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
63 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) < t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
64 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) > t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
65 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) \<le> t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
66 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<ge> t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
67 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) = t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
68 |
"t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<ge> x )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
69 |
"\<forall> (x::real). ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<ge> x )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
70 |
"\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<ge> x) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x )\<rbrakk> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
71 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
72 |
"\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<ge> x) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x )\<rbrakk> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
73 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
74 |
by auto (rule_tac x="t" in bexI,simp,simp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
75 |
lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)\<rbrakk> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
76 |
\<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
77 |
by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
78 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
79 |
(* Synthesis of (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x<u \<and> P x \<and> l < y < u \<longrightarrow> P y*) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
80 |
lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y< t)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
81 |
proof(clarsimp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
82 |
fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
83 |
and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
84 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
85 |
{assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
86 |
with tU noU have "False" by auto} hence "\<not> y>t" by auto hence "y \<le> t" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
87 |
thus "y < t" using tny by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
88 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
89 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
90 |
lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) > t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y> t)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
91 |
proof(clarsimp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
92 |
fix x l u y |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
93 |
assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
94 |
and px: "x > t" and ly: "l<y" and yu:"y < u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
95 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
96 |
{assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
97 |
with tU noU have "False" by auto} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
98 |
hence "\<not> y<t" by auto hence "y \<ge> t" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
99 |
thus "y > t" using tny by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
100 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
101 |
lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
102 |
proof(clarsimp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
103 |
fix x l u y |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
104 |
assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
105 |
and px: "x \<le> t" and ly: "l<y" and yu:"y < u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
106 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
107 |
{assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
108 |
with tU noU have "False" by auto} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
109 |
hence "\<not> y>t" by auto thus "y \<le> t" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
110 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
111 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
112 |
lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<ge> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<ge> t)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
113 |
proof(clarsimp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
114 |
fix x l u y |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
115 |
assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
116 |
and px: "x \<ge> t" and ly: "l<y" and yu:"y < u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
117 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
118 |
{assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
119 |
with tU noU have "False" by auto} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
120 |
hence "\<not> y<t" by auto thus "y \<ge> t" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
121 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
122 |
lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) = t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
123 |
lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<noteq> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
124 |
lemma lin_dense_fm: "\<forall>(x::real) l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
125 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
126 |
lemma lin_dense_conj: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
127 |
"\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 (x::real) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
128 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
129 |
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 (x::real) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
130 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
131 |
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
132 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
133 |
by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
134 |
lemma lin_dense_disj: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
135 |
"\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 (x::real) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
136 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
137 |
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 (x::real) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
138 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
139 |
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
140 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
141 |
by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
142 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
143 |
lemma finite_set_intervals: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
144 |
assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
145 |
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
146 |
shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
147 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
148 |
let ?Mx = "{y. y\<in> S \<and> y \<le> x}" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
149 |
let ?xM = "{y. y\<in> S \<and> x \<le> y}" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
150 |
let ?a = "Max ?Mx" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
151 |
let ?b = "Min ?xM" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
152 |
have MxS: "?Mx \<subseteq> S" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
153 |
hence fMx: "finite ?Mx" using fS finite_subset by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
154 |
from lx linS have linMx: "l \<in> ?Mx" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
155 |
hence Mxne: "?Mx \<noteq> {}" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
156 |
have xMS: "?xM \<subseteq> S" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
157 |
hence fxM: "finite ?xM" using fS finite_subset by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
158 |
from xu uinS have linxM: "u \<in> ?xM" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
159 |
hence xMne: "?xM \<noteq> {}" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
160 |
have ax:"?a \<le> x" using Mxne fMx by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
161 |
have xb:"x \<le> ?b" using xMne fxM by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
162 |
have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
163 |
have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
164 |
have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
165 |
proof(clarsimp) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
166 |
fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
167 |
from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
168 |
moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
169 |
moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
170 |
ultimately show "False" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
171 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
172 |
from ainS binS noy ax xb px show ?thesis by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
173 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
174 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
175 |
lemma finite_set_intervals2: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
176 |
assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
177 |
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
178 |
shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
179 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
180 |
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
181 |
obtain a and b where |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
182 |
as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
183 |
and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
184 |
from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
185 |
thus ?thesis using px as bs noS by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
186 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
187 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
188 |
lemma rinf_U: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
189 |
assumes fU: "finite U" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
190 |
and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
191 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
192 |
and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
193 |
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P (x::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
194 |
shows "\<exists> u\<in> U. \<exists> u' \<in> U. P ((u + u') / 2)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
195 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
196 |
from ex obtain x where px: "P x" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
197 |
from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u'" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
198 |
then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<le> x" and xu':"x \<le> u'" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
199 |
from uU have Une: "U \<noteq> {}" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
200 |
let ?l = "Min U" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
201 |
let ?u = "Max U" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
202 |
have linM: "?l \<in> U" using fU Une by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
203 |
have uinM: "?u \<in> U" using fU Une by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
204 |
have lM: "\<forall> t\<in> U. ?l \<le> t" using Une fU by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
205 |
have Mu: "\<forall> t\<in> U. t \<le> ?u" using Une fU by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
206 |
have "?l \<le> u" using uU Une lM by auto hence lx: "?l \<le> x" using ux by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
207 |
have "u' \<le> ?u" using uU' Une Mu by simp hence xu: "x \<le> ?u" using xu' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
208 |
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
209 |
have "(\<exists> s\<in> U. P s) \<or> |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
210 |
(\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x)" . |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
211 |
moreover { fix u assume um: "u\<in>U" and pu: "P u" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
212 |
have "(u + u) / 2 = u" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
213 |
with um pu have "P ((u + u) / 2)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
214 |
with um have ?thesis by blast} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
215 |
moreover{ |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
216 |
assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
217 |
then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
218 |
and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U" and t1x: "t1 < x" and xt2: "x < t2" and px: "P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
219 |
by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
220 |
from t1x xt2 have t1t2: "t1 < t2" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
221 |
let ?u = "(t1 + t2) / 2" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
222 |
from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
223 |
from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
224 |
with t1M t2M have ?thesis by blast} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
225 |
ultimately show ?thesis by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
226 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
227 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
228 |
theorem fr_eq: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
229 |
assumes fU: "finite U" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
230 |
and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
231 |
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
232 |
and nmibnd: "\<forall>x. \<not> MP \<and> P (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
233 |
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
234 |
and mi: "\<exists>z. \<forall>x<z. P x = MP" and pi: "\<exists>z. \<forall>x>z. P x = PP" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
235 |
shows "(\<exists> x. P (x::real)) = (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P ((u + u') / 2)))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
236 |
(is "_ = (_ \<or> _ \<or> ?F)" is "?E = ?D") |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
237 |
proof |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
238 |
assume px: "\<exists> x. P x" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
239 |
have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
240 |
moreover {assume "MP \<or> PP" hence "?D" by blast} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
241 |
moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
242 |
from npmibnd[OF nmibnd npibnd] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
243 |
have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" . |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
244 |
from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
245 |
ultimately show "?D" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
246 |
next |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
247 |
assume "?D" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
248 |
moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
249 |
moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . } |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
250 |
moreover {assume f:"?F" hence "?E" by blast} |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
251 |
ultimately show "?E" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
252 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
253 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
254 |
lemma fr_simps: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
255 |
"(True | P) = True" "(P | True) = True" "(True & P) = P" "(P & True) = P" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
256 |
"(P & P) = P" "(P & (P & P')) = (P & P')" "(P & (P | P')) = P" "(False | P) = P" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
257 |
"(P | False) = P" "(False & P) = False" "(P & False) = False" "(P | P) = P" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
258 |
"(P | (P | P')) = (P | P')" "(P | (P & P')) = P" "(~ True) = False" "(~ False) = True" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
259 |
"(x::real) \<le> x" "(\<exists> u\<in> {}. Q u) = False" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
260 |
"(\<exists> u\<in> (insert (x::real) U). \<exists>u'\<in> (insert x U). R ((u+u') / 2)) = |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
261 |
((R x) \<or> (\<exists>u\<in>U. R((x+u) / 2))\<or> (\<exists> u\<in> U. \<exists> u'\<in> U. R ((u + u') /2)))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
262 |
"(\<exists> u\<in> (insert (x::real) U). R u) = (R x \<or> (\<exists> u\<in> U. R u))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
263 |
"Q' (((t::real) + t)/2) = Q' t" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
264 |
by (auto simp add: add_ac) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
265 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
266 |
lemma fr_prepqelim: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
267 |
"(\<exists> x. True) = True" "(\<exists> x. False) = False" "(ALL x. A x) = (~ (EX x. ~ (A x)))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
268 |
"(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" "(\<not> (P \<longrightarrow> Q)) = (P \<and> (\<not> Q))" "(\<not> (P = Q)) = ((\<not> P) = Q)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
269 |
"(\<not> (P \<and> Q)) = ((\<not> P) \<or> (\<not> Q))" "(\<not> (P \<or> Q)) = ((\<not> P) \<and> (\<not> Q))" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
270 |
by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
271 |
(* Lemmas for the normalization of Expressions *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
272 |
lemma nadd_cong: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
273 |
assumes m: "m'*m = l" and n: "n'*n = (l::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
274 |
and mz: "m \<noteq> 0" and nz: "n \<noteq> 0" and lz: "l \<noteq> 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
275 |
and ad: "(m'*t + n'*s) = t'" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
276 |
shows "t/m + s/n = (t' / l)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
277 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
278 |
from lz m n have mz': "m'\<noteq>0" and nz':"n' \<noteq> 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
279 |
have "t' / l = (m'*t + n'*s) / l" using ad by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
280 |
also have "\<dots> = (m'*t) / l + (n'*s) / l" by (simp add: add_divide_distrib) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
281 |
also have "\<dots> = (m'*t) /(m'*m) + (n'*s) /(n'*n)" using m n by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
282 |
also have "\<dots> = t/m + s/n" using mz nz mz' nz' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
283 |
finally show ?thesis by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
284 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
285 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
286 |
lemma nadd_cong_same: "\<lbrakk> (n::real) = m ; t+s = t'\<rbrakk> \<Longrightarrow> t/n + s/m = t'/n" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
287 |
by (simp add: add_divide_distrib[symmetric]) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
288 |
lemma plus_cong: "\<lbrakk>t = t'; s = s'; t' + s' = r\<rbrakk> \<Longrightarrow> t+s = r" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
289 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
290 |
lemma diff_cong: "\<lbrakk>t = t'; s = s'; t' - s' = r\<rbrakk> \<Longrightarrow> t-s = r" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
291 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
292 |
lemma mult_cong2: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> t*c = r" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
293 |
by (simp add: mult_ac) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
294 |
lemma mult_cong: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> c*t = r" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
295 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
296 |
lemma divide_cong: "\<lbrakk> (t::real) = t' ; t'/n = r\<rbrakk> \<Longrightarrow> t/n = r" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
297 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
298 |
lemma naddh_cong_ts: "\<lbrakk>t1 + (s::real) = t'\<rbrakk> \<Longrightarrow> (x + t1) + s = x + t'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
299 |
lemma naddh_cong_st: "\<lbrakk>(t::real) + s = t'\<rbrakk> \<Longrightarrow> t+ (x + s) = x + t'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
300 |
lemma naddh_cong_same: "\<lbrakk>(c1::real) + c2 = c ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = c*x + t" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
301 |
by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric]) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
302 |
lemma naddh_cong_same0: "\<lbrakk>(c1::real) + c2 = 0 ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = t" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
303 |
by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric]) simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
304 |
lemma ncmul_congh: "\<lbrakk> c*c' = (k::real) ; c*t = t'\<rbrakk> \<Longrightarrow> c*(c'*x + t) = k*x + t'" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
305 |
by (simp add: ring_eq_simps) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
306 |
lemma ncmul_cong: "\<lbrakk> c / n = c'/n' ; c'*t = (t'::real)\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
307 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
308 |
assume "c / n = c'/n'" and "c'*t = (t'::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
309 |
have "\<lbrakk> c' / n' = c/n ; (t'::real) = c'*t\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
310 |
by (simp add: divide_inverse ring_eq_simps) thus ?thesis using prems by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
311 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
312 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
313 |
lemma nneg_cong: "(-1 ::real)*t = t' \<Longrightarrow> - t = t'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
314 |
lemma uminus_cong: "\<lbrakk> t = t' ; - t' = r\<rbrakk> \<Longrightarrow> - t = r" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
315 |
lemma nsub_cong: "\<lbrakk>- (s::real) = s'; t + s' = t'\<rbrakk> \<Longrightarrow> t - s = t'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
316 |
lemma ndivide_cong: "m*n = (m'::real) \<Longrightarrow> (t/m) / n = t / m'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
317 |
lemma normalizeh_var: "(x::real) = (1*x + 0) / 1" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
318 |
lemma nrefl: "(x::real) = x/1" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
319 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
320 |
(* cong rules for atoms normalization *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
321 |
(* the < -case *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
322 |
lemma normalize_ltxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
323 |
and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
324 |
shows "(s < t) = (x < r'/c')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
325 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
326 |
from cnp have cnz: "c \<noteq> 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
327 |
from cnp have nnz: "n\<noteq>0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
328 |
from rr' have rr'': "-(r/c) = r'/c'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
329 |
have "s < t = (s - t < 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
330 |
also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
331 |
also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
332 |
also have "\<dots> = ( (n/c)*((c/n)*x + r/n) < (n/c)*0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
333 |
using cnp mult_less_cancel_left[where c="(n/c)" and b="0"] by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
334 |
also have "\<dots> = (x + r/c < 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
335 |
using cnz nnz by (simp add: add_divide_distrib ring_eq_simps) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
336 |
also have "\<dots> = (x < - (r/c))" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
337 |
finally show ?thesis using rr'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
338 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
339 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
340 |
lemma normalize_ltxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
341 |
and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
342 |
shows "(s < t) = (x > r'/c')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
343 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
344 |
from cnp have cnz: "c \<noteq> 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
345 |
from cnp have nnz: "n\<noteq>0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
346 |
from cnp have cnp': "\<not> (n/c > 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
347 |
from rr' have rr'': "-(r/c) = r'/c'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
348 |
have "s < t = (s - t < 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
349 |
also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
350 |
also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
351 |
also have "\<dots> = ( (n/c)*((c/n)*x + r/n) > 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
352 |
using zero_less_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp cnp' simp_thms] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
353 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
354 |
also have "\<dots> = (x + r/c > 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
355 |
using cnz nnz by (simp add: add_divide_distrib ring_eq_simps) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
356 |
also have "\<dots> = (x > - (r/c))" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
357 |
finally show ?thesis using rr'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
358 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
359 |
lemma normalize_ltground_cong: "\<lbrakk> s -t = (r::real) ; r < 0 = P\<rbrakk> \<Longrightarrow> s < t = P" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
360 |
lemma normalize_ltnoxpos_cong: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
361 |
assumes st: "s - t = (r::real) / n" and mp: "n > 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
362 |
shows "s < t = (r <0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
363 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
364 |
have "s < t = (s - t < 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
365 |
also have "\<dots> = (r / n < 0)" using st by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
366 |
also have "\<dots> = (n* (r/n) < 0)" using mult_less_0_iff[where a="n" and b="r/n"] mp by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
367 |
finally show ?thesis using mp by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
368 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
369 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
370 |
lemma normalize_ltnoxneg_cong: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
371 |
assumes st: "s - t = (r::real) / n" and mp: "n < 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
372 |
shows "s < t = (r > 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
373 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
374 |
have "s < t = (s - t < 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
375 |
also have "\<dots> = (r / n < 0)" using st by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
376 |
also have "\<dots> = (n* (r/n) > 0)" using zero_less_mult_iff[where a="n" and b="r/n"] mp by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
377 |
finally show ?thesis using mp by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
378 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
379 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
380 |
(* the <= -case *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
381 |
lemma normalize_lexpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
382 |
and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
383 |
shows "(s \<le> t) = (x \<le> r'/c')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
384 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
385 |
from cnp have cnz: "c \<noteq> 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
386 |
from cnp have nnz: "n\<noteq>0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
387 |
from rr' have rr'': "-(r/c) = r'/c'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
388 |
have "s \<le> t = (s - t \<le> 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
389 |
also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
390 |
also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
391 |
also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<le> (n/c)*0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
392 |
using cnp mult_le_cancel_left[where c="(n/c)" and b="0"] by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
393 |
also have "\<dots> = (x + r/c \<le> 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
394 |
using cnz nnz by (simp add: add_divide_distrib ring_eq_simps) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
395 |
also have "\<dots> = (x \<le> - (r/c))" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
396 |
finally show ?thesis using rr'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
397 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
398 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
399 |
lemma normalize_lexneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
400 |
and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
401 |
shows "(s \<le> t) = (x \<ge> r'/c')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
402 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
403 |
from cnp have cnz: "c \<noteq> 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
404 |
from cnp have nnz: "n\<noteq>0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
405 |
from cnp have cnp': "\<not> (n/c \<ge> 0) \<and> n/c \<le> 0" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
406 |
from rr' have rr'': "-(r/c) = r'/c'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
407 |
have "s \<le> t = (s - t \<le> 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
408 |
also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
409 |
also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
410 |
also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<ge> 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
411 |
using zero_le_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp' simp_thms] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
412 |
by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
413 |
also have "\<dots> = (x + r/c \<ge> 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
414 |
using cnz nnz by (simp add: add_divide_distrib ring_eq_simps) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
415 |
also have "\<dots> = (x \<ge> - (r/c))" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
416 |
finally show ?thesis using rr'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
417 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
418 |
lemma normalize_leground_cong: "\<lbrakk> s -t = (r::real) ; r \<le> 0 = P\<rbrakk> \<Longrightarrow> s \<le> t = P" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
419 |
lemma normalize_lenoxpos_cong: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
420 |
assumes st: "s - t = (r::real) / n" and mp: "n > 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
421 |
shows "s \<le> t = (r \<le>0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
422 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
423 |
have "s \<le> t = (s - t \<le> 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
424 |
also have "\<dots> = (r / n \<le> 0)" using st by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
425 |
also have "\<dots> = (n* (r/n) \<le> 0)" using mult_le_0_iff[where a="n" and b="r/n"] mp by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
426 |
finally show ?thesis using mp by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
427 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
428 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
429 |
lemma normalize_lenoxneg_cong: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
430 |
assumes st: "s - t = (r::real) / n" and mp: "n < 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
431 |
shows "s \<le> t = (r \<ge> 0)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
432 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
433 |
have "s \<le> t = (s - t \<le> 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
434 |
also have "\<dots> = (r / n \<le> 0)" using st by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
435 |
also have "\<dots> = (n* (r/n) \<ge> 0)" using zero_le_mult_iff[where a="n" and b="r/n"] mp by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
436 |
finally show ?thesis using mp by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
437 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
438 |
(* The = -case *) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
439 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
440 |
lemma normalize_eqxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
441 |
and cp: "c > 0" and nnz: "n \<noteq> 0" and rr': "r+ r' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
442 |
shows "(s = t) = (x = r'/c)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
443 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
444 |
from rr' have rr'': "-r = r'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
445 |
have "(s = t) = (s - t = 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
446 |
also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
447 |
also have "\<dots> = (c*x = -r)" using nnz by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
448 |
also have "\<dots> = (x = (-r) / c)" using cp eq_divide_eq[where c="c" and a="x" and b="-r"] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
449 |
by (simp add: mult_ac) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
450 |
finally show ?thesis using rr'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
451 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
452 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
453 |
lemma normalize_eqxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
454 |
and cp: "c < 0" and nnz: "n \<noteq> 0" and cc': "c+ c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
455 |
shows "(s = t) = (x = r/c')" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
456 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
457 |
from cc' have cc'': "-c = c'" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
458 |
have "(s = t) = (s - t = 0)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
459 |
also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
460 |
also have "\<dots> = ((-c)*x = r)" using nnz by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
461 |
also have "\<dots> = (x = r / (-c))" using cp eq_divide_eq[where c="-c" and a="x" and b="r"] |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
462 |
by (simp add: mult_ac) |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
463 |
finally show ?thesis using cc'' by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
464 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
465 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
466 |
lemma normalize_eqnox_cong: "\<lbrakk>s - t = (r::real) / n;n \<noteq> 0\<rbrakk> \<Longrightarrow> s = t = (r = 0)" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
467 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
468 |
lemma normalize_eqground_cong: "\<lbrakk>s - t =(r::real)/n;n \<noteq> 0;(r = 0) = P \<rbrakk> \<Longrightarrow> s=t = P" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
469 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
470 |
lemma trivial_sum_of_opposites: "-t = t' \<Longrightarrow> t + t' = (0::real)" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
471 |
lemma sum_of_opposite_denoms: |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
472 |
assumes cc': "(c::real) + c' = 0" shows "r/c + r/c' = 0" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
473 |
proof- |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
474 |
from cc' have "c' = -c" by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
475 |
thus ?thesis by simp |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
476 |
qed |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
477 |
lemma sum_of_same_denoms: " -r = (r'::real) \<Longrightarrow> r/c + r'/c = 0" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
478 |
lemma normalize_not_lt: "t \<le> (s::real) = P \<Longrightarrow> (\<not> s<t) = P" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
479 |
lemma normalize_not_le: "t < (s::real) = P \<Longrightarrow> (\<not> s\<le>t) = P" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
480 |
lemma normalize_not_eq: "\<lbrakk> t = (s::real) = P ; (~P) = P' \<rbrakk> \<Longrightarrow> (s\<noteq>t) = P'" by auto |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
481 |
lemma ex_eq_cong: "(!! x. A x = B x) \<Longrightarrow> ((\<exists>x. A x) = (\<exists> x. B x))" by blast |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
482 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
483 |
use "ferrante_rackoff_proof.ML" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
484 |
use "ferrante_rackoff.ML" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
485 |
setup "Ferrante_Rackoff.setup" |
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
486 |
|
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
diff
changeset
|
487 |
end |