src/HOL/UNITY/WFair.thy
author paulson
Fri, 31 Jan 2003 20:12:44 +0100
changeset 13798 4c1a53627500
parent 13797 baefae13ad37
child 13805 3786b2fd6808
permissions -rw-r--r--
conversion to new-style theories and tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/WFair
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Weak Fairness versions of transient, ensures, leadsTo.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming", 1994
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
    11
header{*Progress under Weak Fairness*}
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
    12
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    13
theory WFair = UNITY:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    17
  (*This definition specifies weak fairness.  The rest of the theory
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    18
    is generic to all forms of fairness.*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    19
  transient :: "'a set => 'a program set"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    20
    "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    22
  ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
8006
paulson
parents: 7346
diff changeset
    23
    "A ensures B == (A-B co A Un B) Int transient (A-B)"
paulson
parents: 7346
diff changeset
    24
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    25
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    26
consts
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    27
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    28
  (*LEADS-TO constant for the inductive definition*)
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    29
  leads :: "'a program => ('a set * 'a set) set"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    30
6801
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    31
9e0037839d63 renamed the underlying relation of leadsTo from "leadsto"
paulson
parents: 6536
diff changeset
    32
inductive "leads F"
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    33
  intros 
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    35
    Basis:  "F : A ensures B ==> (A,B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    36
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    37
    Trans:  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    39
    Union:  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    40
5155
21177b8a4d7f added comments
paulson
parents: 4776
diff changeset
    41
8006
paulson
parents: 7346
diff changeset
    42
constdefs
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    43
8006
paulson
parents: 7346
diff changeset
    44
  (*visible version of the LEADS-TO relation*)
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    45
  leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
8006
paulson
parents: 7346
diff changeset
    46
    "A leadsTo B == {F. (A,B) : leads F}"
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    47
  
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    48
  (*wlt F B is the largest set that leads to B*)
fe887910e32e specifications as sets of programs
paulson
parents: 5340
diff changeset
    49
  wlt :: "['a program, 'a set] => 'a set"
6536
281d44905cab made many specification operators infix
paulson
parents: 5931
diff changeset
    50
    "wlt F B == Union {A. F: A leadsTo B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
9685
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8006
diff changeset
    52
syntax (xsymbols)
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    53
  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    54
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    55
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
    56
subsection{*transient*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    57
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    58
lemma stable_transient_empty: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    59
    "[| F : stable A; F : transient A |] ==> A = {}"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    60
by (unfold stable_def constrains_def transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    61
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    62
lemma transient_strengthen: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    63
    "[| F : transient A; B<=A |] ==> F : transient B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    64
apply (unfold transient_def, clarify)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    65
apply (blast intro!: rev_bexI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    66
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    67
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    68
lemma transientI: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    69
    "[| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> F : transient A"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    70
by (unfold transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    71
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    72
lemma transientE: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    73
    "[| F : transient A;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    74
        !!act. [| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> P |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    75
     ==> P"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    76
by (unfold transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    77
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    78
lemma transient_UNIV [simp]: "transient UNIV = {}"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    79
by (unfold transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    80
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    81
lemma transient_empty [simp]: "transient {} = UNIV"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    82
by (unfold transient_def, auto)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    83
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    84
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
    85
subsection{*ensures*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    86
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    87
lemma ensuresI: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    88
    "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    89
by (unfold ensures_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    90
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    91
lemma ensuresD: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    92
    "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    93
by (unfold ensures_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    94
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    95
lemma ensures_weaken_R: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    96
    "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    97
apply (unfold ensures_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    98
apply (blast intro: constrains_weaken transient_strengthen)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
    99
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   100
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   101
(*The L-version (precondition strengthening) fails, but we have this*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   102
lemma stable_ensures_Int: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   103
    "[| F : stable C;  F : A ensures B |]    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   104
    ==> F : (C Int A) ensures (C Int B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   105
apply (unfold ensures_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   106
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   107
prefer 2 apply (blast intro: transient_strengthen)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   108
apply (blast intro: stable_constrains_Int constrains_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   109
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   110
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   111
lemma stable_transient_ensures:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   112
     "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   113
apply (simp add: ensures_def stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   114
apply (blast intro: constrains_weaken transient_strengthen)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   115
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   116
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   117
lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   118
by (simp (no_asm) add: ensures_def unless_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   119
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   120
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   121
subsection{*leadsTo*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   122
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   123
lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   124
apply (unfold leadsTo_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   125
apply (blast intro: leads.Basis)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   126
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   127
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   128
lemma leadsTo_Trans: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   129
     "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   130
apply (unfold leadsTo_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   131
apply (blast intro: leads.Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   132
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   133
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   134
lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   135
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   136
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   137
(*Useful with cancellation, disjunction*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   138
lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   139
by (simp add: Un_ac)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   140
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   141
lemma leadsTo_Un_duplicate2:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   142
     "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   143
by (simp add: Un_ac)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   144
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   145
(*The Union introduction rule as we should have liked to state it*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   146
lemma leadsTo_Union: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   147
    "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   148
apply (unfold leadsTo_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   149
apply (blast intro: leads.Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   150
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   151
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   152
lemma leadsTo_Union_Int: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   153
 "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   154
apply (unfold leadsTo_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   155
apply (simp only: Int_Union_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   156
apply (blast intro: leads.Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   157
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   158
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   159
lemma leadsTo_UN: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   160
    "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   161
apply (subst Union_image_eq [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   162
apply (blast intro: leadsTo_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   163
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   164
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   165
(*Binary union introduction rule*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   166
lemma leadsTo_Un:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   167
     "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   168
apply (subst Un_eq_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   169
apply (blast intro: leadsTo_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   170
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   171
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   172
lemma single_leadsTo_I: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   173
     "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   174
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   175
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   176
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   177
(*The INDUCTION rule as we should have liked to state it*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   178
lemma leadsTo_induct: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   179
  "[| F : za leadsTo zb;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   180
      !!A B. F : A ensures B ==> P A B;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   181
      !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   182
               ==> P A C;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   183
      !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   184
   |] ==> P za zb"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   185
apply (unfold leadsTo_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   186
apply (drule CollectD, erule leads.induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   187
apply (blast+)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   188
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   189
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   190
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   191
lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   192
by (unfold ensures_def constrains_def transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   193
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   194
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   195
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   196
lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   197
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   198
lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   199
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   200
lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   201
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   202
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   203
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   204
(** Variant induction rule: on the preconditions for B **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   205
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   206
(*Lemma is the weak version: can't see how to do it in one step*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   207
lemma leadsTo_induct_pre_lemma: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   208
  "[| F : za leadsTo zb;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   209
      P zb;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   210
      !!A B. [| F : A ensures B;  P B |] ==> P A;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   211
      !!S. ALL A:S. P A ==> P (Union S)  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   212
   |] ==> P za"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   213
(*by induction on this formula*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   214
apply (subgoal_tac "P zb --> P za")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   215
(*now solve first subgoal: this formula is sufficient*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   216
apply (blast intro: leadsTo_refl)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   217
apply (erule leadsTo_induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   218
apply (blast+)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   219
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   220
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   221
lemma leadsTo_induct_pre: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   222
  "[| F : za leadsTo zb;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   223
      P zb;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   224
      !!A B. [| F : A ensures B;  F : B leadsTo zb;  P B |] ==> P A;  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   225
      !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   226
   |] ==> P za"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   227
apply (subgoal_tac "F : za leadsTo zb & P za")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   228
apply (erule conjunct2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   229
apply (erule leadsTo_induct_pre_lemma)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   230
prefer 3 apply (blast intro: leadsTo_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   231
prefer 2 apply (blast intro: leadsTo_Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   232
apply (blast intro: leadsTo_refl)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   233
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   234
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   235
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   236
lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   237
by (blast intro: subset_imp_leadsTo leadsTo_Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   238
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   239
lemma leadsTo_weaken_L [rule_format]:
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   240
     "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   241
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   242
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   243
(*Distributes over binary unions*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   244
lemma leadsTo_Un_distrib:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   245
     "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   246
by (blast intro: leadsTo_Un leadsTo_weaken_L)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   247
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   248
lemma leadsTo_UN_distrib:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   249
     "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   250
by (blast intro: leadsTo_UN leadsTo_weaken_L)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   251
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   252
lemma leadsTo_Union_distrib:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   253
     "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   254
by (blast intro: leadsTo_Union leadsTo_weaken_L)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   255
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   256
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   257
lemma leadsTo_weaken:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   258
     "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   259
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   260
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   261
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   262
(*Set difference: maybe combine with leadsTo_weaken_L?*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   263
lemma leadsTo_Diff:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   264
     "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   265
by (blast intro: leadsTo_Un leadsTo_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   266
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   267
lemma leadsTo_UN_UN:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   268
   "(!! i. i:I ==> F : (A i) leadsTo (A' i))  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   269
    ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   270
apply (simp only: Union_image_eq [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   271
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   272
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   273
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   274
(*Binary union version*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   275
lemma leadsTo_Un_Un:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   276
     "[| F : A leadsTo A'; F : B leadsTo B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   277
      ==> F : (A Un B) leadsTo (A' Un B')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   278
by (blast intro: leadsTo_Un leadsTo_weaken_R)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   279
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   280
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   281
(** The cancellation law **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   282
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   283
lemma leadsTo_cancel2:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   284
     "[| F : A leadsTo (A' Un B); F : B leadsTo B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   285
      ==> F : A leadsTo (A' Un B')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   286
by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   287
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   288
lemma leadsTo_cancel_Diff2:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   289
     "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   290
      ==> F : A leadsTo (A' Un B')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   291
apply (rule leadsTo_cancel2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   292
prefer 2 apply assumption
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   293
apply (simp_all (no_asm_simp))
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   294
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   295
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   296
lemma leadsTo_cancel1:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   297
     "[| F : A leadsTo (B Un A'); F : B leadsTo B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   298
    ==> F : A leadsTo (B' Un A')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   299
apply (simp add: Un_commute)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   300
apply (blast intro!: leadsTo_cancel2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   301
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   302
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   303
lemma leadsTo_cancel_Diff1:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   304
     "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   305
    ==> F : A leadsTo (B' Un A')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   306
apply (rule leadsTo_cancel1)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   307
prefer 2 apply assumption
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   308
apply (simp_all (no_asm_simp))
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   309
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   310
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   311
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   312
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   313
(** The impossibility law **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   314
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   315
lemma leadsTo_empty: "F : A leadsTo {} ==> A={}"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   316
apply (erule leadsTo_induct_pre)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   317
apply (simp_all add: ensures_def constrains_def transient_def, blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   318
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   319
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   320
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   321
(** PSP: Progress-Safety-Progress **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   322
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   323
(*Special case of PSP: Misra's "stable conjunction"*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   324
lemma psp_stable: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   325
   "[| F : A leadsTo A'; F : stable B |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   326
    ==> F : (A Int B) leadsTo (A' Int B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   327
apply (unfold stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   328
apply (erule leadsTo_induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   329
prefer 3 apply (blast intro: leadsTo_Union_Int)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   330
prefer 2 apply (blast intro: leadsTo_Trans)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   331
apply (rule leadsTo_Basis)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   332
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   333
apply (blast intro: transient_strengthen constrains_Int)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   334
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   335
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   336
lemma psp_stable2: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   337
   "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   338
by (simp add: psp_stable Int_ac)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   339
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   340
lemma psp_ensures: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   341
   "[| F : A ensures A'; F : B co B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   342
    ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   343
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   344
apply (blast intro: transient_strengthen)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   345
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   346
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   347
lemma psp:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   348
     "[| F : A leadsTo A'; F : B co B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   349
      ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   350
apply (erule leadsTo_induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   351
  prefer 3 apply (blast intro: leadsTo_Union_Int)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   352
 txt{*Basis case*}
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   353
 apply (blast intro: psp_ensures)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   354
txt{*Transitivity case has a delicate argument involving "cancellation"*}
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   355
apply (rule leadsTo_Un_duplicate2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   356
apply (erule leadsTo_cancel_Diff1)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   357
apply (simp add: Int_Diff Diff_triv)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   358
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   359
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   360
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   361
lemma psp2:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   362
     "[| F : A leadsTo A'; F : B co B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   363
    ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   364
by (simp (no_asm_simp) add: psp Int_ac)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   365
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   366
lemma psp_unless: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   367
   "[| F : A leadsTo A';  F : B unless B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   368
    ==> F : (A Int B) leadsTo ((A' Int B) Un B')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   369
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   370
apply (unfold unless_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   371
apply (drule psp, assumption)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   372
apply (blast intro: leadsTo_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   373
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   374
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   375
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   376
subsection{*Proving the induction rules*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   377
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   378
(** The most general rule: r is any wf relation; f is any variant function **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   379
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   380
lemma leadsTo_wf_induct_lemma:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   381
     "[| wf r;      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   382
         ALL m. F : (A Int f-`{m}) leadsTo                      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   383
                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   384
      ==> F : (A Int f-`{m}) leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   385
apply (erule_tac a = m in wf_induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   386
apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   387
 apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   388
apply (subst vimage_eq_UN)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   389
apply (simp only: UN_simps [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   390
apply (blast intro: leadsTo_UN)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   391
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   392
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   393
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   394
(** Meta or object quantifier ? **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   395
lemma leadsTo_wf_induct:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   396
     "[| wf r;      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   397
         ALL m. F : (A Int f-`{m}) leadsTo                      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   398
                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   399
      ==> F : A leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   400
apply (rule_tac t = A in subst)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   401
 defer 1
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   402
 apply (rule leadsTo_UN)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   403
 apply (erule leadsTo_wf_induct_lemma)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   404
 apply assumption
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   405
apply fast (*Blast_tac: Function unknown's argument not a parameter*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   406
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   407
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   408
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   409
lemma bounded_induct:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   410
     "[| wf r;      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   411
         ALL m:I. F : (A Int f-`{m}) leadsTo                    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   412
                      ((A Int f-`(r^-1 `` {m})) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   413
      ==> F : A leadsTo ((A - (f-`I)) Un B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   414
apply (erule leadsTo_wf_induct, safe)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   415
apply (case_tac "m:I")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   416
apply (blast intro: leadsTo_weaken)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   417
apply (blast intro: subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   418
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   419
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   420
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   421
(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   422
lemma lessThan_induct: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   423
     "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   424
      ==> F : A leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   425
apply (rule wf_less_than [THEN leadsTo_wf_induct])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   426
apply (simp (no_asm_simp))
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   427
apply blast
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   428
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   429
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   430
lemma lessThan_bounded_induct:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   431
     "!!l::nat. [| ALL m:(greaterThan l).     
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   432
            F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   433
      ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   434
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   435
apply (rule wf_less_than [THEN bounded_induct])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   436
apply (simp (no_asm_simp))
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   437
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   438
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   439
lemma greaterThan_bounded_induct:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   440
     "!!l::nat. [| ALL m:(lessThan l).     
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   441
            F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   442
      ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   443
apply (rule_tac f = f and f1 = "%k. l - k" 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   444
       in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   445
apply (simp (no_asm) add: inv_image_def Image_singleton)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   446
apply clarify
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   447
apply (case_tac "m<l")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   448
prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   449
apply (blast intro: leadsTo_weaken_R diff_less_mono2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   450
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   451
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   452
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   453
subsection{*wlt*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   454
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   455
(*Misra's property W3*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   456
lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   457
apply (unfold wlt_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   458
apply (blast intro!: leadsTo_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   459
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   460
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   461
lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   462
apply (unfold wlt_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   463
apply (blast intro!: leadsTo_Union)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   464
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   465
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   466
(*Misra's property W2*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   467
lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   468
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   469
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   470
(*Misra's property W4*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   471
lemma wlt_increasing: "B <= wlt F B"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   472
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   473
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   474
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   475
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   476
(*Used in the Trans case below*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   477
lemma lemma1: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   478
   "[| B <= A2;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   479
       F : (A1 - B) co (A1 Un B);  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   480
       F : (A2 - C) co (A2 Un C) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   481
    ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   482
by (unfold constrains_def, clarify,  blast)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   483
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   484
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   485
lemma leadsTo_123:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   486
     "F : A leadsTo A'  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   487
      ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   488
apply (erule leadsTo_induct)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   489
(*Basis*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   490
apply (blast dest: ensuresD)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   491
(*Trans*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   492
apply clarify
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   493
apply (rule_tac x = "Ba Un Bb" in exI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   494
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   495
(*Union*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   496
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   497
apply (rule_tac x = "UN A:S. f A" in exI)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   498
apply (auto intro: leadsTo_UN)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   499
(*Blast_tac says PROOF FAILED*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   500
apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" 
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   501
       in constrains_UN [THEN constrains_weaken], auto) 
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   502
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   503
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   504
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   505
(*Misra's property W5*)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   506
lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   507
proof -
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   508
  from wlt_leadsTo [of F B, THEN leadsTo_123]
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   509
  show ?thesis
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   510
  proof (elim exE conjE)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   511
(* assumes have to be in exactly the form as in the goal displayed at
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   512
   this point.  Isar doesn't give you any automation. *)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   513
    fix C
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   514
    assume wlt: "wlt F B \<subseteq> C"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   515
       and lt:  "F \<in> C leadsTo B"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   516
       and co:  "F \<in> C - B co C \<union> B"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   517
    have eq: "C = wlt F B"
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   518
    proof -
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   519
      from lt and wlt show ?thesis 
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   520
           by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   521
    qed
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   522
    from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   523
  qed
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   524
qed
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   525
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   526
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13797
diff changeset
   527
subsection{*Completion: Binary and General Finite versions*}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   528
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   529
lemma completion_lemma :
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   530
     "[| W = wlt F (B' Un C);      
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   531
       F : A leadsTo (A' Un C);  F : A' co (A' Un C);    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   532
       F : B leadsTo (B' Un C);  F : B' co (B' Un C) |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   533
    ==> F : (A Int B) leadsTo ((A' Int B') Un C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   534
apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   535
 prefer 2
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   536
 apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   537
                                         THEN constrains_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   538
apply (subgoal_tac "F : (W-C) co W")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   539
 prefer 2
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   540
 apply (simp add: wlt_increasing Un_assoc Un_absorb2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   541
apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   542
 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   543
(** LEVEL 6 **)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   544
apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   545
 prefer 2
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   546
 apply (rule leadsTo_Un_duplicate2)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   547
 apply (blast intro: leadsTo_Un_Un wlt_leadsTo
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   548
                         [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   549
apply (drule leadsTo_Diff)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   550
apply (blast intro: subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   551
apply (subgoal_tac "A Int B <= A Int W")
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   552
 prefer 2
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   553
 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   554
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   555
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   556
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   557
lemmas completion = completion_lemma [OF refl]
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   558
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   559
lemma finite_completion_lemma:
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   560
     "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   561
                   (ALL i:I. F : (A' i) co (A' i Un C)) -->  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   562
                   F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   563
apply (erule finite_induct, auto)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   564
apply (rule completion)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   565
   prefer 4
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   566
   apply (simp only: INT_simps [symmetric])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   567
   apply (rule constrains_INT, auto)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   568
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   569
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   570
lemma finite_completion: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   571
     "[| finite I;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   572
         !!i. i:I ==> F : (A i) leadsTo (A' i Un C);  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   573
         !!i. i:I ==> F : (A' i) co (A' i Un C) |]    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   574
      ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   575
by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   576
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   577
lemma stable_completion: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   578
     "[| F : A leadsTo A';  F : stable A';    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   579
         F : B leadsTo B';  F : stable B' |]  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   580
    ==> F : (A Int B) leadsTo (A' Int B')"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   581
apply (unfold stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   582
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   583
apply (force+)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   584
done
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   585
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   586
lemma finite_stable_completion: 
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   587
     "[| finite I;   
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   588
         !!i. i:I ==> F : (A i) leadsTo (A' i);  
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   589
         !!i. i:I ==> F : stable (A' i) |]    
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   590
      ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   591
apply (unfold stable_def)
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   592
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   593
apply (simp_all (no_asm_simp))
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   594
apply blast+
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 10834
diff changeset
   595
done
9685
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8006
diff changeset
   596
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   597
end