Theory MM

```(*  Title:      JinjaThreads/MM/MM.thy
Author:     Andreas Lochbihler
*)

chapter ‹Memory Models›

theory MM
imports
"../Common/Heap"
begin

abbreviation (input)

abbreviation (input)

definition "monitor_finfun_to_list ≡ (finfun_to_list :: nat ⇒f nat ⇒ nat list)"
instance
end

where "new_Addr h ≡ if ∃a. h a = None then Some(LEAST a. h a = None) else None"

"new_Addr h = Some a ⟹ h a = None"

"finite (dom h) ⟹ ∃a. new_Addr h = Some a"

subsection ‹Code generation›

where "gen_new_Addr h n ≡ if ∃a. a ≥ n ∧ h a = None then Some(LEAST a. a ≥ n ∧ h a = None) else None"

"gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
apply(rule impI)
apply(rule conjI)
apply safe[1]
apply(auto intro: Least_equality)[2]
apply(rule arg_cong[where f=Least])
apply(rule ext)
apply auto[1]
apply(case_tac "n = ab")
apply simp
apply simp
apply clarify
apply(subgoal_tac "a = n")
apply simp
apply(rule Least_equality)
apply auto[2]
apply(rule ccontr)
apply(erule_tac x="a" in allE)
apply simp
done

end
```