FMap.thy

(* Title:      Finite Maps
   Author:     Michael Walker <mike@barrucadu.co.uk>, 2015
   Maintainer: Michael Walker <mike@barrucadu.co.uk>
*)

(* TODO: Commentary *)
(* TODO: Lift more lemmas *)
(* TODO: Use fset, not set *)

(*<*)
theory FMap
imports BNF_Cardinal_Arithmetic BNF_Def Map FSet
begin
(*>*)

section {* Finite Maps *}

typedef ('k, 'v) fmap = "{M :: ('k ⇀ 'v). finite (dom M)}" morphisms fmap Abs_fmap
proof -
  have "finite (dom empty)"
    by simp
  thus ?thesis
    by blast
qed

type_notation "fmap" (infixr "|~=>|" 0)
type_notation (xsymbols) "fmap" (infixr "↪"  0)

setup_lifting type_definition_fmap

subsection {* Elements, domain, and range *}

lift_definition dom :: "('k ↪ 'v) ⇒ 'k set"
is "Map.dom".

lift_definition ran :: "('k ↪ 'v) ⇒ 'v set"
is "Map.ran".

lift_definition elems :: "('k ↪ 'v) ⇒ ('k × 'v) set"
is "λ m. {(a, b). a ∈ Map.dom m ∧ b = the (m a)}".

lemma elems_def_alt: "elems m = {(k, v). fmap m k = Some v}"
by (smt Collect_cong case_prod_unfold domI domIff elems.rep_eq option.collapse option.sel)

lemma dom_elems: "dom m = fst ` elems m"
by (transfer, force)

lemma ran_elems: "ran m = snd ` elems m"
  apply (transfer, simp add: Map.ran_def)
by force

lemma elems_finite: "finite (elems m)"
apply transfer
unfolding Map.dom_def
apply simp
proof-
  fix m
  assume "finite {a. ∃y. m a = Some y}"
  hence "finite ((λ k. (k, the (m k))) ` {a. ∃y. m a = Some y})"
    by simp
  hence "finite {(a, b). (∃ y. m a = Some y) ∧ b = the (m a)}"
    apply (simp add: image_def)
    by (smt Collect_cong case_prod_unfold fst_conv prod.collapse snd_conv)
  thus "finite {(a, b). (∃y. m a = Some y) ∧ b = the (m a)}"
    by auto
qed

lemma dom_finite: "finite (dom m)"
by (simp add: elems_finite dom_elems)

lemma ran_finite: "finite (ran m)"
by (simp add: elems_finite ran_elems)

(*<*)
abbreviation map_elems :: "('k ⇀ 'v) ⇒ ('k × 'v) set"
where
  "map_elems M ≡ {(a, b). M a = Some b}"

lemma map_elems_card: "card (map_elems m) = card (Map.dom m)"
proof-
  have "Map.dom m = fst ` {(a, b). m a = Some b}"
    by force
  also have "card … = card {(a, b). m a = Some b}"
    by (subst card_image, auto simp: inj_on_def)
  finally show ?thesis by simp
qed
(*>*)

lemma dom_elems_card: "card (dom m) = card (elems m)"
by (simp add: elems_def_alt FMap.dom_def map_elems_card)

lemma dom_ran_card: "card (dom m) ≥ card (ran m)"
by (simp add: ran_elems dom_elems_card elems_finite card_image_le)

lemma ran_dom_card: "card (ran m) ≤ card (dom m)"
by (simp add: dom_ran_card)

lemma ran_elems_card: "card (ran m) ≤ card (elems m)"
by (metis dom_elems_card dom_ran_card)

subsection {* The empty map *}

lift_definition empty :: "('k ↪ 'v)"
is "Map.empty" by simp

lemma elems_empty: "elems x = {} ⟷ x = empty"
by (transfer, auto)

lemma dom_empty: "dom x = {} ⟷ x = empty"
by (auto simp add: dom_elems elems_empty)

lemma ran_empty: "ran x = {} ⟷ x = empty"
by (auto simp add: ran_elems elems_empty)

subsection {* Updating *}

lift_definition fmap_comp :: "('v ↪ 'w) => ('k ↪ 'v) => ('k ↪ 'w)" (infixl "|o'_m|" 55)
is map_comp
by (metis domIff finite_subset map_comp_simps(1) subsetI)

lemma fmap_comp_emptyL: "fmap_comp empty M = empty"
by (transfer, simp)

