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