Quelle  Advanced.thy

(*<*)theory Advanced imports Even begin(*>*)

text ‹
  premises of introduction rules may contain universal quantifiers and
  functions. A universal quantifier lets the rule
  to any number of instances of
  inductively defined set. A monotone function lets the rule refer
  existing constructions (such as ``list of'') over the inductively defined
 . The examples below show how to use the additional expressiveness
  how to reason from the resulting definitions.
 ›

subsection‹Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype}›

text ‹
 index{ground terms example|(}%
 index{quantifiers!and inductive definitions|(}%
  a running example, this section develops the theory of \textbf{ground
 }: terms constructed from constant and function
  but not variables. To simplify matters further, we regard a
  as a function applied to the null argument list. Let us declare a
  ‹gterm› for the type of ground terms. It is a type constructor
  argument is a type of function symbols.
 ›

datatype 'f gterm = Apply 'f "'f gterm list"

text ‹
  try it out, we declare a datatype of some integer operations:
  constants, the unary minus operator and the addition
 .
 ›

datatype integer_op = Number int | UnaryMinus | Plus

text ‹
  the type 🍋‹integer_op gterm› denotes the ground
  built over those symbols.

  type constructor ‹gterm› can be generalized to a function
  sets. It returns
  set of ground terms that can be formed over a set ‹F› of function symbols. For
 , we could consider the set of ground terms formed from the finite
  ‹{Number 2, UnaryMinus, Plus}›.

  concept is inductive. If we have a list ‹args› of ground terms
 ~‹F› and a function symbol ‹f› in ‹F›, then we
  apply ‹f› to ‹args› to obtain another ground term.
  only difficulty is that the argument list may be of any length. Hitherto,
  rule in an inductive definition referred to the inductively
  set a fixed number of times, typically once or twice.
  universal quantifier in the premise of the introduction rule
  that every element of ‹args› belongs
  our inductively defined set: is a ground term
 ~‹F›. The function term‹set› denotes the set of elements in a given
 .
 ›

inductive_set
  gterms :: "'f set ==> 'f gterm set"
  for F :: "'f set"
where
step[intro!]: "[∀t ∈ set args. t ∈ gterms F; f ∈ F]
               ==> (Apply f args) ∈ gterms F"

text ‹
  demonstrate a proof from this definition, let us
  that the function term‹gterms›
  \textbf{monotone}. We shall need this concept shortly.
 ›

lemma gterms_mono: "F⊆G ==> gterms F ⊆ gterms G"
apply clarify
apply (erule gterms.induct)
apply blast
done
(*<*)
lemma gterms_mono: "F⊆G ==> gterms F ⊆ gterms G"
apply clarify
apply (erule gterms.induct)
(*>*)
txt‹
 , this theorem says that
  the set of function symbols enlarges the set of ground
 . The proof is a trivial rule induction.
  we use the ‹clarify› method to assume the existence of an element of
 term‹gterms F›. (We could have used ‹intro subsetI›.) We then
  rule induction. Here is the resulting subgoal:
 {subgoals[display,indent=0]}
  assumptions state that ‹f› belongs
 ~‹F›, which is included in~‹G›, and that every element of the list ‹args› is
  ground term over~‹G›. The ‹blast› method finds this chain of reasoning easily.
 ›
(*<*)oops(*>*)
text ‹
 begin{warn}
  do we call this function ‹gterms› instead
  ‹gterm›? A constant may have the same name as a type. However,
  clashes could arise in the theorems that Isabelle generates.
  choice of names keeps ‹gterms.induct› separate from
 ‹gterm.induct›.
 end{warn}

  a term \textbf{well-formed} if each symbol occurring in it is applied
  the correct number of arguments. (This number is called the symbol's
 textbf{arity}.) We can express well-formedness by
  the inductive definition of
 isa{gterms}.
  we are given a function called ‹arity›, specifying the arities
  all symbols. In the inductive step, we have a list ‹args› of such
  and a function symbol~‹f›. If the length of the list matches the
 's arity then applying ‹f› to ‹args› yields a well-formed
 .
 ›

inductive_set
  well_formed_gterm :: "('f ==> nat) ==> 'f gterm set"
  for arity :: "'f ==> nat"
where
step[intro!]: "[∀t ∈ set args. t ∈ well_formed_gterm arity;
                length args = arity f]
               ==> (Apply f args) ∈ well_formed_gterm arity"

text ‹
  inductive definition neatly captures the reasoning above.
  universal quantification over the
 ‹set› of arguments expresses that all of them are well-formed.%
 index{quantifiers!and inductive definitions|)}
 ›

subsection‹Alternative Definition Using a Monotone Function›