lemma fmap_comp_empty_R: "fmap_comp M empty = empty"
by (transfer, simp)

lift_definition fmap_add :: "('k ↪ 'v) => ('k ↪ 'v) => ('k ↪ 'v)" (infixl "|++|" 100)
is map_add
by simp

lemma fmap_add_emptyL: "fmap_add empty M = M"
by (transfer, simp)

lemma fmap_add_emptyR: "fmap_add M empty = M"
by (transfer, simp)

lift_definition restrict_fmap :: "('k ↪ 'v) => 'k set => ('k ↪ 'v)" (infixl "||`|" 110)
is restrict_map
by simp

lemma restrict_fmap_empty: "restrict_fmap M {} = empty"
by (transfer, simp)

lift_definition set :: "('k ↪ 'v) ⇒ 'k ⇒ 'v option ⇒ ('k ↪ 'v)"
is "λ m k v. m (k := v)"
by simp

lemma set_dom_some: "k ∈ dom (set M k (Some v))"
by (transfer, simp)

lemma set_ran_some: "v ∈ ran (set M k (Some v))"
  apply transfer
by (meson fun_upd_same ranI)

lemma set_elems_some: "(k, v) ∈ elems (set M k (Some v))"
by (transfer, simp)

lemma set_dom_none: "k ∉ dom (set M k None)"
by (transfer, simp)

subsection {* Lists of pairs *}

lift_definition fmap_of :: "('k × 'v) list ⇒ ('k ↪ 'v)"
is map_of
by (simp add: finite_dom_map_of)

lift_definition fmap_upds :: "('k ↪ 'v) ⇒ 'k list ⇒ 'v list ⇒ ('k ↪ 'v)"
is map_upds
by simp

subsection {* Mapping over values *}

lift_definition fmap_map :: "('v ⇒ 'w) ⇒ ('k ↪ 'v) ⇒ ('k ↪ 'w)"
is "λ f m x. Option.bind (m x) (Some ∘ f)"
by (smt Collect_cong Map.dom_def bind.simps comp_def domD mem_Collect_eq option.distinct)

lemma fmap_map_id: "fmap_map id m = m"
by (auto simp add: fmap_map_def map_fun_def fmap_inverse)

lemma fmap_map_comp: "fmap_map (g ∘ f) m = fmap_map g (fmap_map f m)"
  apply transfer
  apply auto
by (simp add: comp_def)

lemma fmap_map_dom: "dom m = dom (fmap_map f m)"
  apply transfer
  apply auto
by (meson bind_eq_Some_conv)

lemma fmap_map_ran: "ran (fmap_map f m) = f ` ran m"
  apply transfer
  apply auto
  apply (smt CollectD Map.ran_def bind_eq_Some_conv comp_apply image_iff option.sel ranI)
by (smt Map.ran_def bind_lunit comp_eq_dest_lhs mem_Collect_eq)

lemma fmap_map_empty: "fmap_map f empty = empty"
by (metis FMap.dom_empty fmap_map_dom)

subsection {* Relations *}

lift_definition fmap_rel :: "('v ⇒ 'w ⇒ bool) ⇒ ('k ↪ 'v) ⇒ ('k ↪ 'w) ⇒ bool"
is "λ R m1 m2. (dom m1 = dom m2 ∧ (∀ x ∈ dom m1. R (the (fmap m1 x)) (the (fmap m2 x))))".

(*<*)
axiomatization map_zip_with :: "('v ⇒ 'w ⇒ 'z) ⇒ ('k ⇀ 'v) ⇒ ('k ⇀ 'w) ⇒ ('k ⇀ 'z)"
where
  map_zip_with_elems: "map_elems (map_zip_with f m1 m2) = {(k, z). m1 k = Some v ∧ m2 k = Some w ∧ z = f v w}" and
  map_zip_with_dom1: "Map.dom (map_zip_with f m1 m2) ⊆ Map.dom m1" and
  map_zip_with_dom2: "Map.dom (map_zip_with f m1 m2) ⊆ Map.dom m2"
(*>*)

lift_definition fmap_zip_with :: "('v ⇒ 'w ⇒ 'z) ⇒ ('k ↪ 'v) ⇒ ('k ↪ 'w) ⇒ ('k ↪ 'z)"
is map_zip_with
by (meson finite_subset map_zip_with_dom1)

lemma fmap_zip_with_dom: "dom (fmap_zip_with f m1 m2) = {k. fmap m1 k ≠ None ∧ fmap m2 k ≠ None}"
sorry

