# Theory Term

Up to index of Isabelle/ZF/Induct

theory Term
imports Main
begin

    (*  Title:      ZF/Induct/Term.thy
        ID:         $Id: Term.thy,v 1.4 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Terms over an alphabet *}

    theory Term imports Main begin

    text {*
      Illustrates the list functor (essentially the same type as in @{text
      Trees_Forest}).
    *}

    consts
      "term" :: "i => i"

    datatype "term(A)" = Apply ("a ∈ A", "l ∈ list(term(A))")
      monos list_mono
      type_elims list_univ [THEN subsetD, elim_format]

    declare Apply [TC]

    constdefs
      term_rec :: "[i, [i, i, i] => i] => i"
      "term_rec(t,d) ==
        Vrec(t, λt g. term_case(λx zs. d(x, zs, map(λz. g`z, zs)), t))"

      term_map :: "[i => i, i] => i"
      "term_map(f,t) == term_rec(t, λx zs rs. Apply(f(x), rs))"

      term_size :: "i => i"
      "term_size(t) == term_rec(t, λx zs rs. succ(list_add(rs)))"

      reflect :: "i => i"
      "reflect(t) == term_rec(t, λx zs rs. Apply(x, rev(rs)))"

      preorder :: "i => i"
      "preorder(t) == term_rec(t, λx zs rs. Cons(x, flat(rs)))"

      postorder :: "i => i"
      "postorder(t) == term_rec(t, λx zs rs. flat(rs) @ [x])"

    lemma term_unfold: "term(A) = A * list(term(A))"
      by (fast intro!: term.intros [unfolded term.con_defs]
        elim: term.cases [unfolded term.con_defs])

    lemma term_induct2:
      "[| t ∈ term(A);
          !!x.      [| x ∈ A |] ==> P(Apply(x,Nil));
          !!x z zs. [| x ∈ A;  z ∈ term(A);  zs: list(term(A));  P(Apply(x,zs))
                    |] ==> P(Apply(x, Cons(z,zs)))
         |] ==> P(t)"
      -- {* Induction on @{term "term(A)"} followed by induction on @{term list}. *}
      apply (induct_tac t)
      apply (erule list.induct)
       apply (auto dest: list_CollectD)
      done

    lemma term_induct_eqn:
      "[| t ∈ term(A);
          !!x zs. [| x ∈ A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==>
                  f(Apply(x,zs)) = g(Apply(x,zs))
       |] ==> f(t) = g(t)"
      -- {* Induction on @{term "term(A)"} to prove an equation. *}
      apply (induct_tac t)
      apply (auto dest: map_list_Collect list_CollectD)
      done

    text {*
      \medskip Lemmas to justify using @{term "term"} in other recursive
      type definitions.
    *}

    lemma term_mono: "A ⊆ B ==> term(A) ⊆ term(B)"
      apply (unfold term.defs)
      apply (rule lfp_mono)
        apply (rule term.bnd_mono)+
      apply (rule univ_mono basic_monos| assumption)+
      done

    lemma term_univ: "term(univ(A)) ⊆ univ(A)"
      -- {* Easily provable by induction also *}
      apply (unfold term.defs term.con_defs)
      apply (rule lfp_lowerbound)
       apply (rule_tac [2] A_subset_univ [THEN univ_mono])
      apply safe
      apply (assumption | rule Pair_in_univ list_univ [THEN subsetD])+
      done

    lemma term_subset_univ: "A ⊆ univ(B) ==> term(A) ⊆ univ(B)"
      apply (rule subset_trans)
       apply (erule term_mono)
      apply (rule term_univ)
      done

    lemma term_into_univ: "[| t ∈ term(A);  A ⊆ univ(B) |] ==> t ∈ univ(B)"
      by (rule term_subset_univ [THEN subsetD])

    text {*
      \medskip @{text term_rec} -- by @{text Vset} recursion.
    *}

    lemma map_lemma: "[| l ∈ list(A);  Ord(i);  rank(l)<i |]
        ==> map(λz. (λx ∈ Vset(i).h(x)) ` z, l) = map(h,l)"
      -- {* @{term map} works correctly on the underlying list of terms. *}
      apply (induct set: list)
       apply simp
      apply (subgoal_tac "rank (a) <i & rank (l) < i")
       apply (simp add: rank_of_Ord)
      apply (simp add: list.con_defs)
      apply (blast dest: rank_rls [THEN lt_trans])
      done

    lemma term_rec [simp]: "ts ∈ list(A) ==>
      term_rec(Apply(a,ts), d) = d(a, ts, map (λz. term_rec(z,d), ts))"
      -- {* Typing premise is necessary to invoke @{text map_lemma}. *}
      apply (rule term_rec_def [THEN def_Vrec, THEN trans])
      apply (unfold term.con_defs)
      apply (simp add: rank_pair2 map_lemma)
      done

    lemma term_rec_type:
      "[| t ∈ term(A);
          !!x zs r. [| x ∈ A;  zs: list(term(A));
                       r ∈ list(\<Union>t ∈ term(A). C(t)) |]
                    ==> d(x, zs, r): C(Apply(x,zs))
       |] ==> term_rec(t,d) ∈ C(t)"
      -- {* Slightly odd typing condition on @{text r} in the second premise! *}
    proof -
      assume a: "!!x zs r. [| x ∈ A;  zs: list(term(A));
                       r ∈ list(\<Union>t ∈ term(A). C(t)) |]
                    ==> d(x, zs, r): C(Apply(x,zs))"
      assume "t ∈ term(A)"
      thus ?thesis
        apply induct
        apply (frule list_CollectD)
        apply (subst term_rec)
         apply (assumption | rule a)+
        apply (erule list.induct)
         apply (simp add: term_rec)
       apply (auto simp add: term_rec)
       done
    qed

    lemma def_term_rec:
      "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==>
        j(Apply(a,ts)) = d(a, ts, map(λZ. j(Z), ts))"
      apply (simp only:)
      apply (erule term_rec)
      done

    lemma term_rec_simple_type [TC]:
      "[| t ∈ term(A);
          !!x zs r. [| x ∈ A;  zs: list(term(A));  r ∈ list(C) |]
                    ==> d(x, zs, r): C
       |] ==> term_rec(t,d) ∈ C"
      apply (erule term_rec_type)
      apply (drule subset_refl [THEN UN_least, THEN list_mono, THEN subsetD])
      apply simp
      done

    text {*
      \medskip @{term term_map}.
    *}

    lemma term_map [simp]:
      "ts ∈ list(A) ==>
        term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
      by (rule term_map_def [THEN def_term_rec])

    lemma term_map_type [TC]:
        "[| t ∈ term(A);  !!x. x ∈ A ==> f(x): B |] ==> term_map(f,t) ∈ term(B)"
      apply (unfold term_map_def)
      apply (erule term_rec_simple_type)
      apply fast
      done

    lemma term_map_type2 [TC]:
        "t ∈ term(A) ==> term_map(f,t) ∈ term({f(u). u ∈ A})"
      apply (erule term_map_type)
      apply (erule RepFunI)
      done

    text {*
      \medskip @{term term_size}.
    *}

    lemma term_size [simp]:
        "ts ∈ list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
      by (rule term_size_def [THEN def_term_rec])

    lemma term_size_type [TC]: "t ∈ term(A) ==> term_size(t) ∈ nat"
      by (auto simp add: term_size_def)

    text {*
      \medskip @{text reflect}.
    *}

    lemma reflect [simp]:
        "ts ∈ list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
      by (rule reflect_def [THEN def_term_rec])

    lemma reflect_type [TC]: "t ∈ term(A) ==> reflect(t) ∈ term(A)"
      by (auto simp add: reflect_def)

    text {*
      \medskip @{text preorder}.
    *}

    lemma preorder [simp]:
        "ts ∈ list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
      by (rule preorder_def [THEN def_term_rec])

    lemma preorder_type [TC]: "t ∈ term(A) ==> preorder(t) ∈ list(A)"
      by (simp add: preorder_def)

    text {*
      \medskip @{text postorder}.
    *}

    lemma postorder [simp]:
        "ts ∈ list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
      by (rule postorder_def [THEN def_term_rec])

    lemma postorder_type [TC]: "t ∈ term(A) ==> postorder(t) ∈ list(A)"
      by (simp add: postorder_def)

    text {*
      \medskip Theorems about @{text term_map}.
    *}

    declare List.map_compose [simp]

    lemma term_map_ident: "t ∈ term(A) ==> term_map(λu. u, t) = t"
      apply (erule term_induct_eqn)
      apply simp
      done

    lemma term_map_compose:
        "t ∈ term(A) ==> term_map(f, term_map(g,t)) = term_map(λu. f(g(u)), t)"
      apply (erule term_induct_eqn)
      apply simp
      done

    lemma term_map_reflect:
        "t ∈ term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"
      apply (erule term_induct_eqn)
      apply (simp add: rev_map_distrib [symmetric])
      done

    text {*
      \medskip Theorems about @{text term_size}.
    *}

    lemma term_size_term_map: "t ∈ term(A) ==> term_size(term_map(f,t)) = term_size(t)"
      apply (erule term_induct_eqn)
      apply simp
      done

    lemma term_size_reflect: "t ∈ term(A) ==> term_size(reflect(t)) = term_size(t)"
      apply (erule term_induct_eqn)
      apply (simp add: rev_map_distrib [symmetric] list_add_rev)
      done

    lemma term_size_length: "t ∈ term(A) ==> term_size(t) = length(preorder(t))"
      apply (erule term_induct_eqn)
      apply (simp add: length_flat)
      done

    text {*
      \medskip Theorems about @{text reflect}.
    *}

    lemma reflect_reflect_ident: "t ∈ term(A) ==> reflect(reflect(t)) = t"
      apply (erule term_induct_eqn)
      apply (simp add: rev_map_distrib)
      done

    text {*
      \medskip Theorems about preorder.
    *}

    lemma preorder_term_map:
        "t ∈ term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
      apply (erule term_induct_eqn)
      apply (simp add: map_flat)
      done

    lemma preorder_reflect_eq_rev_postorder:
        "t ∈ term(A) ==> preorder(reflect(t)) = rev(postorder(t))"
      apply (erule term_induct_eqn)
      apply (simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
      done

    end

lemma term_unfold:

      term(A) = A × list(term(A))

lemma term_induct2:

      [| t ∈ term(A); !!x. x ∈ A ==> P(Apply(x, []));
         !!x z zs.
            [| x ∈ A; z ∈ term(A); zs ∈ list(term(A)); P(Apply(x, zs)) |]
            ==> P(Apply(x, Cons(z, zs))) |]
      ==> P(t)

lemma term_induct_eqn:

      [| t ∈ term(A);
         !!x zs.
            [| x ∈ A; zs ∈ list(term(A)); map(f, zs) = map(g, zs) |]
            ==> f(Apply(x, zs)) = g(Apply(x, zs)) |]
      ==> f(t) = g(t)

lemma term_mono:

      A ⊆ B ==> term(A) ⊆ term(B)

lemma term_univ:

      term(univ(A)) ⊆ univ(A)

lemma term_subset_univ:

      A ⊆ univ(B) ==> term(A) ⊆ univ(B)

lemma term_into_univ:

      [| t ∈ term(A); A ⊆ univ(B) |] ==> t ∈ univ(B)

lemma map_lemma:

      [| l ∈ list(A); Ord(i); rank(l) < i |]
      ==> map(%z. (λx∈Vset(i). h(x)) ` z, l) = map(h, l)

lemma term_rec:

      ts ∈ list(A)
      ==> term_rec(Apply(a, ts), d) = d(a, ts, map(%z. term_rec(z, d), ts))

lemma term_rec_type:

      [| t ∈ term(A);
         !!x zs r.
            [| x ∈ A; zs ∈ list(term(A)); r ∈ list(\<Union>t∈term(A). C(t)) |]
            ==> d(x, zs, r) ∈ C(Apply(x, zs)) |]
      ==> term_rec(t, d) ∈ C(t)

lemma def_term_rec:

      [| !!t. j(t) == term_rec(t, d); ts ∈ list(A) |]
      ==> j(Apply(a, ts)) = d(a, ts, map(%Z. j(Z), ts))

lemma term_rec_simple_type:

      [| t ∈ term(A);
         !!x zs r. [| x ∈ A; zs ∈ list(term(A)); r ∈ list(C) |] ==> d(x, zs, r) ∈ C |]
      ==> term_rec(t, d) ∈ C

lemma term_map:

      ts ∈ list(A) ==> term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))

lemma term_map_type:

      [| t ∈ term(A); !!x. x ∈ A ==> f(x) ∈ B |] ==> term_map(f, t) ∈ term(B)

lemma term_map_type2:

      t ∈ term(A) ==> term_map(f, t) ∈ term({f(u) . u ∈ A})

lemma term_size:

      ts ∈ list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))

lemma term_size_type:

      t ∈ term(A) ==> term_size(t) ∈ nat

lemma reflect:

      ts ∈ list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))

lemma reflect_type:

      t ∈ term(A) ==> reflect(t) ∈ term(A)

lemma preorder:

      ts ∈ list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))

lemma preorder_type:

      t ∈ term(A) ==> preorder(t) ∈ list(A)

lemma postorder:

      ts ∈ list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]

lemma postorder_type:

      t ∈ term(A) ==> postorder(t) ∈ list(A)

lemma term_map_ident:

      t ∈ term(A) ==> term_map(%u. u, t) = t

lemma term_map_compose:

      t ∈ term(A) ==> term_map(f, term_map(g, t)) = term_map(%u. f(g(u)), t)

lemma term_map_reflect:

      t ∈ term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f, t))

lemma term_size_term_map:

      t ∈ term(A) ==> term_size(term_map(f, t)) = term_size(t)

lemma term_size_reflect:

      t ∈ term(A) ==> term_size(reflect(t)) = term_size(t)

lemma term_size_length:

      t ∈ term(A) ==> term_size(t) = length(preorder(t))

lemma reflect_reflect_ident:

      t ∈ term(A) ==> reflect(reflect(t)) = t

lemma preorder_term_map:

      t ∈ term(A) ==> preorder(term_map(f, t)) = map(f, preorder(t))

lemma preorder_reflect_eq_rev_postorder:

      t ∈ term(A) ==> preorder(reflect(t)) = rev(postorder(t))