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