src/HOL/IMP/Def_Init_Exp.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 53015 a1119cf551e8
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
nipkow@50161
     3
theory Def_Init_Exp
nipkow@50161
     4
imports Vars
kleing@43158
     5
begin
kleing@43158
     6
kleing@43158
     7
subsection "Initialization-Sensitive Expressions Evaluation"
kleing@43158
     8
nipkow@45212
     9
type_synonym state = "vname \<Rightarrow> val option"
kleing@43158
    10
kleing@43158
    11
kleing@43158
    12
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
kleing@43158
    13
"aval (N i) s = Some i" |
kleing@43158
    14
"aval (V x) s = s x" |
wenzelm@53015
    15
"aval (Plus a\<^sub>1 a\<^sub>2) s =
wenzelm@53015
    16
  (case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
wenzelm@53015
    17
     (Some i\<^sub>1,Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1+i\<^sub>2) | _ \<Rightarrow> None)"
kleing@43158
    18
kleing@43158
    19
kleing@43158
    20
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
nipkow@45200
    21
"bval (Bc v) s = Some v" |
kleing@43158
    22
"bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
wenzelm@53015
    23
"bval (And b\<^sub>1 b\<^sub>2) s = (case (bval b\<^sub>1 s, bval b\<^sub>2 s) of
wenzelm@53015
    24
  (Some bv\<^sub>1, Some bv\<^sub>2) \<Rightarrow> Some(bv\<^sub>1 & bv\<^sub>2) | _ \<Rightarrow> None)" |
wenzelm@53015
    25
"bval (Less a\<^sub>1 a\<^sub>2) s = (case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
wenzelm@53015
    26
 (Some i\<^sub>1, Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1 < i\<^sub>2) | _ \<Rightarrow> None)"
kleing@43158
    27
kleing@43158
    28
kleing@43158
    29
lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
kleing@43158
    30
by (induct a) auto
kleing@43158
    31
kleing@43158
    32
lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
kleing@43158
    33
by (induct b) (auto dest!: aval_Some)
kleing@43158
    34
kleing@43158
    35
end