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