Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/UNITY/Follows.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section\<open>The Follows Relation of Charpentier and Sivilotte\<close>

theory Follows
imports SubstAx ListOrder "HOL-Library.Multiset"
begin

definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
   "f Fols g == Increasing g \ Increasing f Int
                Always {s. f s \<le> g s} Int
                (\<Inter>k. {s. k \<le> g s} LeadsTo {s. k \<le> f s})"

(*Does this hold for "invariant"?*)
lemma mono_Always_o:
     "mono h ==> Always {s. f s \ g s} \ Always {s. h (f s) \ h (g s)}"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: monoD)
done

lemma mono_LeadsTo_o:
     "mono (h::'a::order => 'b::order)
      ==> (\<Inter>j. {s. j \<le> g s} LeadsTo {s. j \<le> f s}) \<subseteq>
          (\<Inter>k. {s. k \<le> h (g s)} LeadsTo {s. k \<le> h (f s)})"
apply auto
apply (rule single_LeadsTo_I)
apply (drule_tac x = "g s" in spec)
apply (erule LeadsTo_weaken)
apply (blast intro: monoD order_trans)+
done

lemma Follows_constant [iff]: "F \ (%s. c) Fols (%s. c)"
by (simp add: Follows_def)

lemma mono_Follows_o:
  assumes "mono h"
  shows "f Fols g \ (h o f) Fols (h o g)"
proof
  fix x
  assume "x \ f Fols g"
  with assms show "x \ (h \ f) Fols (h \ g)"
  by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD]
    mono_Always_o [THEN [2] rev_subsetD]
    mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
qed

lemma mono_Follows_apply:
     "mono h ==> f Fols g \ (%x. h (f x)) Fols (%x. h (g x))"
apply (drule mono_Follows_o)
apply (force simp add: o_def)
done

lemma Follows_trans:
     "[| F \ f Fols g; F \ g Fols h |] ==> F \ f Fols h"
apply (simp add: Follows_def)
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: order_trans LeadsTo_Trans)
done

subsection\<open>Destruction rules\<close>

lemma Follows_Increasing1: "F \ f Fols g ==> F \ Increasing f"
by (simp add: Follows_def)

lemma Follows_Increasing2: "F \ f Fols g ==> F \ Increasing g"
by (simp add: Follows_def)

lemma Follows_Bounded: "F \ f Fols g ==> F \ Always {s. f s \ g s}"
by (simp add: Follows_def)

lemma Follows_LeadsTo:
     "F \ f Fols g ==> F \ {s. k \ g s} LeadsTo {s. k \ f s}"
by (simp add: Follows_def)

lemma Follows_LeadsTo_pfixLe:
     "F \ f Fols g ==> F \ {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
apply (rule single_LeadsTo_I, clarify)
apply (drule_tac k="g s" in Follows_LeadsTo)
apply (erule LeadsTo_weaken)
apply blast
apply (blast intro: pfixLe_trans prefix_imp_pfixLe)
done

lemma Follows_LeadsTo_pfixGe:
     "F \ f Fols g ==> F \ {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
apply (rule single_LeadsTo_I, clarify)
apply (drule_tac k="g s" in Follows_LeadsTo)
apply (erule LeadsTo_weaken)
apply blast
apply (blast intro: pfixGe_trans prefix_imp_pfixGe)
done

lemma Always_Follows1:
     "[| F \ Always {s. f s = f' s}; F \ f Fols g |] ==> F \ f' Fols g"

apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
apply (erule_tac A = "{s. x \ f s}" and A' = "{s. x \ f s}"
       in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
done

lemma Always_Follows2:
     "[| F \ Always {s. g s = g' s}; F \ f Fols g |] ==> F \ f Fols g'"
apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
apply (erule_tac A = "{s. x \ g s}" and A' = "{s. x \ g s}"
       in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
done

subsection\<open>Union properties (with the subset ordering)\<close>

(*Can replace "Un" by any sup.  But existing max only works for linorders.*)

lemma increasing_Un:
    "[| F \ increasing f; F \ increasing g |]
     ==> F \<in> increasing (%s. (f s) \<union> (g s))"
apply (simp add: increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xb" in spec)
apply (drule_tac x = "g xb" in spec)
apply (blast dest!: bspec)
done

lemma Increasing_Un:
    "[| F \ Increasing f; F \ Increasing g |]
     ==> F \<in> Increasing (%s. (f s) \<union> (g s))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
                      stable_def constrains_def)
apply (drule_tac x = "f xb" in spec)
apply (drule_tac x = "g xb" in spec)
apply (blast dest!: bspec)
done

lemma Always_Un:
     "[| F \ Always {s. f' s \ f s}; F \ Always {s. g' s \ g s} |]
      ==> F \<in> Always {s. f' s \<union> g' s \<le> f s \<union> g s}"
by (simp add: Always_eq_includes_reachable, blast)

(*Lemma to re-use the argument that one variable increases (progress)
  while the other variable doesn't decrease (safety)*)
lemma Follows_Un_lemma:
     "[| F \ Increasing f; F \ Increasing g;
         F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s};
         \<forall>k. F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |]
      ==> F \<in> {s. k \<le> f s \<union> g s} LeadsTo {s. k \<le> f' s \<union> g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in IncreasingD)
apply (drule_tac x = "g s" in IncreasingD)
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
apply (erule Stable_Int, assumption, blast+)
done

lemma Follows_Un:
    "[| F \ f' Fols f; F \ g' Fols g |]
     ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff sup.bounded_iff, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_Un_lemma)
(*Weakening is used to exchange Un's arguments*)
apply (blast intro: Follows_Un_lemma [THEN LeadsTo_weaken])
done

subsection\<open>Multiset union properties (with the multiset ordering)\<close>

lemma increasing_union:
    "[| F \ increasing f; F \ increasing g |]
     ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (simp add: increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xb" in spec)
apply (drule_tac x = "g xb" in spec)
apply (drule bspec, assumption)
apply (blast intro: add_mono order_trans)
done

lemma Increasing_union:
    "[| F \ Increasing f; F \ Increasing g |]
     ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
                      stable_def constrains_def)
apply (drule_tac x = "f xb" in spec)
apply (drule_tac x = "g xb" in spec)
apply (drule bspec, assumption)
apply (blast intro: add_mono order_trans)
done

lemma Always_union:
     "[| F \ Always {s. f' s \ f s}; F \ Always {s. g' s \ g s} |]
      ==> F \<in> Always {s. f' s + g' s \<le> f s + (g s :: ('a::order) multiset)}"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: add_mono)
done

(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
lemma Follows_union_lemma:
     "[| F \ Increasing f; F \ Increasing g;
         F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s};
         \<forall>k::('a::order) multiset.
           F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |]
      ==> F \<in> {s. k \<le> f s + g s} LeadsTo {s. k \<le> f' s + g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in IncreasingD)
apply (drule_tac x = "g s" in IncreasingD)
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
apply (erule Stable_Int, assumption, blast)
apply (blast intro: add_mono order_trans)
done

(*The !! is there to influence to effect of permutative rewriting at the end*)
lemma Follows_union:
     "!!g g' ::'b => ('a::order) multiset.
        [| F \<in> f' Fols f;  F \<in> g' Fols g |]
        ==> F \<in> (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
apply (simp add: Follows_def)
apply (simp add: Increasing_union Always_union, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_union_lemma)
(*now exchange union's arguments*)
apply (simp add: union_commute)
apply (blast intro: Follows_union_lemma)
done

lemma Follows_sum:
     "!!f ::['c,'b] => ('a::order) multiset.
        [| \<forall>i \<in> I. F \<in> f' i Fols f i;  finite I |]
        ==> F \<in> (%s. \<Sum>i \<in> I. f' i s) Fols (%s. \<Sum>i \<in> I. f i s)"
apply (erule rev_mp)
apply (erule finite_induct, simp)
apply (simp add: Follows_union)
done

(*Currently UNUSED, but possibly of interest*)
lemma Increasing_imp_Stable_pfixGe:
     "F \ Increasing func ==> F \ Stable {s. h pfixGe (func s)}"
apply (simp add: Increasing_def Stable_def Constrains_def constrains_def)
apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD]
                    prefix_imp_pfixGe)
done

(*Currently UNUSED, but possibly of interest*)
lemma LeadsTo_le_imp_pfixGe:
     "\z. F \ {s. z \ f s} LeadsTo {s. z \ g s}
      ==> F \<in> {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in spec)
apply (erule LeadsTo_weaken)
prefer 2
apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD]
                     prefix_imp_pfixGe, blast)
done

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.