532 |
532 |
533 |
533 |
534 subsubsection{*Commutativity of Functions and Relation*} |
534 subsubsection{*Commutativity of Functions and Relation*} |
535 text{*Thesis, page 109*} |
535 text{*Thesis, page 109*} |
536 |
536 |
537 (*FIXME: this proof is an ungodly mess*) |
537 (*FIXME: this proof is still an ungodly mess*) |
538 text{*From Meier's thesis, section 4.5.6*} |
538 text{*From Meier's thesis, section 4.5.6*} |
539 lemma commutativity2_lemma: |
539 lemma commutativity2_lemma: |
540 assumes dcommutes: |
540 assumes dcommutes: |
541 "\<forall>act \<in> Acts F. |
541 "\<forall>act \<in> Acts F. |
542 \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> |
542 \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> |
546 and lattice: "lattice L" |
546 and lattice: "lattice L" |
547 and BL: "B \<in> L" |
547 and BL: "B \<in> L" |
548 and TL: "T \<in> L" |
548 and TL: "T \<in> L" |
549 and Fstable: "F \<in> stable T" |
549 and Fstable: "F \<in> stable T" |
550 shows "commutes F T B L" |
550 shows "commutes F T B L" |
551 apply (simp add: commutes_def del: Int_subset_iff, clarify) |
551 apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify) |
552 apply (rename_tac t) |
552 proof - |
553 apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") |
553 fix M and act and t |
554 prefer 2 |
554 assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" |
555 apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify) |
555 then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" |
556 apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") |
556 by (force simp add: cl_eq_Collect_relcl [OF lattice]) |
557 prefer 2 |
557 then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" |
558 apply (intro ballI impI) |
558 by blast |
559 apply (subst cl_ident [symmetric], assumption) |
559 then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u" |
560 apply (simp add: relcl_def) |
560 apply (intro ballI impI) |
561 apply (blast intro: cl_mono [THEN [2] rev_subsetD]) |
561 apply (subst cl_ident [symmetric], assumption) |
562 apply (subgoal_tac "funof act s \<in> T\<inter>M") |
562 apply (simp add: relcl_def) |
563 prefer 2 |
563 apply (blast intro: cl_mono [THEN [2] rev_subsetD]) |
564 apply (cut_tac Fstable) |
564 done |
565 apply (force intro!: funof_in |
565 with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" |
566 simp add: wp_def stable_def constrains_def determ total) |
566 by (force intro!: funof_in |
567 apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L") |
567 simp add: wp_def stable_def constrains_def determ total) |
568 prefer 2 |
568 with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" |
569 apply (rule dcommutes [rule_format], assumption+) |
569 by (intro dcommutes [rule_format]) assumption+ |
570 apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)") |
570 with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)" |
571 prefer 2 |
571 by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) |
572 apply (simp add: relcl_def) |
572 with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))" |
573 apply (blast intro: BL cl_mono [THEN [2] rev_subsetD]) |
573 by (blast intro: funof_imp_wp determ) |
574 apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))") |
574 with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" |
575 prefer 2 |
575 by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) |
576 apply (blast intro: funof_imp_wp determ) |
576 then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" |
577 apply (blast intro: TL cl_mono [THEN [2] rev_subsetD]) |
577 by simp |
578 done |
578 qed |
579 |
579 |
580 |
|
581 text{*Version packaged with @{thm progress_set_Union}*} |
580 text{*Version packaged with @{thm progress_set_Union}*} |
582 lemma commutativity2: |
581 lemma commutativity2: |
583 assumes leadsTo: "F \<in> A leadsTo B" |
582 assumes leadsTo: "F \<in> A leadsTo B" |
584 and dcommutes: |
583 and dcommutes: |
585 "\<forall>act \<in> Acts F. |
584 "\<forall>act \<in> Acts F. |