diff -r 1aaa15ef731b -r 647cab4a72c2 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Wed Apr 01 12:29:10 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Apr 01 15:42:47 2009 +0100
@@ -1,5 +1,5 @@
 theory Ind_Code
-imports "../Base" "../FirstSteps" Ind_Interface Ind_General_Scheme
+imports "../Base" "../FirstSteps" Ind_General_Scheme
 begin
 
 section {* The Gory Details\label{sec:code} *} 
@@ -249,8 +249,8 @@
 *}
 
 lemma 
-  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  shows "\<forall>x y z. P x y z \<Longrightarrow> True"
+fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 apply (tactic {* 
   inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {* 
@@ -495,14 +495,14 @@
 *}
 
 lemma all_elims_test:
-  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  shows "\<forall>x y z. P x y z" sorry
+fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+shows "\<forall>x y z. P x y z" sorry
 
 lemma imp_elims_test:
-  shows "A \<longrightarrow> B \<longrightarrow> C" sorry
+shows "A \<longrightarrow> B \<longrightarrow> C" sorry
 
 lemma imp_elims_test':
-  shows "A" "B" sorry
+shows "A" "B" sorry
 
 text {*
   The function @{ML all_elims} takes a list of (certified) terms and instantiates
@@ -535,7 +535,7 @@
 *}
 
 lemma fresh_Lam:
-  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*<*)oops(*>*)
 
 text {*
@@ -556,7 +556,7 @@
 
 (*<*)
 lemma fresh_Lam:
-  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*>*)
 apply(tactic {* expand_tac @{thms fresh_def} *})
 
@@ -652,7 +652,7 @@
 
 (*<*)
 lemma fresh_Lam:
-  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 apply(tactic {* expand_tac @{thms fresh_def} *})
 (*>*)
 apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})
@@ -714,7 +714,7 @@
 
 (*<*)
 lemma fresh_Lam:
-  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 apply(tactic {* expand_tac @{thms fresh_def} *})
 (*>*)
 apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
@@ -784,7 +784,7 @@
 *}
 
 lemma fresh_Lam:
-  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 apply(tactic {* expand_tac @{thms fresh_def} *})
 apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 done
@@ -798,7 +798,7 @@
 *}
 
 lemma accpartI:
-  shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})
 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
@@ -879,7 +879,7 @@
 *}
 
 lemma accpartI:
-  shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})
 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})
 done
@@ -901,15 +901,15 @@
 *}
 
 lemma even0_intro:
-  shows "even 0"
+shows "even 0"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 0 @{context} *})
 
 lemma evenS_intro:
-  shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
+shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 1 @{context} *})
 
 lemma fresh_App:
-  shows "\<And>a t s. \<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
+shows "\<And>a t s. \<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
 by (tactic {* 
   intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *})
 
@@ -1028,148 +1028,8 @@
   indicates that the first premise of the induction principle (namely
   the predicate over which the induction proceeds) is eliminated. 
 
-  (FIXME: What does @{ML Induct.induct_pred} do?)
-
-  (FIXME: why the mut-name?)
-
-  (FIXME: What does @{ML Binding.qualify} do?)
-
-
   This completes all the code and fits in with the ``front end'' described
-  in Section \ref{sec:interface}
-*}
-
-
-ML{*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{*val spec_parser = 
-   OuterParse.fixes -- 
-   Scan.optional 
-     (OuterParse.$$$ "where" |--
-        OuterParse.!!! 
-          (OuterParse.enum1 "|" 
-             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
-
-ML{*val specification =
-  spec_parser >>
-    (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
-
-ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
-              "define inductive predicates"
-                 OuterKeyword.thy_decl specification*}
-
-
-section {* Extensions (TBD) *}
-
-text {*
-  Things to include at the end:
-
-  \begin{itemize}
-  \item include the code for the parameters
-  \item say something about add-inductive-i to return
-  the rules
-  \item say that the induction principle is weaker (weaker than
-  what the standard inductive package generates)
-  \item say that no conformity test is done
-  \item exercise about strong induction principles
-  \item exercise about the test for the intro rules
-  \end{itemize}
-  
+  in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. Why the mut-name? 
+  What does @{ML Binding.qualify} do?}
 *}
-
-(*
-simple_inductive
-  Even and Odd
-where
-  Even0: "Even 0"
-| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
-| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
-
-thm Even0
-thm EvenS
-thm OddS
-
-thm Even_Odd.intros
-thm Even.induct
-thm Odd.induct
-
-thm Even_def
-thm Odd_def
-*)
-
-(*
-text {* 
-  Second, we want that the user can specify fixed parameters.
-  Remember in the previous section we stated that the user can give the 
-  specification for the transitive closure of a relation @{text R} as 
-*}
-*)
-
-(*
-simple_inductive
-  trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota>\<iota> R x x"
-| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
-*)
-
-(*
-text {*
-  Note that there is no locale given in this specification---the parameter
-  @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
-  stays fixed throughout the specification. The problem with this way of
-  stating the specification for the transitive closure is that it derives the
-  following induction principle.
-
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
-            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
-  \end{center}
-
-  But this does not correspond to the induction principle we derived by hand, which
-  was
-  
-  
-  %\begin{center}\small
-  %\mprset{flushleft}
-  %\mbox{\inferrule{
-  %           @ { thm_style prem1  trcl_induct[no_vars]}\\\\
-  %           @ { thm_style prem2  trcl_induct[no_vars]}\\\\
-  %           @ { thm_style prem3  trcl_induct[no_vars]}}
-  %          {@ { thm_style concl  trcl_induct[no_vars]}}}  
-  %\end{center}
-
-  The difference is that in the one derived by hand the relation @{term R} is not
-  a parameter of the proposition @{term P} to be proved and it is also not universally
-  qunatified in the second and third premise. The point is that the parameter @{term R}
-  stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
-  argument of the transitive closure, but one that can be freely instantiated. 
-  In order to recognise such parameters, we have to extend the specification
-  to include a mechanism to state fixed parameters. The user should be able
-  to write 
-
-*}
-*)
-(*
-simple_inductive
-  trcl'' for R :: "'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
-  accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
-*)
 (*<*)end(*>*)
\ No newline at end of file