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

chapter ‹Memory Models›

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

type_synonym addr = nat
type_synonym thread_id = addr

abbreviation (input) 
  addr2thread_id :: "addr → thread_id"
where "addr2thread_id ≡ λx. x"

abbreviation (input)
  thread_id2addr :: "thread_id → addr"
where "thread_id2addr ≡ λx. x"

instantiation nat :: addr begin
definition "hash_addr ≡ int"
definition "monitor_finfun_to_list ≡ (finfun_to_list :: nat →f nat → nat list)"
instance
by(intro_classes)(simp add: monitor_finfun_to_list_nat_def)
end

definition new_Addr :: "(addr ⇀ 'b) → addr option"
where "new_Addr h ≡ if ∃a. h a = None then Some(LEAST a. h a = None) else None"

lemma new_Addr_SomeD:
  "new_Addr h = Some a ==> h a = None"
by(auto simp add:new_Addr_def split:if_splits intro: LeastI)

lemma new_Addr_SomeI:
  "finite (dom h) ==> ∃a. new_Addr h = Some a"
by(simp add: new_Addr_def) (metis finite_map_freshness infinite_UNIV_nat)

subsection ‹Code generation›

definition gen_new_Addr :: "(addr ⇀ 'b) → addr → addr option"
where "gen_new_Addr h n ≡ if ∃a. a ≥ n ∧ h a = None then Some(LEAST a. a ≥ n ∧ h a = None) else None"

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

lemma gen_new_Addr_code [code]:
  "gen_new_Addr h n = (if h n = None then Some n 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: 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