moved meta_fun_cong lemma into ML-file; tuned
authorbulwahn
Sat Oct 24 16:54:32 2009 +0200 (2009-10-24)
changeset 33104560372b461e5
parent 32949 aa6c470a962a
child 33105 1e4146bf841c
moved meta_fun_cong lemma into ML-file; tuned
src/HOL/Predicate.thy
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/Predicate.thy	Thu Oct 15 21:08:03 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Sat Oct 24 16:54:32 2009 +0200
     1.3 @@ -770,10 +770,6 @@
     1.4     (auto simp add: Seq_def the_only_singleton is_empty_def
     1.5        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
     1.6  
     1.7 -lemma meta_fun_cong:
     1.8 -"f == g ==> f x == g x"
     1.9 -by simp
    1.10 -
    1.11  ML {*
    1.12  signature PREDICATE =
    1.13  sig
     2.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Thu Oct 15 21:08:03 2009 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:54:32 2009 +0200
     2.3 @@ -81,11 +81,13 @@
     2.4      Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
     2.5    | _ => th
     2.6  
     2.7 +val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
     2.8 +
     2.9  fun full_fun_cong_expand th =
    2.10    let
    2.11      val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
    2.12      val i = length (binder_types (fastype_of f)) - length args
    2.13 -  in funpow i (fn th => th RS @{thm meta_fun_cong}) th end;
    2.14 +  in funpow i (fn th => th RS meta_fun_cong) th end;
    2.15  
    2.16  fun declare_names s xs ctxt =
    2.17    let
     3.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Oct 15 21:08:03 2009 +0200
     3.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:54:32 2009 +0200
     3.3 @@ -361,8 +361,8 @@
     3.4  (*quickcheck[generator = pred_compile, size=5, iterations=1]*)
     3.5  oops
     3.6  
     3.7 +section {* Lambda *}
     3.8  
     3.9 -section {* Lambda *}
    3.10  datatype type =
    3.11      Atom nat
    3.12    | Fun type type    (infixr "\<Rightarrow>" 200)