src/HOL/UNITY/PPROD.thy
author wenzelm
Sat, 14 Jun 2008 23:19:51 +0200
changeset 27208 5fe899199f85
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/PPROD.thy
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
     2
    ID:         $Id$
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
     5
7188
2bc63a44721b re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents: 6842
diff changeset
     6
Abstraction over replicated components (PLam)
2bc63a44721b re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents: 6842
diff changeset
     7
General products of programs (Pi operation)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
     8
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
     9
Some dead wood here!
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    10
*)
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    11
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14150
diff changeset
    12
theory PPROD imports Lift_prog begin
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    13
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    14
constdefs
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    15
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 7188
diff changeset
    16
  PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 7188
diff changeset
    17
            => ((nat=>'b) * 'c) program"
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    18
    "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    19
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    20
syntax
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    21
  "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    22
              ("(3plam _:_./ _)" 10)
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    23
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    24
translations
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    25
  "plam x : A. B"   == "PLam A (%x. B)"
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
    26
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    27
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    28
(*** Basic properties ***)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    29
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    30
lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    31
by (simp add: PLam_def lift_def lift_set_def)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    32
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    33
lemma PLam_empty [simp]: "PLam {} F = SKIP"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    34
by (simp add: PLam_def)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    35
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    36
lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    37
by (simp add: PLam_def lift_SKIP JN_constant)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    38
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    39
lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    40
by (unfold PLam_def, auto)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    41
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    42
lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    43
by (simp add: PLam_def JN_component_iff)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    44
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    45
lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    46
apply (unfold PLam_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    47
(*blast_tac doesn't use HO unification*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    48
apply (fast intro: component_JN)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    49
done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    50
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    51
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    52
(** Safety & Progress: but are they used anywhere? **)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    53
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    54
lemma PLam_constrains:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    55
     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    56
      ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    57
                      (lift_set i (B <*> UNIV)))  =
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    58
          (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    59
apply (simp add: PLam_def JN_constrains)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    60
apply (subst insert_Diff [symmetric], assumption)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    61
apply (simp add: lift_constrains)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    62
apply (blast intro: constrains_imp_lift_constrains)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    63
done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    64
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    65
lemma PLam_stable:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    66
     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    67
      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
    68
          (F i \<in> stable (A <*> UNIV))"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    69
by (simp add: stable_def PLam_constrains)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    70
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    71
lemma PLam_transient:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    72
     "i \<in> I ==>
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    73
    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    74
by (simp add: JN_transient PLam_def)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    75
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    76
text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    77
lemma PLam_ensures:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    78
     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    79
         \<forall>j. F j \<in> preserves snd |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    80
      ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    81
apply (simp add: ensures_def PLam_constrains PLam_transient
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    82
              lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    83
              Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    84
apply (rule rev_bexI, assumption)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    85
apply (simp add: lift_transient)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    86
done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    87
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    88
lemma PLam_leadsTo_Basis:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    89
     "[| i \<in> I;
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    90
         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    91
               ((A <*> UNIV) \<union> (B <*> UNIV));
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    92
         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    93
         \<forall>j. F j \<in> preserves snd |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
    94
      ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    95
by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    96
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    97
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    98
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
    99
(** invariant **)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   100
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   101
lemma invariant_imp_PLam_invariant:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   102
     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   103
         \<forall>j. F j \<in> preserves snd |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   104
      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   105
by (auto simp add: PLam_stable invariant_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   106
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   107
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   108
lemma PLam_preserves_fst [simp]:
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   109
     "\<forall>j. F j \<in> preserves snd
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   110
      ==> (PLam I F \<in> preserves (v o sub j o fst)) =
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   111
          (if j \<in> I then F j \<in> preserves (v o fst) else True)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   112
by (simp add: PLam_def lift_preserves_sub)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   113
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   114
lemma PLam_preserves_snd [simp,intro]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   115
     "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   116
by (simp add: PLam_def lift_preserves_snd_I)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   117
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   118
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   119
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   120
(*** guarantees properties ***)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   121
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13812
diff changeset
   122
text{*This rule looks unsatisfactory because it refers to @{term lift}. 
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13812
diff changeset
   123
  One must use
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13812
diff changeset
   124
  @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13812
diff changeset
   125
  something like @{text lift_preserves_sub} to rewrite the third.  However
9a23e4eb5eb3 A document for UNITY
paulson
parents: 13812
diff changeset
   126
  there's no obvious alternative for the third premise.*}
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   127
lemma guarantees_PLam_I:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   128
    "[| lift i (F i): X guarantees Y;  i \<in> I;
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   129
        OK I (%i. lift i (F i)) |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   130
     ==> (PLam I F) \<in> X guarantees Y"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   131
apply (unfold PLam_def)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   132
apply (simp add: guarantees_JN_I)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   133
done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   134
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   135
lemma Allowed_PLam [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   136
     "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   137
by (simp add: PLam_def)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   138
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   139
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   140
lemma PLam_preserves [simp]:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   141
     "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   142
by (simp add: PLam_def lift_def rename_preserves)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   143
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   144
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   145
(**UNUSED
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   146
    (*The f0 premise ensures that the product is well-defined.*)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   147
    lemma PLam_invariant_imp_invariant:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   148
     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   149
             f0: Init (PLam I F) |] ==> F i \<in> invariant A"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   150
    apply (auto simp add: invariant_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   151
    apply (drule_tac c = "f0 (i:=x) " in subsetD)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   152
    apply auto
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   153
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   154
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   155
    lemma PLam_invariant:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   156
     "[| i \<in> I;  f0: Init (PLam I F) |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   157
          ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   158
    apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   159
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   160
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   161
    (*The f0 premise isn't needed if F is a constant program because then
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   162
      we get an initial state by replicating that of F*)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   163
    lemma reachable_PLam:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   164
     "i \<in> I
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   165
          ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   166
    apply (auto simp add: invariant_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   167
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   168
**)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   169
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   170
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   171
(**UNUSED
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   172
    (** Reachability **)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   173
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   174
    Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   175
    apply (erule reachable.induct)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   176
    apply (auto intro: reachable.intrs)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   177
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   178
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   179
    (*Result to justify a re-organization of this file*)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   180
    lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13786
diff changeset
   181
    by auto
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   182
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   183
    lemma reachable_PLam_subset1:
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   184
     "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   185
    apply (force dest!: reachable_PLam)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   186
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   187
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   188
    (*simplify using reachable_lift??*)
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13786
diff changeset
   189
    lemma reachable_lift_Join_PLam [rule_format]:
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   190
      "[| i \<notin> I;  A \<in> reachable (F i) |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   191
       ==> \<forall>f. f \<in> reachable (PLam I F)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   192
                  --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   193
    apply (erule reachable.induct)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   194
    apply (ALLGOALS Clarify_tac)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   195
    apply (erule reachable.induct)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   196
    (*Init, Init case*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   197
    apply (force intro: reachable.intrs)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   198
    (*Init of F, action of PLam F case*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   199
    apply (rule_tac act = act in reachable.Acts)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   200
    apply force
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   201
    apply assumption
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   202
    apply (force intro: ext)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   203
    (*induction over the 2nd "reachable" assumption*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   204
    apply (erule_tac xa = f in reachable.induct)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   205
    (*Init of PLam F, action of F case*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   206
    apply (rule_tac act = "lift_act i act" in reachable.Acts)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   207
    apply force
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   208
    apply (force intro: reachable.Init)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   209
    apply (force intro: ext simp add: lift_act_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   210
    (*last case: an action of PLam I F*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   211
    apply (rule_tac act = acta in reachable.Acts)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   212
    apply force
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   213
    apply assumption
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   214
    apply (force intro: ext)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   215
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   216
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   217
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   218
    (*The index set must be finite: otherwise infinitely many copies of F can
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   219
      perform actions, and PLam can never catch up in finite time.*)
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   220
    lemma reachable_PLam_subset2:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   221
     "finite I
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   222
          ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   223
    apply (erule finite_induct)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   224
    apply (simp (no_asm))
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   225
    apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   226
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   227
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   228
    lemma reachable_PLam_eq:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   229
     "finite I ==>
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   230
          reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   231
    apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   232
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   233
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   234
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   235
    (** Co **)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   236
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   237
    lemma Constrains_imp_PLam_Constrains:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   238
     "[| F i \<in> A Co B;  i \<in> I;  finite I |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   239
          ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   240
    apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   241
    apply (auto simp add: constrains_def PLam_def)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   242
    apply (REPEAT (blast intro: reachable.intrs))
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   243
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   244
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   245
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   246
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   247
    lemma PLam_Constrains:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   248
     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   249
          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   250
              (F i \<in> A Co B)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   251
    apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   252
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   253
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   254
    lemma PLam_Stable:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   255
     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   256
          ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   257
    apply (simp del: Init_PLam add: Stable_def PLam_Constrains)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   258
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   259
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   260
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   261
    (** const_PLam (no dependence on i) doesn't require the f0 premise **)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   262
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   263
    lemma const_PLam_Constrains:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   264
     "[| i \<in> I;  finite I |]
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   265
          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   266
              (F \<in> A Co B)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   267
    apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   268
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   269
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   270
    lemma const_PLam_Stable:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   271
     "[| i \<in> I;  finite I |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   272
          ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   273
    apply (simp add: Stable_def const_PLam_Constrains)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   274
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   275
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   276
    lemma const_PLam_Increasing:
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13805
diff changeset
   277
	 "[| i \<in> I;  finite I |]
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   278
          ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   279
    apply (unfold Increasing_def)
13805
3786b2fd6808 some x-symbols
paulson
parents: 13798
diff changeset
   280
    apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   281
    apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   282
    apply (simp add: finite_lessThan const_PLam_Stable)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   283
    done
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   284
**)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   285
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents: 8251
diff changeset
   286
5899
13d4753079fe new theory PPROD
paulson
parents:
diff changeset
   287
end