author paulson Fri, 07 Jan 2000 11:00:56 +0100 changeset 8112 efbe50e2bef9 parent 8111 68cac7d9d119 child 8113 7110358acded
 src/HOL/UNITY/WFair.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/UNITY/WFair.ML	Fri Jan 07 10:57:06 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML	Fri Jan 07 11:00:56 2000 +0100
@@ -162,6 +162,8 @@

+

@@ -169,6 +171,39 @@

+
+(** Variant induction rule: on the preconditions for B **)
+
+(*Lemma is the weak version: can't see how to do it in one step*)
+val major::prems = Goal
+  "[| F : za leadsTo zb;  \
+\     P zb; \
+\     !!A B. [| F : A ensures B;  P B |] ==> P A; \
+\     !!S. ALL A:S. P A ==> P (Union S) \
+\  |] ==> P za";
+(*by induction on this formula*)
+by (subgoal_tac "P zb --> P za" 1);
+(*now solve first subgoal: this formula is sufficient*)
+by (rtac (major RS leadsTo_induct) 1);
+by (REPEAT (blast_tac (claset() addIs prems) 1));
+val lemma = result();
+
+val major::prems = Goal
+  "[| F : za leadsTo zb;  \
+\     P zb; \
+\     !!A B. [| F : A ensures B;  F : B leadsTo zb;  P B |] ==> P A; \
+\     !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) \
+\  |] ==> P za";
+by (subgoal_tac "F : za leadsTo zb & P za" 1);
+by (etac conjunct2 1);
+by (rtac (major RS lemma) 1);
+
+
Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
@@ -254,15 +289,12 @@

(** The impossibility law **)

-Goal "F : A leadsTo B ==> B={} --> A={}";
-by (ALLGOALS Asm_simp_tac);
-by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
+Goal "F : A leadsTo {} ==> A={}";
+by (ALLGOALS
+    (asm_full_simp_tac
+     (simpset() addsimps [ensures_def, constrains_def, transient_def])));
by (Blast_tac 1);
-val lemma = result() RS mp;
-
-Goal "F : A leadsTo {} ==> A={}";
-by (blast_tac (claset() addSIs [lemma]) 1);