# HG changeset patch
# User paulson
# Date 936801806 -7200
# Node ID 15e4a6db638a001f88251a26084905668edbdb9f
# Parent  3a716ebc2fc020a1de3550a0b6673a1f9e9f7a15
tidied

diff -r 3a716ebc2fc0 -r 15e4a6db638a src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Wed Sep 08 15:50:11 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML	Wed Sep 08 16:43:26 1999 +0200
@@ -35,8 +35,7 @@
 (*** ensures ***)
 
 Goalw [ensures_def]
-    "[| F : (A-B) co (A Un B); F : transient (A-B) |] \
-\    ==> F : A ensures B";
+    "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B";
 by (Blast_tac 1);
 qed "ensuresI";
 
@@ -109,8 +108,7 @@
 qed "leadsTo_Union";
 
 val prems = Goalw [leadsTo_def]
-    "(!!A. A : S ==> F : (A Int C) leadsTo B) \
-\    ==> F : (Union S Int C) leadsTo B";
+ "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B";
 by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
 by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
 qed "leadsTo_Union_Int";
@@ -286,8 +284,8 @@
 by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
 qed "psp_stable";
 
-Goal "[| F : A leadsTo A'; F : stable B |] \
-\   ==> F : (B Int A) leadsTo (B Int A')";
+Goal
+   "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')";
 by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
 qed "psp_stable2";
 
@@ -333,7 +331,7 @@
 
 Goal "[| wf r;     \
 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> F : (A Int f-``{m}) leadsTo B";
 by (eres_inst_tac [("a","m")] wf_induct 1);
 by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
@@ -347,7 +345,7 @@
 (** Meta or object quantifier ????? **)
 Goal "[| wf r;     \
 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> F : A leadsTo B";
 by (res_inst_tac [("t", "A")] subst 1);
 by (rtac leadsTo_UN 2);
@@ -359,7 +357,7 @@
 
 Goal "[| wf r;     \
 \        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
-\                              ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\                     ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> F : A leadsTo ((A - (f-``I)) Un B)";
 by (etac leadsTo_wf_induct 1);
 by Safe_tac;
@@ -371,14 +369,14 @@
 
 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
 Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                            ((A Int f-``(lessThan m)) Un B) |] \
+\                   ((A Int f-``(lessThan m)) Un B) |] \
 \     ==> F : A leadsTo B";
 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
 by (Asm_simp_tac 1);
 qed "lessThan_induct";
 
-Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) leadsTo   \
-\                                  ((A Int f-``(lessThan m)) Un B) |] \
+Goal "[| ALL m:(greaterThan l).    \
+\           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
 \     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
 			       Compl_greaterThan RS sym]) 1);
@@ -386,8 +384,8 @@
 by (Asm_simp_tac 1);
 qed "lessThan_bounded_induct";
 
-Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) leadsTo   \
-\                              ((A Int f-``(greaterThan m)) Un B) |] \
+Goal "[| ALL m:(lessThan l).    \
+\           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
 \     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
@@ -399,7 +397,6 @@
 qed "greaterThan_bounded_induct";
 
 
-
 (*** wlt ****)
 
 (*Misra's property W3*)