Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: mandelbrot.cob Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/DFA/Product.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section \<open>Products as Semilattices\<close>

theory Product
imports Err
begin

definition le :: "'a ord \ 'b ord \ ('a * 'b) ord" where
"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"

definition sup :: "'a ebinop \ 'b ebinop \ ('a * 'b)ebinop" where
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"

definition esl :: "'a esl \ 'b esl \ ('a * 'b ) esl" where
"esl == %(A,rA,fA) (B,rB,fB). (A \ B, le rA rB, sup fA fB)"

abbreviation
  lesubprod_sntax :: "'a * 'b \ 'a ord \ 'b ord \ 'a * 'b \ bool"
       ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
  where "p <=(rA,rB) q == p <=_(le rA rB) q"

lemma unfold_lesub_prod:
  "p <=(rA,rB) q == le rA rB p q"
  by (simp add: lesub_def)

lemma le_prod_Pair_conv [iff]:
  "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"
  by (simp add: lesub_def le_def)

lemma less_prod_Pair_conv:
  "((a1,b1) <_(Product.le rA rB) (a2,b2)) =
  (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"
apply (unfold lesssub_def)
apply simp
apply blast
done

lemma order_le_prod [iff]:
  "order(Product.le rA rB) = (order rA & order rB)"
apply (unfold Semilat.order_def)
apply simp
apply meson
done

lemma acc_le_prodI [intro!]:
  "\ acc r\<^sub>A; acc r\<^sub>B \ \ acc(Product.le r\<^sub>A r\<^sub>B)"
apply (unfold acc_def)
apply (rule wf_subset)
apply (erule wf_lex_prod)
apply assumption
apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
done

lemma closed_lift2_sup:
  "\ closed (err A) (lift2 f); closed (err B) (lift2 g) \ \
  closed (err(A\<times>B)) (lift2(sup f g))"
apply (unfold closed_def plussub_def lift2_def err_def sup_def)
apply (simp split: err.split)
apply blast
done

lemma unfold_plussub_lift2:
  "e1 +_(lift2 f) e2 == lift2 f e1 e2"
  by (simp add: plussub_def)

lemma plus_eq_Err_conv [simp]:
  assumes "x \ A" and "y \ A"
    and "semilat(err A, Err.le r, lift2 f)"
  shows "(x +_f y = Err) = (\(\z\A. x <=_r z & y <=_r z))"
proof -
  have plus_le_conv2:
    "\r f z. \ z \ err A; semilat (err A, r, f); OK x \ err A; OK y \ err A;
                 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
    by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
  from assms show ?thesis
  apply (rule_tac iffI)
   apply clarify
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
        apply assumption
       apply assumption
      apply simp
     apply simp
    apply simp
   apply simp
  apply (case_tac "x +_f y")
   apply assumption
  apply (rename_tac "z")
  apply (subgoal_tac "OK z \ err A")
  apply (frule plus_le_conv2)
       apply assumption
      apply simp
      apply blast
     apply simp
    apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
   apply blast
  apply (erule subst)
  apply (unfold semilat_def err_def closed_def)
  apply simp
  done
qed

lemma err_semilat_Product_esl:
  "\L1 L2. \ err_semilat L1; err_semilat L2 \ \ err_semilat(Product.esl L1 L2)"
apply (unfold esl_def Err.sl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
apply (simp (no_asm) only: semilat_Def)
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
            simp add: lift2_def  split: err.split)
apply (blast dest: Semilat.orderI [OF Semilat.intro])
apply (blast dest: Semilat.orderI [OF Semilat.intro])

apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp

apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
done

end

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