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

FTNode_def

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

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

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

fmap_bij_thm

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

fmaptree_TY_DEF

⊢ ∃rep. TYPE_DEFINITION wf rep

fmtreerec_def

⊢ ∀h ft. fmtreerec h ft = @r. relrec h ft r

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

item_map_def

⊢ ∀ft. ft = FTNode (item ft) (map ft)

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)

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

wf_def

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

Theorems

FTNode_11

⊢ (FTNode i1 f1 = FTNode i2 f2) ⇔ (i1 = i2) ∧ (f1 = f2)

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

fmaptree_nchotomy

⊢ ∀ft. ∃i fm. ft = FTNode i fm

fmtree_Axiom

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

fmtreerec_thm

⊢ fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm

ft_ind

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

item_thm

⊢ item (FTNode i fm) = i

map_thm

⊢ map (FTNode i fm) = fm

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)

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_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_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

wf_cases

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

wf_ind

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

wf_rules

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

wf_strongind

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