# Theory Tr

Up to index of Isabelle/HOLCF

theory Tr
imports Lift
uses [Tr.ML]
begin

    (*  Title:      HOLCF/Tr.thy
        ID:         $Id: Tr.thy,v 1.17 2005/07/08 00:42:42 huffman Exp $
        Author:     Franz Regensburger

    Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
    *)

    header {* The type of lifted booleans *}

    theory Tr
    imports Lift
    begin

    defaultsort pcpo

    types
      tr = "bool lift"

    translations
      "tr" <= (type) "bool lift"

    consts
            TT              :: "tr"
            FF              :: "tr"
            Icifte          :: "tr -> 'c -> 'c -> 'c"
            trand           :: "tr -> tr -> tr"
            tror            :: "tr -> tr -> tr"
            neg             :: "tr -> tr"
            If2             :: "tr=>'c=>'c=>'c"

    syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
            "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
            "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)

    translations
                 "x andalso y" == "trand$x$y"
                 "x orelse y"  == "tror$x$y"
                 "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
    defs
      TT_def:      "TT==Def True"
      FF_def:      "FF==Def False"
      neg_def:     "neg == flift2 Not"
      ifte_def:    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
      andalso_def: "trand == (LAM x y. If x then y else FF fi)"
      orelse_def:  "tror == (LAM x y. If x then TT else y fi)"
      If2_def:     "If2 Q x y == If Q then x else y fi"

    text {* Exhaustion and Elimination for type @{typ tr} *}

    lemma Exh_tr: "t=UU | t = TT | t = FF"
    apply (unfold FF_def TT_def)
    apply (induct_tac "t")
    apply fast
    apply fast
    done

    lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
    apply (rule Exh_tr [THEN disjE])
    apply fast
    apply (erule disjE)
    apply fast
    apply fast
    done

    text {* tactic for tr-thms with case split *}

    lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
    (*
    fun prover t =  prove_goal thy t
     (fn prems =>
            [
            (res_inst_tac [("p","y")] trE 1),
            (REPEAT(asm_simp_tac (simpset() addsimps
                    [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
            ])
    *)
    text {* distinctness for type @{typ tr} *}

    lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
    by (simp_all add: tr_defs)

    lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
    by (simp_all add: tr_defs)

    text {* lemmas about andalso, orelse, neg and if *}

    lemma ifte_thms [simp]:
      "If UU then e1 else e2 fi = UU"
      "If FF then e1 else e2 fi = e2"
      "If TT then e1 else e2 fi = e1"
    by (simp_all add: ifte_def TT_def FF_def)

    lemma andalso_thms [simp]:
      "(TT andalso y) = y"
      "(FF andalso y) = FF"
      "(UU andalso y) = UU"
      "(y andalso TT) = y"
      "(y andalso y) = y"
    apply (unfold andalso_def, simp_all)
    apply (rule_tac p=y in trE, simp_all)
    apply (rule_tac p=y in trE, simp_all)
    done

    lemma orelse_thms [simp]:
      "(TT orelse y) = TT"
      "(FF orelse y) = y"
      "(UU orelse y) = UU"
      "(y orelse FF) = y"
      "(y orelse y) = y"
    apply (unfold orelse_def, simp_all)
    apply (rule_tac p=y in trE, simp_all)
    apply (rule_tac p=y in trE, simp_all)
    done

    lemma neg_thms [simp]:
      "neg$TT = FF"
      "neg$FF = TT"
      "neg$UU = UU"
    by (simp_all add: neg_def TT_def FF_def)

    text {* split-tac for If via If2 because the constant has to be a constant *}

    lemma split_If2:
      "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"
    apply (unfold If2_def)
    apply (rule_tac p = "Q" in trE)
    apply (simp_all)
    done

    ML {*
    val split_If_tac =
      simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
        THEN' (split_tac [thm "split_If2"])
    *}

    subsection "Rewriting of HOLCF operations to HOL functions"

    lemma andalso_or:
    "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
    apply (rule_tac p = "t" in trE)
    apply simp_all
    done

    lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
    apply (rule_tac p = "t" in trE)
    apply simp_all
    done

    lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
    by (simp add: FF_def)

    lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
    by (simp add: FF_def)

    lemma Def_bool3 [simp]: "(Def x = TT) = x"
    by (simp add: TT_def)

    lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
    by (simp add: TT_def)

    lemma If_and_if:
      "(If Def P then A else B fi)= (if P then A else B)"
    apply (rule_tac p = "Def P" in trE)
    apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
    done

    subsection "admissibility"

    text {*
       The following rewrite rules for admissibility should in the future be
       replaced by a more general admissibility test that also checks
       chain-finiteness, of which these lemmata are specific examples
    *}

    lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
    apply (rule_tac p = "x" in trE)
    apply (simp_all)
    done

    lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
    apply (rule_tac p = "x" in trE)
    apply (simp_all)
    done

    lemmas adm_tricks = adm_trick_1 adm_trick_2

    lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
    by (simp add: adm_tricks)

    lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
    by (simp add: adm_tricks)

    end

lemma Exh_tr:

      t = UU ∨ t = TT ∨ t = FF

lemma trE:

      [| p = UU ==> Q; p = TT ==> Q; p = FF ==> Q |] ==> Q

lemmas tr_defs:

      trand == LAM x y. If x then y else FF fi

      tror == LAM x y. If x then TT else y fi

      Tr.neg == flift2 Not

      Icifte == LAM b t e. (FLIFT b. if b then t else e)·b

      TT == Def True

      FF == Def False

lemmas tr_defs:

      trand == LAM x y. If x then y else FF fi

      tror == LAM x y. If x then TT else y fi

      Tr.neg == flift2 Not

      Icifte == LAM b t e. (FLIFT b. if b then t else e)·b

      TT == Def True

      FF == Def False

lemma dist_less_tr:

      ¬ TT << UU

      ¬ FF << UU

      ¬ TT << FF

      ¬ FF << TT

lemma dist_eq_tr:

      TT ≠ UU

      FF ≠ UU

      TT ≠ FF

      UU ≠ TT

      UU ≠ FF

      FF ≠ TT

lemma ifte_thms:

      If UU then e1.0 else e2.0 fi = UU

      If FF then e1.0 else e2.0 fi = e2.0

      If TT then e1.0 else e2.0 fi = e1.0

lemma andalso_thms:

      (TT andalso y) = y

      (FF andalso y) = FF

      (UU andalso y) = UU

      (y andalso TT) = y

      (y andalso y) = y

lemma orelse_thms:

      (TT orelse y) = TT

      (FF orelse y) = y

      (UU orelse y) = UU

      (y orelse FF) = y

      (y orelse y) = y

lemma neg_thms:

      Tr.neg·TT = FF

      Tr.neg·FF = TT

      Tr.neg·UU = UU

lemma split_If2:

      P (If2 Q x y) = ((Q = UU --> P UU) ∧ (Q = TT --> P x) ∧ (Q = FF --> P y))

### Rewriting of HOLCF operations to HOL functions

lemma andalso_or:

      t ≠ UU ==> ((t andalso s) = FF) = (t = FF ∨ s = FF)

lemma andalso_and:

      t ≠ UU ==> ((t andalso s) ≠ FF) = (t ≠ FF ∧ s ≠ FF)

lemma Def_bool1:

      (Def x ≠ FF) = x

lemma Def_bool2:

      (Def x = FF) = (¬ x)

lemma Def_bool3:

      (Def x = TT) = x

lemma Def_bool4:

      (Def x ≠ TT) = (¬ x)

lemma If_and_if:

      If Def P then A else B fi = (if P then A else B)

### admissibility

lemma adm_trick_1:

      (x ≠ FF) = (x = TT ∨ x = UU)

lemma adm_trick_2:

      (x ≠ TT) = (x = FF ∨ x = UU)

lemmas adm_tricks:

      (x ≠ FF) = (x = TT ∨ x = UU)

      (x ≠ TT) = (x = FF ∨ x = UU)

lemmas adm_tricks:

      (x ≠ FF) = (x = TT ∨ x = UU)

      (x ≠ TT) = (x = FF ∨ x = UU)

lemma adm_nTT:

      cont f ==> adm (%x. f x ≠ TT)

lemma adm_nFF:

      cont f ==> adm (%x. f x ≠ FF)