Theory "fmaptree"

Parents finite_map

Signature

Type	Arity
fmaptree	2
Constant	Type
FTNode	:β -> (α \|-> (α, β) fmaptree) -> (α, β) fmaptree
apply_path	:α list -> (α, β) fmaptree -> (α, β) fmaptree option
construct	:α -> (β \|-> (β list -> α option)) -> β list -> α option
fmtreerec	:(β -> (γ \|-> α) -> (γ \|-> (γ, β) fmaptree) -> α) -> (γ, β) fmaptree -> α
fromF	:('key list -> 'value option) -> ('key, 'value) fmaptree
fupd_at_path	:α list -> ((α, β) fmaptree -> (α, β) fmaptree option) -> (α, β) fmaptree -> (α, β) fmaptree option
item	:(α, β) fmaptree -> β
map	:(α, β) fmaptree -> (α \|-> (α, β) fmaptree)
relrec	:(α -> (β \|-> γ) -> (β \|-> (β, α) fmaptree) -> γ) -> (β, α) fmaptree -> γ -> bool
toF	:('key, 'value) fmaptree -> 'key list -> 'value option
update_at_path	:α list -> β -> (α, β) fmaptree -> (α, β) fmaptree option
wf	:(β list -> α option) -> bool

Definitions

construct_def

|- ∀a kfm kl.
     construct a kfm kl =
     case kl of
       [] => SOME a
     | h::t => if h ∈ FDOM kfm then kfm ' h t else NONE

wf_def

|- wf =
   (λa0.
      ∀wf'.
        (∀a0.
           (∃a fm. (a0 = construct a fm) ∧ ∀k. k ∈ FDOM fm ⇒ wf' (fm ' k)) ⇒
           wf' a0) ⇒
        wf' a0)

fmaptree_TY_DEF

|- ∃rep. TYPE_DEFINITION wf rep

fmap_bij_thm

|- (∀a. fromF (toF a) = a) ∧ ∀r. wf r ⇔ (toF (fromF r) = r)

FTNode_def

|- ∀i fm. FTNode i fm = fromF (construct i (toF o_f fm))

item_map_def

|- ∀ft. ft = FTNode (item ft) (map ft)

apply_path_def

|- (∀ft. apply_path [] ft = SOME ft) ∧
   ∀h t ft.
     apply_path (h::t) ft =
     if h ∈ FDOM (map ft) then apply_path t (map ft ' h) else NONE

update_at_path_def

|- (∀a ft. update_at_path [] a ft = SOME (FTNode a (map ft))) ∧
   ∀h t a ft.
     update_at_path (h::t) a ft =
     if h ∈ FDOM (map ft) then
       case update_at_path t a (map ft ' h) of
         NONE => NONE
       | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h,ft')))
     else NONE

fupd_at_path_def

|- (∀f ft. fupd_at_path [] f ft = f ft) ∧
   ∀h t f ft.
     fupd_at_path (h::t) f ft =
     if h ∈ FDOM (map ft) then
       case fupd_at_path t f (map ft ' h) of
         NONE => NONE
       | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h,ft')))
     else NONE

relrec_def

|- relrec =
   (λh a0 a1.
      ∀relrec'.
        (∀a0 a1.
           (∃i fm rfm.
              (a0 = FTNode i fm) ∧ (a1 = h i rfm fm) ∧ (FDOM rfm = FDOM fm) ∧
              ∀d. d ∈ FDOM fm ⇒ relrec' (fm ' d) (rfm ' d)) ⇒
           relrec' a0 a1) ⇒
        relrec' a0 a1)

fmtreerec_def

|- ∀h ft. fmtreerec h ft = @r. relrec h ft r

Theorems

wf_rules

|- ∀a fm. (∀k. k ∈ FDOM fm ⇒ wf (fm ' k)) ⇒ wf (construct a fm)

wf_ind

|- ∀wf'.
     (∀a fm. (∀k. k ∈ FDOM fm ⇒ wf' (fm ' k)) ⇒ wf' (construct a fm)) ⇒
     ∀a0. wf a0 ⇒ wf' a0

wf_strongind

|- ∀wf'.
     (∀a fm.
        (∀k. k ∈ FDOM fm ⇒ wf (fm ' k) ∧ wf' (fm ' k)) ⇒
        wf' (construct a fm)) ⇒
     ∀a0. wf a0 ⇒ wf' a0

wf_cases

|- ∀a0. wf a0 ⇔ ∃a fm. (a0 = construct a fm) ∧ ∀k. k ∈ FDOM fm ⇒ wf (fm ' k)

FTNode_11

|- (FTNode i1 f1 = FTNode i2 f2) ⇔ (i1 = i2) ∧ (f1 = f2)

fmaptree_nchotomy

|- ∀ft. ∃i fm. ft = FTNode i fm

item_thm

|- item (FTNode i fm) = i

map_thm

|- map (FTNode i fm) = fm

ft_ind

|- ∀P. (∀a fm. (∀k. k ∈ FDOM fm ⇒ P (fm ' k)) ⇒ P (FTNode a fm)) ⇒ ∀ft. P ft

applicable_paths_FINITE

|- ∀ft. FINITE {p | ∃ft'. apply_path p ft = SOME ft'}

apply_path_SNOC

|- ∀ft x p.
     apply_path (p ++ [x]) ft =
     case apply_path p ft of NONE => NONE | SOME ft' => FLOOKUP (map ft') x

relrec_rules

|- ∀h i fm rfm.
     (FDOM rfm = FDOM fm) ∧ (∀d. d ∈ FDOM fm ⇒ relrec h (fm ' d) (rfm ' d)) ⇒
     relrec h (FTNode i fm) (h i rfm fm)

relrec_ind

|- ∀h relrec'.
     (∀i fm rfm.
        (FDOM rfm = FDOM fm) ∧
        (∀d. d ∈ FDOM fm ⇒ relrec' (fm ' d) (rfm ' d)) ⇒
        relrec' (FTNode i fm) (h i rfm fm)) ⇒
     ∀a0 a1. relrec h a0 a1 ⇒ relrec' a0 a1

relrec_strongind

|- ∀h relrec'.
     (∀i fm rfm.
        (FDOM rfm = FDOM fm) ∧
        (∀d.
           d ∈ FDOM fm ⇒
           relrec h (fm ' d) (rfm ' d) ∧ relrec' (fm ' d) (rfm ' d)) ⇒
        relrec' (FTNode i fm) (h i rfm fm)) ⇒
     ∀a0 a1. relrec h a0 a1 ⇒ relrec' a0 a1

relrec_cases

|- ∀h a0 a1.
     relrec h a0 a1 ⇔
     ∃i fm rfm.
       (a0 = FTNode i fm) ∧ (a1 = h i rfm fm) ∧ (FDOM rfm = FDOM fm) ∧
       ∀d. d ∈ FDOM fm ⇒ relrec h (fm ' d) (rfm ' d)

fmtreerec_thm

|- fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm

fmtree_Axiom

|- ∀h. ∃f. ∀i fm. f (FTNode i fm) = h i fm (f o_f fm)