(* Title: ZF/Induct/Term.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
section ‹Terms over an alphabet
›
theory Term imports ZF
begin
text ‹
Illustrates the list functor (essentially the same type as
in ‹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]
definition
term_rec ::
"[i, [i, i, i] \ i] \ i" where
"term_rec(t,d) \
Vrec(t, λt g. term_case(λx zs. d(x, zs, map(λz. g`z, zs)), t))
"
definition
term_map ::
"[i \ i, i] \ i" where
"term_map(f,t) \ term_rec(t, \x zs rs. Apply(f(x), rs))"
definition
term_size ::
"i \ i" where
"term_size(t) \ term_rec(t, \x zs rs. succ(list_add(rs)))"
definition
reflect ::
"i \ i" where
"reflect(t) \ term_rec(t, \x zs rs. Apply(x, rev(rs)))"
definition
preorder ::
"i \ i" where
"preorder(t) \ term_rec(t, \x zs rs. Cons(x, flat(rs)))"
definition
postorder ::
"i \ i" where
"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(A)
› followed
by induction on
🍋‹list
›.
›
apply (induct_tac t)
apply (erule list.induct)
apply (auto dest: list_CollectD)
done
lemma term_induct_eqn [consumes 1, case_names
Apply]:
"\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(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› in other recursive
type definitions.
›
lemma term_mono:
"A \ B \ term(A) \ term(B)"
unfolding 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›
unfolding 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 ‹term_rec
› --
by ‹Vset
› recursion.
›
lemma map_lemma:
"\l \ list(A); Ord(i); rank(l)
==> map(λz. (λx
∈ Vset(i).h(x)) ` z, l) = map(h,l)
"
🍋 ‹🍋‹map
› works correctly on the underlying list of terms.
›
apply (induct set: list)
apply simp
apply (subgoal_tac
"rank (a) 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 ‹map_lemma
›.
›
apply (rule term_rec_def [
THEN def_Vrec,
THEN trans])
unfolding term.con_defs
apply (simp add: rank_pair2 map_lemma)
done
lemma term_rec_type:
assumes t:
"t \ term(A)"
and a:
"\x zs r. \x \ A; zs: list(term(A));
r
∈ list(
∪t
∈ term(A). C(t))
]
==> d(x, zs, r): C(
Apply(x,zs))
"
shows "term_rec(t,d) \ C(t)"
🍋 ‹Slightly odd typing condition on
‹r
› in the second premise!
›
using t
apply induct
apply (frule list_CollectD)
apply (subst term_rec)
apply (assumption | rule a)+
apply (erule list.induct)
apply auto
done
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_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)"
unfolding 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_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 ‹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 ‹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 ‹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
‹term_map
›.
›
declare map_compose [simp]
lemma term_map_ident:
"t \ term(A) \ term_map(\u. u, t) = t"
by (induct rule: term_induct_eqn) simp
lemma term_map_compose:
"t \ term(A) \ term_map(f, term_map(g,t)) = term_map(\u. f(g(u)), t)"
by (induct rule: term_induct_eqn) simp
lemma term_map_reflect:
"t \ term(A) \ term_map(f, reflect(t)) = reflect(term_map(f,t))"
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric])
text ‹
\medskip Theorems about
‹term_size
›.
›
lemma term_size_term_map:
"t \ term(A) \ term_size(term_map(f,t)) = term_size(t)"
by (induct rule: term_induct_eqn) simp
lemma term_size_reflect:
"t \ term(A) \ term_size(reflect(t)) = term_size(t)"
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric] list_add_rev)
lemma term_size_length:
"t \ term(A) \ term_size(t) = length(preorder(t))"
by (induct rule: term_induct_eqn) (simp add: length_flat)
text ‹
\medskip Theorems about
‹reflect
›.
›
lemma reflect_reflect_ident:
"t \ term(A) \ reflect(reflect(t)) = t"
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib)
text ‹
\medskip Theorems about preorder.
›
lemma preorder_term_map:
"t \ term(A) \ preorder(term_map(f,t)) = map(f, preorder(t))"
by (induct rule: term_induct_eqn) (simp add: map_flat)
lemma preorder_reflect_eq_rev_postorder:
"t \ term(A) \ preorder(reflect(t)) = rev(postorder(t))"
by (induct rule: term_induct_eqn)
(simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
end
