Theory TrivLat

Up to index of Isabelle/HOL/objinit

(*  Title:      HOL/BCV/Err.thy
    ID:         $Id: TrivLat.html,v 1.1 2002/11/28 14:12:09 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

lemma [intro!]: "acc (op =)"
  by (simp add: acc_def lesssub_def lesub_def wf_def)

end

lemma eq_order:

  order op =

lemma bool_err_semilat:

  semilat (sl TrivLat.esl)

lemma

  acc op =