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

wf_def

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

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

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)

item_map_def

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

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

FTNode_def

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

fmtreerec_def

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

fmaptree_TY_DEF

⊢ ∃rep. TYPE_DEFINITION wf rep

fmap_bij_thm

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

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

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

Theorems

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

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

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

map_thm

⊢ map (FTNode i fm) = fm

item_thm

⊢ item (FTNode i fm) = i

FTNode_11

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

ft_ind

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

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)

fmaptree_nchotomy

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

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

applicable_paths_FINITE

⊢ ∀ft. FINITE {p | (∃ft'. apply_path p ft = SOME ft')}