Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: SemilatAlg.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/DFA/SemilatAlg.thy
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

section \<open>More on Semilattices\<close>

theory SemilatAlg
imports Typing_Framework Product
begin

definition lesubstep_type :: "(nat \ 's) list \ 's ord \ (nat \ 's) list \ bool"
                    ("(_ /\|_| _)" [50, 0, 51] 50) where
  "x \|r| y \ \(p,s) \ set x. \s'. (p,s') \ set y \ s <=_r s'"

primrec plusplussub :: "'a list \ ('a \ 'a \ 'a) \ 'a \ 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) where
  "[] ++_f y = y"
| "(x#xs) ++_f y = xs ++_f (x +_f y)"

definition bounded :: "'s step_type \ nat \ bool" where
"bounded step n == \ps. \(q,t)\set(step p s). q

definition pres_type :: "'s step_type \ nat \ 's set \ bool" where
"pres_type step n A == \s\A. \p(q,s')\set (step p s). s' \ A"

definition mono :: "'s ord \ 's step_type \ nat \ 's set \ bool" where
"mono r step n A ==
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s \<le>|r| step p t"

lemma pres_typeD:
  "\ pres_type step n A; s\A; pset (step p s) \ \ s' \ A"
  by (unfold pres_type_def, blast)

lemma monoD:
  "\ mono r step n A; p < n; s\A; s <=_r t \ \ step p s \|r| step p t"
  by (unfold mono_def, blast)

lemma boundedD:
  "\ bounded step n; p < n; (q,t) \ set (step p xs) \ \ q < n"
  by (unfold bounded_def, blast)

lemma lesubstep_type_refl [simp, intro]:
  "(\x. x <=_r x) \ x \|r| x"
  by (unfold lesubstep_type_def) auto

lemma lesub_step_typeD:
  "a \|r| b \ (x,y) \ set a \ \y'. (x, y') \ set b \ y <=_r y'"
  by (unfold lesubstep_type_def) blast

lemma list_update_le_listI [rule_format]:
  "set xs <= A \ set ys <= A \ xs <=[r] ys \ p < size xs \
   x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
   xs[p := x +_f xs!p] <=[r] ys"
  apply (unfold Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done

lemma plusplus_closed: assumes "semilat (A, r, f)" shows
  "\y. \ set x \ A; y \ A\ \ x ++_f y \ A" (is "PROP ?P")
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)
  show "PROP ?P" proof (induct x)
    show "\y. y \ A \ [] ++_f y \ A" by simp
    fix y x xs
    assume y: "y \ A" and xs: "set (x#xs) \ A"
    assume IH: "\y. \ set xs \ A; y \ A\ \ xs ++_f y \ A"
    from xs obtain x: "x \ A" and xs': "set xs \ A" by simp
    from x y have "(x +_f y) \ A" ..
    with xs' have "xs ++_f (x +_f y) \ A" by (rule IH)
    thus "(x#xs) ++_f y \ A" by simp
  qed
qed

lemma (in Semilat) pp_ub2:
"\y. \ set x \ A; y \ A\ \ y <=_r x ++_f y"
proof (induct x)
  from semilat show "\y. y <=_r [] ++_f y" by simp

  fix y a l
  assume y:  "y \ A"
  assume "set (a#l) \ A"
  then obtain a: "a \ A" and x: "set l \ A" by simp
  assume "\y. \set l \ A; y \ A\ \ y <=_r l ++_f y"
  hence IH: "\y. y \ A \ y <=_r l ++_f y" using x .

  from a y have "y <=_r a +_f y" ..
  also from a y have "a +_f y \ A" ..
  hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
  finally have "y <=_r l ++_f (a +_f y)" .
  thus "y <=_r (a#l) ++_f y" by simp
qed

lemma (in Semilat) pp_ub1:
shows "\y. \set ls \ A; y \ A; x \ set ls\ \ x <=_r ls ++_f y"
proof (induct ls)
  show "\y. x \ set [] \ x <=_r [] ++_f y" by simp

  fix y s ls
  assume "set (s#ls) \ A"
  then obtain s: "s \ A" and ls: "set ls \ A" by simp
  assume y: "y \ A"

  assume
    "\y. \set ls \ A; y \ A; x \ set ls\ \ x <=_r ls ++_f y"
  hence IH: "\y. x \ set ls \ y \ A \ x <=_r ls ++_f y" using ls .

  assume "x \ set (s#ls)"
  then obtain xls: "x = s \ x \ set ls" by simp
  moreover {
    assume xs: "x = s"
    from s y have "s <=_r s +_f y" ..
    also from s y have "s +_f y \ A" ..
    with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
    finally have "s <=_r ls ++_f (s +_f y)" .
    with xs have "x <=_r ls ++_f (s +_f y)" by simp
  }
  moreover {
    assume "x \ set ls"
    hence "\y. y \ A \ x <=_r ls ++_f y" by (rule IH)
    moreover from s y have "s +_f y \ A" ..
    ultimately have "x <=_r ls ++_f (s +_f y)" .
  }
  ultimately
  have "x <=_r ls ++_f (s +_f y)" by blast
  thus "x <=_r (s#ls) ++_f y" by simp
qed

lemma (in Semilat) pp_lub:
  assumes z: "z \ A"
  shows
  "\y. y \ A \ set xs \ A \ \x \ set xs. x <=_r z \ y <=_r z \ xs ++_f y <=_r z"
proof (induct xs)
  fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp
next
  fix y l ls assume y: "y \ A" and "set (l#ls) \ A"
  then obtain l: "l \ A" and ls: "set ls \ A" by auto
  assume "\x \ set (l#ls). x <=_r z"
  then obtain lz: "l <=_r z" and lsz: "\x \ set ls. x <=_r z" by auto
  assume "y <=_r z" with lz have "l +_f y <=_r z" using l y z ..
  moreover
  from l y have "l +_f y \ A" ..
  moreover
  assume "\y. y \ A \ set ls \ A \ \x \ set ls. x <=_r z \ y <=_r z
          \<Longrightarrow> ls ++_f y <=_r z"
  ultimately
  have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
  thus "(l#ls) ++_f y <=_r z" by simp
qed

lemma ub1':
  assumes "semilat (A, r, f)"
  shows "\\(p,s) \ set S. s \ A; y \ A; (a,b) \ set S\
  \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
proof -
  interpret Semilat A r f using assms by (rule Semilat.intro)

  let "b <=_r ?map ++_f y" = ?thesis

  assume "y \ A"
  moreover
  assume "\(p,s) \ set S. s \ A"
  hence "set ?map \ A" by auto
  moreover
  assume "(a,b) \ set S"
  hence "b \ set ?map" by (induct S, auto)
  ultimately
  show ?thesis by - (rule pp_ub1)
qed


lemma plusplus_empty:
  "\s'. (q, s') \ set S \ s' +_f ss ! q = ss ! q \
   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
  by (induct S) auto

end

¤ Dauer der Verarbeitung: 0.1 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.