src/HOL/UNITY/Simple/Reach.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18556 dc39832e9280
child 24853 aab5798e5a33
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
paulson@11195
     1
(*  Title:      HOL/UNITY/Reach.thy
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1998  University of Cambridge
paulson@11195
     5
paulson@11195
     6
Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
paulson@13785
     7
	[this example took only four days!]
paulson@11195
     8
*)
paulson@11195
     9
paulson@18556
    10
theory Reach imports "../UNITY_Main" begin
paulson@11195
    11
paulson@13785
    12
typedecl vertex
paulson@11195
    13
paulson@13785
    14
types    state = "vertex=>bool"
paulson@11195
    15
paulson@11195
    16
consts
paulson@11195
    17
  init ::  "vertex"
paulson@11195
    18
paulson@11195
    19
  edges :: "(vertex*vertex) set"
paulson@11195
    20
paulson@11195
    21
constdefs
paulson@11195
    22
paulson@11195
    23
  asgt  :: "[vertex,vertex] => (state*state) set"
paulson@11195
    24
    "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
paulson@11195
    25
paulson@13785
    26
  Rprg :: "state program"
paulson@13812
    27
    "Rprg == mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
paulson@11195
    28
paulson@13785
    29
  reach_invariant :: "state set"
paulson@13806
    30
    "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
paulson@11195
    31
paulson@13785
    32
  fixedpoint :: "state set"
paulson@13806
    33
    "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
paulson@11195
    34
paulson@13785
    35
  metric :: "state => nat"
paulson@11195
    36
    "metric s == card {v. ~ s v}"
paulson@11195
    37
paulson@13785
    38
paulson@13785
    39
text{**We assume that the set of vertices is finite*}
paulson@13785
    40
axioms 
paulson@13785
    41
  finite_graph:  "finite (UNIV :: vertex set)"
paulson@13785
    42
  
paulson@13785
    43
paulson@13785
    44
paulson@13785
    45
paulson@13785
    46
(*TO SIMPDATA.ML??  FOR CLASET??  *)
paulson@13785
    47
lemma ifE [elim!]:
paulson@13785
    48
    "[| if P then Q else R;     
paulson@13785
    49
        [| P;   Q |] ==> S;     
paulson@13785
    50
        [| ~ P; R |] ==> S |] ==> S"
paulson@13785
    51
by (simp split: split_if_asm) 
paulson@13785
    52
paulson@13785
    53
paulson@13785
    54
declare Rprg_def [THEN def_prg_Init, simp]
paulson@13785
    55
paulson@13785
    56
declare asgt_def [THEN def_act_simp,simp]
paulson@13785
    57
paulson@14150
    58
text{*All vertex sets are finite*}
paulson@13785
    59
declare finite_subset [OF subset_UNIV finite_graph, iff]
paulson@13785
    60
paulson@13785
    61
declare reach_invariant_def [THEN def_set_simp, simp]
paulson@13785
    62
paulson@13806
    63
lemma reach_invariant: "Rprg \<in> Always reach_invariant"
paulson@13785
    64
apply (rule AlwaysI, force) 
paulson@16184
    65
apply (unfold Rprg_def, safety) 
paulson@13785
    66
apply (blast intro: rtrancl_trans)
paulson@13785
    67
done
paulson@13785
    68
paulson@13785
    69
paulson@13785
    70
(*** Fixedpoint ***)
paulson@13785
    71
paulson@13785
    72
(*If it reaches a fixedpoint, it has found a solution*)
paulson@13785
    73
lemma fixedpoint_invariant_correct: 
paulson@13806
    74
     "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges^* }"
paulson@13785
    75
apply (unfold fixedpoint_def)
paulson@13785
    76
apply (rule equalityI)
paulson@13785
    77
apply (auto intro!: ext)
paulson@13785
    78
apply (erule rtrancl_induct, auto)
paulson@13785
    79
done
paulson@13785
    80
paulson@13785
    81
lemma lemma1: 
paulson@13806
    82
     "FP Rprg \<subseteq> fixedpoint"
paulson@13812
    83
apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
paulson@13812
    84
apply (auto simp add: stable_def constrains_def)
paulson@13785
    85
apply (drule bspec, assumption)
paulson@13785
    86
apply (simp add: Image_singleton image_iff)
paulson@13785
    87
