src/HOL/UNITY/Detects.thy
author wenzelm
Wed, 02 Jul 2014 13:23:11 +0200
changeset 57488 58db442609ac
parent 37936 1e4c5015a72e
child 58889 5b7a9633cfa8
permissions -rw-r--r--
modernized definitions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 16417
diff changeset
     1
(*  Title:      HOL/UNITY/Detects.thy
8334
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     2
    Author:     Tanja Vos, Cambridge University Computer Laboratory
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     3
    Copyright   2000  University of Cambridge
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     4
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     5
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     6
*)
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
     7
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13785
diff changeset
     8
header{*The Detects Relation*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13785
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13812
diff changeset
    10
theory Detects imports FP SubstAx begin
8334
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    11
57488
58db442609ac modernized definitions;
wenzelm
parents: 37936
diff changeset
    12
definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
58db442609ac modernized definitions;
wenzelm
parents: 37936
diff changeset
    13
  where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
58db442609ac modernized definitions;
wenzelm
parents: 37936
diff changeset
    14
58db442609ac modernized definitions;
wenzelm
parents: 37936
diff changeset
    15
definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
58db442609ac modernized definitions;
wenzelm
parents: 37936
diff changeset
    16
  where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    17
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    18
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    19
(* Corollary from Sectiom 3.6.4 *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    20
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    21
lemma Always_at_FP:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    22
     "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    23
apply (rule LeadsTo_empty)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    24
apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    25
apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    26
apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    27
apply auto
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    28
apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    29
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    30
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    31
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    32
lemma Detects_Trans: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    33
     "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    34
apply (unfold Detects_def Int_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    35
apply (simp (no_asm))
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    36
apply safe
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    37
apply (rule_tac [2] LeadsTo_Trans, auto)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    38
apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    39
 apply (blast intro: Always_weaken)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    40
apply (simp add: Always_Int_distrib)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    41
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    42
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    43
lemma Detects_refl: "F \<in> A Detects A"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    44
apply (unfold Detects_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    45
apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    46
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    47
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    48
lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    49
by (unfold Equality_def, blast)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    50
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    51
(*Not quite antisymmetry: sets A and B agree in all reachable states *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    52
lemma Detects_antisym: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    53
     "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    54
apply (unfold Detects_def Equality_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    55
apply (simp add: Always_Int_I Un_commute)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    56
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    57
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    58
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    59
(* Theorem from Section 3.8 *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    60
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    61
lemma Detects_Always: 
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    62
     "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    63
apply (unfold Detects_def Equality_def)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    64
apply (simp add: Un_Int_distrib Always_Int_distrib)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    65
apply (blast dest: Always_at_FP intro: Always_weaken)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    66
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    67
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    68
(* Theorem from exercise 11.1 Section 11.3.1 *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    69
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    70
lemma Detects_Imp_LeadstoEQ: 
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    71
     "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    72
apply (unfold Detects_def Equality_def)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    73
apply (rule_tac B = B in LeadsTo_Diff)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    74
 apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    75
apply (blast intro: Always_LeadsTo_weaken)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    76
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 8334
diff changeset
    77
8334
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    78
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    79
end
7896bcbd8641 Added Tanja's Detects and Reachability theories. Also
paulson
parents:
diff changeset
    80