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