Quelle State.thy Sprache: Isabelle

(*  Title:      HOL/MicroJava/J/State.thy
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section \<open>Program State\<close>

theory State
imports TypeRel Value
begin

type_synonym
  fields' = "(vname \ cname \ val)" \ \field name, defining class, value\

type_synonym
  obj = "cname \ fields'" \ \class instance with class name and fields\

definition obj_ty :: "obj => ty" where
"obj_ty obj == Class (fst obj)"

definition init_vars :: "('a \ ty) list => ('a \ val)" where
"init_vars == map_of o map (\(n,T). (n,default_val T))"

type_synonym aheap = "loc \ obj" \ \"\heap\" used in a translation below\
type_synonym locals = "vname \ val" \ \simple state, i.e. variable contents\

type_synonym state = "aheap \ locals" \ \heap, local parameter including This\
type_synonym xstate = "val option \ state" \ \state including exception information\

abbreviation (input)
  heap :: "state => aheap"
  where "heap == fst"

abbreviation (input)
  locals :: "state => locals"
  where "locals == snd"

abbreviation "Norm s == (None, s)"

abbreviation (input)
  abrupt :: "xstate \ val option"
  where "abrupt == fst"

abbreviation (input)
  store :: "xstate \ state"
  where "store == snd"

abbreviation
  lookup_obj :: "state \ val \ obj"
  where "lookup_obj s a' == the (heap s (the_Addr a'))"

definition raise_if :: "bool \ xcpt \ val option \ val option" where
  "raise_if b x xo \ if b \ (xo = None) then Some (Addr (XcptRef x)) else xo"

text \<open>Make \<open>new_Addr\<close> completely specified (at least for the code generator)\<close>
(*
definition new_Addr  :: "aheap => loc \<times> val option" where
  "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
*)
consts nat_to_loc' :: "nat => loc'"
code_datatype nat_to_loc'
definition new_Addr  :: "aheap => loc \ val option" where
  "new_Addr h \
   if \<exists>n. h (Loc (nat_to_loc' n)) = None
   then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None)
   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"

definition np    :: "val => val option => val option" where
"np v == raise_if (v = Null) NullPointer"

definition c_hupd  :: "aheap => xstate => xstate" where
"c_hupd h'== \(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"

definition cast_ok :: "'c prog => cname => aheap => val => bool" where
"cast_ok G C h v == v = Null \ G\obj_ty (the (h (the_Addr v)))\ Class C"

lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
apply (unfold obj_ty_def)
apply (simp (no_asm))
done

lemma new_AddrD: "new_Addr hp = (ref, xcp) \
  hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
apply (drule sym)
apply (unfold new_Addr_def)
apply (simp split: if_split_asm)
apply (erule LeastI)
done

lemma raise_if_True [simp]: "raise_if True x y \ None"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_False [simp]: "raise_if False x y = y"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_Some [simp]: "raise_if c x (Some y) \ None"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_Some2 [simp]:
  "raise_if c z (if x = None then Some y else x) \ None"
unfolding raise_if_def by (induct x) auto

lemma raise_if_SomeD [rule_format (no_asm)]:
  "raise_if c x y = Some z \ c \ Some z = Some (Addr (XcptRef x)) | y = Some z"
apply (unfold raise_if_def)
apply auto
done

lemma raise_if_NoneD [rule_format (no_asm)]:
  "raise_if c x y = None --> \ c \ y = None"
apply (unfold raise_if_def)
apply auto
done

lemma np_NoneD [rule_format (no_asm)]:
  "np a' x' = None --> x' = None \ a' \ Null"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_None [rule_format (no_asm), simp]: "a' \ Null --> np a' x' = x'"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Some [simp]: "np a' (Some xc) = Some xc"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_Addr [simp]: "np (Addr a) None = None"
apply (unfold np_def raise_if_def)
apply auto
done

lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =
  Some (Addr (XcptRef (if c then  xc else NullPointer)))"
apply (unfold raise_if_def)
apply (simp (no_asm))
done

lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
by (simp add: c_hupd_def split_beta)

text \<open>Naive implementation for \<^term>\<open>new_Addr\<close> by exhaustive search\<close>

definition gen_new_Addr :: "aheap => nat \ loc \ val option" where
  "gen_new_Addr h n \
   if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None
   then (Loc (nat_to_loc' (LEAST a. a \ n \ h (Loc (nat_to_loc' a)) = None)), None)
   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"

lemma new_Addr_code_code [code]:
  "new_Addr h = gen_new_Addr h 0"
by(simp only: new_Addr_def gen_new_Addr_def split: if_split) simp

lemma gen_new_Addr_code [code]:
  "gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))"
apply(simp add: gen_new_Addr_def)
apply(rule impI)
apply(rule conjI)
apply safe[1]
  apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1]
apply(rule arg_cong[where f=nat_to_loc'])
apply(rule arg_cong[where f=Least])
apply(rule ext)
apply(safe, simp_all)[1]
apply(rename_tac "n'")
apply(case_tac "n = n'", simp_all)[1]
apply clarify
apply(subgoal_tac "a = n")
apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1]
apply(rule ccontr)
apply(erule_tac x="a" in allE)
apply simp
done

instantiation loc' :: equal
begin

definition "HOL.equal (l :: loc') l' \ l = l'"
instance by standard (simp add: equal_loc'_def)

end

end

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.