lemma fmap_zip_with_ran: "ran (fmap_zip_with f m1 m2) = {c. ∃ k. fmap m1 k = Some a ∧ fmap m2 k = Some b ∧ c = f a b}"
sorry

abbreviation fmap_zip :: "('k ↪ 'v) ⇒ ('k ↪ 'w) ⇒ ('k ↪ 'v × 'w)"
where
  "fmap_zip ≡ fmap_zip_with Pair"

lemma fmap_zip_dom: "dom (fmap_zip m1 m2) = {k. fmap m1 k ≠ None ∧ fmap m2 k ≠ None}"
by (simp add: fmap_zip_with_dom)

lemma fmap_zip_ran: "ran (fmap_zip m1 m2) = {(a,b). ∃ k. fmap m1 k = Some a ∧ fmap m2 k = Some b}"
sorry

lemma fmap_zip_fst_ran: "fst ` ran (fmap_zip m1 m2) ⊆ ran m1"
sorry

lemma fmap_zip_fst: "dom m1 = dom m2 ⟹ m1 = fmap_map fst (fmap_zip m1 m2)"
sorry

lemma fmap_zip_snd_ran: "snd ` ran (fmap_zip m1 m2) ⊆ ran m2"
sorry

lemma fmap_zip_snd: "dom m1 = dom m2 ⟹ m2 = fmap_map snd (fmap_zip m1 m2)"
sorry

lemma fmap_zip_rel: "fmap_rel R m1 m2 ⟷ ran (fmap_zip m1 m2) ⊆ {(x, y). R x y}"
sorry

lift_definition fmap_le :: "('k ↪ 'v) => ('k ↪ 'v) => bool"  (infix "|⊆⇩m|" 50)
is map_le.

subsection {* BNF *}

(*<*)
lemma card_leq_ordLeq:
  assumes "finite x"
  assumes "finite y"
  assumes "card x ≤ card y"
  shows "ordLeq3 (card_of x) (card_of y)"
using assms
by (meson card_le_inj card_of_ordLeq)
(*>*)

bnf "'k ↪ 'v"
  map: fmap_map
  sets: ran
  bd: "BNF_Cardinal_Arithmetic.csum natLeq (card_of (UNIV :: 'k set))"
  wits: empty
  rel: fmap_rel
proof-
  show "fmap_map id = id"
    by (auto simp add: fmap_map_id)
next
  show "⋀ f g. fmap_map (g ∘ f) = fmap_map g ∘ fmap_map f"
    by (auto simp add: fmap_map_comp)
next
  show "⋀ x f g. (⋀z. z ∈ ran x ⟹ f z = g z) ⟹ fmap_map f x = fmap_map g x"
    apply transfer
    by (metis bind.simps comp_apply not_None_eq ranI)
next
  show "⋀f. ran ∘ fmap_map f = op ` f ∘ ran"
    by (auto simp add: fmap_map_ran)
next
  show "card_order (BNF_Cardinal_Arithmetic.csum natLeq (card_of UNIV))"
    apply (rule card_order_csum)
    apply (rule natLeq_card_order)
    by (rule card_of_card_order_on)
next
  show "BNF_Cardinal_Arithmetic.cinfinite (BNF_Cardinal_Arithmetic.csum natLeq (card_of UNIV))"
    apply (rule cinfinite_csum)
    apply (rule disjI1)
    by (rule natLeq_cinfinite)
next
  fix m :: "('k, 'v) fmap"
  have "ordLeq3 (card_of (ran m)) (card_of (dom m))"
    by (simp add: ran_dom_card ran_finite dom_finite card_leq_ordLeq)
  also have "ordLeq3 (card_of (dom m)) (card_of (UNIV::'k set))" (is "ordLeq3 _ ?U")
    by (simp add: card_of_mono1)
  also have "ordLeq3 ?U (BNF_Cardinal_Arithmetic.csum natLeq ?U)"
    by (rule ordLeq_csum2) (rule card_of_Card_order)
  finally show "ordLeq3 (card_of (ran m)) (BNF_Cardinal_Arithmetic.csum natLeq ?U)"
    using ordLeq_transitive
    by blast
next
  show "⋀R S. fmap_rel R OO fmap_rel S ≤ fmap_rel (R OO S)"
    by (smt fmap_rel.transfer pick_middlep predicate2I relcompp.relcompI)
