src/HOL/UNITY/Reach.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5253 82a5ca6290aa
child 5424 771a68a468cc
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     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 	[ this example took only four days!]
     8 *)
     9 
    10 (*TO SIMPDATA.ML??  FOR CLASET??  *)
    11 val major::prems = goal thy 
    12     "[| if P then Q else R;    \
    13 \       [| P;   Q |] ==> S;    \
    14 \       [| ~ P; R |] ==> S |] ==> S";
    15 by (cut_facts_tac [major] 1);
    16 by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
    17 qed "ifE";
    18 
    19 AddSEs [ifE];
    20 
    21 
    22 val cmd_defs = [Rprg_def, asgt_def, fun_upd_def];
    23 
    24 Goalw [Rprg_def] "id : (Acts Rprg)";
    25 by (Simp_tac 1);
    26 qed "id_in_Acts";
    27 AddIffs [id_in_Acts];
    28 
    29 (*All vertex sets are finite*)
    30 AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
    31 
    32 Addsimps [reach_invariant_def];
    33 
    34 Goalw [Rprg_def] "Invariant Rprg reach_invariant";
    35 by (rtac InvariantI 1);
    36 by Auto_tac;  (*for the initial state; proof of stability remains*)
    37 by (constrains_tac [Rprg_def, asgt_def] 1);
    38 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    39 qed "reach_invariant";
    40 
    41 
    42 (*** Fixedpoint ***)
    43 
    44 (*If it reaches a fixedpoint, it has found a solution*)
    45 Goalw [fixedpoint_def, reach_invariant_def]
    46     "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
    47 by (rtac equalityI 1);
    48 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
    49 by (auto_tac (claset() addSIs [ext], simpset()));
    50 by (etac rtrancl_induct 1);
    51 by Auto_tac;
    52 qed "fixedpoint_invariant_correct";
    53 
    54 Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
    55     "FP (Acts Rprg) <= fixedpoint";
    56 by Auto_tac;
    57 by (dtac bspec 1); 
    58 by (Blast_tac 1);
    59 by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
    60 by (dtac fun_cong 1);
    61 by Auto_tac;
    62 val lemma1 = result();
    63 
    64 Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
    65     "fixedpoint <= FP (Acts Rprg)";
    66 by (auto_tac (claset() addIs [ext], simpset()));
    67 val lemma2 = result();
    68 
    69 Goal "FP (Acts Rprg) = fixedpoint";
    70 by (rtac ([lemma1,lemma2] MRS equalityI) 1);
    71 qed "FP_fixedpoint";
    72 
    73 
    74 (*If we haven't reached a fixedpoint then there is some edge for which u but
    75   not v holds.  Progress will be proved via an ENSURES assertion that the
    76   metric will decrease for each suitable edge.  A union over all edges proves
    77   a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
    78   *)
    79 
    80 Goal "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
    81 by (simp_tac (simpset() addsimps
    82 	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
    83 		Rprg_def, asgt_def])) 1);
    84 by Safe_tac;
    85 by (rtac fun_upd_idem 1);
    86 by (Blast_tac 1);
    87 by (Full_simp_tac 1);
    88 by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
    89 by (dtac subsetD 1);
    90 by (Simp_tac 1);
    91 by (asm_full_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
    92 qed "Compl_fixedpoint";
    93 
    94 Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
    95 by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
    96 by (Blast_tac 1);
    97 qed "Diff_fixedpoint";
    98 
    99 
   100 (*** Progress ***)
   101 
   102 Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
   103 by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
   104 by Auto_tac;
   105 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
   106 qed "Suc_metric";
   107 
   108 Goal "~ s x ==> metric (s(x:=True)) < metric s";
   109 by (etac (Suc_metric RS subst) 1);
   110 by (Blast_tac 1);
   111 qed "metric_less";
   112 AddSIs [metric_less];
   113 
   114 Goal "metric (s(y:=s x | s y)) <= metric s";
   115 by (case_tac "s x --> s y" 1);
   116 by (auto_tac (claset() addIs [less_imp_le],
   117 	      simpset() addsimps [fun_upd_idem]));
   118 qed "metric_le";
   119 
   120 Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
   121 by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
   122 by (rtac LeadsTo_UN 1);
   123 by Auto_tac;
   124 by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
   125 by (cut_facts_tac [metric_le RS le_imp_less_or_eq] 1);
   126 by (Fast_tac 1);
   127 qed "LeadsTo_Diff_fixedpoint";
   128 
   129 Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
   130 by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
   131 by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
   132 qed "LeadsTo_Un_fixedpoint";
   133 
   134 
   135 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
   136 Goal "LeadsTo Rprg UNIV fixedpoint";
   137 by (rtac LessThan_induct 1);
   138 by Auto_tac;
   139 by (rtac LeadsTo_Un_fixedpoint 1);
   140 qed "LeadsTo_fixedpoint";
   141 
   142 Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
   143 by (stac (fixedpoint_invariant_correct RS sym) 1);
   144 by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
   145 	  MRS Invariant_LeadsTo_weaken) 1); 
   146 by Auto_tac;
   147 qed "LeadsTo_correct";