Theory TrivLat

Up to index of Isabelle/HOL/verificard

(*  Title:      HOL/BCV/Err.thy
    ID:         $Id: TrivLat.thy,v 1.1.2.1 2001/02/22 13:33:14 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2000 TUM
*)

header "The trivial semilattice";

theory TrivLat = Err:

constdefs 
  esl :: "'a esl"
  "esl \<equiv> (UNIV, op =, \<lambda>a b. if a=b then OK a else Err)"

lemma eq_order:
  "order (op =)"
  by (unfold order_def lesub_def) blast

lemma bool_err_semilat:
  "err_semilat esl"
  apply (unfold esl_def sl_def semilat_def)
  apply (simp add: eq_order)
  apply (auto simp add: closed_def plussub_def lesub_def Err.le_def lift2_def 
              split: err.split)
  done

end

lemma eq_order:

  order op =

lemma bool_err_semilat:

  semilat (sl TrivLat.esl)