author | paulson |
Wed, 08 Dec 1999 13:53:29 +0100 | |
changeset 8055 | bb15396278fb |
parent 7947 | b999c1ab9327 |
child 8065 | 658e0d4e4ed9 |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.ML |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
5 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
6 |
Guarantees, etc. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
7 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
8 |
From Chandy and Sanders, "Reasoning About Program Composition" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
9 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
10 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
11 |
(*** existential properties ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
12 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
13 |
Goalw [ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
14 |
"[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
15 |
by (etac finite_induct 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
16 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
17 |
qed_spec_mp "ex1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
18 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
19 |
Goalw [ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
20 |
"ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
21 |
by (Clarify_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
22 |
by (dres_inst_tac [("x", "{F,G}")] spec 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
23 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
24 |
qed "ex2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
25 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
26 |
(*Chandy & Sanders take this as a definition*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
27 |
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
28 |
by (blast_tac (claset() addIs [ex1,ex2]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
29 |
qed "ex_prop_finite"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
30 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
31 |
(*Their "equivalent definition" given at the end of section 3*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
32 |
Goal "ex_prop X = (ALL G. G:X = (ALL H. G <= H --> H: X))"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
33 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
34 |
by (rewrite_goals_tac [ex_prop_def, component_def]); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
35 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
36 |
by Safe_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
37 |
by (stac Join_commute 2); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
38 |
by (ALLGOALS Blast_tac); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
39 |
qed "ex_prop_equiv"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
40 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
41 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
42 |
(*** universal properties ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
43 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
44 |
Goalw [uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
45 |
"[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
46 |
by (etac finite_induct 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
47 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
48 |
qed_spec_mp "uv1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
49 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
50 |
Goalw [uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
51 |
"ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
52 |
by (rtac conjI 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
53 |
by (Clarify_tac 2); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
54 |
by (dres_inst_tac [("x", "{F,G}")] spec 2); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
55 |
by (dres_inst_tac [("x", "{}")] spec 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
56 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
57 |
qed "uv2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
58 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
59 |
(*Chandy & Sanders take this as a definition*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
60 |
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
61 |
by (blast_tac (claset() addIs [uv1,uv2]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
62 |
qed "uv_prop_finite"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
63 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
64 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
65 |
(*** guarantees ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
66 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
67 |
val prems = Goal |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
68 |
"(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
69 |
\ ==> F : X guarantees[v] Y"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
70 |
by (simp_tac (simpset() addsimps [guar_def, component_def]) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
71 |
by (blast_tac (claset() addIs prems) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
72 |
qed "guaranteesI"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
73 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
74 |
Goalw [guar_def, component_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
75 |
"[| F : X guarantees[v] Y; G : preserves v; F Join G : X |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
76 |
\ ==> F Join G : Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
77 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
78 |
qed "guaranteesD"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
79 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
80 |
(*This version of guaranteesD matches more easily in the conclusion*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
81 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
82 |
"[| F : X guarantees[v] Y; H : X; H = F Join G; G : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
83 |
\ ==> H : Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
84 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
85 |
qed "component_guaranteesD"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
86 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
87 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
88 |
"[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
89 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
90 |
qed "guarantees_weaken"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
91 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
92 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
93 |
"[| F: X guarantees[v] Y; preserves w <= preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
94 |
\ ==> F: X guarantees[w] Y"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
95 |
by (Blast_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
96 |
qed "guarantees_weaken_var"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
97 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
98 |
Goalw [guar_def] "X <= Y ==> X guarantees[v] Y = UNIV"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
99 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
100 |
qed "subset_imp_guarantees_UNIV"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
101 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
102 |
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
103 |
Goalw [guar_def] "X <= Y ==> F : X guarantees[v] Y"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
104 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
105 |
qed "subset_imp_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
106 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
107 |
(*Remark at end of section 4.1 |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
108 |
Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] Y)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
109 |
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
110 |
by (blast_tac (claset() addEs [equalityE]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
111 |
qed "ex_prop_equiv2"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
112 |
*) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
113 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
114 |
(** Distributive laws. Re-orient to perform miniscoping **) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
115 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
116 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
117 |
"(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
118 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
119 |
qed "guarantees_UN_left"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
120 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
121 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
122 |
"(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
123 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
124 |
qed "guarantees_Un_left"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
125 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
126 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
127 |
"X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
128 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
129 |
qed "guarantees_INT_right"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
130 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
131 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
132 |
"Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
133 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
134 |
qed "guarantees_Int_right"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
135 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
136 |
Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
137 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
138 |
qed "shunting"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
139 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
140 |
Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
141 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
142 |
qed "contrapositive"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
143 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
144 |
(** The following two can be expressed using intersection and subset, which |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
145 |
is more faithful to the text but looks cryptic. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
146 |
**) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
147 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
148 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
149 |
"[| F : V guarantees[v] X; F : (X Int Y) guarantees[v] Z |]\ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
150 |
\ ==> F : (V Int Y) guarantees[v] Z"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
151 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
152 |
qed "combining1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
153 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
154 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
155 |
"[| F : V guarantees[v] (X Un Y); F : Y guarantees[v] Z |]\ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
156 |
\ ==> F : V guarantees[v] (X Un Z)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
157 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
158 |
qed "combining2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
159 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
160 |
(** The following two follow Chandy-Sanders, but the use of object-quantifiers |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
161 |
does not suit Isabelle... **) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
162 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
163 |
(*Premise should be (!!i. i: I ==> F: X guarantees[v] Y i) *) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
164 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
165 |
"ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
166 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
167 |
qed "all_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
168 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
169 |
(*Premises should be [| F: X guarantees[v] Y i; i: I |] *) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
170 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
171 |
"EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
172 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
173 |
qed "ex_guarantees"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
174 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
175 |
(*** Additional guarantees laws, by lcp ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
176 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
177 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
178 |
"[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
179 |
\ F : preserves v; G : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
180 |
\ ==> F Join G: (U Int X) guarantees[v] (V Int Y)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
181 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
182 |
by Safe_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
183 |
by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
184 |
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
185 |
by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
186 |
by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
187 |
qed "guarantees_Join_Int"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
188 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
189 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
190 |
"[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
191 |
\ F : preserves v; G : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
192 |
\ ==> F Join G: (U Un X) guarantees[v] (V Un Y)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
193 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
194 |
by Safe_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
195 |
by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
196 |
by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
197 |
by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
198 |
by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
199 |
qed "guarantees_Join_Un"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
200 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
201 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
202 |
"[| ALL i:I. F i : X i guarantees[v] Y i; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
203 |
\ ALL i:I. F i : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
204 |
\ ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
205 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
206 |
by (ball_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
207 |
by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
208 |
by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
209 |
Join_preserves, JN_preserves]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
210 |
qed "guarantees_JN_INT"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
211 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
212 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
213 |
"[| ALL i:I. F i : X i guarantees[v] Y i; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
214 |
\ ALL i:I. F i : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
215 |
\ ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
216 |
by Auto_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
217 |
by (ball_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
218 |
by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
219 |
by (auto_tac |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
220 |
(claset(), |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
221 |
simpset() addsimps [Join_assoc RS sym, JN_absorb, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
222 |
Join_preserves, JN_preserves])); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
223 |
qed "guarantees_JN_UN"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
224 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
225 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
226 |
(*** guarantees[v] laws for breaking down the program, by lcp ***) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
227 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
228 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
229 |
"[| F: X guarantees[v] Y; G: preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
230 |
\ ==> F Join G: X guarantees[v] Y"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
231 |
by (Simp_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
232 |
by Safe_tac; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
233 |
by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
234 |
qed "guarantees_Join_I1"; |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
235 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
236 |
Goal "[| G: X guarantees[v] Y; F: preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
237 |
\ ==> F Join G: X guarantees[v] Y"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
238 |
by (stac Join_commute 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
239 |
by (blast_tac (claset() addIs [guarantees_Join_I1]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
240 |
qed "guarantees_Join_I2"; |
7689 | 241 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
242 |
Goalw [guar_def] |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
243 |
"[| i : I; F i: X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
244 |
\ ALL j:I. i~=j --> F j : preserves v |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
245 |
\ ==> (JN i:I. (F i)) : X guarantees[v] Y"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
246 |
by (Clarify_tac 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
247 |
by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
248 |
by (auto_tac (claset(), |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
249 |
simpset() addsimps [JN_Join_diff, Join_assoc RS sym, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
250 |
Join_preserves, JN_preserves])); |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
251 |
qed "guarantees_JN_I"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
252 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
253 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
254 |
(*** well-definedness ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
255 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
256 |
Goalw [welldef_def] "F Join G: welldef ==> F: welldef"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
257 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
258 |
qed "Join_welldef_D1"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
259 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
260 |
Goalw [welldef_def] "F Join G: welldef ==> G: welldef"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
261 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
262 |
qed "Join_welldef_D2"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
263 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
264 |
(*** refinement ***) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
265 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
266 |
Goalw [refines_def] "F refines F wrt X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
267 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
268 |
qed "refines_refl"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
269 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
270 |
Goalw [refines_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
271 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
272 |
by Auto_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
273 |
qed "refines_trans"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
274 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
275 |
Goalw [strict_ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
276 |
"strict_ex_prop X \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
277 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
278 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
279 |
qed "strict_ex_refine_lemma"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
280 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
281 |
Goalw [strict_ex_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
282 |
"strict_ex_prop X \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
283 |
\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
284 |
\ (F: welldef Int X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
285 |
by Safe_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
286 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
287 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset())); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
288 |
qed "strict_ex_refine_lemma_v"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
289 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
290 |
Goal "[| strict_ex_prop X; \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
291 |
\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
292 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
293 |
by (res_inst_tac [("x","SKIP")] allE 1 |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
294 |
THEN assume_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
295 |
by (asm_full_simp_tac |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
296 |
(simpset() addsimps [refines_def, iso_refines_def, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
297 |
strict_ex_refine_lemma_v]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
298 |
qed "ex_refinement_thm"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
299 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
300 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
301 |
Goalw [strict_uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
302 |
"strict_uv_prop X \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
303 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
304 |
by (Blast_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
305 |
qed "strict_uv_refine_lemma"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
306 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
307 |
Goalw [strict_uv_prop_def] |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
308 |
"strict_uv_prop X \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
309 |
\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
310 |
\ (F: welldef Int X --> G:X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
311 |
by Safe_tac; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
312 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
313 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
314 |
simpset())); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
315 |
qed "strict_uv_refine_lemma_v"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
316 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
317 |
Goal "[| strict_uv_prop X; \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
318 |
\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
319 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
320 |
by (res_inst_tac [("x","SKIP")] allE 1 |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
321 |
THEN assume_tac 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
322 |
by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
323 |
strict_uv_refine_lemma_v]) 1); |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
324 |
qed "uv_refinement_thm"; |