--- a/src/HOL/UNITY/SubstAx.ML Thu Sep 24 11:00:07 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Sep 24 15:20:03 1998 +0200
@@ -13,19 +13,33 @@
(*** Specialized laws for handling invariants ***)
-Goal "[| Invariant prg INV; LeadsTo prg (INV Int A) A' |] \
+(** Conjoining a safety property **)
+
+Goal "[| reachable prg <= C; LeadsTo prg (C Int A) A' |] \
\ ==> LeadsTo prg A A'";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
+ (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
+qed "reachable_LeadsToI";
+
+Goal "[| reachable prg <= C; LeadsTo prg A A' |] \
+\ ==> LeadsTo prg A (C Int A')";
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_def, Int_absorb2,
Int_assoc RS sym]) 1);
-qed "Invariant_LeadsToI";
+qed "reachable_LeadsToD";
+
-Goal "[| Invariant prg INV; LeadsTo prg A A' |] \
-\ ==> LeadsTo prg A (INV Int A')";
-by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
- Int_assoc RS sym]) 1);
-qed "Invariant_LeadsToD";
+(** Conjoining an invariant **)
+
+(* [| Invariant prg C; LeadsTo prg (C Int A) A' |] ==> LeadsTo prg A A' *)
+bind_thm ("Invariant_LeadsToI",
+ Invariant_includes_reachable RS reachable_LeadsToI);
+
+(* [| Invariant prg C; LeadsTo prg A A' |] ==> LeadsTo prg A (C Int A') *)
+bind_thm ("Invariant_LeadsToD",
+ Invariant_includes_reachable RS reachable_LeadsToD);
+
+
(*** Introduction rules: Basis, Trans, Union ***)
@@ -104,6 +118,12 @@
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
+Goal "[| reachable prg <= C; LeadsTo prg A A'; id: Acts prg; \
+\ C Int B <= A; C Int A' <= B' |] \
+\ ==> LeadsTo prg B B'";
+by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
+ addIs [reachable_LeadsToD]) 1);
+qed "reachable_LeadsTo_weaken";
(** Two theorems for "proof lattices" **)
@@ -329,6 +349,20 @@
by (Asm_simp_tac 1);
qed "LessThan_induct";
+(*Integer version. Could generalize from #0 to any lower bound*)
+val [reach, prem, id] =
+Goal "[| reachable prg <= {s. #0 <= f s}; \
+\ !! z. LeadsTo prg (A Int {s. f s = z}) \
+\ ((A Int {s. f s < z}) Un B); \
+\ id: Acts prg |] \
+\ ==> LeadsTo prg A B";
+by (res_inst_tac [("f", "nat_of o f")] (allI RS LessThan_induct) 1);
+by (simp_tac (simpset() addsimps [vimage_def]) 1);
+br ([reach, prem] MRS reachable_LeadsTo_weaken) 1;
+by (auto_tac (claset(),
+ simpset() addsimps [id, nat_of_eq_iff, nat_of_less_iff]));
+qed "integ_0_le_induct";
+
Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
\ id: Acts prg |] \