src/HOL/UNITY/Reach.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 4896 4727272f3db6
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/Reach.thy
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
open Reach;
paulson@4776
    10
paulson@4776
    11
(*TO SIMPDATA.ML??  FOR CLASET??  *)
paulson@4776
    12
val major::prems = goal thy 
paulson@4776
    13
    "[| if P then Q else R;    \
paulson@4776
    14
\       [| P;   Q |] ==> S;    \
paulson@4776
    15
\       [| ~ P; R |] ==> S |] ==> S";
paulson@4776
    16
by (cut_facts_tac [major] 1);
paulson@4776
    17
by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
paulson@4776
    18
qed "ifE";
paulson@4776
    19
paulson@4776
    20
AddSEs [ifE];
paulson@4776
    21
paulson@4776
    22
paulson@4776
    23
val cmd_defs = [racts_def, asgt_def, update_def];
paulson@4776
    24
paulson@4776
    25
goalw thy [racts_def] "id : racts";
paulson@4776
    26
by (Simp_tac 1);
paulson@4776
    27
qed "id_in_racts";
paulson@4776
    28
AddIffs [id_in_racts];
paulson@4776
    29
paulson@4776
    30
(*All vertex sets are finite*)
paulson@4776
    31
AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
paulson@4776
    32
paulson@4776
    33
paulson@4776
    34
(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
paulson@4776
    35
paulson@4776
    36
(*proves "constrains" properties when the program is specified*)
paulson@4776
    37
val constrains_tac = 
paulson@4776
    38
   SELECT_GOAL
paulson@4776
    39
      (EVERY [rtac constrainsI 1,
paulson@4776
    40
	      rewtac racts_def,
paulson@4776
    41
	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
paulson@4776
    42
	      rewrite_goals_tac [racts_def, asgt_def],
paulson@4776
    43
	      ALLGOALS (SELECT_GOAL Auto_tac)]);
paulson@4776
    44
paulson@4776
    45
paulson@4776
    46
(*proves "ensures" properties when the program is specified*)
paulson@4776
    47
fun ensures_tac sact = 
paulson@4776
    48
    SELECT_GOAL
paulson@4776
    49
      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
paulson@4776
    50
	      res_inst_tac [("act", sact)] transient_mem 2,
paulson@4776
    51
	      Simp_tac 2,
paulson@4776
    52
	      constrains_tac 1,
paulson@4776
    53
	      rewrite_goals_tac [racts_def, asgt_def],
paulson@4776
    54
	      Auto_tac]);
paulson@4776
    55
paulson@4776
    56
paulson@4776
    57
goalw thy [stable_def, invariant_def]
paulson@4776
    58
    "stable racts invariant";
paulson@4776
    59
by (constrains_tac 1);
paulson@4776
    60
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
paulson@4776
    61
qed "stable_invariant";
paulson@4776
    62
paulson@4776
    63
goalw thy [rinit_def, invariant_def] "rinit <= invariant";
paulson@4776
    64
by Auto_tac;
paulson@4776
    65
qed "rinit_invariant";
paulson@4776
    66
paulson@4776
    67
goal thy "reachable rinit racts <= invariant";
paulson@4776
    68
by (simp_tac (simpset() addsimps
paulson@4776
    69
	      [strongest_invariant, stable_invariant, rinit_invariant]) 1); 
paulson@4776
    70
qed "reachable_subset_invariant";
paulson@4776
    71
paulson@4776
    72
val reachable_subset_invariant' = 
paulson@4776
    73
    rewrite_rule [invariant_def] reachable_subset_invariant;
paulson@4776
    74
paulson@4776
    75
paulson@4776
    76
(*** Fixedpoint ***)
paulson@4776
    77
paulson@4776
    78
(*If it reaches a fixedpoint, it has found a solution*)
paulson@4776
    79
goalw thy [fixedpoint_def, invariant_def]
paulson@4776
    80
    "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
paulson@4776
    81
by (rtac equalityI 1);
paulson@4776
    82
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
paulson@4776
    83
by (auto_tac (claset() addSIs [ext], simpset()));
paulson@4776
    84
by (etac rtrancl_induct 1);
paulson@4776
    85
by Auto_tac;
paulson@4776
    86
qed "fixedpoint_invariant_correct";
paulson@4776
    87
paulson@4776
    88
goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
paulson@4776
    89
    "FP racts <= fixedpoint";
paulson@4776
    90
by Auto_tac;
paulson@4776
    91
by (dtac bspec 1); 
paulson@4776
    92
by (Blast_tac 1);
paulson@4776
    93
by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
paulson@4776
    94
by (dtac fun_cong 1);
paulson@4776
    95
by Auto_tac;
paulson@4776
    96
val lemma1 = result();
paulson@4776
    97
