author | wenzelm |
Sat, 14 Jun 2008 23:19:51 +0200 | |
changeset 27208 | 5fe899199f85 |
parent 16417 | 9bc16273c2d4 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
5899 | 1 |
(* Title: HOL/UNITY/PPROD.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
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 | 10 |
*) |
11 |
||
16417 | 12 |
theory PPROD imports Lift_prog begin |
5899 | 13 |
|
14 |
constdefs |
|
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 | 18 |
"PLam I F == \<Squnion>i \<in> I. lift i (F i)" |
5899 | 19 |
|
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 | 23 |
|
24 |
translations |
|
13805 | 25 |
"plam x : A. B" == "PLam A (%x. B)" |
5899 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 122 |
text{*This rule looks unsatisfactory because it refers to @{term lift}. |
123 |
One must use |
|
124 |
@{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and |
|
125 |
something like @{text lift_preserves_sub} to rewrite the third. However |
|
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 | 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 | 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 | 141 |
"(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))" |
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 | 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 | 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 | 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 | 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 | 180 |
lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))" |
13798 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 287 |
end |