next
  show "⋀R. fmap_rel R = (BNF_Def.Grp {x. ran x ⊆ {(x, y). R x y}} (fmap_map fst))¯¯ OO BNF_Def.Grp {x. ran x ⊆ {(x, y). R x y}} (fmap_map snd)"
    unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
    apply auto
    proof-
      show "⋀R x xa.
       fmap_rel R x xa ⟹
       ∃b. x = fmap_map fst b ∧
           ran b ⊆ {(x, y). R x y} ∧
           xa = fmap_map snd b ∧ ran b ⊆ {(x, y). R x y}"
        by (meson fmap_rel.abs_eq fmap_zip_fst fmap_zip_rel fmap_zip_snd)
    next
      show "⋀R b. ran b ⊆ {(x, y). R x y} ⟹
           fmap_rel R (fmap_map fst b) (fmap_map snd b)"
        unfolding fmap_rel_def
        apply auto
        apply (metis fmap_map_dom)
        apply (metis fmap_map_dom)
        proof-
          fix R m x
          assume "ran m ⊆ {(x, y). R x y}"
          assume "x ∈ dom (fmap_map fst m)"
          obtain a b where "fmap m x = Some (a, b)"
            by (metis `x ∈ FMap.dom (fmap_map fst m)` dom.rep_eq domD fmap_map_dom prod.swap_def swap_swap)
          have thea: "a = the (fmap (fmap_map fst m) x)"
            by (simp add: `fmap m x = Some (a, b)` fmap_map.rep_eq)
          have theb: "b = the (fmap (fmap_map snd m) x)"
            by (simp add: `fmap m x = Some (a, b)` fmap_map.rep_eq)
          have "R a b"
            using `FMap.ran m ⊆ {(x, y). R x y}` `fmap m x = Some (a, b)` ran.rep_eq ranI
            by fastforce
          thus "R (the (fmap (fmap_map fst m) x)) (the (fmap (fmap_map snd m) x))"
            by (simp add: thea theb)
        qed
    qed
next
  show "⋀x. x ∈ ran empty ⟹ False"
    by (simp add: empty.abs_eq empty.rsp ran.abs_eq)
qed

(*<*)
end
(*>*)

FTrie.thy

(* Title:      Finite N-ary Tries
   Author:     Michael Walker <mike@barrucadu.co.uk>, 2015
   Maintainer: Michael Walker <mike@barrucadu.co.uk>
*)

(* Bits of auxilliary proof not directly related to FTrie are not displayed in
the theory document. *)

(*<*)
theory FTrie
imports Main FMap
begin
(*>*)

section {* Finite N-ary Tries *}

text {*
A trie (also called a prefix tree) is a tree data structure used to implement
efficient associative arrays, where each edge is labelled with a symbol, and
each node may contain a value. Unlike search trees, the key associated with a
node is not stored in the node itself; a key is a list of the symbol values
used to traverse the tree to that point.

Usually, tries are used with string keys, where the edges are labelled with
charcters. For example,

\begin{center}
\begin{forest}
for tree={circle, draw, l sep=20pt}
[, [1,edge label={node[midway,left] {a}}
    [4,edge label={node[midway,left] {c}}]
    [1,edge label={node[midway,left] {d}}]
    [3,edge label={node[midway,right] {e}}]
  ]
  [2,edge label={node[midway,right] {b}}
    [3,edge label={node[midway,left] {y}}]
    [5,edge label={node[midway,right] {z}}]
  ]
]
\end{forest}
\end{center}

There are a few invariants associated with tries:

\begin{itemize}
\item Each of the outgoing edges of a node has a distinct label.
\item All leaf nodes contain a value.
\end{itemize}

Whilst the latter requirement may make it seem like a natural definition of
a trie is in terms of a datatype with two constructors, one for branches and
one for leafs, instead here we opt for requiring \emph{every} node to contain
a value:
*}