text ‹
 index{monotone functions!and inductive definitions|(}%
  inductive definition may refer to the
  defined set through an arbitrary monotone function. To
  this powerful feature, let us
  the inductive definition above, replacing the
  by a use of the function term‹lists›. This
 , from the Isabelle theory of lists, is analogous to the
  term‹gterms› declared above: if ‹A› is a set then
 term‹lists A› is the set of lists whose elements belong to
 term‹A›.

  the inductive definition of well-formed terms, examine the one
  rule. The first premise states that ‹args› belongs to
  ‹lists› of well-formed terms. This formulation is more
 , if more obscure, than using a universal quantifier.
 ›

inductive_set
  well_formed_gterm' :: "('f ==> nat) ==> 'f gterm set"
  for arity :: "'f ==> nat"
where
step[intro!]: "[args ∈ lists (well_formed_gterm' arity);
                length args = arity f]
               ==> (Apply f args) ∈ well_formed_gterm' arity"
monos lists_mono

text ‹
  cite the theorem ‹lists_mono› to justify
  the function term‹lists›.%
 footnote{This particular theorem is installed by default already, but we
  the \isakeyword{monos} declaration in order to illustrate its syntax.}
 {named_thms [display,indent=0] lists_mono [no_vars] (lists_mono)}
  must the function be monotone? An inductive definition describes
  iterative construction: each element of the set is constructed by a
  number of introduction rule applications. For example, the
  of \isa{even} are constructed by finitely many applications of
  rules
 {thm [display,indent=0] even.intros [no_vars]}
  references to a set in its
  definition must be positive. Applications of an
  rule cannot invalidate previous applications, allowing the
  process to converge.
  following pair of rules do not constitute an inductive definition:
 begin{trivlist}
 item term‹0 ∈ even›
 item term‹n ∉ even ==> (Suc n) ∈ even›
 end{trivlist}
  that 4 is even using these rules requires showing that 3 is not
 . It is far from trivial to show that this set of rules
  the even numbers.

  with its use of the function \isa{lists}, the premise of our
  rule is positive:
 {thm [display,indent=0] (prem 1) step [no_vars]}
  apply the rule we construct a list term‹args› of previously
  well-formed terms. We obtain a
  term, term‹Apply f args›. Because term‹lists› is monotone,
  of the rule remain valid as new terms are constructed.
  lists of well-formed
  become available and none are taken away.%
 index{monotone functions!and inductive definitions|)}
 ›

subsection‹A Proof of Equivalence›

text ‹
  naturally hope that these two inductive definitions of ``well-formed''
 . The equality can be proved by separate inclusions in
  direction. Each is a trivial rule induction.
 ›

lemma "well_formed_gterm arity ⊆ well_formed_gterm' arity"
apply clarify
apply (erule well_formed_gterm.induct)
apply auto
done
(*<*)
lemma "well_formed_gterm arity ⊆ well_formed_gterm' arity"
apply clarify
apply (erule well_formed_gterm.induct)
(*>*)
txt ‹
  ‹clarify› method gives
  an element of term‹well_formed_gterm arity› on which to perform
 . The resulting subgoal can be proved automatically:
 {subgoals[display,indent=0]}
  proof resembles the one given in
 \S}\ref{sec:gterm-datatype} above, especially in the form of the
  hypothesis. Next, we consider the opposite inclusion:
 ›
