251 text {*

   251 text {*

   252   The complete tactic for proving the induction principles can now

   252   The complete tactic for proving the induction principles can now

   253   be implemented as follows:

   253   be implemented as follows:

   254 *}

   254 *}

   255 

   255 

   258           cut_facts_tac prem,

   258           cut_facts_tac prem,

   260           inst_spec_tac insts,

   260           inst_spec_tac insts,

   261           assume_tac]*}

   261           assume_tac]*}

   262 

   262 

   263 text {*

   263 text {*

   264   We have to give it as arguments the definitions, the premise (a list of

   264   We have to give it as arguments the definitions, the premise (a list of

   275 *}

   275 *}

   276 

   276 

   277 lemma automatic_ind_prin_even:

   277 lemma automatic_ind_prin_even:

   278 assumes prem: "even z"

   278 assumes prem: "even z"

   279 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"

   279 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"

   281                     [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})

   281                     [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})

   282 

   282 

   283 lemma automatic_ind_prin_fresh:

   283 lemma automatic_ind_prin_fresh:

   284 assumes prem: "fresh z za" 

   284 assumes prem: "fresh z za" 

   285 shows "(\<And>a b. a \<noteq> b \<Longrightarrow> P a (Var b)) \<Longrightarrow> 

   285 shows "(\<And>a b. a \<noteq> b \<Longrightarrow> P a (Var b)) \<Longrightarrow> 

   286         (\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>

   286         (\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>

   287         (\<And>a t. P a (Lam a t)) \<Longrightarrow> 

   287         (\<And>a t. P a (Lam a t)) \<Longrightarrow> 

   288         (\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"

   288         (\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"

   290                           [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})

   290                           [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})

   291 

   291 

   292 

   292 

   293 text {*

   293 text {*

   294   While the tactic for proving the induction principles is relatively simple,

   294   While the tactic for proving the induction principles is relatively simple,

   338   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))

   338   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))

   339   val goal = Logic.list_implies 

   339   val goal = Logic.list_implies 

   340          (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   340          (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   341 in

   341 in

   342   Goal.prove lthy' [] [prem] goal

   342   Goal.prove lthy' [] [prem] goal

   344   |> singleton (Proof_Context.export lthy' lthy)

   344   |> singleton (Proof_Context.export lthy' lthy)

   345 end *}

   345 end *}

   346 

   346 

   347 text {* 

   347 text {* 

   348   In Line 3 we produce names @{text "zs"} for each type in the 

   348   In Line 3 we produce names @{text "zs"} for each type in the 

   537   The first step in the proof will be to expand the definitions of freshness

   537   The first step in the proof will be to expand the definitions of freshness

   538   and then introduce quantifiers and implications. For this we

   538   and then introduce quantifiers and implications. For this we

   539   will use the tactic

   539   will use the tactic

   540 *}

   540 *}

   541 

   541 

   545   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}

   545   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}

   546 

   546 

   547 text {*

   547 text {*

   548   The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} 

   548   The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} 

   549   This will turn out to 

   549   This will turn out to 

   552 

   552 

   553 (*<*)

   553 (*<*)

   554 lemma fresh_Lam:

   554 lemma fresh_Lam:

   555 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   555 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   556 (*>*)

   556 (*>*)

   558 

   558 

   559 txt {*

   559 txt {*

   560   gives us the goal state

   560   gives us the goal state

   561 

   561 

   562   \begin{isabelle}

   562   \begin{isabelle}

   643 *}

   643 *}

   644 

   644 

   645 (*<*)

   645 (*<*)

   646 lemma fresh_Lam:

   646 lemma fresh_Lam:

   647 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   647 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   649 (*>*)

   649 (*>*)

   650 apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})

   650 apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})

   651 (*<*)oops(*>*)

   651 (*<*)oops(*>*)

   652 

   652 

   653 text {*

   653 text {*

   690   let

   690   let

   691     val cparams = map snd params

   691     val cparams = map snd params

   692     val (params1, params2) = chop (length cparams - length preds) cparams

   692     val (params1, params2) = chop (length cparams - length preds) cparams

   693     val (prems1, prems2) = chop (length prems - length rules) prems

   693     val (prems1, prems2) = chop (length prems - length rules) prems

   694   in

   694   in

   696   end) *}

   696   end) *}

   697 

   697 

   698 text {* 

   698 text {* 

   699   The argument @{text i} corresponds to the number of the 

   699   The argument @{text i} corresponds to the number of the 

   700   introduction we want to prove. We will later on let it range

   700   introduction we want to prove. We will later on let it range

   704 *}

   704 *}

   705 

   705 

   706 (*<*)

   706 (*<*)

   707 lemma fresh_Lam:

   707 lemma fresh_Lam:

   708 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   708 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   710 (*>*)

   710 (*>*)

   711 apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})

   711 apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})

   712 (*<*)oops(*>*)

   712 (*<*)oops(*>*)

   713 

   713 

   714 text {*

   714 text {*

   757   with  @{text "params1"} and then @{text "prems1"}. The following 

   757   with  @{text "params1"} and then @{text "prems1"}. The following 

   758   tactic will therefore prove the lemma completely.

   758   tactic will therefore prove the lemma completely.

   759 *}

   759 *}

   760 

   760 

   761 ML %grayML{*fun prove_intro_tac i preds rules =

   761 ML %grayML{*fun prove_intro_tac i preds rules =

   763   let

   763   let

   764     val cparams = map snd params

   764     val cparams = map snd params

   765     val (params1, params2) = chop (length cparams - length preds) cparams

   765     val (params1, params2) = chop (length cparams - length preds) cparams

   766     val (prems1, prems2) = chop (length prems - length rules) prems

   766     val (prems1, prems2) = chop (length prems - length rules) prems

   767   in

   767   in

   769     THEN EVERY1 (map (prepare_prem params2 prems2) prems1)

   769     THEN EVERY1 (map (prepare_prem params2 prems2) prems1)

   770   end) *}

   770   end) *}

   771 

   771 

   772 text {*

   772 text {*

   773   Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. 

   773   Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. 

   774   The full proof of the introduction rule is as follows:

   774   The full proof of the introduction rule is as follows:

   775 *}

   775 *}

   776 

   776 

   777 lemma fresh_Lam:

   777 lemma fresh_Lam:

   778 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   778 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

   780 apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})

   780 apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})

   781 done

   781 done

   782 

   782 

   783 text {* 

   783 text {* 

   784   Phew!\ldots  

   784   Phew!\ldots  

   791 *}

   791 *}

   792 

   792 

   793 

   793 

   794 lemma accpartI:

   794 lemma accpartI:

   795 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   795 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   797 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})

   797 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})

   798 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})

   798 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})

   799 

   799 

   800 txt {*

   800 txt {*

   801   Here @{ML chop_test_tac} prints out the following

   801   Here @{ML chop_test_tac} prints out the following

   862   let

   862   let

   863     val cparams = map snd params

   863     val cparams = map snd params

   864     val (params1, params2) = chop (length cparams - length preds) cparams

   864     val (params1, params2) = chop (length cparams - length preds) cparams

   865     val (prems1, prems2) = chop (length prems - length rules) prems

   865     val (prems1, prems2) = chop (length prems - length rules) prems

   866   in

   866   in

   868     THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)

   868     THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)

   869   end) *}

   869   end) *}

   870 

   870 

   871 text {*

   871 text {*

   872   With these two functions we can now also prove the introduction

   872   With these two functions we can now also prove the introduction

   873   rule for the accessible part. 

   873   rule for the accessible part. 

   874 *}

   874 *}

   875 

   875 

   876 lemma accpartI:

   876 lemma accpartI:

   877 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   877 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   879 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})

   879 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})

   880 done

   880 done

   881 

   881 

   882 text {*

   882 text {*

   883   Finally we need two functions that string everything together. The first

   883   Finally we need two functions that string everything together. The first

   884   function is the tactic that performs the proofs.

   884   function is the tactic that performs the proofs.

   885 *}

   885 *}

   886 

   886 

   887 ML %linenosgray{*fun intro_tac defs rules preds i ctxt =

   887 ML %linenosgray{*fun intro_tac defs rules preds i ctxt =

   890           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),

   890           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),

   891           prove_intro_tac i preds rules ctxt]*}

   891           prove_intro_tac i preds rules ctxt]*}

   892 

   892 

   893 text {*

   893 text {*

   894   Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}. 

   894   Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}.