2 imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims

     2 imports "../Base" "../FirstSteps" Ind_General_Scheme 

     5 datatype trm =

     5 section {* The Gory Details *} 

     6   Var "string"

     7 | App "trm" "trm"

     8 | Lam "string" "trm"

     9 

    10 simple_inductive 

    11   fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)

    12 where

    13   "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"

    14 | "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"

    15 | "a\<sharp>Lam a t"

    16 | "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"

    17 

    18 section {* Code *}

    19 

    20 text {*

    21   

    22   @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}

    23 

    24   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}

    25 

    26   @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}

    27   

    28   @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}

    29 

    30   @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}

    31 

    32   \underline{Induction proof}

    33   

    34   After ``objectivication'' we have 

    35    @{text "pred zs"} and @{text "orules[preds::=Ps]"}; and have to show

    36   @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.

    37   Instantiating the @{text "preds"} with @{text "Ps"} gives

    38   @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.

    39 

    40   \underline{Intro proof}

    41 

    42   Assume we want to prove the $i$th intro rule. 

    43 

    44   We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};

    45   expanding the defs, gives 

    46   

    47   @{text [display]

    48   "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}

    49   

    50   By applying as many allI and impI as possible, we have

    51   

    52   @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},

    53   @{text "orules"}; and have to show @{text "pred ts"}

    54 

    55   the $i$th @{text "orule"} is of the 

    56   form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.

    57   

    58   So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)

    59   and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions

    60   @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.

    61 

    62 

    63   \begin{center}

    64   ****************************

    65   \end{center}

    66 *}

    67 

    68 

    69 text {*

    70   For building testcases let us give some shorthands for the definitions of @{text "even/odd"} and

    71   @{text "fresh"}. (FIXME put in a figure)

    72 *}

    73   

    74 ML{*val eo_defs = [@{thm even_def}, @{thm odd_def}]

    75 val eo_rules =  

    76   [@{prop "even 0"},

    77    @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},

    78    @{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]

    79 val eo_orules =  

    80   [@{prop "even 0"},

    81    @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},

    82    @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]

    83 val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 

    84 val eo_prednames = [@{binding "even"}, @{binding "odd"}]

    85 val eo_syns = [NoSyn, NoSyn] 

    86 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] *}

    87 

    88 

    89 ML{*val fresh_defs = [@{thm fresh_def}]

    90 val fresh_rules =  

    91   [@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"},

    92    @{prop "\<And>a s t. a\<sharp>t \<Longrightarrow> a\<sharp>s \<Longrightarrow> a\<sharp>App t s"},

    93    @{prop "\<And>a t. a\<sharp>Lam a t"},

    94    @{prop "\<And>a b t. a\<noteq>b \<Longrightarrow> a\<sharp>t \<Longrightarrow> a\<sharp>Lam b t"}]

    95 val fresh_orules =  

    96   [@{prop "\<forall>a b. a\<noteq>b \<longrightarrow> a\<sharp>Var b"},

    97    @{prop "\<forall>a s t. a\<sharp>t \<longrightarrow> a\<sharp>s \<longrightarrow> a\<sharp>App t s"},

    98    @{prop "\<forall>a t. a\<sharp>Lam a t"},

    99    @{prop "\<forall>a b t. a\<noteq>b \<longrightarrow> a\<sharp>t \<longrightarrow> a\<sharp>Lam b t"}]

   100 val fresh_preds =  [@{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"}] *}

   101 

   116 ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =

    20 ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy =

   127   theorem (others possibilities are the flags @{ML definitionK in Thm} and @{ML axiomK in Thm}). 

    31   theorem (others possibile flags are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 

   130   use @{ML empty_binding in Attrib} in Line 3, since the definition does 

    34   use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates 

   131   not need to have any theorem attributes. A testcase for this function is

    35   the definitions do not need to have any theorem attributes. A testcase for this 

    36   function is

   137   val (def, lthy') = make_defs arg lthy 

    42   val (def, lthy') = make_defn arg lthy 

   143   which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 

    48   which introduces the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 

   163   The first function constructs the term for one particular predicate, say

    68   The first function constructs the term for one particular predicate (the

   164   @{text "pred"}. The number of arguments of this predicate is

    69   argument @{text "pred"} in the code belo). The number of arguments of this predicate is

   169 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =

    74 ML %linenosgray{*fun defn_aux lthy orules preds (pred, arg_tys) =

   205   val def = defs_aux lthy eo_orules eo_preds (pred, arg_tys)

   110   val def = defn_aux lthy eo_orules eo_preds (pred, arg_tys)

   211   The testcase  calls @{ML defs_aux} for the predicate @{text "even"} and prints

   116   The testcase  calls @{ML defn_aux} for the predicate @{text "even"} and prints

   219   @{ML defs_aux} over all predicates. The argument @{text "preds"} is again

   142   @{ML defn_aux} over all predicates. The argument @{text "preds"} is again

   226 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =

   149 ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy =

   230   val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 

   153   val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 

   231 in

   154 in

   232   fold_map make_defs (prednames ~~ syns ~~ defs) lthy

   155   fold_map make_defn (prednames ~~ syns ~~ defs) lthy

   242   to @{ML defs_aux} in Line 5 produces all right-hand sides of the

   165   to @{ML defn_aux} in Line 5 produces all right-hand sides of the

   251     definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy

   174     defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy

   261   \begin{isabelle}

   184   @{text [display, break]

   262   @{text [break]

   185 "even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))  

   263 "> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   186                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,

   264 >                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,

   187 odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   265 > odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   188                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}

   266 >                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}

   267   \end{isabelle}

   271   on the ambient theory. The reason is that if we make again the

   192   on the ambient theory. The reason is that if we introduce the

   272   definition, we pollute the name space with two versions of @{text "even"} 

   193   definition again, we pollute the name space with two versions of @{text "even"} 

   275   This completes the code for making the definitions. Next we deal with

   196   This completes the code for introducing the definitions. Next we deal with

   279 subsection {* Introduction Rules *}

   200 subsection {* Induction Principles *}

   286 lemma manual_ind_prin: 

   207 lemma manual_ind_prin_even: 

   341 ML %linenosgray{*fun induction_tac defs prem insts =

   262 ML %linenosgray{*fun ind_tac defs prem insts =

   349   We have to give it as arguments the definitions, the premise 

   270   We have to give it as arguments the definitions, the premise (this premise

   350   (for example @{text "even n"}) and the instantiations. Compare this with the 

   271   is @{text "even n"} in lemma @{thm [source] manual_ind_prin_even}) and the

   351   manual proof given for the lemma @{thm [source] manual_ind_prin}: 

   272   instantiations. Compare this tactic with the manual for the lemma @{thm

   352   as you can see there is almost a one-to-one correspondence between the \isacommand{apply}-script 

   273   [source] manual_ind_prin_even}: as you can see there is almost a one-to-one

   353   and the @{ML induction_tac}. A testcase for this tactic is the function

   274   correspondence between the \isacommand{apply}-script and the @{ML

   354 *}

   275   ind_tac}. Two testcases for this tactic are:

   355 

   276 *}

   356 ML{*fun test_tac prem = 

   277 

   357 let

   278 lemma automatic_ind_prin_even:

   358   val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]

   359 in 

   360   induction_tac eo_defs prem insts 

   361 end*}

   362 

   363 text {*

   364   which indeed proves the induction principle: 

   365 *}

   366 

   367 lemma automatic_ind_prin:

   370 apply(tactic {* test_tac @{thms prem} *})

   281 by (tactic {* ind_tac eo_defs @{thms prem} 

   371 done

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

   372 

   283 

   373 text {*

   284 lemma automatic_ind_prin_fresh:

   374   This gives the theorem:

   285 assumes prem: "fresh z za" 

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

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

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

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

   290 by (tactic {* ind_tac @{thms fresh_def} @{thms prem} 

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

   292 

   293 

   294 text {*

   295   Let us have a closer look at the first proved theorem:

   377   \isacommand{thm}~@{thm [source] automatic_ind_prin}\\

   298   \isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\

   378   @{text "> "}~@{thm automatic_ind_prin}

   299   @{text "> "}~@{thm automatic_ind_prin_even}

   381   While the tactic for the induction principle is relatively simple, 

   302   The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic

   382   it is a bit harder to construct the goals from the introduction 

   303   variables (since they are not quantified in the lemma). These schematic

   383   rules the user provides. In general we have to construct for each predicate 

   304   variables are needed so that they can be instantiated by the user later

   384   @{text "pred"} a goal of the form

   305   on. We have to take care to also generate these schematic variables when

   306   generating the goals for the induction principles. While the tactic for

   307   proving the induction principles is relatively simple, it will be a bit

   308   of work to construct the goals from the introduction rules the user

   309   provides. In general we have to construct for each predicate @{text "pred"}

   310   a goal of the form

   400   "pred"} is the predicate for which we prove the introduction principle;

   326   "pred"} is the predicate for which we prove the induction principle;

   405 ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) =

   331 ML %linenosgray{*fun prove_ind lthy defs srules cnewpreds ((pred, newpred), arg_tys) =

   416   (fn {prems, ...} => induction_tac defs prems cnewpreds)

   342       (fn {prems, ...} => ind_tac defs prems cnewpreds)

   423   \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In 

   349   \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. 

   424   Line 5 we construct the terms corresponding to these variables. 

   350   That means they are not (yet) schematic variables.

   351   In Line 5 we construct the terms corresponding to these variables. 

   440   "lthy'"} (which contains the @{text "zs"} as free) to @{text

   367   "lthy'"} (which contains the @{text "zs"} as free variables) to @{text

   447   val srules = [@{prop "P (0::nat)"},

   374   val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]

   448                 @{prop "\<And>n::nat. Q n \<Longrightarrow> P (Suc n)"},

   449                 @{prop "\<And>n::nat. P n \<Longrightarrow> Q (Suc n)"}] 

   451   val pred = @{term "even::nat\<Rightarrow>bool"}

   376   val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules

   455     prove_induction lthy eo_defs srules cnewpreds ((pred, newpred), arg_tys)

   379        prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)

   458 end *} 

   382 end *}

   459 

   383 

   460 text {*

   384 text {*

   461   This prints out:

   385   This prints out the theorem:

   466   Note that the export from @{text lthy'} to @{text lthy} in Line 13 above 

   390   The export from @{text lthy'} to @{text lthy} in Line 13 above 

   467   has turned the free, but fixed, @{text "z"} into a schematic 

   391   has correctly turned the free, but fixed, @{text "z"} into a schematic 

   472   rules are substituted and iterate @{ML prove_induction} over all

   396   rules are substituted and iterate @{ML prove_ind} over all

   476 ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =

   400 ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =

   489   map (prove_induction lthy' defs srules cnewpreds) 

   413   map (prove_ind lthy' defs srules cnewpreds) 

   514   val ind_thms = inductions eo_rules eo_defs eo_preds eo_arg_tyss lthy

   438   val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy

   524 "> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> 

   448 "even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> 

   525 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,

   449  (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,

   526 > odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>

   450 odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>

   527 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}

   451  (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}

   530   variables. The numbers have been introduced by the pretty-printer and are 

   454   variables. The numbers attached to these variables have been introduced by 

   531   not significant.

   455   the pretty-printer and are \emph{not} important for the user. 

   532 

   456 

   533   This completes the code for the induction principles.  

   457   This completes the code for the induction principles. The final peice

   458   of reasoning infrastructure we need are the introduction rules. 

   539   Finally we can prove the introduction rules. Their proofs are quite a bit

   464   The proofs of the introduction rules are quite a bit

   540   more involved. To ease these proofs somewhat we use the following two helper

   465   more involved than the ones for the induction principles. 

   466   To ease somewhat our work here, we use the following two helper

   568   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows

   492   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:

   580   For example: 

   504   For example we can eliminate the preconditions @{text "A"} and @{text "B"} from

   505   @{thm [source] imp_elims_test}:

   587   We now look closely at the proof for the introduction rule

   512   To explain the proof for the introduction rule, our running example will be

   513   the rule:

   590   @{term "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"}

   516   @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}

   593 *}

   519   for freshness of applications. We set up the proof as follows:

   594 

   520 *}

   597   shows "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"

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

   598 apply(tactic {* ObjectLogic.rulify_tac 1 *})

   524 (*<*)oops(*>*)

   599 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})

   525 

   600 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})

   526 text {*

   601 apply(tactic {* print_tac "" *})

   527   The first step will be to expand the definitions of freshness

   528   and then introduce quantifiers and implications. For this we

   529   will use the tactic

   530 *}

   531 

   532 ML{*fun expand_tac defs =

   533   ObjectLogic.rulify_tac 1

   534   THEN rewrite_goals_tac defs

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

   536 

   537 text {*

   538   The first step of ``rulifying'' the lemma will turn out important

   539   later on. Applying this tactic 

   540 *}

   541 

   542 (*<*)

   543 lemma fresh_App:

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

   545 (*>*)

   546 apply(tactic {* expand_tac @{thms fresh_def} *})

   605   @{subgoals}

   552   @{subgoals [display]}

   607 *}

   554 

   608 

   555   As you can see, there are parameters (namely @{text "a"}, @{text "b"} 

   609 ML_prf {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}

   556   and @{text "t"}) which come from the introduction rule and parameters

   610 

   557   (in the case above only @{text "fresh"}) which come from the universal

   611 apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>

   558   quantification in the definition @{term "fresh a (App t s)"}.

   612    let

   559   Similarly, there are preconditions

   613      val (prems1, prems2) = chop (length prems - length fresh_rules) prems

   560   that come from the premises of the rule and premises from the

   614      val (params1, params2) = chop (length params - length fresh_preds) params

   561   definition. We need to treat these 

   615    in

   562   parameters and preconditions differently. In the code below

   616      no_tac

   563   we will therefore separate them into @{text "params1"} and @{text params2},

   617    end) @{context} *})

   564   respectively @{text "prems1"} and @{text "prems2"}. To do this 

   618 oops

   565   separation, it is best to open a subproof with the tactic 

   619 

   566   @{ML SUBPROOF}, since this tactic provides us

   620 

   567   with the parameters (as list of @{ML_type cterm}s) and the premises

   621 ML{*fun subproof2 prem params2 prems2 =  

   568   (as list of @{ML_type thm}s). The problem we have to overcome 

   622  SUBPROOF (fn {prems, ...} =>

   569   with @{ML SUBPROOF} is that this tactic always expects us to completely 

   623    let

   570   discharge with the goal (see Section ???). This is inconvenient for

   624      val prem' = prems MRS prem;

   571   our gradual explanation of the proof. To circumvent this inconvenience

   625      val prem'' = 

   572   we use the following modified tactic: 

   626        case prop_of prem' of

   573 *}

   574 (*<*)oops(*>*)

   575 ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}

   576 

   577 text {*

   578   If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will

   579   still succeed. With this testing tactic, we can gradually implement

   580   all necessary proof steps.

   581 *}

   582 

   583 text_raw {*

   584 \begin{figure}[t]

   585 \begin{minipage}{\textwidth}

   586 \begin{isabelle}

   587 *}

   588 ML{*fun chop_print params1 params2 prems1 prems2 ctxt =

   589 let 

   590   val s = ["Params1 from the rule:", str_of_cterms ctxt params1] 

   591         @ ["Params2 from the predicate:", str_of_cterms ctxt params2] 

   592         @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) 

   593         @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) 

   594 in 

   595   s |> separate "\n"

   596     |> implode

   597     |> warning

   598 end*}

   599 text_raw{*

   600 \end{isabelle}

   601 \end{minipage}

   602 \caption{FIXME\label{fig:chopprint}}

   603 \end{figure}

   604 *}

   605 

   606 text {*

   607   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}

   608   from @{text "params"} and @{text "prems"}, respectively. To see what is

   609   going in our example, we will print out the values using the printing

   610   function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will

   611   supply us the @{text "params"} and @{text "prems"} as lists, we can 

   612   separate them using the function @{ML chop}. 

   613 *}

   614 

   615 ML{*fun chop_test_tac preds rules =

   616   SUBPROOF_test (fn {params, prems, context, ...} =>

   617   let

   618     val (params1, params2) = chop (length params - length preds) params

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

   620   in

   621     chop_print params1 params2 prems1 prems2 context; no_tac

   622   end) *}

   623 

   624 text {* 

   625   For the separation we can rely on that Isabelle deterministically 

   626   produces parameter and premises in a goal state. The last parameters

   627   that were introduced, come from the quantifications in the definitions.

   628   Therefore we only have to subtract the number of predicates (in this

   629   case only @{text "1"} from the lenghts of all parameters. Similarly

   630   with the @{text "prems"}. The last premises in the goal state must

   631   come from unfolding of the conclusion. So we can just subtract

   632   the number of rules from the number of all premises. Applying

   633   this tactic in our example 

   634 *}

   635 

   636 (*<*)

   637 lemma fresh_App:

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

   639 apply(tactic {* expand_tac @{thms fresh_def} *})

   640 (*>*)

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

   642 (*<*)oops(*>*)

   643 

   644 text {*

   645   gives

   646 

   647   \begin{isabelle}

   648   @{text "Params1 from the rule:"}\\

   649   @{text "a, b, t"}\\

   650   @{text "Params2 from the predicate:"}\\

   651   @{text "fresh"}\\

   652   @{text "Prems1 from the rule:"}\\

   653   @{term "a \<noteq> b"}\\

   654   @{text [break]

   655 "\<forall>fresh.

   656       (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>

   657       (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>

   658       (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> 

   659       (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\

   660    @{text "Prems2 from the predicate:"}\\

   661    @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\

   662    @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\

   663    @{term "\<forall>a t. fresh a (Lam a t)"}\\

   664    @{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}

   665   \end{isabelle}

   666 

   667 

   668   We now have to select from @{text prems2} the premise 

   669   that corresponds to the introduction rule we prove, namely:

   670 

   671   @{term [display] "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}

   672 

   673   To use this premise with @{ML rtac}, we need to instantiate its 

   674   quantifiers (with @{text params1}) and transform it into a 

   675   introduction rule (using @{ML "ObjectLogic.rulify"}. 

   676   So we can modify the subproof as follows:

   677 *}

   678 

   679 ML{*fun apply_prem_tac i preds rules =

   680   SUBPROOF_test (fn {params, prems, context, ...} =>

   681   let

   682     val (params1, params2) = chop (length params - length preds) params

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

   684   in

   685     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1

   686     THEN print_tac ""

   687     THEN no_tac

   688   end) *}

   689 

   690 text {* and apply it with *}

   691 

   692 (*<*)

   693 lemma fresh_App:

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

   695 apply(tactic {* expand_tac @{thms fresh_def} *})

   696 (*>*)

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

   698 (*<*)oops(*>*)

   699 

   700 text {*

   701   Since we print out the goal state after the @{ML rtac} we can see

   702   the goal state has the two subgoals

   703 

   704   \begin{isabelle}

   705   @{text "1."}~@{prop "a \<noteq> b"}\\

   706   @{text "2."}~@{prop "fresh a t"}

   707   \end{isabelle}

   708 

   709   where the first comes from a non-recursive precondition of the rule

   710   and the second comes from a recursive precondition. The first kind

   711   can be solved immediately by @{text "prems1"}. The second kind

   712   needs more work. It can be solved with the other premise in @{text "prems1"},

   713   namely

   714 

   715   @{term [break,display]

   716   "\<forall>fresh.

   717       (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>

   718       (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>

   719       (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> 

   720       (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}

   721 

   722   but we have to instantiate it appropriately. These instantiations

   723   come from @{text "params1"} and @{text "prems2"}. We can determine

   724   whether we are in the simple or complicated case by checking whether

   725   the topmost connective is @{text "\<forall>"}. The premises in the simple

   726   case cannot have such a quantification, since in the first step 

   727   of @{ML "expand_tac"} was the ``rulification'' of the lemma. So 

   728   we can implement the following function

   729 *}

   730 

   731 ML{*fun prepare_prem params2 prems2 prem =  

   732   rtac (case prop_of prem of

   628              prem' |> all_elims params2 

   734                  prem |> all_elims params2 

   629                    |> imp_elims prems2

   735                       |> imp_elims prems2

   630          | _ => prem';

   736          | _ => prem) *}

   631    in 

   737 

   632      rtac prem'' 1 

   738 text {* 

   633    end)*}

   739   which either applies the premise outright or if it had an

   634 

   740   outermost universial quantification, instantiates it first with 

   635 text {*

   741   @{text "params1"} and then @{text "prems1"}. The following tactic 

   636 

   742   will therefore prove the lemma.

   637 *}

   743 *}

   638 

   744 

   639 

   745 ML{*fun prove_intro_tac i preds rules =

   640 ML %linenosgray{*fun subproof1 rules preds i = 

   746   SUBPROOF (fn {params, prems, context, ...} =>

   641  SUBPROOF (fn {params, prems, context = ctxt', ...} =>

   747   let

   642    let

   748     val (params1, params2) = chop (length params - length preds) params

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

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

   644      val (params1, params2) = chop (length params - length preds) params

   750   in

   645    in

   751     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1

   646      rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 

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

   647      (* applicateion of the i-ith intro rule *)

   753   end) *}

   648      THEN

   754 

   649      EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)

   755 text {*

   650    end)*}

   756   We can complete the proof of the introduction rule now as follows:

   651 

   757 *}

   652 text {*

   758 

   653   @{text "params1"} are the variables of the rules; @{text "params2"} is

   759 (*<*)

   654   the variables corresponding to the @{text "preds"}.

   760 lemma fresh_App:

   655 

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

   656   @{text "prems1"} are the assumption corresponding to the rules;

   762 apply(tactic {* expand_tac @{thms fresh_def} *})

   657   @{text "prems2"} are the assumptions coming from the allIs/impIs

   763 (*>*)

   658 

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

   659   you instantiate the parameters i-th introduction rule with the parameters

   765 done

   660   that come from the rule; and you apply it to the goal

   766 

   661 

   767 text {* 

   662   this now generates subgoals corresponding to the premisses of this

   768   Unfortunately, not everything is done yet.

   663   intro rule 

   769 *}

   770 

   771 lemma accpartI:

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

   773 apply(tactic {* expand_tac @{thms accpart_def} *})

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

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

   776 

   777 txt {*

   778   

   779   @{subgoals [display]}

   780 

   781   \begin{isabelle}

   782   @{text "Params1 from the rule:"}\\

   783   @{text "x"}\\

   784   @{text "Params2 from the predicate:"}\\

   785   @{text "P"}\\

   786   @{text "Prems1 from the rule:"}\\

   787   @{text "R ?y x \<Longrightarrow> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P ?y"}\\

   788   @{text "Prems2 from the predicate:"}\\

   789   @{term "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x"}\\

   790   \end{isabelle}

   791 

   792 *}

   793 (*<*)oops(*>*)

   794 

   795 

   796 ML{*fun prepare_prem params2 prems2 ctxt prem =  

   797   SUBPROOF (fn {prems, ...} =>

   798   let

   799     val prem' = prems MRS prem

   800   in 

   801     rtac (case prop_of prem' of

   802            _ $ (Const (@{const_name All}, _) $ _) =>

   803                  prem' |> all_elims params2 

   804                        |> imp_elims prems2

   805          | _ => prem') 1

   806   end) ctxt *}

   807 

   808 ML{*fun prove_intro_tac i preds rules =

   809   SUBPROOF (fn {params, prems, context, ...} =>

   810   let

   811     val (params1, params2) = chop (length params - length preds) params

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

   813   in

   814     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1

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

   816   end) *}

   817 

   818 lemma accpartI:

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

   820 apply(tactic {* expand_tac @{thms accpart_def} *})

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

   822 done

   823 

   824 

   825 

   826 text {*

   827 

   671           subproof1 rules preds i ctxt]*}

   835           prove_intro_tac i preds rules ctxt]*}

   695 ML{*fun introductions rules preds defs lthy = 

   859 ML{*fun intros rules preds defs lthy = 

   716   val (defs, lthy') = definitions rules preds prednames syns tyss lthy      

   880   val (defs, lthy') = defns rules preds prednames syns tyss lthy      

   717   val ind_rules = inductions rules defs preds tyss lthy' 	

   881   val ind_rules = inds rules defs preds tyss lthy' 	

   718   val intro_rules = introductions rules preds defs lthy'

   882   val intro_rules = intros rules preds defs lthy'