datatype ('k, 'v) ftrie = FTrie
  (val:  'v)
  (subs: "'k ↪ ('k, 'v) ftrie")

text {*
Here @{term ftrie} means \emph{finite trie}: a trie where each node has a finite
number of subtrees.
*}

subsection {* Elements, domain, and range *}

text {*
We can consider a node in a trie to be a map, if we just throw away the value.
*}

definition dom :: "('k, 'v) ftrie ⇒ 'k set"
where
 "dom ≡ FMap.dom ∘ subs"

definition ran :: "('k, 'v) ftrie  ⇒ ('k, 'v) ftrie set"
where
 "ran ≡ FMap.ran ∘ subs"

definition elems :: "('k, 'v) ftrie  ⇒ ('k × ('k, 'v) ftrie) set"
where
 "elems ≡ FMap.elems ∘ subs"

lemma dom_elems: "dom T = fst ` elems T"
by (simp add: dom_def elems_def FMap.dom_elems)

lemma ran_elems: "ran T = snd ` elems T"
by (simp add: ran_def elems_def FMap.ran_elems)

lemma elems_finite: "finite (elems T)"
by (simp add: elems_def FMap.elems_finite)

lemma dom_finite: "finite (dom T)"
by (simp add: dom_def FMap.dom_finite)

lemma ran_finite: "finite (ran T)"
by (simp add: ran_def FMap.ran_finite)

lemma dom_elems_card: "card (dom T) = card (elems T)"
by (simp add: dom_def elems_def FMap.dom_elems_card)

lemma dom_ran_card: "card (dom T) ≥ card (ran T)"
by (simp add: dom_def ran_def FMap.dom_ran_card)

lemma ran_dom_card: "card (ran T) ≤ card (dom T)"
by (simp add: dom_ran_card)

lemma ran_elems_card: "card (ran T) ≤ card (elems T)"
by (simp add: ran_def elems_def FMap.ran_elems_card)

subsection {* Leaves *}

text {*
A leaf is a node in the tree with no subtrees. As every node has a value, to construct
a leaf, we must provide one.
*}

definition leaf :: "'v ⇒ ('k, 'v) ftrie"
where
  "leaf v ≡ FTrie v empty"

text {*
However, as all Isabelle types are inhabited, we can also construct an arbitrary leaf.
This is probably useless.
*}

definition leaf_arb :: "('k, 'v) ftrie"
where
  "leaf_arb ≡ leaf (SOME v. True)"

definition is_leaf :: "('k, 'v) ftrie ⇒ bool"
where
  "is_leaf T ≡ subs T = empty"

lemma leaf_is_leaf: "is_leaf (leaf v)"
by (simp add: leaf_def is_leaf_def)

lemma leaf_arb_is_leaf: "is_leaf leaf_arb"
by (simp add: leaf_arb_def leaf_is_leaf)

lemma elems_leaf: "elems T = {} ⟷ is_leaf T"
by (simp add: elems_def is_leaf_def FMap.elems_empty)

lemma dom_empty: "dom T = {} ⟷ is_leaf T"
by (simp add: dom_def is_leaf_def FMap.dom_empty)

lemma ran_empty: "ran T = {} ⟷ is_leaf T"
by (simp add: ran_def is_leaf_def FMap.ran_empty)

subsection {* Updating *}

definition restrict_ftrie :: "('k, 'v) ftrie => 'k set => ('k, 'v) ftrie"
where
  "restrict_ftrie T ks ≡ FTrie (val T) (subs T ||`| ks)"

lemma restrict_ftrie_to_leaf: "is_leaf (restrict_ftrie T {})"
by (simp add: restrict_ftrie_def restrict_fmap_empty is_leaf_def)

lemma restrict_ftrie_is_leaf: "is_leaf T ⟷ T = restrict_ftrie T {}"
by (metis ftrie.exhaust_sel ftrie.sel(2) is_leaf_def restrict_ftrie_def restrict_ftrie_to_leaf)

definition set :: "('k, 'v) ftrie ⇒ 'k ⇒ 'v option ⇒ ('k, 'v) ftrie"
where
  "set T k v = FTrie (val T) (FMap.set (subs T) k (Option.bind v (Some ∘ leaf)))"

lemma set_dom_some: "k ∈ dom (set T k (Some v))"
by (simp add: set_def Option.bind_def dom_def FMap.set_dom_some)

lemma set_ran_some: "leaf v ∈ ran (set T k (Some v))"
by (simp add: set_def Option.bind_def ran_def FMap.set_ran_some)

lemma set_elems_some: "(k, leaf v) ∈ elems (set T k (Some v))"
by (simp add: set_def Option.bind_def elems_def FMap.set_elems_some)

lemma set_dom_none: "k ∉ dom (set T k None)"
by (simp add: set_def Option.bind_def dom_def FMap.set_dom_none)

subsection {* Mapping over values *}

function ftrie_map :: "('v ⇒ 'w) ⇒ ('k, 'v) ftrie ⇒ ('k, 'w) ftrie"
where
  "ftrie_map f T = FTrie (f (val T)) (fmap_map (ftrie_map f) (subs T))"
by auto

lemma ftrie_map_id: "ftrie_map id T = T"
sorry

lemma ftrie_map_comp: "ftrie_map (g ∘ f) T = ftrie_map g (ftrie_map f T)"
sorry

lemma ftrie_map_dom: "dom T = dom (ftrie_map f T)"
sorry

lemma ftrie_map_ran: "ran (ftrie_map f T) = ftrie_map f ` ran T"
sorry

subsection {* Folding *}

function same_shape :: "('k, 'v) ftrie ⇒ ('k, 'w) ftrie ⇒ bool"
where
  "same_shape T1 T2 = (dom T1 = dom T2 ∧ (∀ k ∈ dom T1. same_shape (the (fmap (subs T1) k)) (the (fmap (subs T2) k))))"
by auto

function ftrie_collapse :: "('v ⇒ 'v ⇒ 'v) ⇒ ('k, 'v) ftrie ⇒ 'v"
where
  "ftrie_collapse f (FTrie v ss) = folding.F (λ t v'. f (ftrie_collapse f t) v') v (FMap.ran ss)"
by (auto, metis ftrie.collapse)

function ftrie_zip :: "('v ⇒ 'w ⇒ 'z) ⇒ ('k, 'v) ftrie ⇒ ('k, 'w) ftrie ⇒ ('k, 'z) ftrie"
where
  "ftrie_zip f (FTrie v L) (FTrie w R) = FTrie (f v w) (fmap_zip_with (ftrie_zip f) L R)"
by (auto, metis ftrie.collapse)

definition ftrie_rel :: "('v ⇒ 'w ⇒ bool) ⇒ ('k, 'v) ftrie ⇒ ('k, 'w) ftrie ⇒ bool"
where
  "ftrie_rel R T1 T2 ≡ same_shape T1 T2 ∧ ftrie_collapse (λ a b. a ∧ b) (ftrie_zip R T1 T2)"

(*<*)
end
(*>*)

PORType.thy

theory PORType
imports Main ThreadType FSet "~/projects/isabelle-library/FTrie"
begin

datatype PNode = PNode
  (therunnable: "ThreadId fset")
  (thetodo: "ThreadId fset")

type_synonym POR = "(ThreadId, PNode) ftrie"

locale this_por_well_formed =
fixes p
assumes todo_runnable: "thetodo (val p) |⊆| therunnable (val p)"
  and done_runnable: "dom p ⊆ fset (therunnable (val p))"
  and todo_done_disjoint: "fset (thetodo (val p)) ∩ dom p = {}"

inductive por_well_formed :: "POR ⇒ bool" where
por_wf_intro [intro]:"⟦ this_por_well_formed por; 
   ∀ p ∈ ran por. por_well_formed p ⟧ 
   ⟹ por_well_formed por"

definition
  initial_pnode :: PNode
where
  "initial_pnode ≡ PNode {| initial_thread |} {| initial_thread |}"

definition
  initial_por :: POR
where
  "initial_por ≡ leaf initial_pnode"

lemma terminal_por_well_formed [simp]:
  assumes "thetodo (val por) |⊆| therunnable (val por)"
  assumes "subs por = empty"
  shows "por_well_formed por"

  apply (rule por_wf_intro)
  apply (unfold_locales)
  apply (unfold dom_def ran_def elems_def)
  apply (simp_all add: assms)
  using FMap.dom_empty apply fastforce
  using FMap.dom_empty apply fastforce
using FMap.ran_empty
by fastforce

lemma initial_por_well_formed: "por_well_formed initial_por"
  apply (unfold initial_por_def initial_pnode_def leaf_def)
by auto

typedef por = "{por. por_well_formed por}"
  apply (rule_tac x="initial_por" in exI)
by (simp add: initial_por_well_formed)

setup_lifting type_definition_por

lift_definition psubs :: "por ⇒ ThreadId ↪ por"
  is subs
(*Lifting failed for the following types:
Raw type:  'a ↪ ('a, 'b) ftrie
Abstract type:  ThreadId ↪ por

Reason:  No relator for the type "FMap.fmap" found.

'subs' is from:

datatype ('k, 'v) ftrie = FTrie
  (val:  'v)
  (subs: "'k ↪ ('k, 'v) ftrie")*)

end