src/FOL/simpdata.ML
changeset 429 888bbb4119f8
parent 394 432bb9995893
child 745 45a789407806
equal deleted inserted replaced
428:49cc52442678 429:888bbb4119f8
    53 (** Conversion into rewrite rules **)
    53 (** Conversion into rewrite rules **)
    54 
    54 
    55 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    55 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
    56 
    56 
    57 (*Make atomic rewrite rules*)
    57 (*Make atomic rewrite rules*)
    58 fun atomize th = case concl_of th of 
    58 fun atomize r =
    59     _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) @
    59   case concl_of r of
    60 				       atomize(th RS conjunct2)
    60     Const("Trueprop",_) $ p =>
    61   | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
    61       (case p of
    62   | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
    62 	 Const("op -->",_)$_$_ => atomize(r RS mp)
    63   | _ $ (Const("True",_))           => []
    63        | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
    64   | _ $ (Const("False",_))          => []
    64 	  		          atomize(r RS conjunct2)
    65   | _                               => [th];
    65        | Const("All",_)$_      => atomize(r RS spec)
       
    66        | Const("True",_)       => []	(*True is DELETED*)
       
    67        | Const("False",_)      => []	(*should False do something?*)
       
    68        | _                     => [r])
       
    69   | _ => [r];
       
    70 
    66 
    71 
    67 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    72 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
    68 val iff_reflection_F = P_iff_F RS iff_reflection;
    73 val iff_reflection_F = P_iff_F RS iff_reflection;
    69 
    74 
    70 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
    75 val P_iff_T = int_prove_fun "P ==> (P <-> True)";