# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1241486509 -7200
# Node ID dc95a56b19532c3954d773230d776d60cc562d8f
# Parent  6e0f56764ff8f7d160a22a7ab15df39ced4dd059
fixed the problem with double definition of even and odd

diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Package/Ind_General_Scheme.thy
--- 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
diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Package/Ind_Interface.thy
--- 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
diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Package/Ind_Prelims.thy
--- 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.
 *}
 
diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Package/Simple_Inductive_Package.thy
--- 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'
diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Parsing.thy
--- 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
 
diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/document/root.tex
--- 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}
diff -r 6e0f56764ff8 -r dc95a56b1953 progtutorial.pdf
Binary file progtutorial.pdf has changed