doc-src/TutorialI/Datatype/ABexpr.thy
author nipkow
Thu, 29 May 2008 22:45:33 +0200
changeset 27015 f8537d69f514
parent 16417 9bc16273c2d4
child 27144 ef2634bef947
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12334
diff changeset
     2
theory ABexpr imports Main begin;
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     3
(*>*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     4
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
text{*
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
     6
\index{datatypes!mutually recursive}%
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     7
Sometimes it is necessary to define two datatypes that depend on each
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     8
other. This is called \textbf{mutual recursion}. As an example consider a
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     9
language of arithmetic and boolean expressions where
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    10
\begin{itemize}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    11
\item arithmetic expressions contain boolean expressions because there are
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
    12
  conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'',
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    13
  and
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    14
\item boolean expressions contain arithmetic expressions because of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    15
  comparisons like ``$m<n$''.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    16
\end{itemize}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    17
In Isabelle this becomes
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    19
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    20
datatype 'a aexp = IF   "'a bexp" "'a aexp" "'a aexp"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
                 | Sum  "'a aexp" "'a aexp"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    22
                 | Diff "'a aexp" "'a aexp"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    23
                 | Var 'a
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    24
                 | Num nat
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    25
and      'a bexp = Less "'a aexp" "'a aexp"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
                 | And  "'a bexp" "'a bexp"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
                 | Neg  "'a bexp";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    28
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    29
text{*\noindent
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
    30
Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 10971
diff changeset
    31
except that we have added an @{text IF} constructor,
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 10971
diff changeset
    32
fixed the values to be of type @{typ"nat"} and declared the two binary
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 10971
diff changeset
    33
operations @{text Sum} and @{term"Diff"}.  Boolean
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
expressions can be arithmetic comparisons, conjunctions and negations.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
    35
The semantics is given by two evaluation functions:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    37
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    38
primrec evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" and
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    39
         evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    40
"evala (IF b a1 a2) env =
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    41
   (if evalb b env then evala a1 env else evala a2 env)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    42
"evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    43
"evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    44
"evala (Var v) env = env v" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    45
"evala (Num n) env = n" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    46
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    47
"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    48
"evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    49
"evalb (Neg b) env = (\<not> evalb b env)"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    52
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    53
Both take an expression and an environment (a mapping from variables
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    54
@{typ"'a"} to values @{typ"nat"}) and return its arithmetic/boolean
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    55
value. Since the datatypes are mutually recursive, so are functions
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    56
that operate on them. Hence they need to be defined in a single
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    57
\isacommand{primrec} section. Notice the \isakeyword{and} separating
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    58
the declarations of @{const evala} and @{const evalb}. Their defining
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    59
equations need not be split into two groups;
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    60
the empty line is purely for readability.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    61
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    62
In the same fashion we also define two functions that perform substitution:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    63
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    64
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    65
primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" and
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    66
         substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    67
"substa s (IF b a1 a2) =
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    68
   IF (substb s b) (substa s a1) (substa s a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    69
"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    70
"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    71
"substa s (Var v) = s v" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    72
"substa s (Num n) = Num n" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    73
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    74
"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    75
"substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    76
"substb s (Neg b) = Neg (substb s b)"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    77
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    78
text{*\noindent
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    79
Their first argument is a function mapping variables to expressions, the
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    80
substitution. It is applied to all variables in the second argument. As a
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
    81
result, the type of variables in the expression may change from @{typ"'a"}
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
    82
to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    83
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    84
Now we can prove a fundamental theorem about the interaction between
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    85
evaluation and substitution: applying a substitution $s$ to an expression $a$
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    86
and evaluating the result in an environment $env$ yields the same result as
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    87
evaluation $a$ in the environment that maps every variable $x$ to the value
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    88
of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    89
boolean expressions (by induction), you find that you always need the other
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    90
theorem in the induction step. Therefore you need to state and prove both
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    91
theorems simultaneously:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    92
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    93
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10171
diff changeset
    94
lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
6852682eaf16 *** empty log message ***
nipkow
parents: 10171
diff changeset
    95
        evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    96
apply(induct_tac a and b);
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    97
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    98
txt{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    99
The resulting 8 goals (one for each constructor) are proved in one fell swoop:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   100
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   101
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9792
diff changeset
   102
apply simp_all;
59d6633835fa *** empty log message ***
nipkow
parents: 9792
diff changeset
   103
(*<*)done(*>*)
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   104
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   105
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   106
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   107
an inductive proof expects a goal of the form
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   108
\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   109
where each variable $x@i$ is of type $\tau@i$. Induction is started by
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   110
\begin{isabelle}
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10171
diff changeset
   111
\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   112
\end{isabelle}
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   113
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   114
\begin{exercise}
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   115
  Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   116
  replaces @{term"IF"}s with complex boolean conditions by nested
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   117
  @{term"IF"}s; it should eliminate the constructors
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   118
  @{term"And"} and @{term"Neg"}, leaving only @{term"Less"}.
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   119
  Prove that @{text"norma"}
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   120
  preserves the value of an expression and that the result of @{text"norma"}
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9689
diff changeset
   121
  is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   122
  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   123
  of type annotations following lemma @{text subst_id} below).
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   124
\end{exercise}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   125
*}
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   126
(*<*)
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   127
primrec norma :: "'a aexp \<Rightarrow> 'a aexp" and
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   128
        normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   129
"norma (IF b t e)   = (normb b (norma t) (norma e))" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   130
"norma (Sum a1 a2)  = Sum (norma a1) (norma a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   131
"norma (Diff a1 a2) = Diff (norma a1) (norma a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   132
"norma (Var v)      = Var v" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   133
"norma (Num n)      = Num n" |
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   134
            
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   135
"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   136
"normb (And b1 b2)  t e = normb b1 (normb b2 t e) e" |
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   137
"normb (Neg b)      t e = normb b e t"
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   138
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   139
lemma " evala (norma a) env = evala a env 
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   140
      \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   141
apply (induct_tac a and b)
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   142
apply (simp_all)
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   143
done
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   144
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   145
primrec normala :: "'a aexp \<Rightarrow> bool" and
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   146
        normalb :: "'a bexp \<Rightarrow> bool" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   147
"normala (IF b t e)   = (normalb b \<and> normala t \<and> normala e)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   148
"normala (Sum a1 a2)  = (normala a1 \<and> normala a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   149
"normala (Diff a1 a2) = (normala a1 \<and> normala a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   150
"normala (Var v)      = True" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   151
"normala (Num n)      = True" |
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   152
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   153
"normalb (Less a1 a2) = (normala a1 \<and> normala a2)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   154
"normalb (And b1 b2)  = False" |
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   155
"normalb (Neg b)      = False"
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   156
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   157
lemma "normala (norma (a::'a aexp)) \<and>
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   158
       (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   159
apply (induct_tac a and b)
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   160
apply (auto)
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   161
done
60bf75e157e4 *** empty log message ***
nipkow
parents: 11458
diff changeset
   162
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   163
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   164
(*>*)