isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:1aaa15ef731b
+:647cab4a72c2
 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} *}
 text {*
 This tactic expects a list of @{ML_type cterm}s. It allows us in the
 proof below to instantiate the three quantifiers in the assumption.
 *}
 lemma
 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 {*
 We obtain the goal state
 To see what these functions do, let us suppose we have the following three
 theorems.
 *}
 lemma all_elims_test:
 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
 lemma imp_elims_test':
 shows "A" "B" sorry
 text {*
 The function @{ML all_elims} takes a list of (certified) terms and instantiates
 theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
 the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
 Now we set up the proof for the introduction rule as follows:
 *}
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*<*)oops(*>*)
 text {*
 The first step in the proof will be to expand the definitions of freshness
 and then introduce quantifiers and implications. For this we
 be important later on. Applying this tactic in our proof of @{text "fresh_Lem"}
 *}
 (*<*)
 lemma fresh_Lam:
 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} *})
 txt {*
 gives us the goal state
 Applying this tactic in our example
 *}
 (*<*)
 lemma fresh_Lam:
 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} *})
 (*<*)oops(*>*)
 we are proving the fourth introduction rule.
 *}
 (*<*)
 lemma fresh_Lam:
 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} *})
 (*<*)oops(*>*)
 Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}.
 The full proof of the introduction rule is as follows:
 *}
 lemma fresh_Lam:
 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
 text {*
 recursive premises have preconditions. The introduction rule
 of the accessible part is such a rule.
 *}
 lemma accpartI:
 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} *})
 txt {*
 With these two functions we can now also prove the introduction
 rule for the accessible part.
 *}
 lemma accpartI:
 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
 text {*
 Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}.
 Some testcases for this tactic are:
 *}
 lemma even0_intro:
 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)"
 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)"
 by (tactic {*
 intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *})
 text {*
 The second function sets up in Line 4 the goals to be proved (this is easy
 corresponds to the case names that are used by Isar to reference the proof
 obligations in the induction. The second @{ML "consumes 1" in RuleCases}
 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}
+in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. Why the mut-name?
-*}
+What does @{ML Binding.qualify} do?}
+*}
-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}
-*}
-(*
-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(*>*)

changeset 224	647cab4a72c2
parent 219	98d43270024f
child 237	0a8981f52045