theory Ind_Code

imports "../Base" Simple_Inductive_Package Ind_Prelims

begin

section {* Code *}

subsection {* Definitions *}

text {*

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

  constant as the term. 

*}

ML{*fun make_defs ((binding, syn), trm) lthy =

let 

  val arg = ((binding, syn), (Attrib.empty_binding, trm))

  val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy

in 

  (thm, lthy) 

end*}

text {*

  Returns the definition and the local theory in which this definition has 

  been made. What is @{ML Thm.internalK}?

*}

ML {*let

  val lthy = TheoryTarget.init NONE @{theory}

in

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

end*}

text {*

  Why is the output of MyTrue blue?

*}

text {*

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

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

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

  term.

*}

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

let 

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

  val fresh_args = 

        arg_types 

        |> map (pair "z")

        |> Variable.variant_frees lthy orules 

        |> map Free

in

  list_comb (pred, fresh_args)

  |> fold_rev (curry HOLogic.mk_imp) orules

  |> fold_rev mk_all preds

  |> fold_rev lambda fresh_args 

end*}

text {*

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

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

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

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

  unique names.

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

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

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

  the (fresh) arguments of the predicate.

*}

text {*

  The arguments of the main function for the definitions are 

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

  annotations and the argument types of each predicate. It  

  returns a theorem list (the definitions) and a local

  theory where the definitions are made

*}

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

let

  val thy = ProofContext.theory_of lthy

  val orules = map (ObjectLogic.atomize_term thy) rules

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

in

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

end*}

text {*

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

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

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

  The actual definitions are made in Line 7.  

*}

subsection {* Induction Principles *}

ML{*fun inst_spec ct = 

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

text {*

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

*}

text {*

  Instantiates universal qantifications in the premises

*}

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"

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

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

txt {* \begin{minipage}{\textwidth}

       @{subgoals} 

       \end{minipage}*}

(*<*)oops(*>*)

lemma 

  assumes "even n"

  shows "P 0 \<Longrightarrow> 

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

apply(atomize (full))

apply(cut_tac prems)

apply(unfold even_def)

apply(drule spec[where x=P])

apply(drule spec[where x=Q])

apply(assumption)

done

text {*

  The tactic for proving the induction rules: 

*}

ML{*fun induction_tac defs prems insts =

  EVERY1 [K (print_tac "start"),

          ObjectLogic.full_atomize_tac,

          cut_facts_tac prems,

          K (rewrite_goals_tac defs),

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

          assume_tac]*}

lemma 

  assumes "even n"

  shows "P 0 \<Longrightarrow> 

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

apply(tactic {* 

  let

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

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

  in 

    induction_tac defs @{thms prems} insts 

  end *})

done

text {*

  While the generic proof is relatively simple, it is a bit harder to

  set up the goals for the induction principles. 

*}

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

let

  val Ps = replicate (length preds) "P"

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

  val thy = ProofContext.theory_of lthy2

  val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss

  val newpreds = map Free (newprednames ~~ tyss')

  val cnewpreds = map (cterm_of thy) newpreds

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

  fun prove_induction ((pred, newpred), tys)  =

  let

    val zs = replicate (length tys) "z"

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

    val newargs = map Free (newargnames ~~ tys)

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

    val goal = Logic.list_implies 

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

  in

    Goal.prove lthy3 [] [prem] goal

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

      |> singleton (ProofContext.export lthy3 lthy1)

  end 

in

  map prove_induction (preds ~~ newpreds ~~ tyss)

end*}

(*

ML {*

  let 

    val rules = [@{term "even 0"},

                 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

                 @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

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

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

    val tyss = [[@{typ "nat"}],[@{typ "nat"}]]

  in

    inductions rules defs preds tyss @{context}

  end

*}

*)

subsection {* Introduction Rules *}

ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)

val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}

ML{*fun subproof2 prem params2 prems2 =  

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

   let

     val prem' = prems MRS prem;

     val prem'' = 

       case prop_of prem' of

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

             prem' |> all_elims params2 

                   |> imp_elims prems2

         | _ => prem';

   in 

     rtac prem'' 1 

   end)*}

ML{*fun subproof1 rules preds i = 

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

   let

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

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

   in

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

     THEN

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

   end)*}

ML{*

fun introductions_tac defs rules preds i ctxt =

  EVERY1 [ObjectLogic.rulify_tac,

          K (rewrite_goals_tac defs),

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

          subproof1 rules preds i ctxt]*}

ML{*fun introductions rules preds defs lthy = 

let

  fun prove_intro (i, goal) =

    Goal.prove lthy [] [] goal

      (fn {context, ...} => introductions_tac defs rules preds i context)

in

  map_index prove_intro rules

end*}

ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =

let

  val syns = map snd pred_specs

  val pred_specs' = map fst pred_specs

  val prednames = map fst pred_specs'

  val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'

  val tyss = map (binder_types o fastype_of) preds   

  val (attrs, rules) = split_list rule_specs    

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

  val ind_rules = inductions rules defs preds tyss lthy' 	

  val intro_rules = introductions rules preds defs lthy'

  val mut_name = space_implode "_" (map Binding.name_of prednames)

  val case_names = map (Binding.name_of o fst) attrs

in

    lthy' 

    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>

        ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 

    |-> (fn intross => LocalTheory.note Thm.theoremK

         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 

    |>> snd 

    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>

         ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),

          [Attrib.internal (K (RuleCases.case_names case_names)),

           Attrib.internal (K (RuleCases.consumes 1)),

           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))

          (pred_specs ~~ ind_rules)) #>> maps snd) 

    |> snd

end*}

ML{*fun read_specification' vars specs lthy =

let 

  val specs' = map (fn (a, s) => [(a, [s])]) specs

  val ((varst, specst), _) = 

                   Specification.read_specification vars specs' lthy

  val specst' = map (apsnd the_single) specst

in   

  (varst, specst')

end*}

ML{*fun add_inductive pred_specs rule_specs lthy =

let

  val (pred_specs', rule_specs') = 

    read_specification' pred_specs rule_specs lthy

in

  add_inductive_i pred_specs' rule_specs' lthy

end*} 

ML{*val spec_parser = 

   OuterParse.opt_target --

   OuterParse.fixes -- 

   Scan.optional 

     (OuterParse.$$$ "where" |--

        OuterParse.!!! 

          (OuterParse.enum1 "|" 

             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}

ML{*val specification =

  spec_parser >>

    (fn ((loc, pred_specs), rule_specs) =>

      Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}

ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"

          OuterKeyword.thy_decl specification*}

text {*

  Things to include at the end:

  \begin{itemize}

  \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)

  \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)"

end