Structure fmaptreeTheory

signature fmaptreeTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val FTNode_def : thm
    val apply_path_def : thm
    val construct_def : thm
    val fmap_bij_thm : thm
    val fmaptree_TY_DEF : thm
    val fmtreerec_def : thm
    val fupd_at_path_def : thm
    val item_map_def : thm
    val relrec_def : thm
    val update_at_path_def : thm
    val wf_def : thm

  (*  Theorems  *)
    val FTNode_11 : thm
    val applicable_paths_FINITE : thm
    val apply_path_SNOC : thm
    val fmaptree_nchotomy : thm
    val fmtree_Axiom : thm
    val fmtreerec_thm : thm
    val ft_ind : thm
    val item_thm : thm
    val map_thm : thm
    val relrec_cases : thm
    val relrec_ind : thm
    val relrec_rules : thm
    val relrec_strongind : thm
    val wf_cases : thm
    val wf_ind : thm
    val wf_rules : thm
    val wf_strongind : thm

  val fmaptree_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [finite_map] Parent theory of "fmaptree"

   [FTNode_def]  Definition

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

   [apply_path_def]  Definition

      |- (∀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]  Definition

      |- ∀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]  Definition

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

   [fmaptree_TY_DEF]  Definition

      |- ∃rep. TYPE_DEFINITION wf rep

   [fmtreerec_def]  Definition

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

   [fupd_at_path_def]  Definition

      |- (∀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]  Definition

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

   [relrec_def]  Definition

      |- 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]  Definition

      |- (∀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]  Definition

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

   [FTNode_11]  Theorem

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

   [applicable_paths_FINITE]  Theorem

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

   [apply_path_SNOC]  Theorem

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

   [fmaptree_nchotomy]  Theorem

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

   [fmtree_Axiom]  Theorem

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

   [fmtreerec_thm]  Theorem

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

   [ft_ind]  Theorem

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

   [item_thm]  Theorem

      |- item (FTNode i fm) = i

   [map_thm]  Theorem

      |- map (FTNode i fm) = fm

   [relrec_cases]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

      |- ∀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]  Theorem

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

   [wf_ind]  Theorem

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

   [wf_rules]  Theorem

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

   [wf_strongind]  Theorem

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


*)
end

HOL 4, Kananaskis-10