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