--- a/src/HOL/Auth/NS_Shared.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Thu Aug 06 15:48:13 1998 +0200
@@ -18,8 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal
- "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX N K. EX evs: ns_shared. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -28,8 +27,7 @@
by possibility_tac;
result();
-Goal
- "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX evs: ns_shared. \
\ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -53,8 +51,7 @@
by (Blast_tac 1);
qed "NS3_msg_in_parts_spies";
-Goal
- "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
+Goal "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
\ ==> K : parts (spies evs)";
by (Blast_tac 1);
qed "Oops_parts_spies";
@@ -72,15 +69,13 @@
sends messages containing X! **)
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal
- "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal
- "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -109,8 +104,7 @@
(** Lemmas concerning the form of items passed in messages **)
(*Describes the form of K, X and K' when the Server sends this message.*)
-Goal
- "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
+Goal "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
\ evs : ns_shared |] \
\ ==> K ~: range shrK & \
\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
@@ -122,8 +116,7 @@
(*If the encrypted message appears then it originated with the Server*)
-Goal
- "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
+Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
\ A ~: bad; evs : ns_shared |] \
\ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs";
@@ -133,8 +126,7 @@
qed "A_trusts_NS2";
-Goal
- "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
+Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
\ A ~: bad; evs : ns_shared |] \
\ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})";
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
@@ -144,8 +136,7 @@
(*EITHER describes the form of X when the following message is sent,
OR reduces it to the Fake case.
Use Says_Server_message_form if applicable.*)
-Goal
- "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
+Goal "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set evs; \
\ evs : ns_shared |] \
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
@@ -177,8 +168,7 @@
(*NOT useful in this form, but it says that session keys are not used
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
-Goal
- "[| evs : ns_shared; Kab ~: range shrK |] ==> \
+Goal "[| evs : ns_shared; Kab ~: range shrK |] ==> \
\ (Crypt KAB X) : parts (spies evs) & \
\ Key K : parts {X} --> Key K : parts (spies evs)";
by (parts_induct_tac 1);
@@ -193,8 +183,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-Goal
- "evs : ns_shared ==> \
+Goal "evs : ns_shared ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
@@ -209,8 +198,7 @@
qed_spec_mp "analz_image_freshK";
-Goal
- "[| evs : ns_shared; KAB ~: range shrK |] ==> \
+Goal "[| evs : ns_shared; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
@@ -219,8 +207,7 @@
(** The session key K uniquely identifies the message **)
-Goal
- "evs : ns_shared ==> \
+Goal "evs : ns_shared ==> \
\ EX A' NA' B' X'. ALL A NA B X. \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
\ --> A=A' & NA=NA' & B=B' & X=X'";
@@ -237,8 +224,7 @@
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
-Goal
- "[| Says Server A \
+Goal "[| Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
\ Says Server A' \
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
@@ -249,8 +235,7 @@
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
-Goal
- "[| A ~: bad; B ~: bad; evs : ns_shared |] \
+Goal "[| A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
@@ -282,8 +267,7 @@
(*Final version: Server's message in the most abstract form*)
-Goal
- "[| Says Server A \
+Goal "[| Says Server A \
\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : ns_shared \
@@ -299,8 +283,7 @@
(*If the encrypted message appears then it originated with the Server*)
-Goal
- "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
+Goal "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
\ B ~: bad; evs : ns_shared |] \
\ ==> EX NA. Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
@@ -312,8 +295,7 @@
qed "B_trusts_NS3";
-Goal
- "[| Crypt K (Nonce NB) : parts (spies evs); \
+Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs; \
\ Key K ~: analz (spies evs); \
@@ -339,8 +321,7 @@
(*This version no longer assumes that K is secure*)
-Goal
- "[| Crypt K (Nonce NB) : parts (spies evs); \
+Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
\ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : ns_shared |] \
@@ -353,8 +334,7 @@
(*If the session key has been used in NS4 then somebody has forwarded
component X in some instance of NS4. Perhaps an interesting property,
but not needed (after all) for the proofs below.*)
-Goal
- "[| Crypt K (Nonce NB) : parts (spies evs); \
+Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set evs; \
\ Key K ~: analz (spies evs); \
@@ -380,8 +360,7 @@
qed "NS4_implies_NS3";
-Goal
- "[| B ~: bad; evs : ns_shared |] \
+Goal "[| B ~: bad; evs : ns_shared |] \
\ ==> Key K ~: analz (spies evs) --> \
\ Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
@@ -408,8 +387,7 @@
(*Very strong Oops condition reveals protocol's weakness*)
-Goal
- "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \
+Goal "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \
\ Says B A (Crypt K (Nonce NB)) : set evs; \
\ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
\ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
--- a/src/HOL/Auth/OtwayRees.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu Aug 06 15:48:13 1998 +0200
@@ -18,8 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal
- "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
@@ -77,15 +76,13 @@
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-Goal
- "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal
- "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -116,8 +113,7 @@
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
-Goal
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -148,8 +144,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-Goal
- "evs : otway ==> \
+Goal "evs : otway ==> \
\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
@@ -163,8 +158,7 @@
qed_spec_mp "analz_image_freshK";
-Goal
- "[| evs : otway; KAB ~: range shrK |] ==> \
+Goal "[| evs : otway; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
@@ -173,8 +167,7 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal
- "evs : otway ==> \
+Goal "evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
@@ -190,8 +183,7 @@
by (blast_tac (claset() addSEs spies_partsEs) 1);
val lemma = result();
-Goal
- "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
+Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
@@ -202,8 +194,7 @@
(**** Authenticity properties relating to NA ****)
(*Only OR1 can have caused such a part of a message to appear.*)
-Goal
- "[| A ~: bad; evs : otway |] \
+Goal "[| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
@@ -215,8 +206,7 @@
(** The Nonce NA uniquely identifies A's message. **)
-Goal
- "[| evs : otway; A ~: bad |] \
+Goal "[| evs : otway; A ~: bad |] \
\ ==> EX B'. ALL B. \
\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
\ --> B = B'";
@@ -228,8 +218,7 @@
by (Blast_tac 1);
val lemma = result();
-Goal
- "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
+Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
\ evs : otway; A ~: bad |] \
\ ==> B = C";
@@ -240,8 +229,7 @@
(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
-Goal
- "[| A ~: bad; evs : otway |] \
+Goal "[| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
\ ~: parts (spies evs)";
@@ -253,8 +241,7 @@
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
-Goal
- "[| A ~: bad; evs : otway |] \
+Goal "[| A ~: bad; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
@@ -285,8 +272,7 @@
then the key really did come from the Server! CANNOT prove this of the
bad form of this protocol, even though we can prove
Spy_not_see_encrypted_key*)
-Goal
- "[| Says A B {|NA, Agent A, Agent B, \
+Goal "[| Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
\ A ~: bad; evs : otway |] \
@@ -303,8 +289,7 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-Goal
- "[| A ~: bad; B ~: bad; evs : otway |] \
+Goal "[| A ~: bad; B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
@@ -353,8 +338,7 @@
(*Only OR2 can have caused such a part of a message to appear. We do not
know anything about X: it does NOT have to have the right form.*)
-Goal
- "[| B ~: bad; evs : otway |] \
+Goal "[| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
\ : parts (spies evs) --> \
\ (EX X. Says B Server \
@@ -380,8 +364,7 @@
by (Blast_tac 1);
val lemma = result();
-Goal
- "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
+Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
\ evs : otway; B ~: bad |] \
\ ==> NC = NA & C = A";
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Aug 06 15:48:13 1998 +0200
@@ -18,8 +18,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal
- "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
\ : set evs";
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Aug 06 15:48:13 1998 +0200
@@ -21,8 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
-Goal
- "[| A ~= B; A ~= Server; B ~= Server |] \
+Goal "[| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
--- a/src/HOL/Auth/Shared.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Auth/Shared.ML Thu Aug 06 15:48:13 1998 +0200
@@ -246,8 +246,7 @@
@disj_comms);
(*Lemma for the trivial direction of the if-and-only-if*)
-Goal
- "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \
+Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H) ==> \
\ (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
qed "analz_image_freshK_lemma";
--- a/src/HOL/Divides.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Divides.ML Thu Aug 06 15:48:13 1998 +0200
@@ -238,9 +238,7 @@
(*** Further facts about mod (mainly for the mutilated chess board ***)
-Goal
- "!!m n. 0<n ==> \
-\ Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
+Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
by (res_inst_tac [("n","m")] less_induct 1);
by (excluded_middle_tac "Suc(na)<n" 1);
(* case Suc(na) < n *)
--- a/src/HOL/Finite.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Finite.ML Thu Aug 06 15:48:13 1998 +0200
@@ -211,9 +211,8 @@
addcongs [rev_conj_cong]) 1);
qed "finite_has_card";
-Goal
- "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
-\ ? m::nat. m<n & (? g. A = {g i|i. i<m})";
+Goal "[| x ~: A; insert x A = {f i|i. i<n} |] \
+\ ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
by (exhaust_tac "n" 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/IMP/Hoare.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML Thu Aug 06 15:48:13 1998 +0200
@@ -56,13 +56,11 @@
Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
(*Not suitable for rewriting: LOOPS!*)
-Goal
- "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
+Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
by (Simp_tac 1);
qed "wp_While_if";
-Goal
- "wp (WHILE b DO c) Q s = \
+Goal "wp (WHILE b DO c) Q s = \
\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
by (Simp_tac 1);
by (rtac iffI 1);
--- a/src/HOL/IMP/Transition.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/IMP/Transition.ML Thu Aug 06 15:48:13 1998 +0200
@@ -27,8 +27,7 @@
val hlemma = result();
-Goal
- "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
+Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
\ (c;d, s) -*-> (SKIP, u)";
by (induct_tac "n" 1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
@@ -60,8 +59,7 @@
qed "evalc_impl_evalc1";
-Goal
- "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
+Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
\ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
by (induct_tac "n" 1);
(* case n = 0 *)
@@ -117,8 +115,7 @@
section "A Proof Without -n->";
-Goal
- "(c1,s1) -*-> (SKIP,s2) ==> \
+Goal "(c1,s1) -*-> (SKIP,s2) ==> \
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
by (etac converse_rtrancl_induct2 1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
@@ -183,8 +180,7 @@
*)
(*Delsimps [update_apply];*)
-Goal
- "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
+Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
by (etac evalc1.induct 1);
by Auto_tac;
qed_spec_mp "FB_lemma3";
--- a/src/HOL/IMP/VC.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/IMP/VC.ML Thu Aug 06 15:48:13 1998 +0200
@@ -43,8 +43,7 @@
by (fast_tac (HOL_cs addEs [awp_mono]) 1);
qed_spec_mp "vc_mono";
-Goal
- "|- {P}c{Q} ==> \
+Goal "|- {P}c{Q} ==> \
\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
by (etac hoare.induct 1);
by (res_inst_tac [("x","Askip")] exI 1);
--- a/src/HOL/Induct/LList.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Induct/LList.ML Thu Aug 06 15:48:13 1998 +0200
@@ -103,8 +103,7 @@
qed "LList_corec_subset2";
(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-Goal
- "LList_corec a f = sum_case (%u. NIL) \
+Goal "LList_corec a f = sum_case (%u. NIL) \
\ (split(%z w. CONS z (LList_corec w f))) (f a)";
by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
LList_corec_subset2] 1));
@@ -129,8 +128,7 @@
qed "LList_corec_type";
(*Lemma for the proof of llist_corec*)
-Goal
- "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
+Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
\ llist(range Leaf)";
by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
@@ -235,8 +233,7 @@
diag_subset_LListD] 1));
qed "LListD_eq_diag";
-Goal
- "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
+Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
by (rtac (LListD_eq_diag RS subst) 1);
by (rtac LListD_Fun_LListD_I 1);
by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
@@ -246,8 +243,7 @@
(** To show two LLists are equal, exhibit a bisimulation!
[also admits true equality]
Replace "A" by some particular set, like {x.True}??? *)
-Goal
- "[| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
+Goal "[| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
\ |] ==> M=N";
by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
by (etac LListD_coinduct 1);
@@ -538,8 +534,7 @@
(** Alternative type-checking proofs for Lappend **)
(*weak co-induction: bisimulation and case analysis on both variables*)
-Goal
- "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac
[("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
by (Fast_tac 1);
@@ -551,8 +546,7 @@
qed "Lappend_type";
(*strong co-induction: bisimulation and case analysis on one variable*)
-Goal
- "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
by (etac imageI 1);
by (rtac image_subsetI 1);
@@ -627,8 +621,7 @@
by (Fast_tac 1);
qed "LListD_Fun_subset_Sigma_llist";
-Goal
- "prod_fun Rep_llist Rep_llist `` r <= \
+Goal "prod_fun Rep_llist Rep_llist `` r <= \
\ (llist(range Leaf)) Times (llist(range Leaf))";
by (fast_tac (claset() delrules [image_subsetI]
addIs [Rep_llist]) 1);
@@ -643,8 +636,7 @@
by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
qed "prod_fun_lemma";
-Goal
- "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
+Goal "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
\ diag(llist(range Leaf))";
by (rtac equalityI 1);
by (fast_tac (claset() addIs [Rep_llist]) 1);
@@ -779,8 +771,7 @@
(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
-Goal
- "nat_rec (LCons b l) (%m. lmap(f)) n = \
+Goal "nat_rec (LCons b l) (%m. lmap(f)) n = \
\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/Induct/SList.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Induct/SList.ML Thu Aug 06 15:48:13 1998 +0200
@@ -147,8 +147,7 @@
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
hold if pred_sexp^+ were changed to pred_sexp. *)
-Goal
- "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
+Goal "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
\ (%g. List_case c (%x y. d x y (g y)))";
by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
val List_rec_unfold = standard
@@ -339,8 +338,7 @@
(** list_case **)
-Goal
- "P(list_case a f xs) = ((xs=[] --> P(a)) & \
+Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
\ (!y ys. xs=y#ys --> P(f y ys)))";
by (list_ind_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/Induct/Term.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Induct/Term.ML Thu Aug 06 15:48:13 1998 +0200
@@ -108,8 +108,7 @@
(*** Term_rec -- by wf recursion on pred_sexp ***)
-Goal
- "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
+Goal "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
\ (%g. Split(%x y. d x y (Abs_map g y)))";
by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS
--- a/src/HOL/Integ/Equiv.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Integ/Equiv.ML Thu Aug 06 15:48:13 1998 +0200
@@ -66,8 +66,7 @@
by (Blast_tac 1);
qed "subset_equiv_class";
-Goal
- "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r";
+Goal "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r";
by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
qed "eq_equiv_class";
@@ -82,14 +81,12 @@
by (rtac (major RS conjunct1 RS conjunct1) 1);
qed "equiv_type";
-Goal
- "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
+Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
by (blast_tac (claset() addSIs [equiv_class_eq]
addDs [eq_equiv_class, equiv_type]) 1);
qed "equiv_class_eq_iff";
-Goal
- "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
+Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
by (blast_tac (claset() addSIs [equiv_class_eq]
addDs [eq_equiv_class, equiv_type]) 1);
qed "eq_equiv_class_iff";
@@ -193,8 +190,7 @@
by (Blast_tac 1);
qed "congruent2_implies_congruent_UN";
-Goal
- "[| equiv A r; congruent2 r b; a1: A; a2: A |] \
+Goal "[| equiv A r; congruent2 r b; a1: A; a2: A |] \
\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
congruent2_implies_congruent,
--- a/src/HOL/Integ/Integ.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Thu Aug 06 15:48:13 1998 +0200
@@ -316,8 +316,7 @@
by (simp_tac (simpset() addsimps add_ac) 1);
qed "zmult_congruent_lemma";
-Goal
- "congruent2 intrel (%p1 p2. \
+Goal "congruent2 intrel (%p1 p2. \
\ split (%x1 y1. split (%x2 y2. \
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
--- a/src/HOL/List.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/List.ML Thu Aug 06 15:48:13 1998 +0200
@@ -243,8 +243,7 @@
section "map";
-Goal
- "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
+Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
by (induct_tac "xs" 1);
by (Auto_tac);
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
@@ -274,8 +273,7 @@
qed "rev_map";
(* a congruence rule for map: *)
-Goal
- "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
+Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
by (rtac impI 1);
by (hyp_subst_tac 1);
by (induct_tac "ys" 1);
@@ -520,8 +518,7 @@
section "nth";
-Goal
- "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
+Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (rtac allI 1);
@@ -596,8 +593,7 @@
qed "length_butlast";
Addsimps [length_butlast];
-Goal
- "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
+Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
by (induct_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "butlast_append";
@@ -672,8 +668,7 @@
by (Auto_tac);
qed_spec_mp "drop_all";
-Goal
- "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
+Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
--- a/src/HOL/Prod.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Prod.ML Thu Aug 06 15:48:13 1998 +0200
@@ -253,8 +253,7 @@
qed "prod_fun";
Addsimps [prod_fun];
-Goal
- "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
+Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
by (rtac ext 1);
by (pair_tac "x" 1);
by (Asm_simp_tac 1);
@@ -347,8 +346,7 @@
Addsimps [Collect_split];
(*Suggested by Pierre Chartier*)
-Goal
- "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
+Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
by (Blast_tac 1);
qed "UNION_Times_distrib";
--- a/src/HOL/RelPow.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/RelPow.ML Thu Aug 06 15:48:13 1998 +0200
@@ -57,8 +57,7 @@
qed_spec_mp "rel_pow_Suc_D2";
-Goal
-"!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
+Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
by (nat_ind_tac "n" 1);
by (fast_tac (claset() addss (simpset())) 1);
by (fast_tac (claset() addss (simpset())) 1);
--- a/src/HOL/Sexp.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Sexp.ML Thu Aug 06 15:48:13 1998 +0200
@@ -98,8 +98,7 @@
(*** sexp_rec -- by wf recursion on pred_sexp ***)
-Goal
- "(%M. sexp_rec M c d e) = wfrec pred_sexp \
+Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
\ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
--- a/src/HOL/Subst/Subst.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Subst/Subst.ML Thu Aug 06 15:48:13 1998 +0200
@@ -33,8 +33,7 @@
by (Blast_tac 1);
qed_spec_mp "Var_not_occs";
-Goal
- "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
+Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_full_simp_tac);
by (ALLGOALS Blast_tac);
@@ -171,12 +170,11 @@
by (ALLGOALS Blast_tac);
qed_spec_mp "Var_in_srange";
-Goal
- "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)";
+Goal "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)";
by (blast_tac (claset() addIs [Var_in_srange]) 1);
qed "Var_elim";
-Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
+Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
by (induct_tac "t" 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
by (Blast_tac 2);
@@ -184,13 +182,11 @@
by Auto_tac;
qed_spec_mp "Var_intro";
-Goal
- "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
+Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
by (simp_tac (simpset() addsimps [srange_iff]) 1);
qed_spec_mp "srangeD";
-Goal
- "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
+Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1);
by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1);
qed "dom_range_disjoint";
--- a/src/HOL/Subst/Unifier.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Subst/Unifier.ML Thu Aug 06 15:48:13 1998 +0200
@@ -3,7 +3,6 @@
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For Unifier.thy.
Properties of unifiers.
*)
@@ -15,15 +14,13 @@
* Unifiers
*---------------------------------------------------------------------------*)
-Goal
- "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
+Goal "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
by (simp_tac (simpset() addsimps [Unifier_def]) 1);
qed "Unifier_Comb";
AddIffs [Unifier_Comb];
-Goal
- "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
+Goal "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
\ Unifier ((v,r)#s) t u";
by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1);
qed "Cons_Unifier";
@@ -51,8 +48,7 @@
qed "MGU_iff";
-Goal
- "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
+Goal "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
delsimps [subst_Var]) 1);
by Safe_tac;
--- a/src/HOL/Subst/Unify.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Subst/Unify.ML Thu Aug 06 15:48:13 1998 +0200
@@ -87,8 +87,7 @@
* This lemma proves the nested termination condition for the base cases
* 3, 4, and 6.
*---------------------------------------------------------------------------*)
-Goal
- "~(Var x <: M) ==> \
+Goal "~(Var x <: M) ==> \
\ ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
by (case_tac "Var x = M" 1);
@@ -175,8 +174,7 @@
*---------------------------------------------------------------------------*)
(*Desired rule, copied from the theory file. Could it be made available?*)
-Goal
- "unify(Comb M1 N1, Comb M2 N2) = \
+Goal "unify(Comb M1 N1, Comb M2 N2) = \
\ (case unify(M1,M2) \
\ of None => None \
\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \
--- a/src/HOL/Univ.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/Univ.ML Thu Aug 06 15:48:13 1998 +0200
@@ -553,8 +553,7 @@
val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
(*Dependent version*)
-Goal
- "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
+Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
by Safe_tac;
by (stac Split 1);
by (Blast_tac 1);
--- a/src/HOL/WF.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/WF.ML Thu Aug 06 15:48:13 1998 +0200
@@ -317,8 +317,7 @@
(**** TFL variants ****)
-Goal
- "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
+Goal "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
by (Clarify_tac 1);
by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
by (assume_tac 1);
--- a/src/HOL/equalities.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/equalities.ML Thu Aug 06 15:48:13 1998 +0200
@@ -85,8 +85,7 @@
bind_thm ("insert_Collect", prove_goal thy
"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
-Goal
- "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
+Goal "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
by (Blast_tac 1);
qed "UN_insert_distrib";
@@ -305,8 +304,7 @@
by (Blast_tac 1);
qed "Un_Int_distrib2";
-Goal
- "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
+Goal "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
by (Blast_tac 1);
qed "Un_Int_crazy";
@@ -556,13 +554,11 @@
by (Blast_tac 1);
qed "Un_INT_distrib";
-Goal
- "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
+Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
by (Blast_tac 1);
qed "Int_UN_distrib2";
-Goal
- "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
+Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
by (Blast_tac 1);
qed "Un_INT_distrib2";
--- a/src/HOL/ex/MT.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/ex/MT.ML Thu Aug 06 15:48:13 1998 +0200
@@ -439,8 +439,7 @@
by (elab_e_elim_tac prems);
qed "elab_fn_elim_lem";
-Goal
- " te |- fn x1 => e1 ===> t ==> \
+Goal " te |- fn x1 => e1 ===> t ==> \
\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
by (dtac elab_fn_elim_lem 1);
by (Blast_tac 1);
@@ -453,8 +452,7 @@
by (elab_e_elim_tac prems);
qed "elab_fix_elim_lem";
-Goal
- " te |- fix ev1(ev2) = e1 ===> t ==> \
+Goal " te |- fix ev1(ev2) = e1 ===> t ==> \
\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
by (dtac elab_fix_elim_lem 1);
by (Blast_tac 1);
@@ -466,8 +464,7 @@
by (elab_e_elim_tac prems);
qed "elab_app_elim_lem";
-Goal
- "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
+Goal "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
by (dtac elab_app_elim_lem 1);
by (Blast_tac 1);
qed "elab_app_elim";
@@ -589,8 +586,7 @@
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_clos_lem";
-Goal
- "v_clos(<|ev,e,ve|>) hasty t ==> \
+Goal "v_clos(<|ev,e,ve|>) hasty t ==> \
\ ? te. te |- fn ev => e ===> t & ve hastyenv te ";
by (dtac hasty_elim_clos_lem 1);
by (Blast_tac 1);
@@ -600,8 +596,7 @@
(* The pointwise extension of hasty to environments *)
(* ############################################################ *)
-Goal
- "[| ve hastyenv te; v hasty t |] ==> \
+Goal "[| ve hastyenv te; v hasty t |] ==> \
\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
by (rewtac hasty_env_def);
by (asm_full_simp_tac (simpset() delsimps mem_simps
@@ -617,8 +612,7 @@
(* The Consistency theorem *)
(* ############################################################ *)
-Goal
- "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
+Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
by (dtac elab_const_elim 1);
by (etac hasty_const 1);
qed "consistency_const";
@@ -630,8 +624,7 @@
by (Blast_tac 1);
qed "consistency_var";
-Goal
- "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
\ v_clos(<| ev, e, ve |>) hasty t";
by (rtac hasty_clos 1);
by (Blast_tac 1);
@@ -664,8 +657,7 @@
by (Blast_tac 1);
qed "consistency_fix";
-Goal
- "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
+Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
\ ve hastyenv te ; te |- e1 @ e2 ===> t \
\ |] ==> \
@@ -680,8 +672,7 @@
by (Blast_tac 1);
qed "consistency_app1";
-Goal
- "[| ! t te. \
+Goal "[| ! t te. \
\ ve hastyenv te --> \
\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
@@ -707,8 +698,7 @@
by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
qed "consistency_app2";
-Goal
- "ve |- e ---> v ==> \
+Goal "ve |- e ---> v ==> \
\ (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
(* Proof by induction on the structure of evaluations *)
@@ -736,8 +726,7 @@
by (Asm_simp_tac 1);
qed "basic_consistency_lem";
-Goal
- "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
+Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
--- a/src/HOL/ex/Qsort.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/ex/Qsort.ML Thu Aug 06 15:48:13 1998 +0200
@@ -41,8 +41,7 @@
qed"Ball_set_filter";
Addsimps [Ball_set_filter];
-Goal
- "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
+Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
\ (!x:set xs. !y:set ys. le x y))";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/ex/StringEx.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/ex/StringEx.ML Thu Aug 06 15:48:13 1998 +0200
@@ -15,7 +15,6 @@
by (Simp_tac 1);
result();
-Goal
- "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
+Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
by (Simp_tac 1);
result();
--- a/src/HOL/ex/cla.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/ex/cla.ML Thu Aug 06 15:48:13 1998 +0200
@@ -142,8 +142,7 @@
result();
(*From Wishnu Prasetya*)
-Goal
- "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
+Goal "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
\ --> p(t) | r(t)";
by (Blast_tac 1);
result();
@@ -317,8 +316,7 @@
result();
writeln"Problem 38";
-Goal
- "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \
+Goal "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \
\ (? z. ? w. p(z) & r x w & r w z)) = \
\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \
\ (~p(a) | ~(? y. p(y) & r x y) | \
@@ -349,8 +347,7 @@
result();
writeln"Problem 43!!";
-Goal
- "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \
+Goal "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \
\ --> (! x. (! y. q x y = (q y x::bool)))";
by (Blast_tac 1);
result();
@@ -364,8 +361,7 @@
result();
writeln"Problem 45";
-Goal
- "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
+Goal "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
\ --> (! y. g(y) & h x y --> k(y))) & \
\ ~ (? y. l(y) & k(y)) & \
\ (? x. f(x) & (! y. h x y --> l(y)) \
@@ -402,16 +398,14 @@
result();
writeln"Problem 51";
-Goal
- "(? z w. ! x y. P x y = (x=z & y=w)) --> \
+Goal "(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
by (Blast_tac 1);
result();
writeln"Problem 52";
(*Almost the same as 51. *)
-Goal
- "(? z w. ! x y. P x y = (x=z & y=w)) --> \
+Goal "(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
by (Blast_tac 1);
result();
@@ -433,14 +427,12 @@
result();
writeln"Problem 56";
-Goal
- "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
+Goal "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
by (Blast_tac 1);
result();
writeln"Problem 57";
-Goal
- "P (f a b) (f b c) & P (f b c) (f a c) & \
+Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
\ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)";
by (Blast_tac 1);
result();
@@ -457,8 +449,7 @@
result();
writeln"Problem 60";
-Goal
- "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
+Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
by (Blast_tac 1);
result();
--- a/src/HOL/simpdata.ML Thu Aug 06 15:47:26 1998 +0200
+++ b/src/HOL/simpdata.ML Thu Aug 06 15:48:13 1998 +0200
@@ -252,6 +252,9 @@
qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
(K [rtac refl 1]);
+
+(** if-then-else rules **)
+
qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
(K [Blast_tac 1]);