src/HOL/UNITY/Reach.ML
changeset 4776 1f9362e769c1
child 4896 4727272f3db6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Reach.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,188 @@
     1.4 +(*  Title:      HOL/UNITY/Reach.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
    1.10 +*)
    1.11 +
    1.12 +open Reach;
    1.13 +
    1.14 +(*TO SIMPDATA.ML??  FOR CLASET??  *)
    1.15 +val major::prems = goal thy 
    1.16 +    "[| if P then Q else R;    \
    1.17 +\       [| P;   Q |] ==> S;    \
    1.18 +\       [| ~ P; R |] ==> S |] ==> S";
    1.19 +by (cut_facts_tac [major] 1);
    1.20 +by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
    1.21 +qed "ifE";
    1.22 +
    1.23 +AddSEs [ifE];
    1.24 +
    1.25 +
    1.26 +val cmd_defs = [racts_def, asgt_def, update_def];
    1.27 +
    1.28 +goalw thy [racts_def] "id : racts";
    1.29 +by (Simp_tac 1);
    1.30 +qed "id_in_racts";
    1.31 +AddIffs [id_in_racts];
    1.32 +
    1.33 +(*All vertex sets are finite*)
    1.34 +AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
    1.35 +
    1.36 +
    1.37 +(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
    1.38 +
    1.39 +(*proves "constrains" properties when the program is specified*)
    1.40 +val constrains_tac = 
    1.41 +   SELECT_GOAL
    1.42 +      (EVERY [rtac constrainsI 1,
    1.43 +	      rewtac racts_def,
    1.44 +	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
    1.45 +	      rewrite_goals_tac [racts_def, asgt_def],
    1.46 +	      ALLGOALS (SELECT_GOAL Auto_tac)]);
    1.47 +
    1.48 +
    1.49 +(*proves "ensures" properties when the program is specified*)
    1.50 +fun ensures_tac sact = 
    1.51 +    SELECT_GOAL
    1.52 +      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
    1.53 +	      res_inst_tac [("act", sact)] transient_mem 2,
    1.54 +	      Simp_tac 2,
    1.55 +	      constrains_tac 1,
    1.56 +	      rewrite_goals_tac [racts_def, asgt_def],
    1.57 +	      Auto_tac]);
    1.58 +
    1.59 +
    1.60 +goalw thy [stable_def, invariant_def]
    1.61 +    "stable racts invariant";
    1.62 +by (constrains_tac 1);
    1.63 +by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    1.64 +qed "stable_invariant";
    1.65 +
    1.66 +goalw thy [rinit_def, invariant_def] "rinit <= invariant";
    1.67 +by Auto_tac;
    1.68 +qed "rinit_invariant";
    1.69 +
    1.70 +goal thy "reachable rinit racts <= invariant";
    1.71 +by (simp_tac (simpset() addsimps
    1.72 +	      [strongest_invariant, stable_invariant, rinit_invariant]) 1); 
    1.73 +qed "reachable_subset_invariant";
    1.74 +
    1.75 +val reachable_subset_invariant' = 
    1.76 +    rewrite_rule [invariant_def] reachable_subset_invariant;
    1.77 +
    1.78 +
    1.79 +(*** Fixedpoint ***)
    1.80 +
    1.81 +(*If it reaches a fixedpoint, it has found a solution*)
    1.82 +goalw thy [fixedpoint_def, invariant_def]
    1.83 +    "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
    1.84 +by (rtac equalityI 1);
    1.85 +by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
    1.86 +by (auto_tac (claset() addSIs [ext], simpset()));
    1.87 +by (etac rtrancl_induct 1);
    1.88 +by Auto_tac;
    1.89 +qed "fixedpoint_invariant_correct";
    1.90 +
    1.91 +goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
    1.92 +    "FP racts <= fixedpoint";
    1.93 +by Auto_tac;
    1.94 +by (dtac bspec 1); 
    1.95 +by (Blast_tac 1);
    1.96 +by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
    1.97 +by (dtac fun_cong 1);
    1.98 +by Auto_tac;
    1.99 +val lemma1 = result();
   1.100 +
   1.101 +goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
   1.102 +    "fixedpoint <= FP racts";
   1.103 +by (auto_tac (claset() addIs [ext], simpset()));
   1.104 +val lemma2 = result();
   1.105 +
   1.106 +goal thy "FP racts = fixedpoint";
   1.107 +by (rtac ([lemma1,lemma2] MRS equalityI) 1);
   1.108 +qed "FP_fixedpoint";
   1.109 +
   1.110 +
   1.111 +(*If we haven't reached a fixedpoint then there is some edge for which u but
   1.112 +  not v holds.  Progress will be proved via an ENSURES assertion that the
   1.113 +  metric will decrease for each suitable edge.  A union over all edges proves
   1.114 +  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
   1.115 +  *)
   1.116 +
   1.117 +goal thy "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
   1.118 +by (simp_tac (simpset() addsimps
   1.119 +	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
   1.120 +		racts_def, asgt_def])) 1);
   1.121 +by Safe_tac;
   1.122 +by (rtac update_idem 1);
   1.123 +by (Blast_tac 1);
   1.124 +by (Full_simp_tac 1);
   1.125 +by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
   1.126 +by (dtac subsetD 1);
   1.127 +by (Simp_tac 1);
   1.128 +by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
   1.129 +qed "Compl_fixedpoint";
   1.130 +
   1.131 +goal thy "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
   1.132 +by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
   1.133 +by (Blast_tac 1);
   1.134 +qed "Diff_fixedpoint";
   1.135 +
   1.136 +
   1.137 +(*** Progress ***)
   1.138 +
   1.139 +goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
   1.140 +by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
   1.141 +by Auto_tac;
   1.142 +by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
   1.143 +qed "Suc_metric";
   1.144 +
   1.145 +goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
   1.146 +by (etac (Suc_metric RS subst) 1);
   1.147 +by (Blast_tac 1);
   1.148 +qed "metric_less";
   1.149 +AddSIs [metric_less];
   1.150 +
   1.151 +goal thy "metric (s[y|->s x | s y]) <= metric s";
   1.152 +by (case_tac "s x --> s y" 1);
   1.153 +by (auto_tac (claset() addIs [less_imp_le],
   1.154 +	      simpset() addsimps [update_idem]));
   1.155 +qed "metric_le";
   1.156 +
   1.157 +goal thy "!!m. (u,v): edges ==> \
   1.158 +\              ensures racts ((metric-``{m}) Int {s. s u & ~ s v})  \
   1.159 +\                            (metric-``(lessThan m))";
   1.160 +by (ensures_tac "asgt u v" 1);
   1.161 +by (cut_facts_tac [metric_le] 1);
   1.162 +by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
   1.163 +qed "edges_ensures";
   1.164 +
   1.165 +goal thy "leadsTo racts ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
   1.166 +by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
   1.167 +by (rtac leadsTo_UN 1);
   1.168 +by (split_all_tac 1);
   1.169 +by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
   1.170 +qed "leadsTo_Diff_fixedpoint";
   1.171 +
   1.172 +goal thy "leadsTo racts (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
   1.173 +by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
   1.174 +by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
   1.175 +qed "leadsTo_Un_fixedpoint";
   1.176 +
   1.177 +
   1.178 +(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
   1.179 +goal thy "leadsTo racts UNIV fixedpoint";
   1.180 +by (rtac lessThan_induct 1);
   1.181 +by Auto_tac;
   1.182 +by (rtac leadsTo_Un_fixedpoint 1);
   1.183 +qed "leadsTo_fixedpoint";
   1.184 +
   1.185 +goal thy "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
   1.186 +by (stac (fixedpoint_invariant_correct RS sym) 1);
   1.187 +by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); 
   1.188 +by (cut_facts_tac [reachable_subset_invariant] 1);
   1.189 +by (Blast_tac 1);
   1.190 +qed "LeadsTo_correct";
   1.191 +