45   We use the following wrapper function to make the definition via

    43   In order to make definitions, we use the following wrapper for 

    46   @{ML LocalTheory.define}. The function takes a predicate name, a syntax

    44   @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax

    59   It returns the definition (as theorem) and the local theory in which this definition has 

    57   It returns the definition (as a theorem) and the local theory in which this definition has 

    61   theorem (others possibilities are @{ML definitionK in Thm} or @{ML axiomK in Thm}). 

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

    63   for tools such as finding theorems in the theorem database. We also

    61   for tools that, for example, find theorems in the theorem database. We also

    65   not need any theorem attributes. Note the definition has not yet been 

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

    66   stored in the theorem database. So at the moment we can only refer to it

    67   via the return value. A testcase for this functions is

    79   which prints out the theorem @{prop "MyTrue \<equiv> True"}. Since we are

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

    80   testing the function inside \isacommand{local\_setup} we have also

    76   Since we are testing the function inside \isacommand{local\_setup}, i.e.~make

    81   access to theorem associated with this definition.

    77   changes to the ambient theory, we can query the definition using the usual

    78   command \isacommand{thm}:

    88   The next function constructs the term for the definition, namely 

    85   The next two functions construct the terms we need for the definitions, namely 

    86   terms of the form 

    92   The variables @{text "\<^raw:$zs$>"} need to be chosen so to not occur

    90   The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur

    93   in the @{text orules} and also be distinct from @{text "pred"}. The function

    91   in the @{text orules} and also be distinct from @{text "preds"}. 

    94   constructs the term for one particular predicate @{text "pred"}; the number

    92 

    95   of @{text "\<^raw:$zs$>"} is determined by the nunber of types. 

    93   The first function constructs the term for one particular predicate @{text

    94   "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is

    95   determined by the number of argument types of @{text "arg_tys"}.

   115   The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the 

   115   The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this

   116   predicate is applied. For this it pairs every type with a string @{text [quotes] "z"} 

   116   it pairs every argument type with the string @{text [quotes] "z"} (Line 7);

   117   (Line 7); then generates variants for all these strings (names) so that they are 

   117   then generates variants for all these strings so that they are unique

   118   unique w.r.t.~to the orules and predicates; in Line 9 it generates the corresponding 

   118   w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the

   119   variable terms for the unique names.

   119   corresponding variable terms for the unique strings.

   120 

   120 

   121   The unique free variables are applied to the predicate (Line 11); then

   121   The unique free variables are applied to the predicate (Line 11) using the

   122   the @{text orules} are prefixed (Line 12); in Line 13 we

   122   function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in

   123   quantify over all predicates; and in line 14 we just abstract over all

   123   Line 13 we quantify over all predicates; and in line 14 we just abstract

   124   the (fresh)  @{text "\<^raw:$zs$>"}, i.e.~the arguments of the predicate.

   124   over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the

   125   predicate.

   143   It constructs the term for the predicate @{term "even"}. So we obtain as printout

   144   It constructs the left-hand side for the definition of @{term "even"}. So we obtain 

   144   the term

   145   as printout the term

   151   the function @{ML defs_aux} over all predicates. THis is what the

   152   the function @{ML defs_aux} over all predicates. 

   152   next function does. 

   165   The argument @{text "preds"} is the list of predicates as @{ML_type term}s;

   165   The argument @{text "preds"} is again the the list of predicates as 

   166   @{ML_type term}s;

   167   @{text "arg_tyss"} is the list of argument-type-lists. 

   168   @{text "arg_tyss"} is the list of argument-type-lists for each predicate. 

   168   

   169   

   169   In line 4 we generate the intro rules in the object logic; for this we have to 

   170   The user give the introduction rules using meta-implications and meta-quantifications.

   170   obtain the theory behind the local theory (Line 3); with this we can

   171   In line 4 we transform the introduction rules into the object logic (definitions

   171   call @{ML defs_aux} to generate the terms for the left-hand sides.

   172   cannot use them). To do the transformation we have to 

   172   The actual definitions are made in Line 7.

   173   obtain the theory behind the local theory (Line 3); with this theory 

   174   we can use the function @{ML ObjectLogic.atomize_term} to make the

   175   transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all

   176   left-hand sides of the definitions. The actual definitions are then made in Line 7.

   177   As the result we obtain a list of theorems and a local theory. 

   188   warning (str_of_thms lthy' defs); lthy

   193   warning (str_of_thms lthy' defs); lthy'

   193   It prints out the two definitions

   198   \begin{isabelle}

   194 

   199   \isacommand{thm}~@{text "even_def odd_def"}\\

   195   @{text [display] 

   200   @{text [break]

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

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

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

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

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

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

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

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

   205   \end{isabelle}

   206 

   204   Recall the proof for the induction principle for @{term "even"}: 

   211   Let us now turn to the induction principles. Recall that the proof of the 

   212   induction principle for @{term "even"} was:

   208   assumes prems: "even n"

   216 assumes prems: "even n"

   209   shows "P 0 \<Longrightarrow> 

   217 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   210              (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   220   To automate this proof we need to be able to instantiate universal 

   227   We have to implement code that constructs the induction principle and then

   221   quantifiers. For this we use the following helper function. It

   228   a tactic that automatically proves it. 

   222   instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.

   229   

   230   The tactic will use the following helper function for instantiating universal 

   231   quantifiers. This function instantiates the @{text "?x"} in the theorem 

   232   @{thm spec} with a given @{ML_type cterm}.

   229   For example we can use it to instantiate an assumption:

   239   For example we can use it in the following proof to instantiate the 

   230 *}

   240   three quantifiers in the assumption. We use the tactic

   241 *}

   242 

   243 ML{*fun inst_spec_tac ctrms = 

   244   EVERY' (map (dtac o inst_spec) ctrms)*}

   245 

   246 text {*

   247   and then apply use it with the @{ML_type cterm}s @{text "y1\<dots>y3"}. 

   248   *}

   234   let 

   252   inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})

   235     val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]

   236   in 

   237     EVERY1 (map (dtac o inst_spec) ctrms)

   238   end *})

   240   where it produces the goal state

   254   We obtain the goal state

   248   Now the tactic for proving the induction rules can be implemented 

   262   Now the complete tactic for proving the induction principles can 

   249   as follows

   263   be implemented as follows:

   256           EVERY' (map (dtac o inst_spec) insts),

   270           inst_spec_tac insts,

   265   assumes prems: "even n"

   291 assumes prems: "even n"

   266   shows "P 0 \<Longrightarrow> 

   292 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   267            (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   293 apply(tactic {* test_tac @{thms prems} *})

   268 apply(tactic {* 

   269   let

   270      val defs = [@{thm even_def}, @{thm odd_def}]

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

   272   in 

   273     induction_tac defs @{thms prems} insts 

   274   end *})

   277 

   296 text {*

   278 text {*

   279   which indeed proves the lemma. 

   280 

   282   it is a bit harder to set up the goals just from the given introduction 

   298   it is a bit harder to construct the goals from just the introduction 

   283   rules. For this we have to construct for each predicate @{text "pred"}

   299   rules the user states. In general we have to construct for each predicate 

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

   288   where the given predicates @{text preds} are replaced by new distinct 

   305   where the given predicates @{text preds} are replaced in the introduction 

   289   ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to

   306   rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. 

   290   new variables @{text "\<^raw:$zs$>"}. 

   307   We also need to generate fresh arguments for the predicate @{text "pred"} and

   308   the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.

   293   replaced. The argument @{text "mrules"} stands for these modified

   311   substitued. The argument @{text "srules"} stands for these substituted

   297   replacement and @{text "tys"} are the types of its argument.

   315   replacement and @{text "tys"} are the argument types of this predicate.

   298 *}

   316 *}

   299 

   317 

   300 ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =

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

   308          (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

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

   316   In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 

   334   In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the 

   317   list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)

   335   argument type list. Line 4 makes these names unique and declares them as 

   318   variables. These variables are free in the new theory @{text "lthy'"}. In Line 5

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

   319   we just construct the terms corresponding to the variables. The term variables are

   337   Line 5 we just construct the terms corresponding to these variables. 

   320   applied to the predicate in Line 7 (this is the first premise 

   338   The term variables are applied to the predicate in Line 7 (this corresponds

   321   @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9

   339   to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 

   322   we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add

   340   In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 

   323   the (modified) introduction rules as premises.

   341   and then add the (modified) introduction rules as premises. In case that

   324 

   342   no introduction rules are given, the conclusion of this implications needs

   325   In Line 11 we set up the goal to be proved; call the induction tactic in

   343   to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal

   326   Line 13. This returns a theorem. However, it is a theorem proved inside

   344   mechanism will fail. 

   327   the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are

   345 

   328   fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain

   346   In Line 11 we set up the goal to be proved; then call the tactic for proving the 

   329   the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we

   347   induction principle. This tactic expects the (certified) predicates with which

   330   obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.

   348   the introduction rules have been substituted. This will return a theorem. 

   331 

   349   However, it is a theorem proved inside the local theory @{text "lthy'"} where 

   332   So it is left to produce the modified rules and 

   350   the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this 

   333 *}

   351   theorem from @{text "lthy'"} (which contains the  @{text "\<^raw:$zs$>"} 

   334 

   352   as free) to @{text "lthy"} (which does not), we obtain the desired quantifications 

   335 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =

   353   @{text "\<And>\<^raw:$zs$>"}.

   354 

   355   Now it is left to produce the new predicated with which the introduction

   356   rules are substituted. 

   357 *}

   358 

   359 ML %linenosgray{*fun inductions rules defs preds tyss lthy  =

   338   val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1

   362   val (newprednames, lthy') = Variable.variant_fixes Ps lthy

   339   

   363   

   340   val thy = ProofContext.theory_of lthy2

   364   val thy = ProofContext.theory_of lthy'

   348   map (prove_induction lthy2 defs rules' cnewpreds) 

   372   map (prove_induction lthy' defs rules' cnewpreds) 

   350           |> ProofContext.export lthy2 lthy1

   374           |> ProofContext.export lthy' lthy

   473   val (pred_specs', rule_specs') = 

   487   val ((pred_specs', rule_specs'), _) = 

   474     read_specification' pred_specs rule_specs lthy

   488          Specification.read_spec pred_specs rule_specs lthy