2 imports "../Base" Simple_Inductive_Package

     2 imports "../Base" Simple_Inductive_Package Ind_Prelims

     6   What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?

    10   If we give it a term and a constant name, it will define the 

    11   constant as the term. 

    12   @{ML_chunk [display,gray] definitions_aux}

    27 ML {*let

    13   @{ML_chunk [display,gray,linenos] definitions}

    28   val lthy = TheoryTarget.init NONE @{theory}

    29 in

    30   make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy

    31 end*}

    32 

    33 text {*

    34   Why is the output of MyTrue blue?

    35 *}

    36 

    37 text {*

    38   Constructs the term for the definition: the main arguments are a predicate

    39   and the types of the arguments, it also expects orules which are the 

    40   intro rules in the object logic; preds which are all predicates. returns the

    41   term.

    42 *}

    43 

    44 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) =

    45 let 

    46   fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P

    47 

    48   val fresh_args = 

    49         arg_types 

    50         |> map (pair "z")

    51         |> Variable.variant_frees lthy orules 

    52         |> map Free

    53 in

    54   list_comb (pred, fresh_args)

    55   |> fold_rev (curry HOLogic.mk_imp) orules

    56   |> fold_rev mk_all preds

    57   |> fold_rev lambda fresh_args 

    58 end*}

    59 

    60 text {*

    61   The lines 5-9 produce fresh arguments with which the predicate can be applied.

    62   For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then 

    63   generates variants for all these strings (names) so that they are unique w.r.t.~to 

    64   the intro rules; in Line 9 it generates the corresponding variable terms for these 

    65   unique names.

    66 

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

    68   the intro rules are attached as preconditions (Line 12); in Line 13 we

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

    70   the (fresh) arguments of the predicate.

    71 *}

    72 

    73 text {*

    74   The arguments of the main function for the definitions are 

    75   the intro rules; the predicates and their names, their syntax 

    76   annotations and the argument types of each predicate. It  

    77   returns a theorem list (the definitions) and a local

    78   theory where the definitions are made

    79 *}

    80 

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

    82 let

    83   val thy = ProofContext.theory_of lthy

    84   val orules = map (ObjectLogic.atomize_term thy) rules

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

    86 in

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

    88 end*}

    89 

    90 text {*

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

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

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

    94   The actual definitions are made in Line 7.  

    95 *}

    96 

    97 subsection {* Introduction Rules *}

    98 

    99 ML{*fun inst_spec ct = 

   100  Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}

   101 

   102 text {*

   103   Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}.

   104 *}

   105 

   106 text {*

   107   Instantiates universal qantifications in the premises

   108 *}

   109 

   110 lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True"

   111 apply (tactic {* EVERY' (map (dtac o inst_spec) 

   112           [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})

   113 (*<*)oops(*>*)

   114 

   115 text {*

   116   The tactic for proving the induction rules: 

   117 *}

   118 

   119 ML{*fun induction_tac defs prems insts =

   120   EVERY1 [ObjectLogic.full_atomize_tac,

   121           cut_facts_tac prems,

   122           K (rewrite_goals_tac defs),

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

   124           assume_tac]*}

   125 

   126 lemma 

   127   assumes asm: "even n"

   128   shows "P 0 \<Longrightarrow> 

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

   130 apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] 

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

   132 done

   133 

   134 ML %linenosgray{*fun inductions rules defs preds Tss lthy1  =

   135 let

   136   val Ps = replicate (length preds) "P"

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

   138   

   139   val thy = ProofContext.theory_of lthy2

   140 

   141   val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss

   142   val newpreds = map Free (newprednames ~~ Tss')

   143   val cnewpreds = map (cterm_of thy) newpreds

   144   val rules' = map (subst_free (preds ~~ newpreds)) rules

   145 

   146   fun prove_induction ((pred, newpred), Ts)  =

   147   let

   148     val zs = replicate (length Ts) "z"

   149     val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;

   150     val newargs = map Free (newargnames ~~ Ts)

   151 

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

   153     val goal = Logic.list_implies 

   154          (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   155   in

   156     Goal.prove lthy3 [] [prem] goal

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

   158       |> singleton (ProofContext.export lthy3 lthy1)

   159   end 

   160 in

   161   map prove_induction (preds ~~ newpreds ~~ Tss)

   162 end*}

   163 

   164 ML {* Goal.prove  *}

   165 ML {* singleton *}

   166 ML {* ProofContext.export *}

   167 

   168 text {*

    19   @{ML_chunk [display,gray] induction_rules}

   175   @{ML_chunk [display,gray] subproof2}

    20 

    21 *}

    22 

    23 text {*