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