(*<*)oops(*>*)
lemma "well_formed_gterm' arity ⊆ well_formed_gterm arity"
apply clarify
apply (erule well_formed_gterm'.induct)
apply auto
done
(*<*)
lemma "well_formed_gterm' arity ⊆ well_formed_gterm arity"
apply clarify
apply (erule well_formed_gterm'.induct)
(*>*)
txt ‹
  proof script is virtually identical,
  the subgoal after applying induction may be surprising:
 {subgoals[display,indent=0,margin=65]}
  induction hypothesis contains an application of term‹lists›. Using a
  function in the inductive definition always has this effect. The
  may look uninviting, but fortunately
 term‹lists› distributes over intersection:
 {named_thms [display,indent=0] lists_Int_eq [no_vars] (lists_Int_eq)}
  to this default simplification rule, the induction hypothesis
  quickly replaced by its two parts:
 begin{trivlist}
 item term‹args ∈ lists (well_formed_gterm' arity)›
 item term‹args ∈ lists (well_formed_gterm arity)›
 end{trivlist}
  the rule ‹well_formed_gterm.step› completes the proof. The
  to ‹auto› does all this work.

  example is typical of how monotone functions
 index{monotone functions} can be used. In particular, many of them
  over intersection. Monotonicity implies one direction of
  set equality; we have this theorem:
 {named_thms [display,indent=0] mono_Int [no_vars] (mono_Int)}
 ›
(*<*)oops(*>*)


subsection‹Another Example of Rule Inversion›

text ‹
 index{rule inversion|(}%
  term‹gterms› distribute over intersection? We have proved that this
  is monotone, so ‹mono_Int› gives one of the inclusions. The
  inclusion asserts that if term‹t› is a ground term over both of the
 
 term‹F› and~term‹G› then it is also a ground term over their intersection,
 term‹F ∩ G›.
 ›

lemma gterms_IntI:
     "t ∈ gterms F ==> t ∈ gterms G ⟶ t ∈ gterms (F∩G)"
(*<*)oops(*>*)
text ‹
  this proof, we get the assumption
 term‹Apply f args ∈ gterms G›, which cannot be broken down.
  looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}
 ›

inductive_cases gterm_Apply_elim [elim!]: "Apply f args ∈ gterms F"

text ‹
  is the result.
 {named_thms [display,indent=0,margin=50] gterm_Apply_elim [no_vars] (gterm_Apply_elim)}
  rule replaces an assumption about term‹Apply f args› by
  about term‹f› and~term‹args›.
  cases are discarded (there was only one to begin
 ) but the rule applies specifically to the pattern term‹Apply f args›.
  can be applied repeatedly as an elimination rule without looping, so we
  given the ‹elim!› attribute.

  we can prove the other half of that distributive law.
 ›

lemma gterms_IntI [rule_format, intro!]:
     "t ∈ gterms F ==> t ∈ gterms G ⟶ t ∈ gterms (F∩G)"
apply (erule gterms.induct)
apply blast
done
(*<*)
lemma "t ∈ gterms F ==> t ∈ gterms G ⟶ t ∈ gterms (F∩G)"
apply (erule gterms.induct)
(*>*)
txt ‹
  proof begins with rule induction over the definition of
 term‹gterms›, which leaves a single subgoal:
 {subgoals[display,indent=0,margin=65]}
  prove this, we assume term‹Apply f args ∈ gterms G›. Rule inversion,
  the form of ‹gterm_Apply_elim›, infers
  every element of term‹args› belongs to
 term‹gterms G›; hence (by the induction hypothesis) it belongs
  term‹gterms (F ∩ G)›. Rule inversion also yields
 term‹f ∈ G› and hence term‹f ∈ F ∩ G›.
  of this reasoning is done by ‹blast›.

 smallskip
  distributive law is a trivial consequence of previously-proved results:
 ›
(*<*)oops(*>*)
lemma gterms_Int_eq [simp]:
     "gterms (F ∩ G) = gterms F ∩ gterms G"
by (blast intro!: mono_Int monoI gterms_mono)

text_raw ‹
 index{rule inversion|)}%
 index{ground terms example|)}


 begin{isamarkuptext}
 begin{exercise}
  function mapping function symbols to their
  is called a \textbf{signature}. Given a type
  over type symbols, we can represent a function's type by a
  of argument types paired with the result type.
  this inductive definition:
 begin{isabelle}
 ›

inductive_set
  well_typed_gterm :: "('f ==> 't list * 't) ==> ('f gterm * 't)set"
  for sig :: "'f ==> 't list * 't"
(*<*)
where
step[intro!]: 
    "[∀pair ∈ set args. pair ∈ well_typed_gterm sig;
      sig f = (map snd args, rtype)]
     ==> (Apply f (map fst args), rtype)
         ∈ well_typed_gterm sig"
(*>*)
text_raw ‹
 end{isabelle}
 end{exercise}
 end{isamarkuptext}
 ›

(*<*)

text‹the following declaration isn't actually used›
primrec
  integer_arity :: "integer_op ==> nat"
where
  "integer_arity (Number n) = 0"
| "integer_arity UnaryMinus = 1"
| "integer_arity Plus = 2"

text‹the rest isn't used: too complicated. OK for an exercise though.›

inductive_set
  integer_signature :: "(integer_op * (unit list * unit)) set"
where
  Number:     "(Number n, ([], ())) ∈ integer_signature"
| UnaryMinus: "(UnaryMinus, ([()], ())) ∈ integer_signature"
| Plus:       "(Plus, ([(),()], ())) ∈ integer_signature"

inductive_set
  well_typed_gterm' :: "('f ==> 't list * 't) ==> ('f gterm * 't)set"
  for sig :: "'f ==> 't list * 't"
where
step[intro!]: 
    "[args ∈ lists(well_typed_gterm' sig);
      sig f = (map snd args, rtype)]
     ==> (Apply f (map fst args), rtype)
         ∈ well_typed_gterm' sig"
monos lists_mono


lemma "well_typed_gterm sig ⊆ well_typed_gterm' sig"
apply clarify
apply (erule well_typed_gterm.induct)
apply auto
done

lemma "well_typed_gterm' sig ⊆ well_typed_gterm sig"
apply clarify
apply (erule well_typed_gterm'.induct)
apply auto
done


end
(*>*)