src/HOL/IMP/Def_Ass_Exp.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43158 686fa0a0696e
child 45200 1f1897ac7877
permissions -rw-r--r--
remove lemma stupid_ext
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Def_Ass_Exp imports Vars
     4 begin
     5 
     6 subsection "Initialization-Sensitive Expressions Evaluation"
     7 
     8 type_synonym val = "int"
     9 type_synonym state = "name \<Rightarrow> val option"
    10 
    11 
    12 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
    13 "aval (N i) s = Some i" |
    14 "aval (V x) s = s x" |
    15 "aval (Plus a\<^isub>1 a\<^isub>2) s =
    16   (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
    17      (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)"
    18 
    19 
    20 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
    21 "bval (B bv) s = Some bv" |
    22 "bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
    23 "bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
    24   (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
    25 "bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
    26  (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)"
    27 
    28 
    29 lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
    30 by (induct a) auto
    31 
    32 lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
    33 by (induct b) (auto dest!: aval_Some)
    34 
    35 end