--- a/ProgTutorial/Package/Ind_General_Scheme.thy Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy Tue May 05 03:21:49 2009 +0200
@@ -1,11 +1,44 @@
theory Ind_General_Scheme
-imports Ind_Interface
+imports "../Base" Simple_Inductive_Package
begin
+(*<*)
+simple_inductive
+ trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "trcl R x x"
+| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
+
+simple_inductive
+ even and odd
+where
+ even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
+
+simple_inductive
+ accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+
+datatype trm =
+ Var "string"
+| App "trm" "trm"
+| Lam "string" "trm"
+
+simple_inductive
+ fresh :: "string \<Rightarrow> trm \<Rightarrow> bool"
+where
+ fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
+| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
+| fresh_lam1: "fresh a (Lam a t)"
+| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+(*>*)
+
+
section {* The Code in a Nutshell\label{sec:nutshell} *}
-
text {*
The inductive package will generate the reasoning infrastructure for
mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
--- a/ProgTutorial/Package/Ind_Interface.thy Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Tue May 05 03:21:49 2009 +0200
@@ -1,5 +1,5 @@
theory Ind_Interface
-imports "../Base" "../Parsing" Simple_Inductive_Package
+imports "../Base" Simple_Inductive_Package
begin
section {* Parsing and Typing the Specification\label{sec:interface} *}
@@ -46,7 +46,7 @@
\end{boxedminipage}
\caption{Specification given by the user for the inductive predicates
@{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and
-@{text "fresh"}.\label{fig:specs}}
+@{term "fresh"}.\label{fig:specs}}
\end{figure}
*}
@@ -120,7 +120,9 @@
accpart'
where
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
-
+(*<*)ML %no{*fun filtered_input str =
+ filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
+fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)
text {*
Note that in these definitions the parameter @{text R}, standing for the
relation, is left implicit. For the moment we will ignore this kind
@@ -152,19 +154,17 @@
done in Lines 5 to 7 in the code below.
*}
-(*<*)ML %linenos{*fun add_inductive pred_specs rule_specs lthy = lthy
-fun add_inductive_cmd pred_specs rule_specs lthy =
-let
- val ((pred_specs', rule_specs'), _) =
- Specification.read_spec pred_specs rule_specs lthy
-in
- add_inductive pred_specs' rule_specs' lthy
-end*}(*>*)
+(*<*)
+ML %linenos
+{* fun add_inductive_cmd pred_specs rule_specs lthy = lthy
+ fun add_inductive pred_specs rule_specs lthy = lthy *}
+(*>*)
+
ML_val %linenosgray{*val specification =
spec_parser >>
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
-val _ = OuterSyntax.local_theory "simple_inductive"
+val _ = OuterSyntax.local_theory "simple_inductive2"
"definition of simple inductive predicates"
OuterKeyword.thy_decl specification*}
@@ -191,7 +191,7 @@
@{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
*}
-ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
+ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy =
let
val ((pred_specs', rule_specs'), _) =
Specification.read_spec pred_specs rule_specs lthy
@@ -199,11 +199,9 @@
add_inductive pred_specs' rule_specs' lthy
end*}
-ML {* Specification.read_spec *}
-
text {*
Once we have the input data as some internal datastructure, we call
- the function @{ML add_inductive}. This function does the heavy duty
+ the function @{text add_inductive}. This function does the heavy duty
lifting in the package: it generates definitions for the
predicates and derives from them corresponding induction principles and
introduction rules. The description of this function will span over
--- a/ProgTutorial/Package/Ind_Prelims.thy Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy Tue May 05 03:21:49 2009 +0200
@@ -1,5 +1,5 @@
theory Ind_Prelims
-imports Main LaTeXsugar "../Base"
+imports Main "../Base"
begin
section{* Preliminaries *}
@@ -15,9 +15,7 @@
we will figure out a general method for
defining inductive predicates. The aim in this section is \emph{not} to
write proofs that are as beautiful as possible, but as close as possible to
- the ML-code we will develop in later sections.
-
-
+ the ML-implementation we will develop in later sections.
We first consider the transitive closure of a relation @{text R}. The
``pencil-and-paper'' specification for the transitive closure is:
@@ -161,7 +159,7 @@
text {*
Now we are done. It might be surprising that we are not using the automatic
- tactics available in Isabelle for proving this lemmas. After all @{text
+ tactics available in Isabelle/HOL for proving this lemmas. After all @{text
"blast"} would easily dispense of it.
*}
--- a/ProgTutorial/Package/Simple_Inductive_Package.thy Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Tue May 05 03:21:49 2009 +0200
@@ -44,7 +44,6 @@
where
accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
-
context rel
begin
thm accpartI'
--- a/ProgTutorial/Parsing.thy Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Parsing.thy Tue May 05 03:21:49 2009 +0200
@@ -1078,10 +1078,10 @@
An example of a very simple method is:
*}
-method_setup %gray foobar =
+method_setup %gray foo =
{* Scan.succeed
(K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
- "foobar method for conjE and conjI"
+ "foo method for conjE and conjI"
text {*
It defines the method @{text foobar}, which takes no arguments (therefore the
@@ -1091,7 +1091,7 @@
*}
lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
-apply(foobar)
+apply(foo)
txt {*
where it results in the goal state
--- a/ProgTutorial/document/root.tex Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/document/root.tex Tue May 05 03:21:49 2009 +0200
@@ -107,6 +107,11 @@
\renewcommand{\isatagsmall}{\begingroup\small}
\renewcommand{\endisatagsmall}{\endgroup}
+% for code that should not be printed
+\isakeeptag{no}
+\renewcommand{\isatagno}{}
+\renewcommand{\endisatagno}{}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\small\item\relax}
Binary file progtutorial.pdf has changed