# Theory Values

Up to index of Isabelle/ZF/Coind

theory Values
imports Language Map
begin

    (*  Title:      ZF/Coind/Values.thy
        ID:         $Id: Values.thy,v 1.13 2005/06/17 14:15:10 haftmann Exp $
        Author:     Jacob Frost, Cambridge University Computer Laboratory
        Copyright   1995  University of Cambridge
    *)

    theory Values imports Language Map begin

    (* Values, values environments and associated operators *)

    consts
      Val  :: i
      ValEnv  :: i
      Val_ValEnv  :: i;

    codatatype
        "Val" = v_const ("c ∈ Const")
              | v_clos ("x ∈ ExVar","e ∈ Exp","ve ∈ ValEnv")
      and
        "ValEnv" = ve_mk ("m ∈ PMap(ExVar,Val)")
      monos       PMap_mono
      type_intros  A_into_univ mapQU

    consts
      ve_owr :: "[i,i,i] => i"
      ve_dom :: "i=>i"
      ve_app :: "[i,i] => i"

    primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"

    primrec "ve_dom(ve_mk(m)) = domain(m)"

    primrec "ve_app(ve_mk(m), a) = map_app(m,a)"

    constdefs
      ve_emp :: i
       "ve_emp == ve_mk(map_emp)"

    (* Elimination rules *)

    lemma ValEnvE:
      "[| ve ∈ ValEnv; !!m.[| ve=ve_mk(m); m ∈ PMap(ExVar,Val) |] ==> Q |] ==> Q"
    apply (unfold Part_def Val_def ValEnv_def, clarify)
    apply (erule Val_ValEnv.cases)
    apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
    done

    lemma ValE:
      "[| v ∈ Val;
          !!c. [| v = v_const(c); c ∈ Const |] ==> Q;
          !!e ve x.
            [| v = v_clos(x,e,ve); x ∈ ExVar; e ∈ Exp; ve ∈ ValEnv |] ==> Q
       |] ==>
       Q"
    apply (unfold Part_def Val_def ValEnv_def, clarify)
    apply (erule Val_ValEnv.cases)
    apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs)
    done

    (* Nonempty sets *)

    lemma v_closNE [simp]: "v_clos(x,e,ve) ≠ 0"
    by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast)

    declare v_closNE [THEN notE, elim!]

    lemma v_constNE [simp]: "c ∈ Const ==> v_const(c) ≠ 0"
    apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
    apply (drule constNEE, auto)
    done

    (* Proving that the empty set is not a value *)

    lemma ValNEE: "v ∈ Val ==> v ≠ 0"
    by (erule ValE, auto)

    (* Equalities for value environments *)

    lemma ve_dom_owr [simp]:
         "[| ve ∈ ValEnv; v ≠0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
    apply (erule ValEnvE)
    apply (auto simp add: map_domain_owr)
    done

    lemma ve_app_owr [simp]:
         "ve ∈ ValEnv
          ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
    by (erule ValEnvE, simp add: map_app_owr)

    (* Introduction rules for operators on value environments *)

    lemma ve_appI: "[| ve ∈ ValEnv; x ∈ ve_dom(ve) |] ==> ve_app(ve,x):Val"
    by (erule ValEnvE, simp add: pmap_appI)

    lemma ve_domI: "[| ve ∈ ValEnv; x ∈ ve_dom(ve) |] ==> x ∈ ExVar"
    apply (erule ValEnvE, simp)
    apply (blast dest: pmap_domainD)
    done

    lemma ve_empI: "ve_emp ∈ ValEnv"
    apply (unfold ve_emp_def)
    apply (rule Val_ValEnv.intros)
    apply (rule pmap_empI)
    done

    lemma ve_owrI:
         "[|ve ∈ ValEnv; x ∈ ExVar; v ∈ Val |] ==> ve_owr(ve,x,v):ValEnv"
    apply (erule ValEnvE, simp)
    apply (blast intro: pmap_owrI Val_ValEnv.intros)
    done

    end

lemma ValEnvE:

      [| ve ∈ ValEnv; !!m. [| ve = ve_mk(m); m ∈ PMap(ExVar, Val) |] ==> Q |] ==> Q

lemma ValE:

      [| v ∈ Val; !!c. [| v = v_const(c); c ∈ Const |] ==> Q;
         !!e ve x.
            [| v = v_clos(x, e, ve); x ∈ ExVar; e ∈ Exp; ve ∈ ValEnv |] ==> Q |]
      ==> Q

lemma v_closNE:

      v_clos(x, e, ve) ≠ 0

lemma v_constNE:

      c ∈ Const ==> v_const(c) ≠ 0

lemma ValNEE:

      v ∈ Val ==> v ≠ 0

lemma ve_dom_owr:

      [| ve ∈ ValEnv; v ≠ 0 |] ==> ve_dom(ve_owr(ve, x, v)) = ve_dom(ve) ∪ {x}

lemma ve_app_owr:

      ve ∈ ValEnv
      ==> ve_app(ve_owr(ve, y, v), x) = (if x = y then v else ve_app(ve, x))

lemma ve_appI:

      [| ve ∈ ValEnv; x ∈ ve_dom(ve) |] ==> ve_app(ve, x) ∈ Val

lemma ve_domI:

      [| ve ∈ ValEnv; x ∈ ve_dom(ve) |] ==> x ∈ ExVar

lemma ve_empI:

      ve_emp ∈ ValEnv

lemma ve_owrI:

      [| ve ∈ ValEnv; x ∈ ExVar; v ∈ Val |] ==> ve_owr(ve, x, v) ∈ ValEnv