src/ZF/Coind/Values.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 46822 95f1e700b712
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      ZF/Coind/Values.thy
     2     Author:     Jacob Frost, Cambridge University Computer Laboratory
     3     Copyright   1995  University of Cambridge
     4 *)
     5 
     6 theory Values imports Language Map begin
     7 
     8 (* Values, values environments and associated operators *)
     9 
    10 consts
    11   Val  :: i
    12   ValEnv  :: i
    13   Val_ValEnv  :: i
    14 
    15 codatatype
    16     "Val" = v_const ("c \<in> Const")
    17           | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv")
    18   and
    19     "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)")
    20   monos       PMap_mono
    21   type_intros  A_into_univ mapQU
    22 
    23 consts
    24   ve_owr :: "[i,i,i] => i"
    25   ve_dom :: "i=>i"
    26   ve_app :: "[i,i] => i"
    27 
    28 
    29 primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
    30 
    31 primrec "ve_dom(ve_mk(m)) = domain(m)"
    32 
    33 primrec "ve_app(ve_mk(m), a) = map_app(m,a)"
    34 
    35 definition
    36   ve_emp :: i  where
    37    "ve_emp == ve_mk(map_emp)"
    38 
    39 
    40 (* Elimination rules *)
    41 
    42 lemma ValEnvE:
    43   "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
    44 apply (unfold Part_def Val_def ValEnv_def, clarify) 
    45 apply (erule Val_ValEnv.cases) 
    46 apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
    47 done
    48 
    49 lemma ValE:
    50   "[| v \<in> Val;  
    51       !!c. [| v = v_const(c); c \<in> Const |] ==> Q; 
    52       !!e ve x.  
    53         [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q  
    54    |] ==>  
    55    Q"
    56 apply (unfold Part_def Val_def ValEnv_def, clarify) 
    57 apply (erule Val_ValEnv.cases) 
    58 apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs)
    59 done
    60 
    61 (* Nonempty sets *)
    62 
    63 lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
    64 by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast)
    65 
    66 declare v_closNE [THEN notE, elim!]
    67 
    68 
    69 lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
    70 apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
    71 apply (drule constNEE, auto)
    72 done
    73 
    74 
    75 (* Proving that the empty set is not a value *)
    76 
    77 lemma ValNEE: "v \<in> Val ==> v \<noteq> 0"
    78 by (erule ValE, auto)
    79 
    80 (* Equalities for value environments *)
    81 
    82 lemma ve_dom_owr [simp]:
    83      "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) \<union> {x}"
    84 apply (erule ValEnvE)
    85 apply (auto simp add: map_domain_owr)
    86 done
    87 
    88 lemma ve_app_owr [simp]:
    89      "ve \<in> ValEnv  
    90       ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
    91 by (erule ValEnvE, simp add: map_app_owr)
    92 
    93 (* Introduction rules for operators on value environments *)
    94 
    95 lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val"
    96 by (erule ValEnvE, simp add: pmap_appI) 
    97 
    98 lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
    99 apply (erule ValEnvE, simp) 
   100 apply (blast dest: pmap_domainD)
   101 done
   102 
   103 lemma ve_empI: "ve_emp \<in> ValEnv"
   104 apply (unfold ve_emp_def)
   105 apply (rule Val_ValEnv.intros)
   106 apply (rule pmap_empI)
   107 done
   108 
   109 lemma ve_owrI:
   110      "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
   111 apply (erule ValEnvE, simp)
   112 apply (blast intro: pmap_owrI Val_ValEnv.intros)
   113 done
   114 
   115 end