theory Ind_Code

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

begin

section {* Code *}

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

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

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

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

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

*}

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

  \begin{isabelle}

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

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

  \end{isabelle}

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

*}

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

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

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

*}

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 "prednames"} is the list of names of the predicates;

  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

end *}

text {*

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

  the induction principles. 

*}

lemma 

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

*}

ML{*fun inst_spec ctrm = 

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

text {*

*}

lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"

apply (tactic {* 

txt {* 

  \begin{minipage}{\textwidth}

  @{subgoals} 

  \end{minipage}*}

(*<*)oops(*>*)

text {*

*}

ML %linenosgray{*fun induction_tac defs prems insts =

  EVERY1 [ObjectLogic.full_atomize_tac,

          cut_facts_tac prems,

          K (rewrite_goals_tac defs),

          assume_tac]*}

text {*

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

  A testcase for the tactic is

*}

lemma 

done

text {*

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

  @{text [display] 

  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}

  The function below expects that the rules are already appropriately

  introduction rules; @{text cnewpreds} are the certified terms coresponding

  to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for

  which we prove the introduction principle; @{text "newpred"} is its

*}

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

text {* 

*}

let

  val Ps = replicate (length preds) "P"

  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

        (preds ~~ newpreds ~~ tyss)

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 add_inductive pred_specs rule_specs lthy =