paulson@4776
    98
goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
paulson@4776
    99
    "fixedpoint <= FP racts";
paulson@4776
   100
by (auto_tac (claset() addIs [ext], simpset()));
paulson@4776
   101
val lemma2 = result();
paulson@4776
   102
paulson@4776
   103
goal thy "FP racts = fixedpoint";
paulson@4776
   104
by (rtac ([lemma1,lemma2] MRS equalityI) 1);
paulson@4776
   105
qed "FP_fixedpoint";
paulson@4776
   106
paulson@4776
   107
paulson@4776
   108
(*If we haven't reached a fixedpoint then there is some edge for which u but
paulson@4776
   109
  not v holds.  Progress will be proved via an ENSURES assertion that the
paulson@4776
   110
  metric will decrease for each suitable edge.  A union over all edges proves
paulson@4776
   111
  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
paulson@4776
   112
  *)
paulson@4776
   113
paulson@4776
   114
goal thy "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
paulson@4776
   115
by (simp_tac (simpset() addsimps
paulson@4776
   116
	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
paulson@4776
   117
		racts_def, asgt_def])) 1);
paulson@4776
   118
by Safe_tac;
paulson@4776
   119
by (rtac update_idem 1);
paulson@4776
   120
by (Blast_tac 1);
paulson@4776
   121
by (Full_simp_tac 1);
paulson@4776
   122
by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
paulson@4776
   123
by (dtac subsetD 1);
paulson@4776
   124
by (Simp_tac 1);
paulson@4776
   125
by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
paulson@4776
   126
qed "Compl_fixedpoint";
paulson@4776
   127
paulson@4776
   128
goal thy "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
paulson@4776
   129
by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
paulson@4776
   130
by (Blast_tac 1);
paulson@4776
   131
qed "Diff_fixedpoint";
paulson@4776
   132
paulson@4776
   133
paulson@4776
   134
(*** Progress ***)
paulson@4776
   135
paulson@4776
   136
goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
paulson@4776
   137
by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
paulson@4776
   138
by Auto_tac;
paulson@4776
   139
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
paulson@4776
   140
qed "Suc_metric";
paulson@4776
   141
paulson@4776
   142
goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
paulson@4776
   143
by (etac (Suc_metric RS subst) 1);
paulson@4776
   144
by (Blast_tac 1);
paulson@4776
   145
qed "metric_less";
paulson@4776
   146
AddSIs [metric_less];
paulson@4776
   147
paulson@4776
   148
goal thy "metric (s[y|->s x | s y]) <= metric s";
paulson@4776
   149
by (case_tac "s x --> s y" 1);
paulson@4776
   150
by (auto_tac (claset() addIs [less_imp_le],
paulson@4776
   151
	      simpset() addsimps [update_idem]));
paulson@4776
   152
qed "metric_le";
paulson@4776
   153
paulson@4776
   154
goal thy "!!m. (u,v): edges ==> \
paulson@4776
   155
\              ensures racts ((metric-``{m}) Int {s. s u & ~ s v})  \
paulson@4776
   156
\                            (metric-``(lessThan m))";
paulson@4776
   157
by (ensures_tac "asgt u v" 1);
paulson@4776
   158
by (cut_facts_tac [metric_le] 1);
paulson@4776
   159
by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
paulson@4776
   160
qed "edges_ensures";
paulson@4776
   161
paulson@4776
   162
goal thy "leadsTo racts ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
paulson@4776
   163
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
paulson@4776
   164
by (rtac leadsTo_UN 1);
paulson@4776
   165
by (split_all_tac 1);
paulson@4776
   166
by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
paulson@4776
   167
qed "leadsTo_Diff_fixedpoint";
paulson@4776
   168
paulson@4776
   169
goal thy "leadsTo racts (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
paulson@4776
   170
by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
paulson@4776
   171
by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
paulson@4776
   172
qed "leadsTo_Un_fixedpoint";
paulson@4776
   173
paulson@4776
   174
paulson@4776
   175
(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
paulson@4776
   176
goal thy "leadsTo racts UNIV fixedpoint";
paulson@4776
   177
by (rtac lessThan_induct 1);
paulson@4776
   178
by Auto_tac;
paulson@4776
   179
by (rtac leadsTo_Un_fixedpoint 1);
paulson@4776
   180
qed "leadsTo_fixedpoint";
paulson@4776
   181
paulson@4776
   182
goal thy "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
paulson@4776
   183
by (stac (fixedpoint_invariant_correct RS sym) 1);
paulson@4776
   184
by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); 
paulson@4776
   185
by (cut_facts_tac [reachable_subset_invariant] 1);
paulson@4776
   186
by (Blast_tac 1);
paulson@4776
   187
qed "LeadsTo_correct";
paulson@4776
   188