theory Ind_Code

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

begin

section {* Code *}

subsection {* Definitions *}

text {*

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

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

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

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

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

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

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

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

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

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

  expanding the defs 

  @{text [display]

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

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

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

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

  using the @{text "As"} we ????

*}

text {*

  First we have to produce for each predicate its definitions of the form

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

  We use the following wrapper function to make the definition via

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

  annotation and a term representing the right-hand side of the definition.

*}

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

let 

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

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

in 

  (thm, lthy') 

end*}

text {*

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

  been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the 

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

  These flags just classify theorems and have no significant meaning, except 

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

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

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

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

  via the return value. A testcase for this functions is

*}

local_setup %gray {* fn lthy =>

let

  val arg =  ((Binding.name "MyTrue", NoSyn), @{term True})

  val (def, lthy') = make_defs arg lthy 

in

  warning (str_of_thm lthy' def); lthy'

end *}

text {*

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

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

  access to theorem associated with this definition.

  \begin{isabelle}

  \isacommand{thm}~@{text "MyTrue_def"}\\

  @{text "> MyTrue \<equiv> True"}

  \end{isabelle}

  The next function constructs the term for the definition, namely 

  @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"}

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

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

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

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

*}

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

let 

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

  val fresh_args = 

        arg_tys 

        |> map (pair "z")

        |> Variable.variant_frees lthy (preds @ 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 code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the 

  predicate is 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 orules and predicates; in Line 9 it generates the corresponding 

  variable terms for the unique names.

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

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

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

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

  A testcase for this function is

*}

local_setup %gray{* fn lthy =>

let

  val orules = [@{prop "even 0"},

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

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

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

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

  val arg_tys = [@{typ "nat"}]

  val def = defs_aux lthy orules preds (pred, arg_tys)

in

  warning (Syntax.string_of_term lthy def); lthy

end *}

text {*

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

  the term

  @{text [display] 

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

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

  The main function for the definitions now has to just iterate

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

  next function does. 

*}

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 {*

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

  the argument @{text "prednames"} is the list of names of the predicates;

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

  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.

  A testcase for this function is 

*}

local_setup %gray {* fn lthy =>

let

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

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

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

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

  val prednames = [Binding.name "even", Binding.name "odd"] 

  val syns = [NoSyn, NoSyn] 

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

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

in

  warning (str_of_thms lthy' defs); lthy

end *}

text {*

  It prints out the two definitions

  @{text [display] 

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

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

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

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

  This completes the code concerning the definitions. Next comes the code for

  the induction principles. 

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

*}

lemma 

  assumes prems: "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 {* 

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

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

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

*}

ML{*fun inst_spec ctrm = 

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

text {*

  For example we can use it to instantiate an assumption:

*}

apply (tactic {* 

  let 

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

  in 

    EVERY1 (map (dtac o inst_spec) ctrms)

  end *})

txt {* 

  where it produces the goal state

  \begin{minipage}{\textwidth}

  @{subgoals} 

  \end{minipage}*}

(*<*)oops(*>*)

text {*

  Now the tactic for proving the induction rules can be implemented 

  as follows

*}

  EVERY1 [ObjectLogic.full_atomize_tac,

          cut_facts_tac prems,

          K (rewrite_goals_tac defs),

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

          assume_tac]*}

text {*

  We only have to give it as arguments the premises and the instantiations.

  A testcase for the tactic is

*}

lemma 

  assumes prems: "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 {*

  which indeed proves the lemma. 

  While the generic proof for the induction principle is relatively simple, 

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

  @{text [display] 

*}

let

  val zs = replicate (length tys) "z"

  val (newargnames, lthy') = Variable.variant_fixes zs lthy;

  val newargs = map Free (newargnames ~~ tys)

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

  val goal = Logic.list_implies 

in

  Goal.prove lthy' [] [prem] goal

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

  |> singleton (ProofContext.export lthy' lthy)

end *}

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

in

  map (prove_induction lthy2 defs rules' cnewpreds) 

        (preds ~~ newpreds ~~ tyss)

          |> ProofContext.export lthy2 lthy1

end*}

ML {*

  let 

    val rules = [@{prop "even (0::nat)"},

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

                 @{prop "\<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]*}

lemma evenS: 

  shows "odd m \<Longrightarrow> even (Suc m)"

apply(tactic {* 

let

  val rules = [@{prop "even (0::nat)"},

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

                 @{prop "\<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"}]

in

  introductions_tac defs rules preds 1 @{context}

end *})

done

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*}

text {* main internal function *}

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))) []*}