Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Increasing.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      ZF/UNITY/Increasing.thy
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    Copyright   2001  University of Cambridge

Increasing's parameters are a state function f, a domain A and an order
relation r over the domain A.
*)

section\<open>Charpentier's "Increasing" Relation\<close>

theory Increasing imports Constrains Monotonicity begin

definition
  increasing :: "[i, i, i=>i] => i" (\<open>increasing[_]'(_, _')\<close>)  where
  "increasing[A](r, f) ==
    {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) &
                (\<forall>x \<in> state. f(x):A)}"

definition
  Increasing :: "[i, i, i=>i] => i" (\<open>Increasing[_]'(_, _')\<close>)  where
  "Increasing[A](r, f) ==
    {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
                (\<forall>x \<in> state. f(x):A)}"

abbreviation (input)
  IncWrt ::  "[i=>i, i, i] => i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
  "f IncreasingWrt r/A == Increasing[A](r,f)"

(** increasing **)

lemma increasing_type: "increasing[A](r, f) \ program"
by (unfold increasing_def, blast)

lemma increasing_into_program: "F \ increasing[A](r, f) ==> F \ program"
by (unfold increasing_def, blast)

lemma increasing_imp_stable:
"[| F \ increasing[A](r, f); x \ A |] ==>F \ stable({s \ state. :r})"
by (unfold increasing_def, blast)

lemma increasingD:
"F \ increasing[A](r,f) ==> F \ program & (\a. a \ A) & (\s \ state. f(s):A)"
apply (unfold increasing_def)
apply (subgoal_tac "\x. x \ state")
apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
done

lemma increasing_constant [simp]:
"F \ increasing[A](r, %s. c) \ F \ program & c \ A"
apply (unfold increasing_def stable_def)
apply (subgoal_tac "\x. x \ state")
apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
done

lemma subset_increasing_comp:
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==>
   increasing[A](r, f) \<subseteq> increasing[B](s, g comp f)"
apply (unfold increasing_def stable_def part_order_def
       constrains_def mono1_def metacomp_def, clarify, simp)
apply clarify
apply (subgoal_tac "xa \ state")
prefer 2 apply (blast dest!: ActsD)
apply (subgoal_tac ":r")
prefer 2 apply (force simp add: refl_def)
apply (rotate_tac 5)
apply (drule_tac x = "f (xb) " in bspec)
apply (rotate_tac [2] -1)
apply (drule_tac [2] x = act in bspec, simp_all)
apply (drule_tac A = "act``u" and c = xa for u in subsetD, blast)
apply (drule_tac x = "f(xa) " and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done

lemma imp_increasing_comp:
     "[| F \ increasing[A](r, f); mono1(A, r, B, s, g);
         refl(A, r); trans[B](s) |] ==> F \<in> increasing[B](s, g comp f)"
by (rule subset_increasing_comp [THEN subsetD], auto)

lemma strict_increasing:
   "increasing[nat](Le, f) \ increasing[nat](Lt, f)"
by (unfold increasing_def Lt_def, auto)

lemma strict_gt_increasing:
   "increasing[nat](Ge, f) \ increasing[nat](Gt, f)"
apply (unfold increasing_def Gt_def Ge_def, auto)
apply (erule natE)
apply (auto simp add: stable_def)
done

(** Increasing **)

lemma increasing_imp_Increasing:
     "F \ increasing[A](r, f) ==> F \ Increasing[A](r, f)"

apply (unfold increasing_def Increasing_def)
apply (auto intro: stable_imp_Stable)
done

lemma Increasing_type: "Increasing[A](r, f) \ program"
by (unfold Increasing_def, auto)

lemma Increasing_into_program: "F \ Increasing[A](r, f) ==> F \ program"
by (unfold Increasing_def, auto)

lemma Increasing_imp_Stable:
"[| F \ Increasing[A](r, f); a \ A |] ==> F \ Stable({s \ state. :r})"
by (unfold Increasing_def, blast)

lemma IncreasingD:
"F \ Increasing[A](r, f) ==> F \ program & (\a. a \ A) & (\s \ state. f(s):A)"
apply (unfold Increasing_def)
apply (subgoal_tac "\x. x \ state")
apply (auto intro: st0_in_state)
done

