src/HOL/UNITY/ELT.ML
author paulson
Wed, 08 Dec 1999 13:53:29 +0100
changeset 8055 bb15396278fb
parent 8044 296b03b79505
child 8067 225e3b45b766
permissions -rw-r--r--
abolition of localTo: instead "guarantees" has local vars as extra argument
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/ELT
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     5
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     6
leadsTo strengthened with a specification of the allowable sets transient parts
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     7
*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
     8
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
     9
Goalw [givenBy_def] "givenBy id = UNIV";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    10
by Auto_tac;
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    11
qed "givenBy_id";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    12
Addsimps [givenBy_id];
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    13
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    14
Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    15
by Safe_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    16
by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    17
by Auto_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    18
qed "givenBy_eq_all";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    19
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    20
Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    21
by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    22
by Safe_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    23
by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    24
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    25
by Auto_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    26
qed "givenBy_eq_Collect";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    27
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    28
val prems =
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    29
Goal "(!!x y. [|  x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    30
by (stac givenBy_eq_all 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    31
by (blast_tac (claset() addIs prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    32
qed "givenByI";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    33
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    34
Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    35
by Auto_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    36
qed "givenByD";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    37
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    38
Goal "{} : givenBy v";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    39
by (blast_tac (claset() addSIs [givenByI]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    40
qed "empty_mem_givenBy";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    41
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    42
AddIffs [empty_mem_givenBy];
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    43
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    44
Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    45
by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    46
by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    47
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    48
qed "givenBy_imp_eq_Collect";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    49
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    50
Goalw [givenBy_def] "EX P. A = {s. P(v s)} ==> A: givenBy v";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    51
by (Best_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    52
qed "eq_Collect_imp_givenBy";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    53
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    54
Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    55
by (blast_tac (claset() addIs [eq_Collect_imp_givenBy,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    56
			       givenBy_imp_eq_Collect]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    57
qed "givenBy_eq_eq_Collect";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    58
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    59
(*preserving v preserves properties given by v*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    60
Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    61
by (force_tac (claset(), 
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    62
	       simpset() addsimps [impOfSubs preserves_subset_stable, 
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    63
				   givenBy_eq_Collect]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
    64
qed "preserves_givenBy_imp_stable";
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    65
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    66
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    67
(** Standard leadsTo rules **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    68
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    69
Goalw [leadsETo_def] "[| F: A ensures B;  A-B: CC |] ==> F : A leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    70
by (blast_tac (claset() addIs [elt.Basis]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    71
qed "leadsETo_Basis";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    72
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    73
Goalw [leadsETo_def]
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    74
     "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    75
by (blast_tac (claset() addIs [elt.Trans]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    76
qed "leadsETo_Trans";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    77
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    78
(*Useful with cancellation, disjunction*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    79
Goal "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    80
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    81
qed "leadsETo_Un_duplicate";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    82
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    83
Goal "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    84
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    85
qed "leadsETo_Un_duplicate2";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    86
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    87
(*The Union introduction rule as we should have liked to state it*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    88
val prems = Goalw [leadsETo_def]
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    89
    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    90
by (blast_tac (claset() addIs [elt.Union] addDs prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    91
qed "leadsETo_Union";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    92
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    93
val prems = Goal
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    94
    "(!!i. i : I ==> F : (A i) leadsTo[CC] B) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    95
\    ==> F : (UN i:I. A i) leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    96
by (stac (Union_image_eq RS sym) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    97
by (blast_tac (claset() addIs leadsETo_Union::prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    98
qed "leadsETo_UN";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
    99
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   100
(*The INDUCTION rule as we should have liked to state it*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   101
val major::prems = Goalw [leadsETo_def]
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   102
  "[| F : za leadsTo[CC] zb;  \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   103
\     !!A B. [| F : A ensures B;  A-B : CC |] ==> P A B; \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   104
\     !!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   105
\              ==> P A C; \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   106
\     !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   107
\  |] ==> P za zb";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   108
by (rtac (major RS CollectD RS elt.induct) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   109
by (REPEAT (blast_tac (claset() addIs prems) 1));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   110
qed "leadsETo_induct";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   111
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   112
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   113
(** New facts involving leadsETo **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   114
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   115
Goal "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   116
by Safe_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   117
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   118
by (blast_tac (claset() addIs [leadsETo_Union]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   119
by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   120
by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   121
qed "leadsETo_mono";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   122
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   123
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   124
val prems = Goalw [leadsETo_def]
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   125
 "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   126
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   127
by (blast_tac (claset() addIs [elt.Union] addDs prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   128
qed "leadsETo_Union_Int";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   129
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   130
(*Binary union introduction rule*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   131
Goal "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] ==> F : (A Un B) leadsTo[CC] C";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   132
by (stac Un_eq_Union 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   133
by (blast_tac (claset() addIs [leadsETo_Union]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   134
qed "leadsETo_Un";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   135
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   136
val prems = 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   137
Goal "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   138
by (stac (UN_singleton RS sym) 1 THEN rtac leadsETo_UN 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   139
by (blast_tac (claset() addIs prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   140
qed "single_leadsETo_I";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   141
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   142
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   143
Goal "[| A<=B;  {}:CC |]  ==> F : A leadsTo[CC] B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   144
by (asm_simp_tac (simpset() addsimps [subset_imp_ensures RS leadsETo_Basis,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   145
				      Diff_eq_empty_iff RS iffD2]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   146
qed "subset_imp_leadsETo";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   147
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   148
bind_thm ("empty_leadsETo", empty_subsetI RS subset_imp_leadsETo);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   149
Addsimps [empty_leadsETo];
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   150
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   151
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   152
(** Weakening laws all require {}:CC **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   153
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   154
Goal "[| F : A leadsTo[CC] A';  A'<=B';  {}:CC |] ==> F : A leadsTo[CC] B'";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   155
by (blast_tac (claset() addIs [subset_imp_leadsETo, leadsETo_Trans]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   156
qed "leadsETo_weaken_R";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   157
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   158
Goal "[| F : A leadsTo[CC] A'; B<=A;  {}:CC |] ==> F : B leadsTo[CC] A'";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   159
by (blast_tac (claset() addIs [leadsETo_Trans, subset_imp_leadsETo]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   160
qed_spec_mp "leadsETo_weaken_L";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   161
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   162
(*Distributes over binary unions*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   163
Goal "{} : CC ==> \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   164
\ F : (A Un B) leadsTo[CC] C  =  (F : A leadsTo[CC] C & F : B leadsTo[CC] C)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   165
by (blast_tac (claset() addIs [leadsETo_Un, leadsETo_weaken_L]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   166
qed "leadsETo_Un_distrib";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   167
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   168
Goal "{} : CC ==> \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   169
\   F : (UN i:I. A i) leadsTo[CC] B  =  (ALL i : I. F : (A i) leadsTo[CC] B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   170
by (blast_tac (claset() addIs [leadsETo_UN, leadsETo_weaken_L]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   171
qed "leadsETo_UN_distrib";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   172
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   173
Goal "{} : CC \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   174
\     ==> F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   175
by (blast_tac (claset() addIs [leadsETo_Union, leadsETo_weaken_L]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   176
qed "leadsETo_Union_distrib";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   177
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   178
Goal "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC;  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   179
\     ==> F : B leadsTo[CC] B'";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   180
by (dtac (impOfSubs leadsETo_mono) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   181
by (assume_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   182
by (blast_tac (claset() addIs [leadsETo_weaken_R, leadsETo_weaken_L,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   183
			       leadsETo_Trans]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   184
qed "leadsETo_weaken";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   185
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   186
Goal "[| F : A leadsTo[CC] A';  CC <= givenBy v |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   187
\     ==> F : A leadsTo[givenBy v] A'";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   188
by (blast_tac (claset() addIs [empty_mem_givenBy, leadsETo_weaken]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   189
qed "leadsETo_givenBy";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   190
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   191
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   192
(*Set difference*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   193
Goal "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C;  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   194
\     ==> F : A leadsTo[CC] C";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   195
by (blast_tac (claset() addIs [leadsETo_Un, leadsETo_weaken]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   196
qed "leadsETo_Diff";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   197
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   198
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   199
(** Meta or object quantifier ???
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   200
    see ball_constrains_UN in UNITY.ML***)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   201
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   202
val prems = goal thy
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   203
   "[| !! i. i:I ==> F : (A i) leadsTo[CC] (A' i);  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   204
\   ==> F : (UN i:I. A i) leadsTo[CC] (UN i:I. A' i)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   205
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   206
by (blast_tac (claset() addIs [leadsETo_Union, leadsETo_weaken_R] 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   207
                        addIs prems) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   208
qed "leadsETo_UN_UN";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   209
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   210
(*Binary union version*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   211
Goal "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B';  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   212
\     ==> F : (A Un B) leadsTo[CC] (A' Un B')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   213
by (blast_tac (claset() addIs [leadsETo_Un, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   214
			       leadsETo_weaken_R]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   215
qed "leadsETo_Un_Un";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   216
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   217
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   218
(** The cancellation law **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   219
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   220
Goal "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B';  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   221
\     ==> F : A leadsTo[CC] (A' Un B')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   222
by (blast_tac (claset() addIs [leadsETo_Un_Un, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   223
			       subset_imp_leadsETo, leadsETo_Trans]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   224
qed "leadsETo_cancel2";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   225
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   226
Goal "[| F : A leadsTo[CC] (A' Un B); F : (B-A') leadsTo[CC] B';  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   227
\     ==> F : A leadsTo[CC] (A' Un B')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   228
by (rtac leadsETo_cancel2 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   229
by (assume_tac 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   230
by (ALLGOALS Asm_simp_tac);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   231
qed "leadsETo_cancel_Diff2";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   232
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   233
Goal "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B';  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   234
\   ==> F : A leadsTo[CC] (B' Un A')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   235
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   236
by (blast_tac (claset() addSIs [leadsETo_cancel2]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   237
qed "leadsETo_cancel1";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   238
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   239
Goal "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B';  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   240
\   ==> F : A leadsTo[CC] (B' Un A')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   241
by (rtac leadsETo_cancel1 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   242
by (assume_tac 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   243
by (ALLGOALS Asm_simp_tac);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   244
qed "leadsETo_cancel_Diff1";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   245
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   246
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   247
(** The impossibility law **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   248
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   249
Goal "F : A leadsTo[CC] B ==> B={} --> A={}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   250
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   251
by (ALLGOALS Asm_simp_tac);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   252
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   253
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   254
val lemma = result() RS mp;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   255
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   256
Goal "F : A leadsTo[CC] {} ==> A={}";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   257
by (blast_tac (claset() addSIs [lemma]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   258
qed "leadsETo_empty";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   259
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   260
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   261
(** PSP: Progress-Safety-Progress **)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   262
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   263
(*Special case of PSP: Misra's "stable conjunction"*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   264
Goalw [stable_def]
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   265
   "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   266
\   ==> F : (A Int B) leadsTo[CC] (A' Int B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   267
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   268
by (blast_tac (claset() addIs [leadsETo_Union_Int]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   269
by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   270
by (rtac leadsETo_Basis 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   271
by (asm_full_simp_tac
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   272
    (simpset() addsimps [ensures_def, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   273
			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   274
by (asm_simp_tac (simpset() addsimps [Diff_Int_distrib2 RS sym]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   275
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   276
qed "e_psp_stable";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   277
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   278
Goal "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   279
\     ==> F : (B Int A) leadsTo[CC] (B Int A')";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   280
by (asm_simp_tac (simpset() addsimps e_psp_stable::Int_ac) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   281
qed "e_psp_stable2";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   282
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   283
Goal "[| F : A leadsTo[CC] A'; F : B co B';  \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   284
\        ALL C:CC. C Int B Int B' : CC;  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   285
\     ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   286
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   287
by (blast_tac (claset() addIs [leadsETo_Union_Int]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   288
(*Transitivity case has a delicate argument involving "cancellation"*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   289
by (rtac leadsETo_Un_duplicate2 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   290
by (etac leadsETo_cancel_Diff1 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   291
by (assume_tac 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   292
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   293
by (blast_tac (claset() addIs [leadsETo_weaken_L] 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   294
                        addDs [constrains_imp_subset]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   295
(*Basis case*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   296
by (rtac leadsETo_Basis 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   297
by (blast_tac (claset() addIs [psp_ensures]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   298
by (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'" 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   299
by Auto_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   300
qed "e_psp";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   301
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   302
Goal "[| F : A leadsTo[CC] A'; F : B co B';  \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   303
\        ALL C:CC. C Int B Int B' : CC;  {}:CC |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   304
\     ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   305
by (asm_full_simp_tac (simpset() addsimps e_psp::Int_ac) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   306
qed "e_psp2";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   307
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   308
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   309
(*** Special properties involving the parameter [CC] ***)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   310
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   311
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   312
Goal "[| F: (A leadsTo[givenBy v] B);  G : preserves v;  \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   313
\        F Join G : stable C |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   314
\     ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   315
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   316
by (stac Int_Union 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   317
by (blast_tac (claset() addIs [leadsETo_UN]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   318
by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   319
			       leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   320
by (rtac leadsETo_Basis 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   321
by (auto_tac (claset(),
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   322
	      simpset() addsimps [Int_Diff, ensures_def,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   323
				  givenBy_eq_Collect, Join_stable,
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   324
				  Join_constrains, Join_transient]));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   325
by (blast_tac (claset() addIs [transient_strengthen]) 3);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   326
by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   327
by (rewtac stable_def);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   328
by (blast_tac (claset() addSEs [equalityE]
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   329
			addIs [constrains_Int RS constrains_weaken]) 2);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   330
by (blast_tac (claset() addSEs [equalityE]
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   331
			addIs [constrains_Int RS constrains_weaken]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   332
qed "gen_leadsETo_imp_Join_leadsETo";
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   333
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   334
(*useful??*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   335
Goal "[| F Join G : (A leadsTo[CC] B);  ALL C:CC. G : stable C |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   336
\     ==> F: (A leadsTo[CC] B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   337
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   338
by (blast_tac (claset() addIs [leadsETo_Union]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   339
by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   340
by (rtac leadsETo_Basis 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   341
by (case_tac "A <= B" 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   342
by (etac subset_imp_ensures 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   343
by (auto_tac (claset() addIs [constrains_weaken],
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   344
	      simpset() addsimps [stable_def, ensures_def, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   345
				  Join_constrains, Join_transient]));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   346
by (REPEAT (thin_tac "?F : ?A co ?B" 1));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   347
by (etac transientE 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   348
by (rewtac constrains_def);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   349
by (blast_tac (claset() addSDs [bspec]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   350
qed "Join_leadsETo_stable_imp_leadsETo";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   351
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   352
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   353
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   354
(**** EXTEND/PROJECT PROPERTIES ****)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   355
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   356
Open_locale "Extend";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   357
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   358
(*Here h and f are locale constants*)
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   359
Goal "extend_set h `` (givenBy v) <= (givenBy (v o f))";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   360
by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   361
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   362
qed "extend_set_givenBy_subset";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   363
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   364
Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   365
by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   366
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   367
qed "extend_set_givenBy_I";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   368
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   369
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   370
Goal "F : A leadsTo[CC] B \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   371
\     ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   372
\                      (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   373
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   374
by (asm_simp_tac (simpset() addsimps [leadsETo_UN, extend_set_Union]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   375
by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   376
by (asm_simp_tac (simpset() addsimps [leadsETo_Basis, extend_ensures,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   377
				      extend_set_Diff_distrib RS sym]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   378
qed "leadsETo_imp_extend_leadsETo";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   379
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   380
(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   381
Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   382
by (auto_tac (claset() addIs [project_set_I], 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   383
	      simpset()));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   384
qed "Int_extend_set_lemma";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   385
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   386
(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   387
Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   388
by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   389
				       project_act_def, project_set_def]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   390
by (Blast_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   391
qed "project_constrains_project_set";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   392
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   393
(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   394
Goal "G : stable C ==> project h C G : stable (project_set h C)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   395
by (asm_full_simp_tac (simpset() addsimps [stable_def, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   396
					   project_constrains_project_set]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   397
qed "project_stable_project_set";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   398
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   399
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   400
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   401
(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   402
Goal "[| G : preserves (v o f);  project h C G : transient D;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   403
\        D : givenBy v |] ==> D={}";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   404
by (rtac stable_transient_empty 1);
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   405
by (assume_tac 2);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   406
(*If addIs then PROOF FAILED at depth 2*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   407
by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   408
				project_preserves_I]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   409
result();
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   410
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   411
(*Generalizes the version proved in Project.ML*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   412
Goal "[| G : preserves (v o f);  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   413
\        project h C G : transient (C' Int D);  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   414
\        project h C G : stable C';  D : givenBy v |]    \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   415
\     ==> C' Int D = {}";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   416
by (rtac stable_transient_empty 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   417
by (assume_tac 2);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   418
(*If addIs then PROOF FAILED at depth 3*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   419
by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   420
				project_preserves_I]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   421
qed "preserves_o_project_transient_empty";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   422
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   423
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   424
(*This version's stronger in the "ensures" precondition
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   425
  BUT there's no ensures_weaken_L*)
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   426
Goal "[| project h C G ~: transient (project_set h C Int (A-B)) | \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   427
\          project_set h C Int (A - B) = {};  \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   428
\        extend h F Join G : stable C;  \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   429
\        F Join project h C G : (project_set h C Int A) ensures B |] \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   430
\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   431
by (stac (Int_extend_set_lemma RS sym) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   432
by (rtac Join_project_ensures 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   433
by (auto_tac (claset(), simpset() addsimps [Int_Diff]));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   434
qed "Join_project_ensures_strong";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   435
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   436
Goal "[| extend h F Join G : stable C;  \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   437
\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   438
\        G : preserves (v o f) |] \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   439
\     ==> extend h F Join G : \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   440
\           (C Int extend_set h (project_set h C Int A)) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   441
\           leadsTo[(%D. C Int extend_set h D)``givenBy v]  (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   442
by (etac leadsETo_induct 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   443
by (asm_simp_tac (simpset() delsimps UN_simps
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   444
		  addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   445
by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   446
			       leadsETo_Trans]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   447
by (Clarify_tac 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   448
by (rtac leadsETo_Basis 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   449
by (etac rev_image_eqI 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   450
by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   451
				      extend_set_Diff_distrib RS sym]) 2);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   452
by (rtac Join_project_ensures_strong 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   453
by (auto_tac (claset() addDs [preserves_o_project_transient_empty]
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   454
		       addIs [project_stable_project_set], 
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   455
	      simpset() addsimps [Int_left_absorb, Join_stable]));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   456
by (asm_simp_tac
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   457
    (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   458
			 Int_lower2, project_stable_project_set,
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   459
			 Join_stable, extend_stable_project_set]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   460
val lemma = result();
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   461
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   462
Goal "[| extend h F Join G : stable C;  \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   463
\        F Join project h C G : \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   464
\            (project_set h C Int A) \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   465
\            leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   466
\        G : preserves (v o f) |] \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   467
\     ==> extend h F Join G : (C Int extend_set h A) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   468
\           leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   469
by (rtac (lemma RS leadsETo_weaken) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   470
by (auto_tac (claset() addIs [project_set_I], simpset()));
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   471
qed "project_leadsETo_lemma";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   472
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   473
Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   474
\        G : preserves (v o f) |]  \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   475
\     ==> extend h F Join G : (extend_set h A) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   476
\           leadsTo[givenBy (v o f)] (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   477
by (rtac (make_elim project_leadsETo_lemma) 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   478
by (stac stable_UNIV 1);
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   479
by Auto_tac;
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   480
by (etac leadsETo_givenBy 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   481
by (rtac extend_set_givenBy_subset 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   482
qed "project_leadsETo_D";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   483
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   484
Goal "[| F Join project h (reachable (extend h F Join G)) G \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   485
\            : A LeadsTo[givenBy v] B;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   486
\        G : preserves (v o f) |] \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   487
\     ==> extend h F Join G : \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   488
\           (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   489
by (rtac (make_elim (subset_refl RS stable_reachable RS 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   490
		     project_leadsETo_lemma)) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   491
by (auto_tac (claset(), 
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   492
	      simpset() addsimps [LeadsETo_def]));
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   493
by (asm_full_simp_tac 
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   494
    (simpset() addsimps [project_set_reachable_extend_eq RS sym]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   495
by (etac (impOfSubs leadsETo_mono) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   496
by (blast_tac (claset() addIs [extend_set_givenBy_I]) 1);
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   497
qed "project_LeadsETo_D";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   498
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   499
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   500
     "extending (v o f) (%G. UNIV) h F \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   501
\               (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   502
\               (A leadsTo[givenBy v] B)";
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   503
by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   504
qed "extending_leadsETo";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   505
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   506
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   507
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   508
     "extending (v o f) (%G. reachable (extend h F Join G)) h F \
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   509
\               (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   510
\               (A LeadsTo[givenBy v]  B)";
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8044
diff changeset
   511
by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
8044
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   512
qed "extending_LeadsETo";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   513
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   514
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   515
Close_locale "Extend";
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   516
296b03b79505 new generalized leads-to theory
paulson
parents:
diff changeset
   517