src/HOL/Nominal/nominal_induct.ML
author urbanc
Mon Nov 07 10:47:25 2005 +0100 (2005-11-07)
changeset 18099 e956b04fea22
parent 18052 004515accc10
child 18157 72e1956440ad
permissions -rw-r--r--
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
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
urbanc@18052
    12
fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
urbanc@18052
    13
  | tuple_lambda [x] t = lambda x t
urbanc@18052
    14
  | tuple_lambda (x::xs) t =
urbanc@18052
    15
    let
urbanc@18052
    16
        val t' = tuple_lambda xs t;
urbanc@18052
    17
        val Type ("fun", [T,U]) = fastype_of t';
urbanc@18052
    18
    in
urbanc@18052
    19
        HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
urbanc@18052
    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
urbanc@18099
    24
    NONE =>   error ("No such Variable in term: " ^ quote name) 
berghofe@17870
    25
  | SOME v => v);
berghofe@17870
    26
urbanc@18052
    27
(* - names specifies the variables that are involved in the *)
urbanc@18052
    28
(*   induction                                              *)
urbanc@18052
    29
(* - rule is the induction rule to be applied               *)              
berghofe@17870
    30
fun nominal_induct_tac (names, rule) facts state =
berghofe@17870
    31
  let
berghofe@17870
    32
    val sg     = Thm.sign_of_thm state;
berghofe@17870
    33
    val cert   = Thm.cterm_of sg;
urbanc@18099
    34
urbanc@18099
    35
    val facts1 = Library.take (1, facts);
urbanc@18099
    36
    val facts2 = Library.drop (1, facts);
urbanc@18099
    37
berghofe@17870
    38
    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
urbanc@18099
    39
    val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
berghofe@17870
    40
    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
urbanc@18099
    41
    val vars = map (find_var frees) names; 
urbanc@18099
    42
                 (* FIXME - check what one can do in case of *)
urbanc@18099
    43
                 (* rule inductions                          *)
berghofe@17870
    44
berghofe@17870
    45
    fun inst_rule rule =
berghofe@17870
    46
      let
berghofe@17870
    47
        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
berghofe@17870
    48
        val (P :: ts, x) = split_last concl_vars
berghofe@17870
    49
          handle Empty => error "Malformed conclusion of induction rule"
urbanc@18052
    50
               | Bind  => error "Malformed conclusion of induction rule";
berghofe@17870
    51
      in
berghofe@17870
    52
        cterm_instantiate
berghofe@17870
    53
          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
berghofe@17870
    54
           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
berghofe@17870
    55
           (map cert ts ~~ map cert vars)) rule
berghofe@17870
    56
      end;
berghofe@17870
    57
berghofe@17870
    58
    val simplify_rule =
berghofe@17870
    59
      Simplifier.full_simplify (HOL_basic_ss addsimps
berghofe@17870
    60
        [split_conv, split_paired_All, split_paired_all]);
berghofe@17870
    61
berghofe@17870
    62
  in
berghofe@17870
    63
    rule
berghofe@17870
    64
    |> inst_rule
berghofe@17870
    65
    |> Method.multi_resolve facts1
berghofe@17870
    66
    |> Seq.map simplify_rule
berghofe@17870
    67
    |> Seq.map (RuleCases.save rule)
berghofe@17870
    68
    |> Seq.map RuleCases.add
berghofe@17870
    69
    |> Seq.map (fn (r, (cases, _)) =>
berghofe@17870
    70
        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
berghofe@17870
    71
        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
berghofe@17870
    72
    |> Seq.flat
berghofe@17870
    73
  end
berghofe@17870
    74
  handle Subscript => Seq.empty;
berghofe@17870
    75
berghofe@17870
    76
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
berghofe@17870
    77
berghofe@17870
    78
val nominal_induct_args =
berghofe@17870
    79
  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
berghofe@17870
    80
berghofe@17870
    81
in
berghofe@17870
    82
berghofe@17870
    83
val nominal_induct_method =
berghofe@17870
    84
  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
berghofe@17870
    85
berghofe@17870
    86
(* nominal_induc_method needs to have the type
berghofe@17870
    87
berghofe@17870
    88
   Args.src -> Proof.context -> Proof.method
berghofe@17870
    89
berghofe@17870
    90
   CHECK THAT
berghofe@17870
    91
berghofe@17870
    92
*)
berghofe@17870
    93
berghofe@17870
    94
end;