equal
deleted
inserted
replaced
3 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
4 By default, assumptions are part of the simplification process: they are used |
4 By default, assumptions are part of the simplification process: they are used |
5 as simplification rules and are simplified themselves. For example:% |
5 as simplification rules and are simplified themselves. For example:% |
6 \end{isamarkuptext}% |
6 \end{isamarkuptext}% |
7 \isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline |
7 \isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline |
8 \isacommand{apply}~simp\isacommand{.}% |
8 \isacommand{by}~simp% |
9 \begin{isamarkuptext}% |
9 \begin{isamarkuptext}% |
10 \noindent |
10 \noindent |
11 The second assumption simplifies to \isa{xs = []}, which in turn |
11 The second assumption simplifies to \isa{xs = []}, which in turn |
12 simplifies the first assumption to \isa{zs = ys}, thus reducing the |
12 simplifies the first assumption to \isa{zs = ys}, thus reducing the |
13 conclusion to \isa{ys = ys} and hence to \isa{True}. |
13 conclusion to \isa{ys = ys} and hence to \isa{True}. |
22 simplification rule \isa{f x = g(f(g x))} extracted from the assumption |
22 simplification rule \isa{f x = g(f(g x))} extracted from the assumption |
23 does not terminate. Isabelle notices certain simple forms of |
23 does not terminate. Isabelle notices certain simple forms of |
24 nontermination but not this one. The problem can be circumvented by |
24 nontermination but not this one. The problem can be circumvented by |
25 explicitly telling the simplifier to ignore the assumptions:% |
25 explicitly telling the simplifier to ignore the assumptions:% |
26 \end{isamarkuptxt}% |
26 \end{isamarkuptxt}% |
27 \isacommand{apply}(simp~(no\_asm))\isacommand{.}% |
27 \isacommand{by}(simp~(no\_asm))% |
28 \begin{isamarkuptext}% |
28 \begin{isamarkuptext}% |
29 \noindent |
29 \noindent |
30 There are three options that influence the treatment of assumptions: |
30 There are three options that influence the treatment of assumptions: |
31 \begin{description} |
31 \begin{description} |
32 \item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored. |
32 \item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored. |