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

  In order to make definitions, we use the following wrapper for 
  @{ML LocalTheory.define}. The wrapper 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 a 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} and @{ML axiomK in Thm}). 
  These flags just classify theorems and have no significant meaning, except 
  for tools that, for example, find theorems in the theorem database. We also
  use @{ML empty_binding in Attrib} in Line 3, since the definition does 
  not need to have any theorem attributes. A testcase for this function 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 makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out. 
  Since we are testing the function inside \isacommand{local\_setup}, i.e.~make
  changes to the ambient theory, we can query the definition using the usual
  command \isacommand{thm}:

  \begin{isabelle}
  \isacommand{thm}~@{text "MyTrue_def"}\\
  @{text "> MyTrue \<equiv> True"}
  \end{isabelle}

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

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

  The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur
  in the @{text orules} and also be distinct from @{text "preds"}. 

  The first function constructs the term for one particular predicate @{text
  "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is
  determined by the number of argument types of @{text "arg_tys"}.
*}

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$>"}. For this
  it pairs every argument type with the string @{text [quotes] "z"} (Line 7);
  then generates variants for all these strings so that they are unique
  w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the
  corresponding variable terms for the unique strings.

  The unique free variables are applied to the predicate (Line 11) using the
  function @{ML list_comb}; 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 @{text "\<^raw:$zs$>"}, i.e.~the fresh 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 left-hand side for the definition of @{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. 
*}

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 again the 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 for each predicate. 
  
  The user give the introduction rules using meta-implications and meta-quantifications.
  In line 4 we transform the introduction rules into the object logic (definitions
  cannot use them). To do the transformation we have to 
  obtain the theory behind the local theory (Line 3); with this theory 
  we can use the function @{ML ObjectLogic.atomize_term} to make the
  transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all
  left-hand sides of the definitions. The actual definitions are then made in Line 7.
  As the result we obtain a list of theorems and a local theory. 

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

  \begin{isabelle}
  \isacommand{thm}~@{text "even_def odd_def"}\\
  @{text [break]
"> 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"}
  \end{isabelle}


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

  Let us now turn to the induction principles. Recall that the proof of the 
  induction principle for @{term "even"} was:
*}

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 {* 
  We have to implement code that constructs the induction principle and then
  a tactic that automatically proves it. 
  
  The tactic will use the following helper function for instantiating universal 
  quantifiers. This function instantiates the @{text "?x"} in the theorem 
  @{thm spec} with a given @{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 in the following proof to instantiate the 
  three quantifiers in the assumption. We use the tactic
*}

ML{*fun inst_spec_tac ctrms = 
  EVERY' (map (dtac o inst_spec) ctrms)*}

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

lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
apply (tactic {* 
  inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
txt {* 
  We obtain the goal state

  \begin{minipage}{\textwidth}
  @{subgoals} 
  \end{minipage}*}
(*<*)oops(*>*)

text {*
  Now the complete tactic for proving the induction principles can 
  be implemented as follows:
*}

ML %linenosgray{*fun induction_tac defs prems insts =
  EVERY1 [ObjectLogic.full_atomize_tac,
          cut_facts_tac prems,
          K (rewrite_goals_tac defs),
          inst_spec_tac insts,
          assume_tac]*}

text {*
  We only have to give it as arguments the premises and the instantiations.
  A testcase for the tactic is
*}

ML{*fun test_tac prems = 
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 prems insts 
end*}

text {*
  which indeed proves the induction principle. 
*}

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 {* test_tac @{thms prems} *})
done

text {*
  While the generic proof for the induction principle is relatively simple, 
  it is a bit harder to construct the goals from just the introduction 
  rules the user states. In general we have to construct for each predicate 
  @{text "pred"} a goal of the form

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

  where the given predicates @{text preds} are replaced in the introduction 
  rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. 
  We also need to generate fresh arguments for the predicate @{text "pred"} and
  the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.

  The function below expects that the rules are already appropriately
  substitued. The argument @{text "srules"} stands for these substituted
  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
  replacement and @{text "tys"} are the argument types of this predicate.
*}

ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =
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 
         (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
in
  Goal.prove lthy' [] [prem] goal
  (fn {prems, ...} => induction_tac defs prems cnewpreds)
  |> singleton (ProofContext.export lthy' lthy)
end *}

text {* 
  In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the 
  argument type list. Line 4 makes these names unique and declares them as 
  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In 
  Line 5 we just construct the terms corresponding to these variables. 
  The term variables are applied to the predicate in Line 7 (this corresponds
  to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 
  In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 
  and then add the (modified) introduction rules as premises. In case that
  no introduction rules are given, the conclusion of this implications needs
  to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
  mechanism will fail. 

  In Line 11 we set up the goal to be proved; then call the tactic for proving the 
  induction principle. This tactic expects the (certified) predicates with which
  the introduction rules have been substituted. This will return a theorem. 
  However, it is a theorem proved inside the local theory @{text "lthy'"} where 
  the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this 
  theorem from @{text "lthy'"} (which contains the  @{text "\<^raw:$zs$>"} 
  as free) to @{text "lthy"} (which does not), we obtain the desired quantifications 
  @{text "\<And>\<^raw:$zs$>"}.

  Now it is left to produce the new predicated with which the introduction
  rules are substituted. 
*}

ML %linenosgray{*fun inductions rules defs preds tyss lthy  =
let
  val Ps = replicate (length preds) "P"
  val (newprednames, lthy') = Variable.variant_fixes Ps lthy
  
  val thy = ProofContext.theory_of lthy'

  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 lthy' defs rules' cnewpreds) 
        (preds ~~ newpreds ~~ tyss)
          |> ProofContext.export lthy' lthy
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 =
let
  val ((pred_specs', rule_specs'), _) = 
         Specification.read_spec 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