src/HOL/Nominal/nominal_induct.ML
author berghofe
Mon Oct 17 12:30:57 2005 +0200 (2005-10-17)
changeset 17870 c35381811d5c
child 18052 004515accc10
permissions -rw-r--r--
Initial revision.
berghofe@17870
     1
(* $Id$ *)
berghofe@17870
     2
berghofe@17870
     3
local
berghofe@17870
     4
berghofe@17870
     5
(* A function that takes a list of Variables and a term t;                    *)
berghofe@17870
     6
(* it builds up an abstraction of the Variables packaged in a tuple(!)        *)
berghofe@17870
     7
(* over the term t.                                                           *)
berghofe@17870
     8
(* E.g  tuple_lambda [] t        produces %x . t where x is a dummy Variable  *) 
berghofe@17870
     9
(*      tuple_lambda [a] t       produces %a . t                              *) 
berghofe@17870
    10
(*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
berghofe@17870
    11
berghofe@17870
    12
  fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
berghofe@17870
    13
    | tuple_lambda [x] t = lambda x t
berghofe@17870
    14
    | tuple_lambda (x::xs) t =
berghofe@17870
    15
       let
berghofe@17870
    16
         val t' = tuple_lambda xs t;
berghofe@17870
    17
         val Type ("fun", [T,U]) = fastype_of t';
berghofe@17870
    18
       in
berghofe@17870
    19
         HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
berghofe@17870
    20
       end; 
berghofe@17870
    21
berghofe@17870
    22
fun find_var frees name =
berghofe@17870
    23
  (case Library.find_first (equal name o fst o dest_Free) frees of
berghofe@17870
    24
    NONE => error ("No such Variable in term: " ^ quote name)
berghofe@17870
    25
  | SOME v => v);
berghofe@17870
    26
berghofe@17870
    27
fun nominal_induct_tac (names, rule) facts state =
berghofe@17870
    28
  let
berghofe@17870
    29
    val sg     = Thm.sign_of_thm state;
berghofe@17870
    30
    val cert   = Thm.cterm_of sg;
berghofe@17870
    31
    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
berghofe@17870
    32
    val frees  = Term.term_frees goal;
berghofe@17870
    33
    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
berghofe@17870
    34
    val vars = map (find_var frees) names;
berghofe@17870
    35
berghofe@17870
    36
    fun inst_rule rule =
berghofe@17870
    37
      let
berghofe@17870
    38
        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
berghofe@17870
    39
        val (P :: ts, x) = split_last concl_vars
berghofe@17870
    40
          handle Empty => error "Malformed conclusion of induction rule"
berghofe@17870
    41
            | Bind => error "Malformed conclusion of induction rule";
berghofe@17870
    42
      in
berghofe@17870
    43
        cterm_instantiate
berghofe@17870
    44
          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
berghofe@17870
    45
           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
berghofe@17870
    46
           (map cert ts ~~ map cert vars)) rule
berghofe@17870
    47
      end;
berghofe@17870
    48
berghofe@17870
    49
    val simplify_rule =
berghofe@17870
    50
      Simplifier.full_simplify (HOL_basic_ss addsimps
berghofe@17870
    51
        [split_conv, split_paired_All, split_paired_all]);
berghofe@17870
    52
berghofe@17870
    53
    val facts1 = Library.take (1, facts);
berghofe@17870
    54
    val facts2 = Library.drop (1, facts);
berghofe@17870
    55
berghofe@17870
    56
  in
berghofe@17870
    57
    rule
berghofe@17870
    58
    |> inst_rule
berghofe@17870
    59
    |> Method.multi_resolve facts1
berghofe@17870
    60
    |> Seq.map simplify_rule
berghofe@17870
    61
    |> Seq.map (RuleCases.save rule)
berghofe@17870
    62
    |> Seq.map RuleCases.add
berghofe@17870
    63
    |> Seq.map (fn (r, (cases, _)) =>
berghofe@17870
    64
        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
berghofe@17870
    65
        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
berghofe@17870
    66
    |> Seq.flat
berghofe@17870
    67
  end
berghofe@17870
    68
  handle Subscript => Seq.empty;
berghofe@17870
    69
berghofe@17870
    70
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
berghofe@17870
    71
berghofe@17870
    72
val nominal_induct_args =
berghofe@17870
    73
  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
berghofe@17870
    74
berghofe@17870
    75
in
berghofe@17870
    76
berghofe@17870
    77
val nominal_induct_method =
berghofe@17870
    78
  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
berghofe@17870
    79
berghofe@17870
    80
(* nominal_induc_method needs to have the type
berghofe@17870
    81
berghofe@17870
    82
   Args.src -> Proof.context -> Proof.method
berghofe@17870
    83
berghofe@17870
    84
   CHECK THAT
berghofe@17870
    85
berghofe@17870
    86
*)
berghofe@17870
    87
berghofe@17870
    88
end;