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 actually 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 {*
  Returns the definition (as theorem) and the local theory in which this definition has 
  been made. The @{ML internalK in Thm} in Line 4 is just a flag attached to the 
  theorem (others flags 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. 
*}

local_setup %gray {* fn lthy =>
let
  val arg =  ((Binding.name "MyTrue", NoSyn), @{term True})
  val (def, lthy') = make_defs arg lthy 
  val _ = warning (str_of_thm lthy' def)
in
  lthy'
end *}

text {*
  Prints out the theorem @{prop "MyTrue \<equiv> True"}.
*}

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


local_setup {*
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 {*
  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.  
*}

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


subsection {* Induction Principles *}

text {* 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 {* We need to be able to instantiate universal quantifiers. *}

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 {* 
  let 
    val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]
  in 
    EVERY1 (map (dtac o inst_spec) ctrms)
  end *})
txt {* \begin{minipage}{\textwidth}
       @{subgoals} 
       \end{minipage}*}
(*<*)oops(*>*)

text {*
  Now the tactic for proving the induction rules: 
*}

ML{*fun induction_tac defs prems insts =
  EVERY1 [ObjectLogic.full_atomize_tac,
          cut_facts_tac prems,
          K (rewrite_goals_tac defs),
          EVERY' (map (dtac o inst_spec) insts),
          assume_tac]*}

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 {*
  While the generic proof is relatively simple, it is a bit harder to
  set up the goals for the induction principles. 
*}

ML {*
fun prove_induction lthy2 defs rules cnewpreds ((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 lthy2)
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))) []*}

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