src/HOL/Nominal/nominal_induct.ML

fixed bug with nominal induct
- the bug occured in rule inductions when
the goal did not use all variables from
the relation over which the induction
was done

(* $Id$ *)

local

(* A function that takes a list of Variables and a term t;                    *)
(* it builds up an abstraction of the Variables packaged in a tuple(!)        *)
(* over the term t.                                                           *)
(* E.g  tuple_lambda [] t        produces %x . t where x is a dummy Variable  *) 
(*      tuple_lambda [a] t       produces %a . t                              *) 
(*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)

fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
  | tuple_lambda [x] t = lambda x t
  | tuple_lambda (x::xs) t =
    let
        val t' = tuple_lambda xs t;
        val Type ("fun", [T,U]) = fastype_of t';
    in
        HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
    end; 

fun find_var frees name =
  (case Library.find_first (equal name o fst o dest_Free) frees of
    NONE =>   error ("No such Variable in term: " ^ quote name) 
  | SOME v => v);

(* - names specifies the variables that are involved in the *)
(*   induction                                              *)
(* - rule is the induction rule to be applied               *)              
fun nominal_induct_tac (names, rule) facts state =
  let
    val sg     = Thm.sign_of_thm state;
    val cert   = Thm.cterm_of sg;

    val facts1 = Library.take (1, facts);
    val facts2 = Library.drop (1, facts);

    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
    val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
    val vars = map (find_var frees) names; 
                 (* FIXME - check what one can do in case of *)
                 (* rule inductions                          *)

    fun inst_rule rule =
      let
        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
        val (P :: ts, x) = split_last concl_vars
          handle Empty => error "Malformed conclusion of induction rule"
               | Bind  => error "Malformed conclusion of induction rule";
      in
        cterm_instantiate
          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
           (map cert ts ~~ map cert vars)) rule
      end;

    val simplify_rule =
      Simplifier.full_simplify (HOL_basic_ss addsimps
        [split_conv, split_paired_All, split_paired_all]);

  in
    rule
    |> inst_rule
    |> Method.multi_resolve facts1
    |> Seq.map simplify_rule
    |> Seq.map (RuleCases.save rule)
    |> Seq.map RuleCases.add
    |> Seq.map (fn (r, (cases, _)) =>
        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
    |> Seq.flat
  end
  handle Subscript => Seq.empty;

val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;

val nominal_induct_args =
  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;

in

val nominal_induct_method =
  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);

(* nominal_induc_method needs to have the type

   Args.src -> Proof.context -> Proof.method

   CHECK THAT

*)

end;