CookBook/Package/Ind_Examples.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 29 Jan 2009 09:46:17 +0000
changeset 88 ebbd0dd008c8
parent 38 e21b2f888fa2
child 102 5e309df58557
permissions -rw-r--r--
adaptation of the package chapter to fit the rest
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     1
theory Ind_Examples
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
     2
imports Main LaTeXsugar
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     3
begin
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     4
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
     5
section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     6
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     7
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
     8
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
     9
  In this section, we will give three examples showing how to define inductive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    10
  predicates by hand and prove characteristic properties such as introduction
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    11
  rules and an induction rule. From these examples, we will then figure out a
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    12
  general method for defining inductive predicates.  It should be noted that
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    13
  our aim in this section is not to write proofs that are as beautiful as
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    14
  possible, but as close as possible to the ML code producing the proofs that
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    15
  we will develop later.  As a first example, we consider the transitive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    16
  closure of a relation @{text R}. It is an inductive predicate characterized
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    17
  by the two introduction rules
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    18
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    19
  \begin{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    20
  @{term[mode=Axiom] "trcl R x x"} \hspace{5mm}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    21
  @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    22
  \end{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    23
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    24
  (FIXME first rule should be an ``axiom'')
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    25
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    26
  Note that the @{text trcl} predicate has two different kinds of parameters: the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    27
  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    28
  the second and third parameter changes in the ``recursive call''.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    29
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    30
  Since an inductively defined predicate is the least predicate closed under
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    31
  a collection of introduction rules, we define the predicate @{text "trcl R x y"} in
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    32
  such a way that it holds if and only if @{text "P x y"} holds for every predicate
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    33
  @{text P} closed under the rules above. This gives rise to the definition 
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    34
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    35
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    36
definition "trcl R x y \<equiv> 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    37
      \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    38
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    39
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    40
  where we quantify over the predicate @{text P}.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    41
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    42
  Since the predicate @{term "trcl R x y"} yields an element of the type of object
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    43
  level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    44
  above introduction rules have to be converted to object-level implications
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    45
  @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    46
  rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    47
  the variable parameters of the introduction rules. Isabelle already offers some
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    48
  infrastructure for converting between meta-level and object-level connectives,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    49
  which we will use later on.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    50
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    51
  With this definition of the transitive closure, the proof of the (weak) induction
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    52
  theorem is almost immediate. It suffices to convert all the meta-level connectives
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    53
  in the induction rule to object-level connectives using the @{text atomize} proof
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    54
  method, expand the definition of @{text trcl}, eliminate the universal quantifier
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    55
  contained in it, and then solve the goal by assumption.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    56
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    57
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    58
lemma trcl_induct:
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    59
  assumes trcl: "trcl R x y"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    60
  shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    61
  apply (atomize (full))
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    62
  apply (cut_tac trcl)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    63
  apply (unfold trcl_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    64
  apply (drule spec [where x=P])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    65
  apply assumption
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    66
  done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    67
(*<*)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    68
lemma "trcl R x x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    69
  apply (unfold trcl_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    70
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    71
(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    72
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    73
txt {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    74
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    75
  The above induction rule is \emph{weak} in the sense that the induction step may
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    76
  only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    77
  using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    78
  containing this additional assumption can be derived from the weaker one with the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    79
  help of the introduction rules for @{text trcl}.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    80
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    81
  We now turn to the proofs of the introduction rules, which are slightly more complicated.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    82
  In order to prove the first introduction rule, we again unfold the definition and
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    83
  then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    84
  We then end up in a proof state of the following form:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    85
  
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    86
  @{subgoals [display]}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    87
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    88
  The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    89
  replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    90
  in front of the first assumption, and then solve the goal by assumption:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    91
  *}
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    92
(*<*)oops(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    93
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    94
lemma trcl_base: "trcl R x x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    95
  apply (unfold trcl_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    96
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    97
  apply (drule spec)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    98
  apply assumption
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
    99
  done
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   100
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   101
(*<*)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   102
lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   103
  apply (unfold trcl_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   104
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   105
(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   106
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   107
txt {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   108
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   109
  Since the second introduction rule has premises, its proof is not as easy as the previous
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   110
  one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   111
  and @{text "\<longrightarrow>"}, we get the proof state
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   112
  @{subgoals [display]}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   113
  The third and fourth assumption corresponds to the first and second introduction rule,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   114
  respectively, whereas the first and second assumption corresponds to the premises of
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   115
  the introduction rule. Since we want to prove the second introduction rule, we apply
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   116
  the fourth assumption to the goal @{term "P x z"}. In order for the assumption to
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   117
  be applicable, we have to eliminate the universal quantifiers and turn the object-level
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   118
  implications into meta-level ones. This can be accomplished using the @{text rule_format}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   119
  attribute. Applying the assumption produces two new subgoals, which can be solved using
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   120
  the first and second assumption. The second assumption again involves a quantifier and
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   121
  implications that have to be eliminated before it can be applied. To avoid problems
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   122
  with higher order unification, it is advisable to provide an instantiation for the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   123
  universally quantified predicate variable in the assumption.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   124
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   125
(*<*)oops(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   126
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   127
lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   128
  apply (unfold trcl_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   129
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   130
  proof -
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   131
    case goal1
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   132
    show ?case
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   133
      apply (rule goal1(4) [rule_format])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   134
      apply (rule goal1(1))
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   135
      apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   136
	OF goal1(3-4)])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   137
      done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   138
  qed
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   139
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   140
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   141
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   142
  This method of defining inductive predicates easily generalizes to mutually inductive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   143
  predicates, like the predicates @{text even} and @{text odd} characterized by the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   144
  following introduction rules:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   145
 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   146
  \begin{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   147
  @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   148
  @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   149
  @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   150
  \end{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   151
  
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   152
  Since the predicates are mutually inductive, each of the definitions contain two
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   153
  quantifiers over the predicates @{text P} and @{text Q}.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   154
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   155
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   156
definition "even n \<equiv> 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   157
  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   158
             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   159
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   160
definition "odd n \<equiv>
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   161
  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   162
             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   163
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   164
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   165
  For proving the induction rule, we use exactly the same technique as in the transitive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   166
  closure example:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   167
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   168
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   169
lemma even_induct:
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   170
  assumes even: "even n"
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 32
diff changeset
   171
  shows "P 0 \<Longrightarrow> 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 32
diff changeset
   172
             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   173
  apply (atomize (full))
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   174
  apply (cut_tac even)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   175
  apply (unfold even_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   176
  apply (drule spec [where x=P])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   177
  apply (drule spec [where x=Q])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   178
  apply assumption
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   179
  done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   180
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   181
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   182
  A similar induction rule having @{term "Q n"} as a conclusion can be proved for
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   183
  the @{text odd} predicate.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   184
  The proofs of the introduction rules are also very similar to the ones in the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   185
  previous example. We only show the proof of the second introduction rule,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   186
  since it is almost the same as the one for the third introduction rule,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   187
  and the proof of the first rule is trivial.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   188
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   189
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   190
lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   191
  apply (unfold odd_def even_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   192
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   193
  proof -
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   194
    case goal1
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   195
    show ?case
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   196
      apply (rule goal1(3) [rule_format])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   197
      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   198
	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   199
      done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   200
  qed
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   201
(*<*)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   202
lemma even0: "even 0"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   203
  apply (unfold even_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   204
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   205
  apply assumption
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   206
  done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   207
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   208
lemma oddS: "even m \<Longrightarrow> odd (Suc m)"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   209
  apply (unfold odd_def even_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   210
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   211
  proof -
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   212
    case goal1
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   213
    show ?case
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   214
      apply (rule goal1(4) [rule_format])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   215
      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   216
	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   217
      done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   218
  qed
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   219
(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   220
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   221
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   222
  As a final example, we will consider the definition of the accessible
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   223
  part of a relation @{text R} characterized by the introduction rule
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   224
  
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   225
  \begin{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   226
  @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   227
  \end{center}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   228
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   229
  whose premise involves a universal quantifier and an implication. The
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   230
  definition of @{text accpart} is as follows:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   231
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   232
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   233
definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   234
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   235
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   236
  The proof of the induction theorem is again straightforward:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   237
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   238
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   239
lemma accpart_induct:
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   240
  assumes acc: "accpart R x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   241
  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   242
  apply (atomize (full))
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   243
  apply (cut_tac acc)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   244
  apply (unfold accpart_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   245
  apply (drule spec [where x=P])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   246
  apply assumption
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   247
  done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   248
(*<*)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   249
lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   250
  apply (unfold accpart_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   251
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   252
(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   253
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   254
txt {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   255
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   256
  Proving the introduction rule is a little more complicated, due to the quantifier
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   257
  and the implication in the premise. We first convert the meta-level universal quantifier
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   258
  and implication to their object-level counterparts. Unfolding the definition of
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   259
  @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   260
  yields the following proof state:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   261
  @{subgoals [display]}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   262
  Applying the second assumption produces a proof state with the new local assumption
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   263
  @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   264
  first assumption.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   265
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   266
(*<*)oops(*>*)
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   267
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   268
lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   269
  apply (unfold accpart_def)
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   270
  apply (rule allI impI)+
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   271
  proof -
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   272
    case goal1
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   273
    note goal1' = this
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   274
    show ?case
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   275
      apply (rule goal1'(2) [rule_format])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   276
      proof -
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   277
        case goal1
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   278
        show ?case
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   279
	  apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   280
            THEN mp, OF goal1'(2)])
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   281
	  done
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   282
      qed
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   283
    qed
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   284
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   285
end