apply (drule fun_cong, auto)
paulson@13785
    88
done
paulson@13785
    89
paulson@13785
    90
lemma lemma2: 
paulson@13806
    91
     "fixedpoint \<subseteq> FP Rprg"
paulson@13812
    92
apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
paulson@13812
    93
apply (auto intro!: ext simp add: stable_def constrains_def)
paulson@13785
    94
done
paulson@13785
    95
paulson@13785
    96
lemma FP_fixedpoint: "FP Rprg = fixedpoint"
paulson@13785
    97
by (rule equalityI [OF lemma1 lemma2])
paulson@13785
    98
paulson@11195
    99
paulson@13785
   100
(*If we haven't reached a fixedpoint then there is some edge for which u but
paulson@13785
   101
  not v holds.  Progress will be proved via an ENSURES assertion that the
paulson@13785
   102
  metric will decrease for each suitable edge.  A union over all edges proves
paulson@13785
   103
  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
paulson@13785
   104
  *)
paulson@13785
   105
paulson@13806
   106
lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
paulson@13812
   107
apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
paulson@13812
   108
apply (auto simp add: Compl_FP UN_UN_flatten)
paulson@13785
   109
 apply (rule fun_upd_idem, force)
paulson@13785
   110
apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
paulson@13785
   111
done
paulson@13785
   112
paulson@13785
   113
lemma Diff_fixedpoint:
paulson@13806
   114
     "A - fixedpoint = (\<Union>(u,v)\<in>edges. A \<inter> {s. s u & ~ s v})"
paulson@13806
   115
by (simp add: Diff_eq Compl_fixedpoint, blast)
paulson@13785
   116
paulson@13785
   117
paulson@13785
   118
(*** Progress ***)
paulson@13785
   119
paulson@13785
   120
lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s"
paulson@13785
   121
apply (unfold metric_def)
paulson@13785
   122
apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
paulson@13785
   123
 prefer 2 apply force
paulson@13785
   124
apply (simp add: card_Suc_Diff1)
paulson@13785
   125
done
paulson@13785
   126
paulson@13785
   127
lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
paulson@13785
   128
by (erule Suc_metric [THEN subst], blast)
paulson@13785
   129
paulson@13806
   130
lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
paulson@13785
   131
apply (case_tac "s x --> s y")
paulson@13785
   132
apply (auto intro: less_imp_le simp add: fun_upd_idem)
paulson@13785
   133
done
paulson@13785
   134
paulson@13785
   135
lemma LeadsTo_Diff_fixedpoint:
paulson@13806
   136
     "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
paulson@13785
   137
apply (simp (no_asm) add: Diff_fixedpoint Rprg_def)
paulson@13785
   138
apply (rule LeadsTo_UN, auto)
paulson@13785
   139
apply (ensures_tac "asgt a b")
paulson@13785
   140
 prefer 2 apply blast
paulson@16796
   141
apply (simp (no_asm_use) add: linorder_not_less)
paulson@13785
   142
apply (drule metric_le [THEN order_antisym]) 
paulson@13785
   143
apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
paulson@13785
   144
done
paulson@13785
   145
paulson@13785
   146
lemma LeadsTo_Un_fixedpoint:
paulson@13806
   147
     "Rprg \<in> (metric-`{m}) LeadsTo (metric-`(lessThan m) \<union> fixedpoint)"
paulson@13785
   148
apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R]
paulson@13785
   149
                             subset_imp_LeadsTo], auto)
paulson@13785
   150
done
paulson@13785
   151
paulson@13785
   152
paulson@13785
   153
(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
paulson@13806
   154
lemma LeadsTo_fixedpoint: "Rprg \<in> UNIV LeadsTo fixedpoint"
paulson@13785
   155
apply (rule LessThan_induct, auto)
paulson@13785
   156
apply (rule LeadsTo_Un_fixedpoint)
paulson@13785
   157
done
paulson@13785
   158
paulson@13806
   159
lemma LeadsTo_correct: "Rprg \<in> UNIV LeadsTo { %v. (init, v) \<in> edges^* }"
paulson@13785
   160
apply (subst fixedpoint_invariant_correct [symmetric])
paulson@13785
   161
apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
paulson@13785
   162
done
paulson@13785
   163
paulson@11195
   164
end