author | wenzelm |
Mon, 21 Feb 2011 23:47:19 +0100 | |
changeset 41807 | ab5d2d81f9fb |
parent 33356 | 9157d0f9f00e |
child 44779 | 98d597c4193d |
permissions | -rw-r--r-- |
31021 | 1 |
(* Author: Bernhard Haeupler |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
2 |
|
17388 | 3 |
This theory is about of the relative completeness of method comm-ring |
4 |
method. As long as the reified atomic polynomials of type 'a pol are |
|
5 |
in normal form, the cring method is complete. |
|
6 |
*) |
|
7 |
||
8 |
header {* Proof of the relative completeness of method comm-ring *} |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
9 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
10 |
theory Commutative_Ring_Complete |
17508 | 11 |
imports Commutative_Ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
12 |
begin |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
13 |
|
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
14 |
text {* Formalization of normal form *} |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
15 |
fun |
31021 | 16 |
isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool" |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
17 |
where |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
18 |
"isnorm (Pc c) \<longleftrightarrow> True" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
19 |
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
20 |
| "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
21 |
| "isnorm (Pinj 0 P) \<longleftrightarrow> False" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
22 |
| "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
23 |
| "isnorm (PX P 0 Q) \<longleftrightarrow> False" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
24 |
| "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
25 |
| "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
26 |
| "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
27 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
28 |
(* Some helpful lemmas *) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
29 |
lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
30 |
by(cases P, auto) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
31 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
32 |
lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
33 |
by(cases i, auto) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
34 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
35 |
lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
36 |
by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
37 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
38 |
lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
39 |
by(cases i, auto, cases P, auto, case_tac pol2, auto) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
40 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
41 |
lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
42 |
by(cases i, auto, cases P, auto, case_tac pol2, auto) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
43 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
44 |
lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
45 |
apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
46 |
apply(case_tac nat, auto simp add: norm_Pinj_0_False) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
47 |
by(case_tac pol, auto) (case_tac y, auto) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
48 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
49 |
lemma norm_PXtrans: |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
50 |
assumes A:"isnorm (PX P x Q)" and "isnorm Q2" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
51 |
shows "isnorm (PX P x Q2)" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
52 |
proof(cases P) |
41807 | 53 |
case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
54 |
next |
41807 | 55 |
case Pc with assms show ?thesis by (cases x) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
56 |
next |
41807 | 57 |
case Pinj with assms show ?thesis by (cases x) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
58 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
59 |
|
41807 | 60 |
lemma norm_PXtrans2: |
61 |
assumes "isnorm (PX P x Q)" and "isnorm Q2" |
|
62 |
shows "isnorm (PX P (Suc (n+x)) Q2)" |
|
63 |
proof (cases P) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
64 |
case (PX p1 y p2) |
41807 | 65 |
with assms show ?thesis by (cases x, auto, cases p2, auto) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
66 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
67 |
case Pc |
41807 | 68 |
with assms show ?thesis by (cases x) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
69 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
70 |
case Pinj |
41807 | 71 |
with assms show ?thesis by (cases x) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
72 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
73 |
|
23266 | 74 |
text {* mkPX conserves normalizedness (@{text "_cn"}) *} |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
75 |
lemma mkPX_cn: |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
76 |
assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
77 |
shows "isnorm (mkPX P x Q)" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
78 |
proof(cases P) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
79 |
case (Pc c) |
41807 | 80 |
with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
81 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
82 |
case (Pinj i Q) |
41807 | 83 |
with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
84 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
85 |
case (PX P1 y P2) |
41807 | 86 |
with assms have Y0: "y>0" by (cases y) auto |
87 |
from assms PX have "isnorm P1" "isnorm P2" |
|
88 |
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) |
|
89 |
from assms PX Y0 show ?thesis |
|
90 |
by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
91 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
92 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
93 |
text {* add conserves normalizedness *} |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
94 |
lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
95 |
proof(induct P Q rule: add.induct) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
96 |
case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
97 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
98 |
case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
99 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
100 |
case (4 c P2 i Q2) |
41807 | 101 |
then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
102 |
with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
103 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
104 |
case (5 P2 i Q2 c) |
41807 | 105 |
then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
106 |
with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
107 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
108 |
case (6 x P2 y Q2) |
41807 | 109 |
then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) |
110 |
with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
111 |
have "x < y \<or> x = y \<or> x > y" by arith |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
112 |
moreover |
41807 | 113 |
{ assume "x<y" hence "EX d. y =d + x" by arith |
114 |
then obtain d where y: "y = d + x" .. |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
115 |
moreover |
41807 | 116 |
note 6 X0 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
117 |
moreover |
41807 | 118 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
119 |
moreover |
41807 | 120 |
from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) |
121 |
ultimately have ?case by (simp add: mkPinj_cn) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
122 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
123 |
{ assume "x=y" |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
124 |
moreover |
41807 | 125 |
from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
126 |
moreover |
41807 | 127 |
note 6 Y0 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
128 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
129 |
ultimately have ?case by (simp add: mkPinj_cn) } |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
130 |
moreover |
41807 | 131 |
{ assume "x>y" hence "EX d. x = d + y" by arith |
132 |
then obtain d where x: "x = d + y".. |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
133 |
moreover |
41807 | 134 |
note 6 Y0 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
135 |
moreover |
41807 | 136 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
137 |
moreover |
41807 | 138 |
from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
139 |
ultimately have ?case by (simp add: mkPinj_cn)} |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
140 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
141 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
142 |
case (7 x P2 Q2 y R) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
143 |
have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
144 |
moreover |
41807 | 145 |
{ assume "x = 0" |
146 |
with 7 have ?case by (auto simp add: norm_Pinj_0_False) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
147 |
moreover |
41807 | 148 |
{ assume "x = 1" |
149 |
from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
150 |
with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp |
|
151 |
with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
152 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
153 |
{ assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
154 |
then obtain d where X:"x=Suc (Suc d)" .. |
41807 | 155 |
with 7 have NR: "isnorm R" "isnorm P2" |
156 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
157 |
with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
|
158 |
with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp |
|
159 |
with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
160 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
161 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
162 |
case (8 Q2 y R x P2) |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
163 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
164 |
moreover |
41807 | 165 |
{ assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
166 |
moreover |
41807 | 167 |
{ assume "x = 1" |
168 |
with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
169 |
with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp |
|
170 |
with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
171 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
172 |
{ assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith |
41807 | 173 |
then obtain d where X: "x = Suc (Suc d)" .. |
174 |
with 8 have NR: "isnorm R" "isnorm P2" |
|
175 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
176 |
with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
|
177 |
with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp |
|
178 |
with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
179 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
180 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
181 |
case (9 P1 x P2 Q1 y Q2) |
41807 | 182 |
then have Y0: "y>0" by (cases y) auto |
183 |
with 9 have X0: "x>0" by (cases x) auto |
|
184 |
with 9 have NP1: "isnorm P1" and NP2: "isnorm P2" |
|
185 |
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) |
|
186 |
with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2" |
|
187 |
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
188 |
have "y < x \<or> x = y \<or> x < y" by arith |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
189 |
moreover |
41807 | 190 |
{ assume sm1: "y < x" hence "EX d. x = d + y" by arith |
191 |
then obtain d where sm2: "x = d + y" .. |
|
192 |
note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
193 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
194 |
have "isnorm (PX P1 d (Pc 0))" |
41807 | 195 |
proof (cases P1) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
196 |
case (PX p1 y p2) |
41807 | 197 |
with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto) |
198 |
next |
|
199 |
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
200 |
next |
|
201 |
case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
202 |
qed |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
203 |
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto |
41807 | 204 |
with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) } |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
205 |
moreover |
41807 | 206 |
{ assume "x = y" |
207 |
with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto |
|
208 |
with `x = y` Y0 have ?case by (simp add: mkPX_cn) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
209 |
moreover |
41807 | 210 |
{ assume sm1: "x < y" hence "EX d. y = d + x" by arith |
211 |
then obtain d where sm2: "y = d + x" .. |
|
212 |
note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
213 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
214 |
have "isnorm (PX Q1 d (Pc 0))" |
41807 | 215 |
proof (cases Q1) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
216 |
case (PX p1 y p2) |
41807 | 217 |
with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto) |
218 |
next |
|
219 |
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
220 |
next |
|
221 |
case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
222 |
qed |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
223 |
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
224 |
with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)} |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
225 |
ultimately show ?case by blast |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
226 |
qed simp |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
227 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
228 |
text {* mul concerves normalizedness *} |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
229 |
lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
230 |
proof(induct P Q rule: mul.induct) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
231 |
case (2 c i P2) thus ?case |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
232 |
by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
233 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
234 |
case (3 i P2 c) thus ?case |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
235 |
by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
236 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
237 |
case (4 c P2 i Q2) |
41807 | 238 |
then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
239 |
with 4 show ?case |
|
240 |
by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
241 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
242 |
case (5 P2 i Q2 c) |
41807 | 243 |
then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
244 |
with 5 show ?case |
|
245 |
by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
246 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
247 |
case (6 x P2 y Q2) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
248 |
have "x < y \<or> x = y \<or> x > y" by arith |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
249 |
moreover |
41807 | 250 |
{ assume "x < y" hence "EX d. y = d + x" by arith |
251 |
then obtain d where y: "y = d + x" .. |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
252 |
moreover |
41807 | 253 |
note 6 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
254 |
moreover |
41807 | 255 |
from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
256 |
moreover |
41807 | 257 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
258 |
moreover |
41807 | 259 |
from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto) |
260 |
ultimately have ?case by (simp add: mkPinj_cn) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
261 |
moreover |
41807 | 262 |
{ assume "x = y" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
263 |
moreover |
41807 | 264 |
from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
265 |
moreover |
41807 | 266 |
from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
267 |
moreover |
41807 | 268 |
note 6 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
269 |
moreover |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
270 |
ultimately have ?case by (simp add: mkPinj_cn) } |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
271 |
moreover |
41807 | 272 |
{ assume "x > y" hence "EX d. x = d + y" by arith |
273 |
then obtain d where x: "x = d + y" .. |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
274 |
moreover |
41807 | 275 |
note 6 |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
276 |
moreover |
41807 | 277 |
from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
278 |
moreover |
41807 | 279 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
280 |
moreover |
41807 | 281 |
from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
282 |
ultimately have ?case by (simp add: mkPinj_cn) } |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
283 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
284 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
285 |
case (7 x P2 Q2 y R) |
41807 | 286 |
then have Y0: "y > 0" by (cases y) auto |
287 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
288 |
moreover |
41807 | 289 |
{ assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) } |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
290 |
moreover |
41807 | 291 |
{ assume "x = 1" |
292 |
from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
293 |
with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) |
|
294 |
with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
295 |
moreover |
41807 | 296 |
{ assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith |
297 |
then obtain d where X: "x = Suc (Suc d)" .. |
|
298 |
from 7 have NR: "isnorm R" "isnorm Q2" |
|
299 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
300 |
moreover |
41807 | 301 |
from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
302 |
moreover |
|
303 |
from 7 have "isnorm (Pinj x P2)" by (cases P2) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
304 |
moreover |
41807 | 305 |
note 7 X |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
306 |
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto |
41807 | 307 |
with Y0 X have ?case by (simp add: mkPX_cn) } |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
308 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
309 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
310 |
case (8 Q2 y R x P2) |
41807 | 311 |
then have Y0: "y>0" by (cases y) auto |
312 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
313 |
moreover |
41807 | 314 |
{ assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
315 |
moreover |
41807 | 316 |
{ assume "x = 1" |
317 |
from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
318 |
with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) |
|
319 |
with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) } |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
320 |
moreover |
41807 | 321 |
{ assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith |
322 |
then obtain d where X: "x = Suc (Suc d)" .. |
|
323 |
from 8 have NR: "isnorm R" "isnorm Q2" |
|
324 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
325 |
moreover |
41807 | 326 |
from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
327 |
moreover |
41807 | 328 |
from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
329 |
moreover |
41807 | 330 |
note 8 X |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
331 |
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
332 |
with Y0 X have ?case by (simp add: mkPX_cn) } |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
333 |
ultimately show ?case by blast |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
334 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
335 |
case (9 P1 x P2 Q1 y Q2) |
41807 | 336 |
from 9 have X0: "x > 0" by (cases x) auto |
337 |
from 9 have Y0: "y > 0" by (cases y) auto |
|
338 |
note 9 |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
339 |
moreover |
41807 | 340 |
from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
341 |
moreover |
41807 | 342 |
from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
343 |
ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
344 |
"isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
345 |
by (auto simp add: mkPinj_cn) |
41807 | 346 |
with 9 X0 Y0 have |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
347 |
"isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
348 |
"isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
349 |
"isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
350 |
by (auto simp add: mkPX_cn) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
351 |
thus ?case by (simp add: add_cn) |
41807 | 352 |
qed simp |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
353 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
354 |
text {* neg conserves normalizedness *} |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
355 |
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)" |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
356 |
proof (induct P) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
357 |
case (Pinj i P2) |
41807 | 358 |
then have "isnorm P2" by (simp add: norm_Pinj[of i P2]) |
359 |
with Pinj show ?case by - (cases P2, auto, cases i, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
360 |
next |
41807 | 361 |
case (PX P1 x P2) note PX1 = this |
362 |
from PX have "isnorm P2" "isnorm P1" |
|
363 |
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
|
364 |
with PX show ?case |
|
365 |
proof (cases P1) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
366 |
case (PX p1 y p2) |
41807 | 367 |
with PX1 show ?thesis by - (cases x, auto, cases p2, auto) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
368 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
369 |
case Pinj |
41807 | 370 |
with PX1 show ?thesis by (cases x) auto |
371 |
qed (cases x, auto) |
|
372 |
qed simp |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
373 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
374 |
text {* sub conserves normalizedness *} |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
375 |
lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
376 |
by (simp add: sub_def add_cn neg_cn) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
377 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
378 |
text {* sqr conserves normalizizedness *} |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
379 |
lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)" |
41807 | 380 |
proof (induct P) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
381 |
case (Pinj i Q) |
41807 | 382 |
then show ?case |
383 |
by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
384 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
385 |
case (PX P1 x P2) |
41807 | 386 |
then have "x + x ~= 0" "isnorm P2" "isnorm P1" |
387 |
by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
|
388 |
with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" |
|
389 |
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" |
|
390 |
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
|
391 |
then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
392 |
qed simp |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
393 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
394 |
text {* pow conserves normalizedness *} |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
395 |
lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
396 |
proof (induct n arbitrary: P rule: nat_less_induct) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
397 |
case (1 k) |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
398 |
show ?case |
41807 | 399 |
proof (cases "k = 0") |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
400 |
case False |
41807 | 401 |
then have K2: "k div 2 < k" by (cases k) auto |
402 |
from 1 have "isnorm (sqr P)" by (simp add: sqr_cn) |
|
403 |
with 1 False K2 show ?thesis |
|
404 |
by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
405 |
qed simp |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
406 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
407 |
|
17388 | 408 |
end |