--- a/ProgTutorial/Package/Ind_Prelims.thy Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
imports Ind_Intro
begin
-section{* Preliminaries *}
+section\<open>Preliminaries\<close>
-text {*
+text \<open>
The user will just give a specification of inductive predicate(s) and
expects from the package to produce a convenient reasoning
infrastructure. This infrastructure needs to be derived from the definition
@@ -18,7 +18,7 @@
the ML-implementation we will develop in later sections.
- We first consider the transitive closure of a relation @{text R}. The
+ We first consider the transitive closure of a relation \<open>R\<close>. The
``pencil-and-paper'' specification for the transitive closure is:
\begin{center}\small
@@ -29,18 +29,17 @@
As mentioned before, the package has to make an appropriate definition for
@{term "trcl"}. Since an inductively defined predicate is the least
predicate closed under a collection of introduction rules, the predicate
- @{text "trcl R x y"} can be defined so that it holds if and only if @{text
- "P x y"} holds for every predicate @{text P} closed under the rules
+ \<open>trcl R x y\<close> can be defined so that it holds if and only if \<open>P x y\<close> holds for every predicate \<open>P\<close> closed under the rules
above. This gives rise to the definition
-*}
+\<close>
definition "trcl \<equiv>
\<lambda>R x y. \<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"
-text {*
- Note we have to use the object implication @{text "\<longrightarrow>"} and object
- quantification @{text "\<forall>"} for stating this definition (there is no other
+text \<open>
+ Note we have to use the object implication \<open>\<longrightarrow>\<close> and object
+ quantification \<open>\<forall>\<close> for stating this definition (there is no other
way for definitions in HOL). However, the introduction rules and induction
principles associated with the transitive closure should use the
meta-connectives, since they simplify the reasoning for the user.
@@ -49,11 +48,11 @@
With this definition, the proof of the induction principle for @{term trcl}
is almost immediate. It suffices to convert all the meta-level
connectives in the lemma to object-level connectives using the
- proof method @{text atomize} (Line 4 below), expand the definition of @{term trcl}
+ proof method \<open>atomize\<close> (Line 4 below), expand the definition of @{term trcl}
(Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
- and then solve the goal by @{text assumption} (Line 8).
+ and then solve the goal by \<open>assumption\<close> (Line 8).
-*}
+\<close>
lemma %linenos trcl_induct:
assumes "trcl R x y"
@@ -65,10 +64,10 @@
apply(assumption)
done
-text {*
+text \<open>
The proofs for the introduction rules are slightly more complicated.
For the first one, we need to prove the following lemma:
-*}
+\<close>
lemma %linenos trcl_base:
shows "trcl R x x"
@@ -78,45 +77,45 @@
apply(assumption)
done
-text {*
+text \<open>
We again unfold first the definition and apply introduction rules
- for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).
+ for \<open>\<forall>\<close> and \<open>\<longrightarrow>\<close> as often as possible (Lines 3 and 4).
We then end up in the goal state:
-*}
+\<close>
(*<*)lemma "trcl R x x"
apply (unfold trcl_def)
apply (rule allI impI)+(*>*)
-txt {* @{subgoals [display]} *}
+txt \<open>@{subgoals [display]}\<close>
(*<*)oops(*>*)
-text {*
+text \<open>
The two assumptions come from the definition of @{term trcl} and correspond
to the introduction rules. Thus, all we have to do is to eliminate the
universal quantifier in front of the first assumption (Line 5), and then
- solve the goal by @{text assumption} (Line 6).
-*}
+ solve the goal by \<open>assumption\<close> (Line 6).
+\<close>
-text {*
+text \<open>
Next we have to show that the second introduction rule also follows from the
definition. Since this rule has premises, the proof is a bit more
involved. After unfolding the definitions and applying the introduction
- rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
-*}
+ rules for \<open>\<forall>\<close> and \<open>\<longrightarrow>\<close>
+\<close>
lemma trcl_step:
shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
apply (unfold trcl_def)
apply (rule allI impI)+
-txt {*
+txt \<open>
we obtain the goal state
@{subgoals [display]}
To see better where we are, let us explicitly name the assumptions
by starting a subproof.
-*}
+\<close>
proof -
case (goal1 P)
@@ -127,42 +126,40 @@
have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
show "P x z"
-txt {*
- The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
- the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}
- come from the definition of @{term trcl}. We apply @{text "r2"} to the goal
+txt \<open>
+ The assumptions \<open>p1\<close> and \<open>p2\<close> correspond to the premises of
+ the second introduction rule (unfolded); the assumptions \<open>r1\<close> and \<open>r2\<close>
+ come from the definition of @{term trcl}. We apply \<open>r2\<close> to the goal
@{term "P x z"}. In order for this assumption to be applicable as a rule, we
have to eliminate the universal quantifier and turn the object-level
- implications into meta-level ones. This can be accomplished using the @{text
- rule_format} attribute. So we continue the proof with:
+ implications into meta-level ones. This can be accomplished using the \<open>rule_format\<close> attribute. So we continue the proof with:
-*}
+\<close>
apply (rule r2[rule_format])
-txt {*
+txt \<open>
This gives us two new subgoals
@{subgoals [display]}
- which can be solved using assumptions @{text p1} and @{text p2}. The latter
+ which can be solved using assumptions \<open>p1\<close> and \<open>p2\<close>. The latter
involves a quantifier and implications that have to be eliminated before it
can be applied. To avoid potential problems with higher-order unification,
- we explicitly instantiate the quantifier to @{text "P"} and also match
- explicitly the implications with @{text "r1"} and @{text "r2"}. This gives
+ we explicitly instantiate the quantifier to \<open>P\<close> and also match
+ explicitly the implications with \<open>r1\<close> and \<open>r2\<close>. This gives
the proof:
-*}
+\<close>
apply(rule p1)
apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
done
qed
-text {*
+text \<open>
Now we are done. It might be surprising that we are not using the automatic
- tactics available in Isabelle/HOL for proving this lemmas. After all @{text
- "blast"} would easily dispense of it.
-*}
+ tactics available in Isabelle/HOL for proving this lemmas. After all \<open>blast\<close> would easily dispense of it.
+\<close>
lemma trcl_step_blast:
shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
@@ -170,9 +167,9 @@
apply(blast)
done
term "even"
-text {*
+text \<open>
Experience has shown that it is generally a bad idea to rely heavily on
- @{text blast}, @{text auto} and the like in automated proofs. The reason is
+ \<open>blast\<close>, \<open>auto\<close> and the like in automated proofs. The reason is
that you do not have precise control over them (the user can, for example,
declare new intro- or simplification rules that can throw automatic tactics
off course) and also it is very hard to debug proofs involving automatic
@@ -181,7 +178,7 @@
The method of defining inductive predicates by impredicative quantification
also generalises to mutually inductive predicates. The next example defines
- the predicates @{text even} and @{text odd} given by
+ the predicates \<open>even\<close> and \<open>odd\<close> given by
\begin{center}\small
@{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
@@ -191,8 +188,8 @@
Since the predicates @{term even} and @{term odd} are mutually inductive, each
corresponding definition must quantify over both predicates (we name them
- below @{text "P"} and @{text "Q"}).
-*}
+ below \<open>P\<close> and \<open>Q\<close>).
+\<close>
hide_const even
hide_const odd
@@ -205,10 +202,10 @@
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
-text {*
+text \<open>
For proving the induction principles, we use exactly the same technique
as in the transitive closure example, namely:
-*}
+\<close>
lemma even_induct:
assumes "even n"
@@ -221,14 +218,14 @@
apply(assumption)
done
-text {*
- The only difference with the proof @{text "trcl_induct"} is that we have to
+text \<open>
+ The only difference with the proof \<open>trcl_induct\<close> is that we have to
instantiate here two universal quantifiers. We omit the other induction
principle that has @{prop "even n"} as premise and @{term "Q n"} as conclusion.
The proofs of the introduction rules are also very similar to the ones in
- the @{text "trcl"}-example. We only show the proof of the second introduction
+ the \<open>trcl\<close>-example. We only show the proof of the second introduction
rule.
-*}
+\<close>
lemma %linenos evenS:
shows "odd m \<Longrightarrow> even (Suc m)"
@@ -248,18 +245,18 @@
done
qed
-text {*
+text \<open>
The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
- @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
- to @{text "r3"} come from the definition of @{text "even"}.
- In Line 13, we apply the assumption @{text "r2"} (since we prove the second
- introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
+ \<open>p1\<close> corresponds to the premise of the introduction rule; \<open>r1\<close>
+ to \<open>r3\<close> come from the definition of \<open>even\<close>.
+ In Line 13, we apply the assumption \<open>r2\<close> (since we prove the second
+ introduction rule). In Lines 14 and 15 we apply assumption \<open>p1\<close> (if
the second introduction rule had more premises we have to do that for all
of them). In order for this assumption to be applicable, the quantifiers
need to be instantiated and then also the implications need to be resolved
with the other rules.
- Next we define the accessible part of a relation @{text R} given by
+ Next we define the accessible part of a relation \<open>R\<close> given by
the single rule:
\begin{center}\small
@@ -268,16 +265,16 @@
The interesting point of this definition is that it contains a quantification
that ranges only over the premise and the premise has also a precondition.
- The definition of @{text "accpart"} is:
-*}
+ The definition of \<open>accpart\<close> is:
+\<close>
definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
-text {*
+text \<open>
The proof of the induction principle is again straightforward and omitted.
Proving the introduction rule is a little more complicated, because the
quantifier and the implication in the premise. The proof is as follows.
-*}
+\<close>
lemma %linenos accpartI:
shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
@@ -299,13 +296,11 @@
qed
qed
-text {*
+text \<open>
As you can see, there are now two subproofs. The assumptions fall as usual into
- two categories (Lines 7 to 9). In Line 11, applying the assumption @{text
- "r1"} generates a goal state with the new local assumption @{term "R y x"},
- named @{text "r1_prem"} in the second subproof (Line 14). This local assumption is
- used to solve the goal @{term "P y"} with the help of assumption @{text
- "p1"}.
+ two categories (Lines 7 to 9). In Line 11, applying the assumption \<open>r1\<close> generates a goal state with the new local assumption @{term "R y x"},
+ named \<open>r1_prem\<close> in the second subproof (Line 14). This local assumption is
+ used to solve the goal @{term "P y"} with the help of assumption \<open>p1\<close>.
\begin{exercise}
@@ -328,5 +323,5 @@
them. This is usually the first step in writing a package. We next explain
the parsing and typing part of the package.
-*}
+\<close>
(*<*)end(*>*)