# Theory Namespace

```chapter ‹Generated by Lem from ‹semantics/namespace.lem›.›

theory "Namespace"

imports
Main
"HOL-Library.Datatype_Records"
"LEM.Lem_pervasives"
"LEM.Lem_set_extra"

begin

― ‹‹open import Pervasives››
― ‹‹open import Set_extra››

type_synonym( 'k, 'v) alist0 =" ('k * 'v) list "

― ‹‹ Identifiers ››
datatype( 'm, 'n) id0 =
Short " 'n "
| Long " 'm " " ('m, 'n) id0 "

― ‹‹val mk_id : forall 'n 'm. list 'm -> 'n -> id 'm 'n››
fun  mk_id  :: " 'm list ⇒ 'n ⇒('m,'n)id0 "  where
" mk_id [] n = ( Short n )"
|" mk_id (mn # mns) n = ( Long mn (mk_id mns n))"

― ‹‹val id_to_n : forall 'n 'm. id 'm 'n -> 'n››
fun  id_to_n  :: "('m,'n)id0 ⇒ 'n "  where
" id_to_n (Short n) = ( n )"
|" id_to_n (Long _ id1) = ( id_to_n id1 )"

― ‹‹val id_to_mods : forall 'n 'm. id 'm 'n -> list 'm››
fun  id_to_mods  :: "('m,'n)id0 ⇒ 'm list "  where
" id_to_mods (Short _) = ( [])"
|" id_to_mods (Long mn id1) = ( mn # id_to_mods id1 )"

datatype( 'm, 'n, 'v) namespace =
Bind " ('n, 'v) alist0 " " ('m, ( ('m, 'n, 'v)namespace)) alist0 "

― ‹‹val nsLookup : forall 'v 'm 'n. Eq 'n, Eq 'm => namespace 'm 'n 'v -> id 'm 'n -> maybe 'v››
fun  nsLookup  :: "('m,'n,'v)namespace ⇒('m,'n)id0 ⇒ 'v option "  where
" nsLookup (Bind v2 m) (Short n) = ( Map.map_of v2 n )"
|" nsLookup (Bind v2 m) (Long mn id1) = (
(case  Map.map_of m mn of
None => None
| Some env => nsLookup env id1
))"

― ‹‹val nsLookupMod : forall 'm 'n 'v. Eq 'n, Eq 'm => namespace 'm 'n 'v -> list 'm -> maybe (namespace 'm 'n 'v)››
fun  nsLookupMod  :: "('m,'n,'v)namespace ⇒ 'm list ⇒(('m,'n,'v)namespace)option "  where
" nsLookupMod e [] = ( Some e )"
|" nsLookupMod (Bind v2 m) (mn # path) = (
(case  Map.map_of m mn of
None => None
| Some env => nsLookupMod env path
))"

― ‹‹val nsEmpty : forall 'v 'm 'n. namespace 'm 'n 'v››
definition nsEmpty  :: "('m,'n,'v)namespace "  where
" nsEmpty = ( Bind [] [])"

― ‹‹val nsAppend : forall 'v 'm 'n. namespace 'm 'n 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v››
fun nsAppend  :: "('m,'n,'v)namespace ⇒('m,'n,'v)namespace ⇒('m,'n,'v)namespace "  where
" nsAppend (Bind v1 m1) (Bind v2 m2) = ( Bind (v1 @ v2) (m1 @ m2))"

― ‹‹val nsLift : forall 'v 'm 'n. 'm -> namespace 'm 'n 'v -> namespace 'm 'n 'v››
definition nsLift  :: " 'm ⇒('m,'n,'v)namespace ⇒('m,'n,'v)namespace "  where
" nsLift mn env = ( Bind [] [(mn, env)])"

― ‹‹val alist_to_ns : forall 'v 'm 'n. alist 'n 'v -> namespace 'm 'n 'v››
definition alist_to_ns  :: "('n*'v)list ⇒('m,'n,'v)namespace "  where
" alist_to_ns a = ( Bind a [])"

― ‹‹val nsBind : forall 'v 'm 'n. 'n -> 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v››
fun nsBind  :: " 'n ⇒ 'v ⇒('m,'n,'v)namespace ⇒('m,'n,'v)namespace "  where
" nsBind k x (Bind v2 m) = ( Bind ((k,x)# v2) m )"

― ‹‹val nsBindList : forall 'v 'm 'n. list ('n * 'v) -> namespace 'm 'n 'v -> namespace 'm 'n 'v››
definition nsBindList  :: "('n*'v)list ⇒('m,'n,'v)namespace ⇒('m,'n,'v)namespace "  where
" nsBindList l e = ( List.foldr ( λx .
(case  x of (x,v2) => λ e .  nsBind x v2 e )) l e )"

― ‹‹val nsOptBind : forall 'v 'm 'n. maybe 'n -> 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v››
fun nsOptBind  :: " 'n option ⇒ 'v ⇒('m,'n,'v)namespace ⇒('m,'n,'v)namespace "  where
" nsOptBind None x env = ( env )"
|" nsOptBind (Some n') x env = ( nsBind n' x env )"

― ‹‹val nsSing : forall 'v 'm 'n. 'n -> 'v -> namespace 'm 'n 'v››
definition nsSing  :: " 'n ⇒ 'v ⇒('m,'n,'v)namespace "  where
" nsSing n x = ( Bind ([(n,x)]) [])"

― ‹‹val nsSub : forall 'v1 'v2 'm 'n. Eq 'm, Eq 'n, Eq 'v1, Eq 'v2 =>
(id 'm 'n -> 'v1 -> 'v2 -> bool) -> namespace 'm 'n 'v1 -> namespace 'm 'n 'v2 -> bool››
definition nsSub  :: "(('m,'n)id0 ⇒ 'v1 ⇒ 'v2 ⇒ bool)⇒('m,'n,'v1)namespace ⇒('m,'n,'v2)namespace ⇒ bool "  where
" nsSub r env1 env2 = (
((∀ id0. ∀ v1.
(nsLookup env1 id0 = Some v1)
⟶
((∃ v2.  (nsLookup env2 id0 = Some v2) ∧ r id0 v1 v2))))
∧
((∀ path.
(nsLookupMod env2 path = None) ⟶ (nsLookupMod env1 path = None))))"

― ‹‹val nsAll : forall 'v 'm 'n. Eq 'm, Eq 'n, Eq 'v => (id 'm 'n -> 'v -> bool) -> namespace 'm 'n 'v -> bool››
fun  nsAll  :: "(('m,'n)id0 ⇒ 'v ⇒ bool)⇒('m,'n,'v)namespace ⇒ bool "  where
" nsAll f env = (
((∀ id0. ∀ v1.
(nsLookup env id0 = Some v1)
⟶
f id0 v1)))"

― ‹‹val eAll2 : forall 'v1 'v2 'm 'n. Eq 'm, Eq 'n, Eq 'v1, Eq 'v2 =>
(id 'm 'n -> 'v1 -> 'v2 -> bool) -> namespace 'm 'n 'v1 -> namespace 'm 'n 'v2 -> bool››
definition nsAll2  :: "(('d,'c)id0 ⇒ 'b ⇒ 'a ⇒ bool)⇒('d,'c,'b)namespace ⇒('d,'c,'a)namespace ⇒ bool "  where
" nsAll2 r env1 env2 = (
nsSub r env1 env2 ∧
nsSub (λ x y z .  r x z y) env2 env1 )"

― ‹‹val nsDom : forall 'v 'm 'n. Eq 'm, Eq 'n, Eq 'v, SetType 'v => namespace 'm 'n 'v -> set (id 'm 'n)››
definition nsDom  :: "('m,'n,'v)namespace ⇒(('m,'n)id0)set "  where
" nsDom env = ( (let x2 =
({}) in  Finite_Set.fold
(λv2 x2 .  Finite_Set.fold
(λn x2 .
if nsLookup env n = Some v2 then Set.insert n x2
else x2) x2 UNIV) x2 UNIV))"

― ‹‹val nsDomMod : forall 'v 'm 'n. SetType 'm, Eq 'm, Eq 'n, Eq 'v => namespace 'm 'n 'v -> set (list 'm)››
definition nsDomMod  :: "('m,'n,'v)namespace ⇒('m list)set "  where
" nsDomMod env = ( (let x2 =
({}) in  Finite_Set.fold
(λv2 x2 .  Finite_Set.fold
(λn x2 .
if nsLookupMod env n = Some v2 then Set.insert n x2
else x2) x2 UNIV) x2 UNIV))"

― ‹‹val nsMap : forall 'v 'w 'm 'n. ('v -> 'w) -> namespace 'm 'n 'v -> namespace 'm 'n 'w››
function (sequential,domintros)  nsMap  :: "('v ⇒ 'w)⇒('m,'n,'v)namespace ⇒('m,'n,'w)namespace "  where
" nsMap f (Bind v2 m) = (
Bind (List.map ( λx .
(case  x of (n,x) => (n, f x) )) v2)
(List.map ( λx .
(case  x of (mn,e) => (mn, nsMap f e) )) m))"
by pat_completeness auto

end
```