hide more internal names
authorblanchet
Tue May 13 11:10:23 2014 +0200 (2014-05-13)
changeset 5694610d9bd4ea94f
parent 56945 3d1ead21a055
child 56947 01ab2e94a713
hide more internal names
src/HOL/ATP.thy
src/HOL/Metis.thy
     1.1 --- a/src/HOL/ATP.thy	Tue May 13 11:10:22 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue May 13 11:10:23 2014 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  ML_file "Tools/ATP/atp_proof.ML"
     1.5  ML_file "Tools/ATP/atp_proof_redirect.ML"
     1.6  
     1.7 +
     1.8  subsection {* Higher-order reasoning helpers *}
     1.9  
    1.10  definition fFalse :: bool where
    1.11 @@ -39,15 +40,15 @@
    1.12  definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.13  "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    1.14  
    1.15 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.16 -"fequal x y \<longleftrightarrow> (x = y)"
    1.17 -
    1.18  definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.19  "fAll P \<longleftrightarrow> All P"
    1.20  
    1.21  definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.22  "fEx P \<longleftrightarrow> Ex P"
    1.23  
    1.24 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.25 +"fequal x y \<longleftrightarrow> (x = y)"
    1.26 +
    1.27  lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    1.28  unfolding fFalse_def fTrue_def by simp
    1.29  
    1.30 @@ -74,11 +75,6 @@
    1.31  "fimplies fTrue fFalse = fFalse"
    1.32  unfolding fFalse_def fTrue_def fimplies_def by auto
    1.33  
    1.34 -lemma fequal_table:
    1.35 -"fequal x x = fTrue"
    1.36 -"x = y \<or> fequal x y = fFalse"
    1.37 -unfolding fFalse_def fTrue_def fequal_def by auto
    1.38 -
    1.39  lemma fAll_table:
    1.40  "Ex (fComp P) \<or> fAll P = fTrue"
    1.41  "All P \<or> fAll P = fFalse"
    1.42 @@ -89,6 +85,11 @@
    1.43  "Ex P \<or> fEx P = fFalse"
    1.44  unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    1.45  
    1.46 +lemma fequal_table:
    1.47 +"fequal x x = fTrue"
    1.48 +"x = y \<or> fequal x y = fFalse"
    1.49 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.50 +
    1.51  lemma fNot_law:
    1.52  "fNot P \<noteq> P"
    1.53  unfolding fNot_def by auto
    1.54 @@ -114,12 +115,6 @@
    1.55  "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
    1.56  unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
    1.57  
    1.58 -lemma fequal_laws:
    1.59 -"fequal x y = fequal y x"
    1.60 -"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
    1.61 -"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
    1.62 -unfolding fFalse_def fTrue_def fequal_def by auto
    1.63 -
    1.64  lemma fAll_law:
    1.65  "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
    1.66  unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.67 @@ -128,6 +123,13 @@
    1.68  "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
    1.69  unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.70  
    1.71 +lemma fequal_laws:
    1.72 +"fequal x y = fequal y x"
    1.73 +"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
    1.74 +"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
    1.75 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.76 +
    1.77 +
    1.78  subsection {* Setup *}
    1.79  
    1.80  ML_file "Tools/ATP/atp_problem_generate.ML"
     2.1 --- a/src/HOL/Metis.thy	Tue May 13 11:10:22 2014 +0200
     2.2 +++ b/src/HOL/Metis.thy	Tue May 13 11:10:23 2014 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4  ML_file "~~/src/Tools/Metis/metis.ML"
     2.5  declare [[ML_print_depth = 10]]
     2.6  
     2.7 +
     2.8  subsection {* Literal selection and lambda-lifting helpers *}
     2.9  
    2.10  definition select :: "'a \<Rightarrow> 'a" where
    2.11 @@ -45,12 +46,11 @@
    2.12  
    2.13  setup {* Metis_Tactic.setup *}
    2.14  
    2.15 -hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
    2.16 -    lambda
    2.17 -hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
    2.18 -    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    2.19 -    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
    2.20 -    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
    2.21 -    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    2.22 +hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    2.23 +hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    2.24 +  fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
    2.25 +  fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
    2.26 +  fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws
    2.27 +  fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    2.28  
    2.29  end