src/HOL/Nominal/nominal_induct.ML
author urbanc
Sun Nov 13 22:36:30 2005 +0100 (2005-11-13)
changeset 18158 57cba2a340f2
parent 18157 72e1956440ad
child 18265 f3f81becc1f1
permissions -rw-r--r--
changed the HOL_basic_ss back and selectively added
simp_thms and triv_forall_equality. (Otherwise the
goals would have been simplified too much)
     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 
    35     val facts1 = Library.take (1, facts);
    36     val facts2 = Library.drop (1, facts);
    37 
    38     val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
    39     val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
    40     val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
    41     val vars = map (find_var frees) names; 
    42                  (* FIXME - check what one can do in case of *)
    43                  (* rule inductions                          *)
    44 
    45     fun inst_rule rule =
    46       let
    47         val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
    48         val (P :: ts, x) = split_last concl_vars
    49           handle Empty => error "Malformed conclusion of induction rule"
    50                | Bind  => error "Malformed conclusion of induction rule";
    51       in
    52         cterm_instantiate
    53           ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
    54            (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
    55            (map cert ts ~~ map cert vars)) rule
    56       end;
    57 
    58     val simplify_rule =
    59       Simplifier.full_simplify (HOL_basic_ss addsimps
    60         simp_thms @ [triv_forall_equality, split_conv, split_paired_All, split_paired_all]);
    61 
    62   in
    63     rule
    64     |> inst_rule
    65     |> Method.multi_resolve facts1
    66     |> Seq.map simplify_rule 
    67     |> Seq.map (RuleCases.save rule)
    68     |> Seq.map RuleCases.add
    69     |> Seq.map (fn (r, (cases, _)) =>
    70         HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
    71         |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
    72     |> Seq.flat
    73   end
    74   handle Subscript => Seq.empty;
    75 
    76 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
    77 
    78 val nominal_induct_args =
    79   Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
    80 
    81 in
    82 
    83 val nominal_induct_method =
    84   Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
    85 
    86 (* nominal_induc_method needs to have the type
    87 
    88    Args.src -> Proof.context -> Proof.method
    89 
    90    CHECK THAT
    91 
    92 *)
    93 
    94 end;