src/HOL/Metis.thy
changeset 45511 9b0f8ca4388e
parent 44651 5d6a11e166cf
child 46320 0b8b73b49848
     1.1 --- a/src/HOL/Metis.thy	Tue Nov 15 22:13:39 2011 +0100
     1.2 +++ b/src/HOL/Metis.thy	Tue Nov 15 22:13:39 2011 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4       ("Tools/try_methods.ML")
     1.5  begin
     1.6  
     1.7 -subsection {* Literal selection helpers *}
     1.8 +subsection {* Literal selection and lambda-lifting helpers *}
     1.9  
    1.10  definition select :: "'a \<Rightarrow> 'a" where
    1.11  [no_atp]: "select = (\<lambda>x. x)"
    1.12 @@ -31,6 +31,12 @@
    1.13  
    1.14  lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    1.15  
    1.16 +definition lambda :: "'a \<Rightarrow> 'a" where
    1.17 +[no_atp]: "lambda = (\<lambda>x. x)"
    1.18 +
    1.19 +lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
    1.20 +unfolding lambda_def by assumption
    1.21 +
    1.22  
    1.23  subsection {* Metis package *}
    1.24  
    1.25 @@ -40,10 +46,11 @@
    1.26  
    1.27  setup {* Metis_Tactic.setup *}
    1.28  
    1.29 -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    1.30 +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
    1.31  hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.32      fequal_def select_def not_atomize atomize_not_select not_atomize_select
    1.33 -    select_FalseI
    1.34 +    select_FalseI lambda_def eq_lambdaI
    1.35 +
    1.36  
    1.37  subsection {* Try Methods *}
    1.38