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