diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Constrains.ML --- /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. : 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); :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. :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;