--- 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