lemma Increasing_constant [simp]:
     "F \ Increasing[A](r, %s. c) \ F \ program & (c \ A)"
apply (subgoal_tac "\x. x \ state")
apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing)
done

lemma subset_Increasing_comp:
"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==>
   Increasing[A](r, f) \<subseteq> Increasing[B](s, g comp f)"
apply (unfold Increasing_def Stable_def Constrains_def part_order_def
       constrains_def mono1_def metacomp_def, safe)
apply (simp_all add: ActsD)
apply (subgoal_tac "xb \ state & xa \ state")
prefer 2 apply (simp add: ActsD)
apply (subgoal_tac ":r")
prefer 2 apply (force simp add: refl_def)
apply (rotate_tac 5)
apply (drule_tac x = "f (xb) " in bspec)
apply simp_all
apply clarify
apply (rotate_tac -2)
apply (drule_tac x = act in bspec)
apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, simp_all, blast)
apply (drule_tac x = "f(xa)" and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done

lemma imp_Increasing_comp:
"[| F \ Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |]
  ==> F \<in> Increasing[B](s, g comp f)"
apply (rule subset_Increasing_comp [THEN subsetD], auto)
done

lemma strict_Increasing: "Increasing[nat](Le, f) \ Increasing[nat](Lt, f)"
by (unfold Increasing_def Lt_def, auto)

lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)"
apply (unfold Increasing_def Ge_def Gt_def, auto)
apply (erule natE)
apply (auto simp add: Stable_def)
done

(** Two-place monotone operations **)

lemma imp_increasing_comp2:
"[| F \ increasing[A](r, f); F \ increasing[B](s, g);
    mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |]
==> F \<in> increasing[C](t, %x. h(f(x), g(x)))"
apply (unfold increasing_def stable_def
       part_order_def constrains_def mono2_def, clarify, simp)
apply clarify
apply (rename_tac xa xb)
apply (subgoal_tac "xb \ state & xa \ state")
prefer 2 apply (blast dest!: ActsD)
apply (subgoal_tac ":r & :s")
prefer 2 apply (force simp add: refl_def)
apply (rotate_tac 6)
apply (drule_tac x = "f (xb) " in bspec)
apply (rotate_tac [2] 1)
apply (drule_tac [2] x = "g (xb) " in bspec)
apply simp_all
apply (rotate_tac -1)
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
apply (drule_tac A = "act``u" and c = xa for u in subsetD)
apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, blast, blast)
apply (rotate_tac -4)
apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
apply (drule_tac [3] x = "g (xa) " and x1 = "g (xb) " in bspec [THEN bspec])
apply simp_all
apply (rule_tac b = "h (f (xb), g (xb))" and A = C in trans_onD)
apply simp_all
done

lemma imp_Increasing_comp2:
"[| F \ Increasing[A](r, f); F \ Increasing[B](s, g);
  mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==>
  F \<in> Increasing[C](t, %x. h(f(x), g(x)))"
apply (unfold Increasing_def stable_def
       part_order_def constrains_def mono2_def Stable_def Constrains_def, safe)
apply (simp_all add: ActsD)
apply (subgoal_tac "xa \ state & x \ state")
prefer 2 apply (blast dest!: ActsD)
apply (subgoal_tac ":r & :s")
prefer 2 apply (force simp add: refl_def)
apply (rotate_tac 6)
apply (drule_tac x = "f (xa) " in bspec)
apply (rotate_tac [2] 1)
apply (drule_tac [2] x = "g (xa) " in bspec)
apply simp_all
apply clarify
apply (rotate_tac -2)
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
apply (drule_tac A = "act``u" and c = x for u in subsetD)
apply (drule_tac [2] A = "act``u" and c = x for u in subsetD, blast, blast)
apply (rotate_tac -9)
apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
apply (drule_tac [3] x = "g (x) " and x1 = "g (xa) " in bspec [THEN bspec])
apply simp_all
apply (rule_tac b = "h (f (xa), g (xa))" and A = C in trans_onD)
apply simp_all
done

end

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