--- a/Admin/Release/CHECKLIST Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/Release/CHECKLIST Tue Apr 26 22:59:25 2016 +0200
@@ -69,10 +69,13 @@
Packaging
=========
-- fully-automated packaging (requires Mac OS X with gnutar, avoid Mavericks):
+- fully-automated packaging:
hg up -r DISTNAME && Admin/Release/build -O -l -r DISTNAME /home/isabelle/dist
+ Mac OS X: requires gnutar, avoid Mavericks (problems with hdiutil?)
+ Linux: avoid Debian (bitmap fonts for prog-prove)
+
Final release stage
===================
--- a/Admin/lib/Tools/makedist Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/lib/Tools/makedist Tue Apr 26 22:59:25 2016 +0200
@@ -180,7 +180,7 @@
echo "### Preparing distribution $DISTNAME"
-find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
+find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -print | xargs chmod -f -x
find . -print | xargs chmod -f u+rw
export CLASSPATH="$ISABELLE_CLASSPATH"
--- a/Admin/lib/Tools/makedist_bundle Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle Tue Apr 26 22:59:25 2016 +0200
@@ -320,8 +320,13 @@
"contrib/cygwin/isabelle/."
done
- find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
- -print0 > "contrib/cygwin/isabelle/executables"
+ if [ "$ISABELLE_PLATFORM_FAMILY" = macos ]; then
+ find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
+ -print0 > "contrib/cygwin/isabelle/executables"
+ else
+ find . -type f -not -name '*.exe' -not -name '*.dll' -executable \
+ -print0 > "contrib/cygwin/isabelle/executables"
+ fi
find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
> "contrib/cygwin/isabelle/symlinks"
--- a/NEWS Fri Apr 22 17:22:29 2016 +0200
+++ b/NEWS Tue Apr 26 22:59:25 2016 +0200
@@ -64,6 +64,9 @@
'definition' and 'obtain'. It fits better into the Isar language than
old 'def', which is now a legacy feature.
+* Command 'obtain' supports structured statements with 'if' / 'for'
+context.
+
* Command '\<proof>' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.
--- a/src/Doc/Isar_Ref/Proof.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Apr 26 22:59:25 2016 +0200
@@ -1322,8 +1322,12 @@
@{rail \<open>
@@{command consider} @{syntax obtain_clauses}
;
- @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
- @'where' (@{syntax props} + @'and')
+ @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
+ @'where' concl prems @{syntax for_fixes}
+ ;
+ concl: (@{syntax props} + @'and')
+ ;
+ prems: (@'if' (@{syntax props'} + @'and'))?
;
@@{command guess} (@{syntax "fixes"} + @'and')
\<close>}
--- a/src/HOL/Library/ContNotDenum.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Tue Apr 26 22:59:25 2016 +0200
@@ -41,9 +41,10 @@
by (auto simp add: not_le cong: conj_cong)
(metis dense le_less_linear less_linear less_trans order_refl)
then obtain i j where ij:
- "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
- "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
- "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+ "a < b \<Longrightarrow> i a b c < j a b c"
+ "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
+ "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+ for a b c :: real
by metis
define ivl where "ivl =
@@ -78,7 +79,7 @@
finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
by auto
qed (auto simp: I_def)
- then obtain x where "\<And>n. x \<in> I n"
+ then obtain x where "x \<in> I n" for n
by blast
moreover from \<open>surj f\<close> obtain j where "x = f j"
by blast
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Apr 26 22:59:25 2016 +0200
@@ -1483,7 +1483,7 @@
case (real r)
then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
by (auto simp: le_ennreal_iff)
- then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
+ then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
by metis
from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
proof eventually_elim
--- a/src/HOL/Library/Extended_Real.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Apr 26 22:59:25 2016 +0200
@@ -1696,7 +1696,7 @@
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
case True
- then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
+ then obtain y where y: "a \<le> ereal y" if "a\<in>S" for a
by auto
then have "\<infinity> \<notin> S"
by force
@@ -1705,7 +1705,7 @@
case True
with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
by auto
- obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
+ obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "(\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z" for z
proof (atomize_elim, rule complete_real)
show "\<exists>x. x \<in> ereal -` S"
using x by auto
@@ -1919,7 +1919,7 @@
assumes *: "bdd_below A" "A \<noteq> {}"
shows "ereal (Inf A) = (INF a:A. ereal a)"
proof (rule ereal_Inf)
- from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
+ from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
by (auto simp: bdd_below_def)
then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
by (auto intro!: INF_greatest INF_lower)
@@ -2193,7 +2193,7 @@
by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
next
assume "Sup A \<noteq> -\<infinity>"
- then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
+ then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
by (auto dest: countable_approach)
have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
@@ -2456,7 +2456,7 @@
from \<open>open S\<close>
have "open (ereal -` S)"
by (rule ereal_openE)
- then obtain e where "e > 0" and e: "\<And>y. dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S"
+ then obtain e where "e > 0" and e: "dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S" for y
using assms unfolding open_dist by force
show thesis
proof (intro that subsetI)
@@ -2830,11 +2830,12 @@
assume "open S" and "x \<in> S"
then have "open (ereal -` S)"
unfolding open_ereal_def by auto
- with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
+ with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "dist y rx < r \<Longrightarrow> ereal y \<in> S" for y
unfolding open_dist rx by auto
- then obtain n where
- upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
- lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
+ then obtain n
+ where upper: "u N < x + ereal r"
+ and lower: "x < u N + ereal r"
+ if "n \<le> N" for N
using assms(2)[of "ereal r"] by auto
show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
proof (safe intro!: exI[of _ n])
--- a/src/HOL/Library/Fun_Lexorder.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Fun_Lexorder.thy Tue Apr 26 22:59:25 2016 +0200
@@ -24,9 +24,9 @@
assumes "less_fun f g"
shows "\<not> less_fun g f"
proof
- from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
+ from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
by (blast elim!: less_funE)
- assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
+ assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \<Longrightarrow> g k' = f k'" for k'
by (blast elim!: less_funE)
show False proof (cases k1 k2 rule: linorder_cases)
case equal with k1 k2 show False by simp
@@ -52,9 +52,9 @@
assumes "less_fun f g" and "less_fun g h"
shows "less_fun f h"
proof (rule less_funI)
- from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
- by (blast elim!: less_funE)
- from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
+ from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
+ by (blast elim!: less_funE)
+ from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
by (blast elim!: less_funE)
show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
proof (cases k1 k2 rule: linorder_cases)
--- a/src/HOL/Library/FuncSet.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Apr 26 22:59:25 2016 +0200
@@ -96,9 +96,9 @@
assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
by auto
- from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
+ from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
by auto
- obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+ obtain k where k: "n i \<le> k" if "i \<in> I" for i
using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
have "f \<in> Pi I (A k)"
proof (intro Pi_I)
--- a/src/HOL/Library/Function_Growth.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy Tue Apr 26 22:59:25 2016 +0200
@@ -163,7 +163,7 @@
and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
proof -
from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
- from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+ from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
by (rule less_eq_funE) blast
{ fix c n :: nat
assume "c > 0"
@@ -202,8 +202,8 @@
shows "f \<prec> g"
proof (rule less_funI)
have "1 > (0::nat)" by simp
- from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
- then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
+ with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
+ by blast
have "\<forall>m>n. f m \<le> 1 * g m"
proof (rule allI, rule impI)
fix m
@@ -214,7 +214,7 @@
with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
fix c n :: nat
assume "c > 0"
- with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
+ with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
moreover have "Suc (q + n) > n" by simp
ultimately show "\<exists>m>n. c * f m < g m" by blast
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Apr 26 22:59:25 2016 +0200
@@ -312,7 +312,7 @@
assumes ep: "e > 0"
shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
proof -
- obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
+ obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
proof
show "degree (offset_poly p z) = degree p"
by (rule degree_offset_poly)
@@ -329,7 +329,7 @@
next
case (pCons c cs)
from poly_bound_exists[of 1 "cs"]
- obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
+ obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
by blast
from ep m(1) have em0: "e/m > 0"
by (simp add: field_simps)
@@ -535,12 +535,14 @@
proof (cases "cs = 0")
case False
from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
- obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+ obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+ if "r \<le> cmod z" for z
by blast
have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
by arith
from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
- obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+ obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+ if "cmod w \<le> \<bar>r\<bar>" for w
by blast
have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
using v[of 0] r[OF z] by simp
--- a/src/HOL/Library/Multiset.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Apr 26 22:59:25 2016 +0200
@@ -2075,7 +2075,7 @@
"a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
proof -
from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
- "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+ "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
moreover from this(3) [of a] have "a \<notin># K" by auto
ultimately show thesis by (auto intro: that)
qed
--- a/src/HOL/Library/Polynomial.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Apr 26 22:59:25 2016 +0200
@@ -3353,7 +3353,7 @@
fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
define cs where "cs = coeffs p"
from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
- then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))"
+ then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
by (subst (asm) bchoice_iff) blast
define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
define d where "d = Lcm (set (map snd cs'))"
@@ -3392,9 +3392,8 @@
moreover from root have "poly p' x = 0" by (simp add: p'_def)
ultimately show "algebraic x" unfolding algebraic_def by blast
next
-
assume "algebraic x"
- then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0"
+ then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
by (force simp: algebraic_def)
moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
ultimately show "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
--- a/src/HOL/Library/Ramsey.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Ramsey.thy Tue Apr 26 22:59:25 2016 +0200
@@ -231,8 +231,8 @@
qed
qed
from dependent_choice [OF transr propr0 proprstep]
- obtain g where pg: "!!n::nat. ?propr (g n)"
- and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
+ obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
+ by blast
let ?gy = "fst o g"
let ?gt = "snd o snd o g"
have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Tue Apr 26 22:59:25 2016 +0200
@@ -609,12 +609,13 @@
next
case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
by simp_all
- then obtain A B C where fact:
- "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
+ then obtain A B C
+ where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
- and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
- and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
- and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
+ and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
+ and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
+ and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
+ for p
by (blast elim!: factorizationE)
moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
by simp_all
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Apr 26 22:59:25 2016 +0200
@@ -40,9 +40,9 @@
by (rule types_snocE)
from snoc have "listall ?R bs" by simp
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
- then obtain bs' where
- bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
- and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
+ then obtain bs' where bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
+ and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
+ by iprover
from snoc have "?R b" by simp
with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
by iprover
--- a/src/HOL/ex/Abstract_NAT.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Tue Apr 26 22:59:25 2016 +0200
@@ -23,13 +23,13 @@
by (rule succ_neq_zero [symmetric])
-text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
+text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
where
- Rec_zero: "Rec e r zero e"
- | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
+ Rec_zero: "Rec e r zero e"
+| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
lemma Rec_functional:
fixes x :: 'n
@@ -42,26 +42,30 @@
show "\<exists>!y. ?R zero y"
proof
show "?R zero e" ..
- fix y assume "?R zero y"
- then show "y = e" by cases simp_all
+ show "y = e" if "?R zero y" for y
+ using that by cases simp_all
qed
next
case (succ m)
from \<open>\<exists>!y. ?R m y\<close>
- obtain y where y: "?R m y"
- and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
+ obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
+ by blast
show "\<exists>!z. ?R (succ m) z"
proof
from y show "?R (succ m) (r m y)" ..
- fix z assume "?R (succ m) z"
- then obtain u where "z = r m u" and "?R m u" by cases simp_all
- with yy' show "z = r m y" by (simp only:)
+ next
+ fix z
+ assume "?R (succ m) z"
+ then obtain u where "z = r m u" and "?R m u"
+ by cases simp_all
+ with yy' show "z = r m y"
+ by (simp only:)
qed
qed
qed
-text \<open>\medskip The recursion operator -- polymorphic!\<close>
+text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
where "rec e r x = (THE y. Rec e r x y)"
@@ -86,7 +90,7 @@
qed
-text \<open>\medskip Example: addition (monomorphic)\<close>
+text \<open>\<^medskip> Example: addition (monomorphic)\<close>
definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
where "add m n = rec n (\<lambda>_ k. succ k) m"
@@ -109,7 +113,7 @@
by simp
-text \<open>\medskip Example: replication (polymorphic)\<close>
+text \<open>\<^medskip> Example: replication (polymorphic)\<close>
definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
@@ -124,17 +128,17 @@
end
-text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
+text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
interpretation NAT 0 Suc
proof (rule NAT.intro)
fix m n
show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
show "Suc m \<noteq> 0" by simp
- fix P
- assume zero: "P 0"
+ show "P n"
+ if zero: "P 0"
and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
- show "P n"
+ for P
proof (induct n)
case 0
show ?case by (rule zero)
--- a/src/HOL/ex/CTL.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/CTL.thy Tue Apr 26 22:59:25 2016 +0200
@@ -25,9 +25,8 @@
type_synonym 'a ctl = "'a set"
-definition
- imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) where
- "p \<rightarrow> q = - p \<union> q"
+definition imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
+ where "p \<rightarrow> q = - p \<union> q"
lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
@@ -43,37 +42,38 @@
axiomatization \<M> :: "('a \<times> 'a) set"
text \<open>
- The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken as primitives, while
- \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are defined as derived ones. The formula \<open>\<EX> p\<close>
- holds in a state @{term s}, iff there is a successor state @{term s'} (with
- respect to the model @{term \<M>}), such that @{term p} holds in @{term s'}.
- The formula \<open>\<EF> p\<close> holds in a state @{term s}, iff there is a path in
- \<open>\<M>\<close>, starting from @{term s}, such that there exists a state @{term s'} on
- the path, such that @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close>
- holds in a state @{term s}, iff there is a path, starting from @{term s},
- such that for all states @{term s'} on the path, @{term p} holds in @{term
- s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using
- least and greatest fixed points @{cite "McMillan-PhDThesis"}.
+ The operators \<open>\<^bold>E\<^bold>X\<close>, \<open>\<^bold>E\<^bold>F\<close>, \<open>\<^bold>E\<^bold>G\<close> are taken as primitives, while \<open>\<^bold>A\<^bold>X\<close>,
+ \<open>\<^bold>A\<^bold>F\<close>, \<open>\<^bold>A\<^bold>G\<close> are defined as derived ones. The formula \<open>\<^bold>E\<^bold>X p\<close> holds in a
+ state \<open>s\<close>, iff there is a successor state \<open>s'\<close> (with respect to the model
+ \<open>\<M>\<close>), such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>F p\<close> holds in a state
+ \<open>s\<close>, iff there is a path in \<open>\<M>\<close>, starting from \<open>s\<close>, such that there exists a
+ state \<open>s'\<close> on the path, such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>G p\<close>
+ holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
+ all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
+ p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
+ @{cite "McMillan-PhDThesis"}.
\<close>
-definition EX ("\<EX> _" [80] 90)
- where [simp]: "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
-definition EF ("\<EF> _" [80] 90)
- where [simp]: "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
-definition EG ("\<EG> _" [80] 90)
- where [simp]: "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
+definition EX ("\<^bold>E\<^bold>X _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
+
+definition EF ("\<^bold>E\<^bold>F _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
+
+definition EG ("\<^bold>E\<^bold>G _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)"
text \<open>
- \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined dually in terms of \<open>\<EX>\<close>,
- \<open>\<EF>\<close> and \<open>\<EG>\<close>.
+ \<open>\<^bold>A\<^bold>X\<close>, \<open>\<^bold>A\<^bold>F\<close> and \<open>\<^bold>A\<^bold>G\<close> are now defined dually in terms of \<open>\<^bold>E\<^bold>X\<close>,
+ \<open>\<^bold>E\<^bold>F\<close> and \<open>\<^bold>E\<^bold>G\<close>.
\<close>
-definition AX ("\<AX> _" [80] 90)
- where [simp]: "\<AX> p = - \<EX> - p"
-definition AF ("\<AF> _" [80] 90)
- where [simp]: "\<AF> p = - \<EG> - p"
-definition AG ("\<AG> _" [80] 90)
- where [simp]: "\<AG> p = - \<EF> - p"
+definition AX ("\<^bold>A\<^bold>X _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
+definition AF ("\<^bold>A\<^bold>F _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
+definition AG ("\<^bold>A\<^bold>G _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
subsection \<open>Basic fixed point properties\<close>
@@ -86,8 +86,7 @@
proof
show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
proof
- fix x assume l: "x \<in> lfp f"
- show "x \<in> - gfp (\<lambda>s. - f (- s))"
+ show "x \<in> - gfp (\<lambda>s. - f (- s))" if l: "x \<in> lfp f" for x
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
@@ -100,7 +99,8 @@
qed
show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
proof (rule lfp_greatest)
- fix u assume "f u \<subseteq> u"
+ fix u
+ assume "f u \<subseteq> u"
then have "- u \<subseteq> - f u" by auto
then have "- u \<subseteq> - f (- (- u))" by simp
then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
@@ -115,43 +115,44 @@
by (simp add: lfp_gfp)
text \<open>
- In order to give dual fixed point representations of @{term "\<AF> p"} and
- @{term "\<AG> p"}:
+ In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and
+ @{term "\<^bold>A\<^bold>G p"}:
\<close>
-lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)"
- by (simp add: lfp_gfp)
-lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)"
+lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
by (simp add: lfp_gfp)
-lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
+lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
+ by (simp add: lfp_gfp)
+
+lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
proof -
- have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
+ have "mono (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)" by rule auto
then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
qed
-lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
+lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
proof -
- have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
+ have "mono (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)" by rule auto
then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
qed
-lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
+lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
proof -
- have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
+ have "mono (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)" by rule auto
then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
qed
text \<open>
- From the greatest fixed point definition of @{term "\<AG> p"}, we derive as
+ From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G p"}, we derive as
a consequence of the Knaster-Tarski theorem on the one hand that @{term
- "\<AG> p"} is a fixed point of the monotonic function
- @{term "\<lambda>s. p \<inter> \<AX> s"}.
+ "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function
+ @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"}.
\<close>
-lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
+lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
proof -
- have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
+ have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
qed
@@ -160,27 +161,27 @@
of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
\<close>
-lemma AG_fp_1: "\<AG> p \<subseteq> p"
+lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
+ note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
finally show ?thesis .
qed
-lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
+lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
+ note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by auto
finally show ?thesis .
qed
text \<open>
On the other hand, we have from the Knaster-Tarski fixed point theorem that
- any other post-fixed point of @{term "\<lambda>s. p \<inter> \<AX> s"} is smaller than
- @{term "\<AG> p"}. A post-fixed point is a set of states @{term q} such that
- @{term "q \<subseteq> p \<inter> \<AX> q"}. This leads to the following co-induction
- principle for @{term "\<AG> p"}.
+ any other post-fixed point of @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"} is smaller than
+ @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \<open>q\<close> such that @{term
+ "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for
+ @{term "\<^bold>A\<^bold>G p"}.
\<close>
-lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
+lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
by (simp only: AG_gfp) (rule gfp_upperbound)
@@ -188,92 +189,91 @@
text \<open>
With the most basic facts available, we are now able to establish a few more
- interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<AG>\<close>
+ interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<close>
(see below). We will use some elementary monotonicity and distributivity
rules.
\<close>
-lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
-lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
-lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
- by (simp only: AG_gfp, rule gfp_mono) auto
+lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
+lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G q"
+ by (simp only: AG_gfp, rule gfp_mono) auto
text \<open>
The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of
\<open>\<subseteq>\<close> with monotonicity).
\<close>
-lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
+lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p"
proof -
- have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
- also have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
+ have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+ also have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
moreover note AX_mono
finally show ?thesis .
qed
text \<open>
- Furthermore we show idempotency of the \<open>\<AG>\<close> operator. The proof is a good
+ Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<close> operator. The proof is a good
example of how accumulated facts may get used to feed a single rule step.
\<close>
-lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
+lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
proof
- show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
+ show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
next
- show "\<AG> p \<subseteq> \<AG> \<AG> p"
+ show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"
proof (rule AG_I)
- have "\<AG> p \<subseteq> \<AG> p" ..
- moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
- ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
+ have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
+ moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+ ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..
qed
qed
text \<open>
\<^smallskip>
- We now give an alternative characterization of the \<open>\<AG>\<close> operator, which
- describes the \<open>\<AG>\<close> operator in an ``operational'' way by tree induction:
- In a state holds @{term "AG p"} iff in that state holds @{term p}, and in
- all reachable states @{term s} follows from the fact that @{term p} holds in
- @{term s}, that @{term p} also holds in all successor states of @{term s}.
- We use the co-induction principle @{thm [source] AG_I} to establish this in
- a purely algebraic manner.
+ We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
+ describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
+ In a state holds @{term "AG p"} iff in that state holds \<open>p\<close>, and in all
+ reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
+ also holds in all successor states of \<open>s\<close>. We use the co-induction principle
+ @{thm [source] AG_I} to establish this in a purely algebraic manner.
\<close>
-theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
+theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
proof
- show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
+ show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p" (is "?lhs \<subseteq> _")
proof (rule AG_I)
- show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
+ show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
proof
show "?lhs \<subseteq> p" ..
- show "?lhs \<subseteq> \<AX> ?lhs"
+ show "?lhs \<subseteq> \<^bold>A\<^bold>X ?lhs"
proof -
{
- have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
- also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
- finally have "?lhs \<subseteq> \<AX> p" by auto
- }
+ have "\<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" by (rule AG_fp_1)
+ also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
+ finally have "?lhs \<subseteq> \<^bold>A\<^bold>X p" by auto
+ }
moreover
{
- have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
- also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
- finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
- }
- ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
- also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
+ have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+ also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
+ finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
+ }
+ ultimately have "?lhs \<subseteq> \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+ also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
finally show ?thesis .
qed
qed
qed
next
- show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
+ show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
proof
- show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
- show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
+ show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
+ show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
proof -
- have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
- also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
- also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
+ have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+ also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
+ also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
finally show ?thesis .
qed
qed
@@ -284,30 +284,30 @@
text \<open>
Further interesting properties of CTL expressions may be demonstrated with
- the help of tree induction; here we show that \<open>\<AX>\<close> and \<open>\<AG>\<close> commute.
+ the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
\<close>
-theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
+theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
proof -
- have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
- also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
- also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
- proof
- have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
- also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
+ have "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" by (rule AG_fp)
+ also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
+ also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p" (is "?lhs = _")
+ proof
+ have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
+ also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)
also note Int_mono AG_mono
- ultimately show "?lhs \<subseteq> \<AG> p" by fast
- next
- have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
- moreover
+ ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
+ next
+ have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
+ moreover
{
- have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
- also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
+ have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+ also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
also note AG_mono
- ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
- }
- ultimately show "\<AG> p \<subseteq> ?lhs" ..
- qed
+ ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
+ }
+ ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
+ qed
finally show ?thesis .
qed
--- a/src/HOL/ex/Cartouche_Examples.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Apr 26 22:59:25 2016 +0200
@@ -13,14 +13,14 @@
subsection \<open>Regular outer syntax\<close>
-text \<open>Text cartouches may be used in the outer syntax category "text",
- as alternative to the traditional "verbatim" tokens. An example is
+text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>,
+ as alternative to the traditional \<open>verbatim\<close> tokens. An example is
this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close>
notepad
begin
txt \<open>Moreover, cartouches work as additional syntax in the
- "altstring" category, for literal fact references. For example:\<close>
+ \<open>altstring\<close> category, for literal fact references. For example:\<close>
fix x y :: 'a
assume "x = y"
--- a/src/HOL/ex/Coherent.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Coherent.thy Tue Apr 26 22:59:25 2016 +0200
@@ -16,65 +16,63 @@
relcomp (infixr "O" 75)
lemma p1p2:
- assumes
- "col a b c l \<and> col d e f m"
- "col b f g n \<and> col c e g o"
- "col b d h p \<and> col a e h q"
- "col c d i r \<and> col a f i s"
- "el n o \<Longrightarrow> goal"
- "el p q \<Longrightarrow> goal"
- "el s r \<Longrightarrow> goal"
- "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
- "\<And>A B. pl A B \<Longrightarrow> ep A A"
- "\<And>A B. ep A B \<Longrightarrow> ep B A"
- "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
- "\<And>A B. pl A B \<Longrightarrow> el B B"
- "\<And>A B. el A B \<Longrightarrow> el B A"
- "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
- "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
- "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
- "\<And>A B C D E F G H I J K L M N O P Q.
- col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
- col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
- (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
- "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
- "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+ assumes "col a b c l \<and> col d e f m"
+ and "col b f g n \<and> col c e g o"
+ and "col b d h p \<and> col a e h q"
+ and "col c d i r \<and> col a f i s"
+ and "el n o \<Longrightarrow> goal"
+ and "el p q \<Longrightarrow> goal"
+ and "el s r \<Longrightarrow> goal"
+ and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+ and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+ and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+ and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+ and "\<And>A B. pl A B \<Longrightarrow> el B B"
+ and "\<And>A B. el A B \<Longrightarrow> el B A"
+ and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+ and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+ and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+ and "\<And>A B C D E F G H I J K L M N O P Q.
+ col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
+ col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
+ (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
+ and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
+ and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
shows goal using assms
by coherent
lemma p2p1:
- assumes
- "col a b c l \<and> col d e f m"
- "col b f g n \<and> col c e g o"
- "col b d h p \<and> col a e h q"
- "col c d i r \<and> col a f i s"
- "pl a m \<Longrightarrow> goal"
- "pl b m \<Longrightarrow> goal"
- "pl c m \<Longrightarrow> goal"
- "pl d l \<Longrightarrow> goal"
- "pl e l \<Longrightarrow> goal"
- "pl f l \<Longrightarrow> goal"
- "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
- "\<And>A B. pl A B \<Longrightarrow> ep A A"
- "\<And>A B. ep A B \<Longrightarrow> ep B A"
- "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
- "\<And>A B. pl A B \<Longrightarrow> el B B"
- "\<And>A B. el A B \<Longrightarrow> el B A"
- "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
- "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
- "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
- "\<And>A B C D E F G H I J K L M N O P Q.
- col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
- col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
- (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
- "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
- "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+ assumes "col a b c l \<and> col d e f m"
+ and "col b f g n \<and> col c e g o"
+ and "col b d h p \<and> col a e h q"
+ and "col c d i r \<and> col a f i s"
+ and "pl a m \<Longrightarrow> goal"
+ and "pl b m \<Longrightarrow> goal"
+ and "pl c m \<Longrightarrow> goal"
+ and "pl d l \<Longrightarrow> goal"
+ and "pl e l \<Longrightarrow> goal"
+ and "pl f l \<Longrightarrow> goal"
+ and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+ and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+ and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+ and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+ and "\<And>A B. pl A B \<Longrightarrow> el B B"
+ and "\<And>A B. el A B \<Longrightarrow> el B A"
+ and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+ and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+ and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+ and "\<And>A B C D E F G H I J K L M N O P Q.
+ col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
+ col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
+ (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
+ and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
+ and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
shows goal using assms
by coherent
@@ -82,16 +80,15 @@
subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
lemma diamond:
- assumes
- "reflexive_rewrite a b" "reflexive_rewrite a c"
- "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
- "\<And>A. equalish A A"
- "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
- "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
- "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
- "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
- "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
- "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
+ assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
+ and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
+ and "\<And>A. equalish A A"
+ and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
+ and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
+ and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
+ and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
+ and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
+ and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
shows goal using assms
by coherent
--- a/src/HOL/ex/Cubic_Quartic.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Cubic_Quartic.thy Tue Apr 26 22:59:25 2016 +0200
@@ -2,144 +2,160 @@
Author: Amine Chaieb
*)
-section "The Cubic and Quartic Root Formulas"
+section \<open>The Cubic and Quartic Root Formulas\<close>
theory Cubic_Quartic
imports Complex_Main
begin
-section "The Cubic Formula"
+section \<open>The Cubic Formula\<close>
definition "ccbrt z = (SOME (w::complex). w^3 = z)"
lemma ccbrt: "(ccbrt z) ^ 3 = z"
-proof-
- from rcis_Ex obtain r a where ra: "z = rcis r a" by blast
+proof -
+ from rcis_Ex obtain r a where ra: "z = rcis r a"
+ by blast
let ?r' = "if r < 0 then - root 3 (-r) else root 3 r"
let ?a' = "a/3"
- have "rcis ?r' ?a' ^ 3 = rcis r a" by (cases "r<0", simp_all add: DeMoivre2)
- hence th: "\<exists>w. w^3 = z" unfolding ra by blast
- from someI_ex[OF th] show ?thesis unfolding ccbrt_def by blast
+ have "rcis ?r' ?a' ^ 3 = rcis r a"
+ by (cases "r < 0") (simp_all add: DeMoivre2)
+ then have *: "\<exists>w. w^3 = z"
+ unfolding ra by blast
+ from someI_ex [OF *] show ?thesis
+ unfolding ccbrt_def by blast
qed
-text "The reduction to a simpler form:"
+
+text \<open>The reduction to a simpler form:\<close>
lemma cubic_reduction:
fixes a :: complex
- assumes H: "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and> p = (3* a * c - b^2) / (9 * a^2) \<and>
- q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
+ assumes
+ "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and> p = (3* a * c - b^2) / (9 * a^2) \<and>
+ q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
shows "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> y^3 + 3 * p * y - 2 * q = 0"
-proof-
- from H have "3*a \<noteq> 0" "9*a^2 \<noteq> 0" "54*a^3 \<noteq> 0" by auto
- hence th: "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b"
- "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
- "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow>
- (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
+proof -
+ from assms have "3 * a \<noteq> 0" "9 * a^2 \<noteq> 0" "54 * a^3 \<noteq> 0" by auto
+ then have *:
+ "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b"
+ "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
+ "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow>
+ (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
by (simp_all add: field_simps)
- from H[unfolded th] show ?thesis by algebra
+ from assms [unfolded *] show ?thesis
+ by algebra
qed
-text "The solutions of the special form:"
-lemma cubic_basic:
+text \<open>The solutions of the special form:\<close>
+
+lemma cubic_basic:
fixes s :: complex
- assumes H: "s^2 = q^2 + p^3 \<and>
- s1^3 = (if p = 0 then 2 * q else q + s) \<and>
- s2 = -s1 * (1 + i * t) / 2 \<and>
- s3 = -s1 * (1 - i * t) / 2 \<and>
- i^2 + 1 = 0 \<and>
- t^2 = 3"
- shows
+ assumes
+ "s^2 = q^2 + p^3 \<and>
+ s1^3 = (if p = 0 then 2 * q else q + s) \<and>
+ s2 = -s1 * (1 + i * t) / 2 \<and>
+ s3 = -s1 * (1 - i * t) / 2 \<and>
+ i^2 + 1 = 0 \<and>
+ t^2 = 3"
+ shows
"if p = 0
then y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> y = s1 \<or> y = s2 \<or> y = s3
else s1 \<noteq> 0 \<and>
- (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
-proof-
- { assume p0: "p = 0"
- with H have ?thesis by (simp add: field_simps) algebra
- }
- moreover
- { assume p0: "p \<noteq> 0"
- with H have th1: "s1 \<noteq> 0" by (simp add: field_simps) algebra
- from p0 H th1 have th0: "s2 \<noteq> 0" "s3 \<noteq>0"
- by (simp_all add: field_simps) algebra+
- from th1 th0
- have th: "y = s1 - p / s1 \<longleftrightarrow> s1*y = s1^2 - p"
- "y = s2 - p / s2 \<longleftrightarrow> s2*y = s2^2 - p"
- "y = s3 - p / s3 \<longleftrightarrow> s3*y = s3^2 - p"
- by (simp_all add: field_simps power2_eq_square)
- from p0 H have ?thesis unfolding th by (simp add: field_simps) algebra
- }
- ultimately show ?thesis by blast
+ (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
+proof (cases "p = 0")
+ case True
+ with assms show ?thesis
+ by (simp add: field_simps) algebra
+next
+ case False
+ with assms have *: "s1 \<noteq> 0" by (simp add: field_simps) algebra
+ with assms False have "s2 \<noteq> 0" "s3 \<noteq> 0"
+ by (simp_all add: field_simps) algebra+
+ with * have **:
+ "y = s1 - p / s1 \<longleftrightarrow> s1 * y = s1^2 - p"
+ "y = s2 - p / s2 \<longleftrightarrow> s2 * y = s2^2 - p"
+ "y = s3 - p / s3 \<longleftrightarrow> s3 * y = s3^2 - p"
+ by (simp_all add: field_simps power2_eq_square)
+ from assms False show ?thesis
+ unfolding ** by (simp add: field_simps) algebra
qed
-text "Explicit formula for the roots:"
+
+text \<open>Explicit formula for the roots:\<close>
lemma cubic:
assumes a0: "a \<noteq> 0"
- shows "
- let p = (3 * a * c - b^2) / (9 * a^2) ;
+ shows
+ "let
+ p = (3 * a * c - b^2) / (9 * a^2);
q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
s = csqrt(q^2 + p^3);
s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
s2 = -s1 * (1 + ii * csqrt 3) / 2;
s3 = -s1 * (1 - ii * csqrt 3) / 2
- in if p = 0 then
- a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
- x = s1 - b / (3 * a) \<or>
- x = s2 - b / (3 * a) \<or>
- x = s3 - b / (3 * a)
+ in
+ if p = 0 then
+ a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+ x = s1 - b / (3 * a) \<or>
+ x = s2 - b / (3 * a) \<or>
+ x = s3 - b / (3 * a)
else
s1 \<noteq> 0 \<and>
- (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+ (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
x = s1 - p / s1 - b / (3 * a) \<or>
x = s2 - p / s2 - b / (3 * a) \<or>
x = s3 - p / s3 - b / (3 * a))"
-proof-
+proof -
let ?p = "(3 * a * c - b^2) / (9 * a^2)"
let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
- let ?s = "csqrt(?q^2 + ?p^3)"
+ let ?s = "csqrt (?q^2 + ?p^3)"
let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)"
let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2"
let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2"
let ?y = "x + b / (3 * a)"
- from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a*3)\<noteq> 0" by auto
- have eq:"a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
+ from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a * 3) \<noteq> 0"
+ by auto
+ have eq: "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
by (rule cubic_reduction) (auto simp add: field_simps zero a0)
have "csqrt 3^2 = 3" by (rule power2_csqrt)
- hence th0: "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
- ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
- ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
- ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
+ then have th0:
+ "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
+ ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
+ ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
+ ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
using zero by (simp add: field_simps ccbrt)
from cubic_basic[OF th0, of ?y]
- show ?thesis
+ show ?thesis
apply (simp only: Let_def eq)
using zero apply (simp add: field_simps ccbrt)
using zero
- apply (cases "a * (c * 3) = b^2", simp_all add: field_simps)
+ apply (cases "a * (c * 3) = b^2")
+ apply (simp_all add: field_simps)
done
qed
-section "The Quartic Formula"
+section \<open>The Quartic Formula\<close>
lemma quartic:
- "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
- R^2 = a^2 / 4 - b + y \<and>
- s^2 = y^2 - 4 * d \<and>
- (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
- else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
- (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
- else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
+ "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
+ R^2 = a^2 / 4 - b + y \<and>
+ s^2 = y^2 - 4 * d \<and>
+ (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
+ else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
+ (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
+ else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
\<Longrightarrow> x^4 + a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
x = -a / 4 + R / 2 + D / 2 \<or>
x = -a / 4 + R / 2 - D / 2 \<or>
x = -a / 4 - R / 2 + E / 2 \<or>
x = -a / 4 - R / 2 - E / 2"
-apply (cases "R=0", simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
- apply algebra
-apply algebra
-done
+ apply (cases "R = 0")
+ apply (simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
+ apply algebra
+ apply algebra
+ done
end
--- a/src/HOL/ex/Gauge_Integration.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Tue Apr 26 22:59:25 2016 +0200
@@ -133,7 +133,7 @@
proof (cases "b < x")
case True
with 2 obtain N where *: "N < length D"
- and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+ and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
hence "Suc N < length ((a,t,b)#D) \<and>
(\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
thus ?thesis by auto
@@ -372,11 +372,11 @@
hence "a < b" and "b < c" by auto
obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
- and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+ and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
- and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+ and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
define \<delta> where "\<delta> x =
@@ -541,7 +541,7 @@
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
by (simp add: DERIV_iff2 LIM_eq)
with \<open>0 < e\<close> obtain s
- where "\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+ where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
by (drule_tac x="e/2" in spec, auto)
with strad1 [of x s f f' e] have strad:
"\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
@@ -586,8 +586,8 @@
from lemma_straddle [OF f' this]
obtain \<delta> where "gauge {a..b} \<delta>"
- and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
- \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+ and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+ \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
proof (clarify)
--- a/src/HOL/ex/document/root.tex Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/document/root.tex Tue Apr 26 22:59:25 2016 +0200
@@ -10,14 +10,6 @@
\urlstyle{rm}
\isabellestyle{it}
-\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
-\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
-\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
-\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
-\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
-\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
-
-
\begin{document}
--- a/src/Pure/Isar/obtain.ML Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Apr 26 22:59:25 2016 +0200
@@ -15,8 +15,10 @@
val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
val obtain: binding -> (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list -> (term * term list) list list ->
(Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
val obtain_cmd: binding -> (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list -> (string * string list) list list ->
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
((string * cterm) list * thm list) * Proof.context
@@ -193,28 +195,32 @@
local
-fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state =
let
val _ = Proof.assert_forward_or_chain state;
val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
- val (((vars, xs, params), propss, binds, binds'), params_ctxt) =
- prep_spec raw_vars (map #2 raw_asms) thesis_ctxt;
- val cparams = map (Thm.cterm_of params_ctxt) params;
- val asms =
- map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
- map (map (rpair [])) propss;
+ val ((vars, propss, binds, binds'), params_ctxt) =
+ prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
+ val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
+ val (premss, conclss) = chop (length raw_prems) propss;
+ val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss;
val that_prop =
- Logic.list_rename_params xs
- (fold_rev Logic.all params (Logic.list_implies (flat propss, thesis)));
+ Logic.list_rename_params (map (#1 o #2) decls)
+ (fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis)));
+
+ val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls;
+ val asms =
+ map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~
+ map (map (rpair [])) propss';
fun after_qed (result_ctxt, results) state' =
let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
state'
- |> Proof.fix vars
- |> Proof.map_context (fold Variable.bind_term binds)
+ |> Proof.fix (map #1 decls)
+ |> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds)
|> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
end;
in
@@ -229,8 +235,8 @@
in
-val obtain = gen_obtain Proof_Context.cert_spec (K I);
-val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd;
+val obtain = gen_obtain Proof_Context.cert_stmt (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd;
end;
--- a/src/Pure/Isar/proof.ML Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/proof.ML Tue Apr 26 22:59:25 2016 +0200
@@ -641,66 +641,18 @@
end;
-(* structured clause *)
-
-fun export_binds ctxt' ctxt binds =
- let
- val rhss =
- map (the_list o snd) binds
- |> burrow (Variable.export_terms ctxt' ctxt)
- |> map (try the_single);
- in map fst binds ~~ rhss end;
-
-fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
- let
- (*fixed variables*)
- val ((xs', vars), fix_ctxt) = ctxt
- |> fold_map prep_var raw_fixes
- |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
-
- (*propositions with term bindings*)
- val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows);
- val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss;
-
- (*params*)
- val (ps, params_ctxt) = fix_ctxt
- |> (fold o fold) Variable.declare_term all_propss
- |> fold Variable.bind_term binds
- |> fold_map Proof_Context.inferred_param xs';
- val xs = map (Variable.check_name o #1) vars;
- val params = xs ~~ map Free ps;
-
- val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-
- (*result term bindings*)
- val shows_props = flat shows_propss;
- val binds' =
- (case try List.last shows_props of
- NONE => []
- | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
- val result_binds =
- (Auto_Bind.facts params_ctxt shows_props @ binds')
- |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
- |> export_binds params_ctxt ctxt;
- in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end;
-
-
(* assume *)
local
-fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state =
+fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
let
val ctxt = context_of state;
val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
- val (params, prems_propss, concl_propss, result_binds) =
- #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
-
- fun close prop =
- fold_rev Logic.dependent_all_name params
- (Logic.list_implies (flat prems_propss, prop));
- val propss = (map o map) close concl_propss;
+ val ((params, prems_propss, concl_propss, result_binds), _) =
+ prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
+ val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
in
state
|> assert_forward
@@ -716,8 +668,8 @@
in
-val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I);
-val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd;
+val assm = gen_assume Proof_Context.cert_statement (K I);
+val assm_cmd = gen_assume Proof_Context.read_statement Attrib.attribute_cmd;
val assume = assm Assumption.assume_export;
val assume_cmd = assm_cmd Assumption.assume_export;
@@ -893,45 +845,37 @@
local
-fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
- if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
- else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
- | match_defs [] [] = []
- | match_defs more_decls more_defs =
- error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
- (if null more_decls then "" else " ") ^
- "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
-
-fun invisible_fixes vars ctxt = ctxt
- |> Context_Position.set_visible false
- |> Proof_Context.add_fixes vars |> #2
- |> Context_Position.restore_visible ctxt;
-
-fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
+fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
let
val _ = assert_forward state;
val ctxt = context_of state;
(*vars*)
- val n_vars = length raw_vars;
- val (((all_vars, _, all_params), defss, _, binds'), _) =
- prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
- val (vars, fixes) = chop n_vars all_vars;
- val (params, _) = chop n_vars all_params;
+ val ((vars, propss, _, binds'), vars_ctxt) =
+ prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
+ val (decls, fixes) = chop (length raw_decls) vars;
+ val show_term = Syntax.string_of_term vars_ctxt;
(*defs*)
- val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
- val defs1 = map derived_def (flat defss);
- val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
+ fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
+ if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+ else
+ error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
+ show_term (Free (y, U)))
+ | match_defs [] [] = []
+ | match_defs more_decls more_defs =
+ error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^
+ (if null more_decls then "" else " ") ^
+ "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
+
+ val derived_def = Local_Defs.derived_def ctxt {conditional = false};
+ val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
+ val defs2 = match_defs decls defs1;
val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
- (*fixes*)
- val fixes_ctxt = invisible_fixes fixes defs_ctxt;
- val export = singleton (Variable.export fixes_ctxt defs_ctxt);
-
(*notes*)
val def_thmss =
- map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
+ map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th))
(defs1 ~~ defs2 ~~ defs3)
|> unflat (map snd raw_defs);
val notes =
@@ -947,8 +891,8 @@
in
-val define = gen_define Proof_Context.cert_spec (K I);
-val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
+val define = gen_define Proof_Context.cert_stmt (K I);
+val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd;
end;
@@ -1128,7 +1072,7 @@
(* local goals *)
-fun local_goal print_results prep_att prep_propp prep_var strict_asm
+fun local_goal print_results prep_statement prep_att strict_asm
kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
let
val ctxt = context_of state;
@@ -1139,7 +1083,7 @@
(*params*)
val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
- |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
+ |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
(*prems*)
val (assumes_bindings, shows_bindings) =
@@ -1254,18 +1198,16 @@
(* common goal statements *)
fun internal_goal print_results mode =
- local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
- Proof_Context.cert_var;
+ local_goal print_results
+ (fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I);
local
-fun gen_have prep_att prep_propp prep_var
- strict_asm before_qed after_qed fixes assumes shows int =
+fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
local_goal (Proof_Display.print_results int (Position.thread_data ()))
- prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
+ prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
-fun gen_show prep_att prep_propp prep_var
- strict_asm before_qed after_qed fixes assumes shows int state =
+fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
let
val testing = Unsynchronized.ref false;
val rule = Unsynchronized.ref (NONE: thm option);
@@ -1296,7 +1238,7 @@
|> after_qed (result_ctxt, results);
in
state
- |> local_goal print_results prep_att prep_propp prep_var strict_asm
+ |> local_goal print_results prep_statement prep_att strict_asm
"show" before_qed after_qed' fixes assumes shows
||> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
@@ -1306,10 +1248,10 @@
in
-val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
-val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val have = gen_have Proof_Context.cert_statement (K I);
+val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd;
+val show = gen_show Proof_Context.cert_statement (K I);
+val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 26 22:59:25 2016 +0200
@@ -166,12 +166,22 @@
val generic_add_abbrev: string -> binding * term -> Context.generic ->
(term * term) * Context.generic
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
- val cert_spec: (binding * typ option * mixfix) list -> (term * term list) list list ->
- Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
- term list list * (indexname * term) list * (indexname * term) list) * Proof.context
- val read_spec: (binding * string option * mixfix) list -> (string * string list) list list ->
- Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
- term list list * (indexname * term) list * (indexname * term) list) * Proof.context
+ val cert_stmt:
+ (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * term)) list * term list list *
+ (indexname * term) list * (indexname * term) list) * Proof.context
+ val read_stmt:
+ (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * term)) list * term list list *
+ (indexname * term) list * (indexname * term) list) * Proof.context
+ val cert_statement: (binding * typ option * mixfix) list ->
+ (term * term list) list list -> (term * term list) list list -> Proof.context ->
+ ((string * term) list * term list list * term list list * (indexname * term option) list) *
+ Proof.context
+ val read_statement: (binding * string option * mixfix) list ->
+ (string * string list) list list -> (string * string list) list list -> Proof.context ->
+ ((string * term) list * term list list * term list list * (indexname * term option) list) *
+ Proof.context
val print_syntax: Proof.context -> unit
val print_abbrevs: bool -> Proof.context -> unit
val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1326,38 +1336,60 @@
end;
-(* specification with parameters *)
+(* structured statements *)
local
-fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt =
+fun export_binds ctxt' ctxt params binds =
+ let
+ val rhss =
+ map (the_list o Option.map (Logic.close_term params) o snd) binds
+ |> burrow (Variable.export_terms ctxt' ctxt)
+ |> map (try the_single);
+ in map fst binds ~~ rhss end;
+
+fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
let
- (*vars*)
- val ((xs', vars), vars_ctxt) = ctxt
- |> fold_map prep_var raw_vars
- |-> (fn vars => add_fixes vars ##>> pair vars);
+ val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
val xs = map (Variable.check_name o #1) vars;
+ val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
- (*propps*)
- val (propss, binds) = prep_propp vars_ctxt raw_propps;
- val props = flat propss;
+ val (propss, binds) = prep_propp fixes_ctxt raw_propps;
+ val (ps, params_ctxt) = fixes_ctxt
+ |> (fold o fold) Variable.declare_term propss
+ |> fold_map inferred_param xs';
+ val params = xs ~~ map Free ps;
- (*params*)
- val (ps, params_ctxt) = vars_ctxt
- |> fold Variable.declare_term props
- |> fold Variable.bind_term binds
- |> fold_map inferred_param xs';
- val params = map Free ps;
- val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
+ val binds' = binds
+ |> map (apsnd SOME)
+ |> export_binds params_ctxt ctxt params
+ |> map (apsnd the);
- val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt;
- in (((vars', xs, params), propss, binds, binds'), params_ctxt) end;
+ val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
+ in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
+
+fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
+ let
+ val ((fixes, (assumes, shows), binds), ctxt') = ctxt
+ |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
+ |-> (fn (vars, propss, binds, _) =>
+ fold Variable.bind_term binds #>
+ pair (map #2 vars, chop (length raw_assumes) propss, binds));
+ val binds' =
+ (Auto_Bind.facts ctxt' (flat shows) @
+ (case try List.last (flat shows) of
+ NONE => []
+ | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
+ |> export_binds ctxt' ctxt fixes;
+ in ((fixes, assumes, shows, binds'), ctxt') end;
in
-val cert_spec = prep_spec cert_var cert_propp;
-val read_spec = prep_spec read_var read_propp;
+val cert_stmt = prep_stmt cert_var cert_propp;
+val read_stmt = prep_stmt read_var read_propp;
+val cert_statement = prep_statement cert_var cert_propp;
+val read_statement = prep_statement read_var read_propp;
end;
--- a/src/Pure/Pure.thy Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Pure.thy Tue Apr 26 22:59:25 2016 +0200
@@ -758,8 +758,8 @@
val _ =
Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
- (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
- >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
+ (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+ >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
val _ =
Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
--- a/src/Pure/logic.ML Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/logic.ML Tue Apr 26 22:59:25 2016 +0200
@@ -26,6 +26,8 @@
val strip_prems: int * term list * term -> term list * term
val count_prems: term -> int
val nth_prem: int * term -> term
+ val close_term: (string * term) list -> term -> term
+ val close_prop: (string * term) list -> term list -> term -> term
val true_prop: term
val conjunction: term
val mk_conjunction: term * term -> term
@@ -147,7 +149,6 @@
end;
-
(** equality **)
fun mk_equals (t, u) =
@@ -204,6 +205,11 @@
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+(* close *)
+
+val close_term = fold_rev Term.dependent_lambda_name;
+fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B));
+
(** conjunction **)