fixed bug with nominal induct
authorurbanc
Mon Nov 07 10:47:25 2005 +0100 (2005-11-07)
changeset 18099e956b04fea22
parent 18098 227ecb2cfa3d
child 18100 193c3382bbfe
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
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Nov 07 09:34:51 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Nov 07 10:47:25 2005 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  fun find_var frees name =
     1.6    (case Library.find_first (equal name o fst o dest_Free) frees of
     1.7 -    NONE => error ("No such Variable in term: " ^ quote name)
     1.8 +    NONE =>   error ("No such Variable in term: " ^ quote name) 
     1.9    | SOME v => v);
    1.10  
    1.11  (* - names specifies the variables that are involved in the *)
    1.12 @@ -31,10 +31,16 @@
    1.13    let
    1.14      val sg     = Thm.sign_of_thm state;
    1.15      val cert   = Thm.cterm_of sg;
    1.16 +
    1.17 +    val facts1 = Library.take (1, facts);
    1.18 +    val facts2 = Library.drop (1, facts);
    1.19 +
    1.20      val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
    1.21 -    val frees  = Term.term_frees goal;
    1.22 +    val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
    1.23      val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
    1.24 -    val vars = map (find_var frees) names;
    1.25 +    val vars = map (find_var frees) names; 
    1.26 +                 (* FIXME - check what one can do in case of *)
    1.27 +                 (* rule inductions                          *)
    1.28  
    1.29      fun inst_rule rule =
    1.30        let
    1.31 @@ -53,9 +59,6 @@
    1.32        Simplifier.full_simplify (HOL_basic_ss addsimps
    1.33          [split_conv, split_paired_All, split_paired_all]);
    1.34  
    1.35 -    val facts1 = Library.take (1, facts);
    1.36 -    val facts2 = Library.drop (1, facts);
    1.37 -
    1.38    in
    1.39      rule
    1.40      |> inst_rule