--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Constrains.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,595 @@
+(* Title: ZF/UNITY/Constrains.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+
+Proofs ported from HOL.
+*)
+
+(*** traces and reachable ***)
+
+Goalw [condition_def]
+ "reachable(F):condition";
+by (auto_tac (claset() addSDs [reachable.dom_subset RS subsetD]
+ addDs [InitD, ActsD], simpset()));
+qed "reachable_type";
+Addsimps [reachable_type];
+AddIs [reachable_type];
+
+Goal "x:reachable(F) ==> x:state";
+by (cut_inst_tac [("F", "F")] reachable_type 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "reachableD";
+
+Goal "F:program ==> \
+\ reachable(F) = {s:state. EX evs. <s,evs>: traces(Init(F), Acts(F))}";
+by (rtac equalityI 1);
+by Safe_tac;
+by (blast_tac (claset() addDs [reachableD]) 1);
+by (etac traces.induct 2);
+by (etac reachable.induct 1);
+by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
+qed "reachable_equiv_traces";
+
+Goal "Init(F) <= reachable(F)";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_into_reachable";
+
+Goal "[| F:program; G:program; \
+\ Acts(G) <= Acts(F) |] ==> G:stable(reachable(F))";
+by (blast_tac (claset()
+ addIs [stableI, constrainsI, reachable_type] @ reachable.intrs) 1);
+qed "stable_reachable";
+
+AddSIs [stable_reachable];
+Addsimps [stable_reachable];
+
+(*The set of all reachable states is an invariant...*)
+Goalw [invariant_def, initially_def]
+ "F:program ==> F:invariant(reachable(F))";
+by (blast_tac (claset() addIs [reachable_type]@reachable.intrs) 1);
+qed "invariant_reachable";
+
+(*...in fact the strongest invariant!*)
+Goal "F : invariant(A) ==> reachable(F) <= A";
+by (full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "invariant_includes_reachable";
+
+(*** Co ***)
+
+(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+val lemma = subset_refl RSN (3, rewrite_rule
+ [stable_def] stable_reachable RS constrains_Int);
+Goal "F:B co B' ==> F: (reachable(F) Int B) co (reachable(F) Int B')";
+by (blast_tac (claset() addSIs [lemma]
+ addDs [constrainsD2]) 1);
+qed "constrains_reachable_Int";
+
+(*Resembles the previous definition of Constrains*)
+Goalw [Constrains_def]
+ "A Co B = \
+\ {F:program. F : (reachable(F) Int A) co (reachable(F) Int B) & \
+\ A:condition & B:condition}";
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (subgoal_tac "reachable(x) Int B:condition" 2);
+by (blast_tac (claset() addDs [constrains_reachable_Int]
+ addIs [constrains_weaken]) 2);
+by (subgoal_tac "reachable(x) Int B:condition" 1);
+by (blast_tac (claset() addDs [constrains_reachable_Int]
+ addIs [constrains_weaken]) 1);
+by (REPEAT(blast_tac (claset() addIs [reachable_type]) 1));
+qed "Constrains_eq_constrains";
+
+Goalw [Constrains_def]
+ "F : A co A' ==> F : A Co A'";
+by (blast_tac (claset() addIs [constrains_weaken_L]
+ addDs [constrainsD2]) 1);
+qed "constrains_imp_Constrains";
+
+Goalw [stable_def, Stable_def]
+"F : stable(A) ==> F : Stable(A)";
+by (etac constrains_imp_Constrains 1);
+qed "stable_imp_Stable";
+
+
+val prems = Goal
+ "[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A |] \
+\ ==> s':A'); F:program; A:condition; A':condition |] ==> F:A Co A'";
+by (rtac constrains_imp_Constrains 1);
+by (blast_tac (claset() addIs (constrainsI::prems)) 1);
+qed "ConstrainsI";
+
+Goalw [Constrains_def]
+ "F:A Co B ==> F:program & A:condition & B:condition";
+by (Blast_tac 1);
+qed "ConstrainsD";
+
+Goal "[| F:program; B:condition |] ==> F : 0 Co B";
+by (blast_tac (claset() addIs
+ [constrains_imp_Constrains, constrains_empty]) 1);
+qed "Constrains_empty";
+
+Goal "[| F:program; A:condition |] ==> F : A Co state";
+by (blast_tac (claset() addIs
+ [constrains_imp_Constrains, constrains_state2]) 1);
+qed "Constrains_state";
+Addsimps [Constrains_empty, Constrains_state];
+
+val Constrains_def2 = Constrains_eq_constrains RS eq_reflection;
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; A'<=B'; B':condition |] ==> F : A Co B'";
+by (Clarify_tac 1);
+by (blast_tac (claset()
+ addIs [reachable_type, constrains_weaken_R]) 1);
+qed "Constrains_weaken_R";
+
+
+Goalw [condition_def]
+ "[| A<=B; B:condition |] ==>A:condition";
+by (Blast_tac 1);
+qed "condition_subset_mono";
+
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; B<=A |] ==> F : B Co A'";
+by (Clarify_tac 1);
+by (forward_tac [condition_subset_mono] 1);
+by (assume_tac 1);
+by (blast_tac (claset()
+ addIs [reachable_type, constrains_weaken_L]) 1);
+qed "Constrains_weaken_L";
+
+Goalw [Constrains_def]
+ "[| F : A Co A'; B<=A; A'<=B'; B':condition |] ==> F : B Co B'";
+by (Clarify_tac 1);
+by (forward_tac [condition_subset_mono] 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [reachable_type, constrains_weaken]) 1);
+qed "Constrains_weaken";
+
+(** Union **)
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Un B) Co (A' Un B')";
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
+by (blast_tac (claset() addIs [constrains_Un]) 1);
+qed "Constrains_Un";
+
+Goalw [Constrains_def2]
+ "[| F:program; \
+\ ALL i:I. F : A(i) Co A'(i) |] \
+\ ==> F : (UN i:I. A(i)) Co (UN i:I. A'(i))";
+by (rtac CollectI 1);
+by Safe_tac;
+by (simp_tac (simpset() addsimps [Int_UN_distrib]) 1);
+by (blast_tac (claset() addIs [constrains_UN, CollectD2 RS conjunct1]) 1);
+by (rewrite_goals_tac [condition_def]);
+by (ALLGOALS(Blast_tac));
+qed "Constrains_UN";
+
+(** Intersection **)
+
+Goal "A Int (B Int C) = (A Int B) Int (A Int C)";
+by (Blast_tac 1);
+qed "Int_duplicate";
+
+Goalw [Constrains_def]
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Int B) Co (A' Int B')";
+by (Step_tac 1);
+by (subgoal_tac "reachable(F) Int (A Int B) = \
+ \ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
+by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (rtac constrains_Int 1);
+by (ALLGOALS(Asm_simp_tac));
+qed "Constrains_Int";
+
+Goal
+ "[| F:program; \
+\ ALL i:I. F: A(i) Co A'(i) |] \
+\ ==> F : (INT i:I. A(i)) Co (INT i:I. A'(i))";
+by (case_tac "I=0" 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
+by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 2);
+by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
+by (Step_tac 1);
+by (rtac constrains_INT 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS(Blast_tac));
+qed "Constrains_INT";
+
+Goal "F : A Co A' ==> reachable(F) Int A <= A'";
+by (asm_full_simp_tac (simpset() addsimps
+ [Constrains_def, reachable_type]) 1);
+by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
+qed "Constrains_imp_subset";
+
+Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
+qed "Constrains_trans";
+
+Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
+by (full_simp_tac (simpset()
+ addsimps [Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1);
+by (Step_tac 1);
+by (blast_tac (claset() addIs [constrains_cancel]) 1);
+qed "Constrains_cancel";
+
+(*** Stable ***)
+
+(*Useful because there's no Stable_weaken. [Tanja Vos]*)
+Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)";
+by (Blast_tac 1);
+qed "Stable_eq";
+
+Goal "A:condition ==> F : Stable(A) <-> (F : stable(reachable(F) Int A))";
+by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains,
+ stable_def]) 1);
+by (blast_tac (claset() addDs [constrainsD2]) 1);
+qed "Stable_eq_stable";
+
+Goalw [Stable_def] "F : A Co A ==> F : Stable(A)";
+by (assume_tac 1);
+qed "StableI";
+
+Goalw [Stable_def] "F : Stable(A) ==> F : A Co A";
+by (assume_tac 1);
+qed "StableD";
+
+Goalw [Stable_def]
+ "[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')";
+by (blast_tac (claset() addIs [Constrains_Un]) 1);
+qed "Stable_Un";
+
+Goalw [Stable_def]
+ "[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')";
+by (blast_tac (claset() addIs [Constrains_Int]) 1);
+qed "Stable_Int";
+
+Goalw [Stable_def]
+ "[| F : Stable(C); F : A Co (C Un A') |] \
+\ ==> F : (C Un A) Co (C Un A')";
+by (subgoal_tac "C Un A' :condition & C Un A:condition" 1);
+by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "Stable_Constrains_Un";
+
+
+Goalw [Stable_def]
+ "[| F : Stable(C); F : (C Int A) Co A' |] \
+\ ==> F : (C Int A) Co (C Int A')";
+by (blast_tac (claset() addDs [ConstrainsD]
+ addIs [Constrains_Int RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Int";
+
+val [major, prem] = Goalw [Stable_def]
+ "[| F:program; \
+\ (!!i. i:I ==> F : Stable(A(i))) |]==> F : Stable (UN i:I. A(i))";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addIs [major, Constrains_UN, prem]) 1);
+qed "Stable_UN";
+
+val [major, prem] = Goalw [Stable_def]
+ "[| F:program; \
+\ (!!i. i:I ==> F:Stable(A(i))) |]==> F : Stable (INT i:I. A(i))";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addIs [major, Constrains_INT, prem]) 1);
+qed "Stable_INT";
+
+Goal "F:program ==>F : Stable (reachable(F))";
+by (asm_simp_tac (simpset()
+ addsimps [Stable_eq_stable, Int_absorb, subset_refl]) 1);
+qed "Stable_reachable";
+
+Goalw [Stable_def]
+"F:Stable(A) ==> F:program & A:condition";
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "StableD2";
+
+(*** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. ***)
+
+Goalw [condition_def]
+ "Collect(state,P):condition";
+by Auto_tac;
+qed "Collect_in_condition";
+AddIffs [Collect_in_condition];
+
+Goalw [Constrains_def]
+ "[| ALL m:M. F : {s:S. x(s) = m} Co B(m); F:program |] \
+\ ==> F : {s:S. x(s):M} Co (UN m:M. B(m))";
+by Safe_tac;
+by (res_inst_tac [("S1", "reachable(F) Int S")]
+ (elimination RS constrains_weaken_L) 1);
+by Auto_tac;
+by (rtac constrains_weaken_L 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "Elimination";
+
+(* As above, but for the special case of S=state *)
+
+Goal
+ "[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \
+\ ==> F : {s:state. x(s):M} Co (UN m:M. B(m))";
+by (blast_tac (claset() addIs [Elimination]) 1);
+qed "Elimination2";
+
+(** Unless **)
+
+Goalw [Unless_def]
+"F:A Unless B ==> F:program & A:condition & B:condition";
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "UnlessD";
+
+(*** Specialized laws for handling Always ***)
+
+(** Natural deduction rules for "Always A" **)
+Goalw [Always_def, initially_def]
+ "Always(A) = initially(A) Int Stable(A)";
+by (blast_tac (claset() addDs [StableD2]) 1);
+qed "Always_eq";
+
+val Always_def2 = Always_eq RS eq_reflection;
+
+Goalw [Always_def]
+"[| Init(F)<=A; F : Stable(A) |] ==> F : Always(A)";
+by (asm_simp_tac (simpset() addsimps [StableD2]) 1);
+qed "AlwaysI";
+
+Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)";
+by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
+qed "AlwaysD";
+
+bind_thm ("AlwaysE", AlwaysD RS conjE);
+bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);
+
+
+(*The set of all reachable states is Always*)
+Goal "F : Always(A) ==> reachable(F) <= A";
+by (full_simp_tac
+ (simpset() addsimps [Stable_def, Constrains_def, constrains_def,
+ Always_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "Always_includes_reachable";
+
+Goalw [Always_def2, invariant_def2, Stable_def, stable_def]
+ "F : invariant(A) ==> F : Always(A)";
+by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
+qed "invariant_imp_Always";
+
+bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
+
+Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A) & A:condition}";
+by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
+ Constrains_eq_constrains, stable_def]) 1);
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset() addDs [constrainsD]
+ addIs reachable.intrs@[reachable_type]) 1));
+qed "Always_eq_invariant_reachable";
+
+(*the RHS is the traditional definition of the "always" operator*)
+Goal "Always(A) = {F:program. reachable(F) <= A & A:condition}";
+br equalityI 1;
+by (ALLGOALS(Clarify_tac));
+by (auto_tac (claset() addDs [invariant_includes_reachable],
+ simpset() addsimps [subset_Int_iff, invariant_reachable,
+ Always_eq_invariant_reachable]));
+qed "Always_eq_includes_reachable";
+
+Goalw [Always_def]
+"F:Always(A)==> F:program & A:condition";
+by (blast_tac (claset() addDs [StableD2]) 1);
+qed "AlwaysD2";
+
+Goal "Always(state) = program";
+br equalityI 1;
+by (ALLGOALS(Clarify_tac));
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+by (auto_tac (claset() addDs [reachableD],
+ simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_state_eq";
+Addsimps [Always_state_eq];
+
+Goal "[| state <= A; F:program; A:condition |] ==> F : Always(A)";
+by (auto_tac (claset(), simpset()
+ addsimps [Always_eq_includes_reachable]));
+by (auto_tac (claset() addSDs [reachableD],
+ simpset() addsimps [condition_def]));
+qed "state_AlwaysI";
+
+Goal "A:condition ==> Always(A) = (UN I: Pow(A). invariant(I))";
+by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset()
+ addIs [invariantI, impOfSubs Init_into_reachable,
+ impOfSubs invariant_includes_reachable]
+ addDs [invariantD2]) 1));
+qed "Always_eq_UN_invariant";
+
+Goal "[| F : Always(A); A <= B; B:condition |] ==> F : Always(B)";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_weaken";
+
+
+(*** "Co" rules involving Always ***)
+val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp;
+
+Goal "[| F:Always(INV); A:condition |] \
+ \ ==> (F:(INV Int A) Co A') <-> (F : A Co A')";
+by (asm_simp_tac
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
+ Constrains_def, Int_assoc RS sym]) 1);
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+qed "Always_Constrains_pre";
+
+Goal "[| F : Always(INV); A':condition |] \
+\ ==> (F : A Co (INV Int A')) <->(F : A Co A')";
+by (asm_simp_tac
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
+ Constrains_eq_constrains, Int_assoc RS sym]) 1);
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+qed "Always_Constrains_post";
+
+(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
+bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
+
+(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *)
+bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
+
+(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
+Goal "[| F : Always(C); F : A Co A'; \
+\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \
+\ ==> F : B Co B'";
+by (rtac Always_ConstrainsI 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (dtac Always_ConstrainsD 1);
+by (assume_tac 2);
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+by (blast_tac (claset() addIs [Constrains_weaken]) 1);
+qed "Always_Constrains_weaken";
+
+
+(** Conjoining Always properties **)
+
+Goal "[| A:condition; B:condition |] ==> \
+\ Always(A Int B) = Always(A) Int Always(B)";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Int_distrib";
+
+(* the premise i:I is need since INT is formally not defined for I=0 *)
+Goal "[| i:I; ALL i:I. A(i):condition |] \
+\ ==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))";
+by (rtac equalityI 1);
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_INT_distrib";
+
+
+Goal "[| F : Always(A); F : Always(B) |] ==> F : Always(A Int B)";
+by (asm_simp_tac (simpset() addsimps
+ [Always_Int_distrib,AlwaysD2]) 1);
+qed "Always_Int_I";
+
+(*Allows a kind of "implication introduction"*)
+Goal "F : Always(A) ==> (F : Always (state-A Un B)) <-> (F : Always(B))";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Compl_Un_eq";
+
+(*Delete the nearest invariance assumption (which will be the second one
+ used by Always_Int_I) *)
+val Always_thin =
+ read_instantiate_sg (sign_of thy)
+ [("V", "?F : Always(?A)")] thin_rl;
+
+(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
+val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
+
+(*Combines a list of invariance THEOREMS into one.*)
+val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
+
+(*** Increasing ***)
+
+Goalw [Increasing_on_def]
+"[| F:Increasing_on(A, f, r); a:A |] ==> F: Stable({s:state. <a,f`s>:r})";
+by (Blast_tac 1);
+qed "Increasing_onD";
+
+Goalw [Increasing_on_def]
+"F:Increasing_on(A, f, r) ==> F:program & f:state->A & part_order(A,r)";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+qed "Increasing_onD2";
+
+Goalw [Increasing_on_def, Stable_def, Constrains_def, stable_def, constrains_def, part_order_def]
+ "!!f. g:mono_map(A,r,A,r) \
+\ ==> Increasing_on(A, f, r) <= Increasing_on(A, g O f, r)";
+by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
+by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
+by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1);
+by (subgoal_tac "xd:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by (subgoal_tac "f`xe:A & f`xd:A" 1);
+by (blast_tac (claset() addDs [apply_type]) 2);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (Asm_simp_tac 1);
+by (REPEAT(etac conjE 1));
+by (rotate_tac ~3 1);
+by (dres_inst_tac [("x", "xc")] bspec 1);
+by (Asm_simp_tac 1);
+by (dres_inst_tac [("c", "xd")] subsetD 1);
+by (rtac imageI 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (dres_inst_tac [("x", "f`xd")] bspec 2);
+by (ALLGOALS(Asm_simp_tac));
+by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
+by Auto_tac;
+qed "mono_Increasing_on_comp";
+
+Goalw [increasing_on_def, Increasing_on_def]
+ "F : increasing_on(A, f,r) ==> F : Increasing_on(A, f,r)";
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
+qed "increasing_on_imp_Increasing_on";
+
+bind_thm("Increasing_on_constant", increasing_on_constant RS increasing_on_imp_Increasing_on);
+Addsimps [Increasing_on_constant];
+
+Goalw [Increasing_on_def, nat_order_def]
+ "[| F:Increasing_on(nat,f, nat_order); z:nat |] \
+\ ==> F: Stable({s:state. z < f`s})";
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by Safe_tac;
+by (dres_inst_tac [("x", "succ(z)")] bspec 1);
+by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
+by (subgoal_tac "{x: state . f ` x : nat} = state" 1);
+by Auto_tac;
+qed "strict_Increasing_onD";
+
+(*To allow expansion of the program's definition when appropriate*)
+val program_defs_ref = ref ([] : thm list);
+
+(*proves "co" properties when the program is specified*)
+
+fun constrains_tac i =
+ SELECT_GOAL
+ (EVERY [REPEAT (Always_Int_tac 1),
+ REPEAT (etac Always_ConstrainsI 1
+ ORELSE
+ resolve_tac [StableI, stableI,
+ constrains_imp_Constrains] 1),
+ rtac constrainsI 1,
+ full_simp_tac (simpset() addsimps !program_defs_ref) 1,
+ ALLGOALS Clarify_tac,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS Clarify_tac,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS Clarify_tac,
+ ALLGOALS Asm_full_simp_tac,
+ ALLGOALS Clarify_tac]) i;
+
+(*For proving invariants*)
+fun always_tac i =
+ rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;