src/HOL/UNITY/Follows.ML
author paulson
Mon, 24 May 1999 15:47:06 +0200
changeset 6706 d8067e272d4f
child 6809 5b8912f7bb69
permissions -rw-r--r--
Theory of the "Follows" relation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6706
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Follows
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     2
    ID:         $Id$
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     5
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     6
The Follows relation of Charpentier and Sivilotte
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     7
*)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     8
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
     9
(*Does this hold for "invariant"?*)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    10
Goal "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    11
by (asm_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    12
by (blast_tac (claset() addIs [monoD]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    13
qed "mono_Always_o";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    14
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    15
Goalw [Follows_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    16
    "mono (h::'a::order => 'b::order) \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    17
\    ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    18
\        (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    19
by Auto_tac;
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    20
by (rtac single_LeadsTo_I 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    21
by (dres_inst_tac [("x", "g s")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    22
by (etac LeadsTo_weaken 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    23
by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    24
qed "mono_LeadsTo_o";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    25
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    26
Goalw [Follows_def] "mono h ==> f Follows g <= (h o f) Follows (h o g)";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    27
by (Clarify_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    28
by (asm_full_simp_tac
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    29
    (simpset() addsimps [impOfSubs mono_Increasing_o,
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    30
			 impOfSubs mono_Always_o,
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    31
			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    32
qed "mono_Follows_o";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    33
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    34
Goalw [Follows_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    35
     "[| F : f Follows g;  F: g Follows h |] ==> F : f Follows h";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    36
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    37
by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    38
qed "Follows_trans";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    39
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    40
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    41
(*Can replace "Un" by any sup.  But existing max only works for linorders.*)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    42
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    43
Goalw [increasing_def, stable_def, constrains_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    44
    "[| F : increasing f;  F: increasing g |] \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    45
\    ==> F : increasing (%s. (f s) Un (g s))";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    46
by Auto_tac;
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    47
by (dres_inst_tac [("x","f xa")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    48
by (dres_inst_tac [("x","g xa")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    49
by (blast_tac (claset() addSDs [bspec]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    50
qed "increasing_Un";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    51
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    52
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    53
    "[| F : Increasing f;  F: Increasing g |] \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    54
\    ==> F : Increasing (%s. (f s) Un (g s))";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    55
by Auto_tac;
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    56
by (dres_inst_tac [("x","f xa")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    57
by (dres_inst_tac [("x","g xa")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    58
by (blast_tac (claset() addSDs [bspec]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    59
qed "Increasing_Un";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    60
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    61
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    62
Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    63
\     ==> F : Always {s. f' s Un g' s <= f s Un g s}";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    64
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    65
by (Blast_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    66
qed "Always_Un";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    67
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    68
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    69
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    70
Goalw [Increasing_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    71
     "F : Increasing f ==> F : Stable {s. x <= f s}";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    72
by (Blast_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    73
qed "IncreasingD";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    74
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    75
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    76
(*Lemma to re-use the argument that one variable increases (progress)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    77
  while the other variable doesn't decrease (safety)*)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    78
Goal "[| F : Increasing f; F : Increasing g; \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    79
\        F : Increasing g'; F : Always {s. f' s <= f s};\
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    80
\        ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    81
\     ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    82
by (rtac single_LeadsTo_I 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    83
by (dres_inst_tac [("x", "f s")] IncreasingD 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    84
by (dres_inst_tac [("x", "g s")] IncreasingD 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    85
by (rtac LeadsTo_weaken 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    86
by (rtac PSP_Stable 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    87
by (eres_inst_tac [("x", "f s")] spec 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    88
by (etac Stable_Int 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    89
by (assume_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    90
by (Blast_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    91
by (Blast_tac 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    92
qed "Follows_Un_lemma";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    93
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    94
Goalw [Follows_def]
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    95
    "[| F : f' Follows f;  F: g' Follows g |] \
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    96
\    ==> F : (%s. (f' s) Un (g' s)) Follows (%s. (f s) Un (g s))";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    97
by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    98
by Auto_tac;
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
    99
by (rtac LeadsTo_Trans 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
   100
by (blast_tac (claset() addIs [Follows_Un_lemma]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
   101
(*Weakening is used to exchange Un's arguments*)
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
   102
by (blast_tac (claset() addIs [Follows_Un_lemma RS LeadsTo_weaken]) 1);
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
   103
qed "Follows_Un";
d8067e272d4f Theory of the "Follows" relation
paulson
parents:
diff changeset
   104