wneuper/isa: src/ZF/UNITY/SubstAx.thy@5af15f1e2ef6

     1 (*  Title:      ZF/UNITY/SubstAx.thy

     2     Author:     Sidi O Ehmety, Computer Laboratory

     3     Copyright   2001  University of Cambridge

     5 Theory ported from HOL.

     6 *)

     8 header{*Weak LeadsTo relation (restricted to the set of reachable states)*}

    10 theory SubstAx

    11 imports WFair Constrains

    12 begin

    14 definition

    15   (* The definitions below are not `conventional', but yield simpler rules *)

    16   Ensures :: "[i,i] => i"            (infixl "Ensures" 60)  where

    17   "A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }"

    19 definition

    20   LeadsTo :: "[i, i] => i"            (infixl "LeadsTo" 60)  where

    21   "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo (reachable(F) Int B)}"

    23 notation (xsymbols)

    24   LeadsTo  (infixl " \<longmapsto>w " 60)

    28 (*Resembles the previous definition of LeadsTo*)

    30 (* Equivalence with the HOL-like definition *)

    31 lemma LeadsTo_eq:

    32 "st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) Int A) leadsTo B}"

    33 apply (unfold LeadsTo_def)

    34 apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)

    35 done

    37 lemma LeadsTo_type: "A LeadsTo B <=program"

    38 by (unfold LeadsTo_def, auto)

    40 (*** Specialized laws for handling invariants ***)

    42 (** Conjoining an Always property **)

    43 lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \<in> A LeadsTo A')"

    44 by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)

    46 lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I Int A')) <-> (F \<in> A LeadsTo A')"

    47 apply (unfold LeadsTo_def)

    48 apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)

    49 done

    51 (* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)

    52 lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C Int A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"

    53 by (blast intro: Always_LeadsTo_pre [THEN iffD1])

    55 (* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)

    56 lemma Always_LeadsToD: "[| F \<in> Always(C);  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C Int A')"

    57 by (blast intro: Always_LeadsTo_post [THEN iffD2])

    59 (*** Introduction rules \<in> Basis, Trans, Union ***)

    61 lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"

    62 by (auto simp add: Ensures_def LeadsTo_def)

    64 lemma LeadsTo_Trans:

    65      "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"

    66 apply (simp (no_asm_use) add: LeadsTo_def)

    67 apply (blast intro: leadsTo_Trans)

    68 done

    70 lemma LeadsTo_Union:

    71 "[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> Union(S) LeadsTo B"

    72 apply (simp add: LeadsTo_def)

    73 apply (subst Int_Union_Union2)

    74 apply (rule leadsTo_UN, auto)

    75 done

    77 (*** Derived rules ***)

    79 lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"

    80 apply (frule leadsToD2, clarify)

    81 apply (simp (no_asm_simp) add: LeadsTo_eq)

    82 apply (blast intro: leadsTo_weaken_L)

    83 done

    85 (*Useful with cancellation, disjunction*)

    86 lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' Un A') ==> F \<in> A LeadsTo A'"

    87 by (simp add: Un_ac)

    89 lemma LeadsTo_Un_duplicate2:

    90      "F \<in> A LeadsTo (A' Un C Un C) ==> F \<in> A LeadsTo (A' Un C)"

    91 by (simp add: Un_ac)

    93 lemma LeadsTo_UN:

    94     "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]

    95      ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"

    96 apply (simp add: LeadsTo_def)

    97 apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)

    98 apply (rule leadsTo_UN, auto)

    99 done

   101 (*Binary union introduction rule*)

   102 lemma LeadsTo_Un:

   103      "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A Un B) LeadsTo C"

   104 apply (subst Un_eq_Union)

   105 apply (rule LeadsTo_Union)

   106 apply (auto dest: LeadsTo_type [THEN subsetD])

   107 done

   109 (*Lets us look at the starting state*)

   110 lemma single_LeadsTo_I:

   111     "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"

   112 apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)

   113 done

   115 lemma subset_imp_LeadsTo: "[| A <= B; F \<in> program |] ==> F \<in> A LeadsTo B"

   116 apply (simp (no_asm_simp) add: LeadsTo_def)

   117 apply (blast intro: subset_imp_leadsTo)

   118 done

   120 lemma empty_LeadsTo: "F:0 LeadsTo A <-> F \<in> program"

   121 by (auto dest: LeadsTo_type [THEN subsetD]

   122             intro: empty_subsetI [THEN subset_imp_LeadsTo])

   123 declare empty_LeadsTo [iff]

   125 lemma LeadsTo_state: "F \<in> A LeadsTo state <-> F \<in> program"

   126 by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)

   127 declare LeadsTo_state [iff]

   129 lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A';  A'<=B'|] ==> F \<in> A LeadsTo B'"

   130 apply (unfold LeadsTo_def)

   131 apply (auto intro: leadsTo_weaken_R)

   132 done

   134 lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B <= A |] ==> F \<in> B LeadsTo A'"

   135 apply (unfold LeadsTo_def)

   136 apply (auto intro: leadsTo_weaken_L)

   137 done

   139 lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"

   140 by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)

   142 lemma Always_LeadsTo_weaken:

   143 "[| F \<in> Always(C);  F \<in> A LeadsTo A'; C Int B <= A;   C Int A' <= B' |]

   144       ==> F \<in> B LeadsTo B'"

   145 apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)

   146 done

   148 (** Two theorems for "proof lattices" **)

   150 lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A Un B) LeadsTo B"

   151 by (blast dest: LeadsTo_type [THEN subsetD]

   152              intro: LeadsTo_Un subset_imp_LeadsTo)

   154 lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]

   155       ==> F \<in> (A Un B) LeadsTo C"

   156 apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])

   157 done

   159 (** Distributive laws **)

   160 lemma LeadsTo_Un_distrib: "(F \<in> (A Un B) LeadsTo C)  <-> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"

   161 by (blast intro: LeadsTo_Un LeadsTo_weaken_L)

   163 lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) <->  (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"

   164 by (blast dest: LeadsTo_type [THEN subsetD]

   165              intro: LeadsTo_UN LeadsTo_weaken_L)

   167 lemma LeadsTo_Union_distrib: "(F \<in> Union(S) LeadsTo B)  <->  (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"

   168 by (blast dest: LeadsTo_type [THEN subsetD]

   169              intro: LeadsTo_Union LeadsTo_weaken_L)

   171 (** More rules using the premise "Always(I)" **)

   173 lemma EnsuresI: "[| F:(A-B) Co (A Un B);  F \<in> transient (A-B) |] ==> F \<in> A Ensures B"

   174 apply (simp add: Ensures_def Constrains_eq_constrains)

   175 apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)

   176 done

   178 lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I Int (A-A')) Co (A Un A');

   179          F \<in> transient (I Int (A-A')) |]

   180   ==> F \<in> A LeadsTo A'"

   181 apply (rule Always_LeadsToI, assumption)

   182 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)

   183 done

   185 (*Set difference: maybe combine with leadsTo_weaken_L??

   186   This is the most useful form of the "disjunction" rule*)

   187 lemma LeadsTo_Diff:

   188      "[| F \<in> (A-B) LeadsTo C;  F \<in> (A Int B) LeadsTo C |] ==> F \<in> A LeadsTo C"

   189 by (blast intro: LeadsTo_Un LeadsTo_weaken)

   191 lemma LeadsTo_UN_UN:

   192      "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]

   193       ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"

   194 apply (rule LeadsTo_Union, auto)

   195 apply (blast intro: LeadsTo_weaken_R)

   196 done

   198 (*Binary union version*)

   199 lemma LeadsTo_Un_Un:

   200   "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')"

   201 by (blast intro: LeadsTo_Un LeadsTo_weaken_R)

   203 (** The cancellation law **)

   205 lemma LeadsTo_cancel2: "[| F \<in> A LeadsTo(A' Un B); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"

   206 by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])

   208 lemma Un_Diff: "A Un (B - A) = A Un B"

   209 by auto

   211 lemma LeadsTo_cancel_Diff2: "[| F \<in> A LeadsTo (A' Un B); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"

   212 apply (rule LeadsTo_cancel2)

   213 prefer 2 apply assumption

   214 apply (simp (no_asm_simp) add: Un_Diff)

   215 done

   217 lemma LeadsTo_cancel1: "[| F \<in> A LeadsTo (B Un A'); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"

   218 apply (simp add: Un_commute)

   219 apply (blast intro!: LeadsTo_cancel2)

   220 done

   222 lemma Diff_Un2: "(B - A) Un A = B Un A"

   223 by auto

   225 lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B Un A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"

   226 apply (rule LeadsTo_cancel1)

   227 prefer 2 apply assumption

   228 apply (simp (no_asm_simp) add: Diff_Un2)

   229 done

   231 (** The impossibility law **)

   233 (*The set "A" may be non-empty, but it contains no reachable states*)

   234 lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"

   235 apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)

   236 apply (cut_tac reachable_type)

   237 apply (auto dest!: leadsTo_empty)

   238 done

   240 (** PSP \<in> Progress-Safety-Progress **)

   242 (*Special case of PSP \<in> Misra's "stable conjunction"*)

   243 lemma PSP_Stable: "[| F \<in> A LeadsTo A';  F \<in> Stable(B) |]==> F:(A Int B) LeadsTo (A' Int B)"

   244 apply (simp add: LeadsTo_def Stable_eq_stable, clarify)

   245 apply (drule psp_stable, assumption)

   246 apply (simp add: Int_ac)

   247 done

   249 lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B Int A) LeadsTo (B Int A')"

   250 apply (simp (no_asm_simp) add: PSP_Stable Int_ac)

   251 done

   253 lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A Int B') LeadsTo ((A' Int B) Un (B' - B))"

   254 apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)

   255 apply (blast dest: psp intro: leadsTo_weaken)

   256 done

   258 lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"

   259 by (simp (no_asm_simp) add: PSP Int_ac)

   261 lemma PSP_Unless:

   262 "[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"

   263 apply (unfold op_Unless_def)

   264 apply (drule PSP, assumption)

   265 apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)

   266 done

   268 (*** Induction rules ***)

   270 (** Meta or object quantifier ????? **)

   271 lemma LeadsTo_wf_induct: "[| wf(r);

   272          \<forall>m \<in> I. F \<in> (A Int f-``{m}) LeadsTo

   273                             ((A Int f-``(converse(r) `` {m})) Un B);

   274          field(r)<=I; A<=f-``I; F \<in> program |]

   275       ==> F \<in> A LeadsTo B"

   276 apply (simp (no_asm_use) add: LeadsTo_def)

   277 apply auto

   278 apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)

   279 apply (drule_tac [2] x = m in bspec, safe)

   280 apply (rule_tac [2] A' = "reachable (F) Int (A Int f -`` (converse (r) ``{m}) Un B) " in leadsTo_weaken_R)

   281 apply (auto simp add: Int_assoc)

   282 done

   285 lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B);

   286       A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"

   287 apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])

   288 apply (simp_all add: nat_measure_field)

   289 apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])

   290 done

   293 (******

   294  To be ported ??? I am not sure.

   296   integ_0_le_induct

   297   LessThan_bounded_induct

   298   GreaterThan_bounded_induct

   300 *****)

   302 (*** Completion \<in> Binary and General Finite versions ***)

   304 lemma Completion: "[| F \<in> A LeadsTo (A' Un C);  F \<in> A' Co (A' Un C);

   305          F \<in> B LeadsTo (B' Un C);  F \<in> B' Co (B' Un C) |]

   306       ==> F \<in> (A Int B) LeadsTo ((A' Int B') Un C)"

   307 apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)

   308 apply (blast intro: completion leadsTo_weaken)

   309 done

   311 lemma Finite_completion_aux:

   312      "[| I \<in> Fin(X);F \<in> program |]

   313       ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) Un C)) -->

   314           (\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) Un C)) -->

   315           F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"

   316 apply (erule Fin_induct)

   317 apply (auto simp del: INT_simps simp add: Inter_0)

   318 apply (rule Completion, auto)

   319 apply (simp del: INT_simps add: INT_extend_simps)

   320 apply (blast intro: Constrains_INT)

   321 done

   323 lemma Finite_completion:

   324      "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) Un C);

   325          !!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) Un C);

   326          F \<in> program |]

   327       ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"

   328 by (blast intro: Finite_completion_aux [THEN mp, THEN mp])

   330 lemma Stable_completion:

   331      "[| F \<in> A LeadsTo A';  F \<in> Stable(A');

   332          F \<in> B LeadsTo B';  F \<in> Stable(B') |]

   333     ==> F \<in> (A Int B) LeadsTo (A' Int B')"

   334 apply (unfold Stable_def)

   335 apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])

   336     prefer 5

   337     apply blast

   338 apply auto

   339 done

   341 lemma Finite_stable_completion:

   342      "[| I \<in> Fin(X);

   343          (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));

   344          (!!i. i \<in> I ==>F \<in> Stable(A'(i)));   F \<in> program  |]

   345       ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"

   346 apply (unfold Stable_def)

   347 apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)

   348 apply (rule_tac [3] subset_refl, auto)

   349 done

   351 ML {*

   352 (*proves "ensures/leadsTo" properties when the program is specified*)

   353 fun ensures_tac ctxt sact =

   354   let val ss = simpset_of ctxt in

   355     SELECT_GOAL

   356       (EVERY [REPEAT (Always_Int_tac 1),

   357               etac @{thm Always_LeadsTo_Basis} 1

   358                   ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)

   359                   REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},

   360                                     @{thm EnsuresI}, @{thm ensuresI}] 1),

   361               (*now there are two subgoals: co & transient*)

   362               simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,

   363               res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,

   364                  (*simplify the command's domain*)

   365               simp_tac (ss addsimps [@{thm domain_def}]) 3,

   366               (* proving the domain part *)

   367              clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,

   368              rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,

   369              asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,

   370              REPEAT (rtac @{thm state_update_type} 3),

   371              constrains_tac ctxt 1,

   372              ALLGOALS (clarify_tac ctxt),

   373              ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])),

   374                         ALLGOALS (clarify_tac ctxt),

   375             ALLGOALS (asm_lr_simp_tac ss)])

   376   end;

   377 *}

   379 method_setup ensures = {*

   380     Args.goal_spec -- Scan.lift Args.name_source >>

   381     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))

   382 *} "for proving progress properties"

   384 end

author	wenzelm
	Sun, 15 May 2011 17:45:53 +0200
changeset 43685	5af15f1e2ef6
parent 43665	88bee9f6eec7
child 47694	57bf0cecb366
permissions	-rw-r--r--