src/HOL/ATP.thy
changeset 56946 10d9bd4ea94f
parent 54148 c8cc5ab4a863
child 57255 488046fdda59
equal deleted inserted replaced
56945:3d1ead21a055 56946:10d9bd4ea94f
    13 ML_file "Tools/monomorph.ML"
    13 ML_file "Tools/monomorph.ML"
    14 ML_file "Tools/ATP/atp_util.ML"
    14 ML_file "Tools/ATP/atp_util.ML"
    15 ML_file "Tools/ATP/atp_problem.ML"
    15 ML_file "Tools/ATP/atp_problem.ML"
    16 ML_file "Tools/ATP/atp_proof.ML"
    16 ML_file "Tools/ATP/atp_proof.ML"
    17 ML_file "Tools/ATP/atp_proof_redirect.ML"
    17 ML_file "Tools/ATP/atp_proof_redirect.ML"
       
    18 
    18 
    19 
    19 subsection {* Higher-order reasoning helpers *}
    20 subsection {* Higher-order reasoning helpers *}
    20 
    21 
    21 definition fFalse :: bool where
    22 definition fFalse :: bool where
    22 "fFalse \<longleftrightarrow> False"
    23 "fFalse \<longleftrightarrow> False"
    37 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    38 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    38 
    39 
    39 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    40 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    40 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    41 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    41 
    42 
    42 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
       
    43 "fequal x y \<longleftrightarrow> (x = y)"
       
    44 
       
    45 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    43 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    46 "fAll P \<longleftrightarrow> All P"
    44 "fAll P \<longleftrightarrow> All P"
    47 
    45 
    48 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    46 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    49 "fEx P \<longleftrightarrow> Ex P"
    47 "fEx P \<longleftrightarrow> Ex P"
       
    48 
       
    49 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
       
    50 "fequal x y \<longleftrightarrow> (x = y)"
    50 
    51 
    51 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    52 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    52 unfolding fFalse_def fTrue_def by simp
    53 unfolding fFalse_def fTrue_def by simp
    53 
    54 
    54 lemma fNot_table:
    55 lemma fNot_table:
    72 "fimplies P fTrue = fTrue"
    73 "fimplies P fTrue = fTrue"
    73 "fimplies fFalse P = fTrue"
    74 "fimplies fFalse P = fTrue"
    74 "fimplies fTrue fFalse = fFalse"
    75 "fimplies fTrue fFalse = fFalse"
    75 unfolding fFalse_def fTrue_def fimplies_def by auto
    76 unfolding fFalse_def fTrue_def fimplies_def by auto
    76 
    77 
    77 lemma fequal_table:
       
    78 "fequal x x = fTrue"
       
    79 "x = y \<or> fequal x y = fFalse"
       
    80 unfolding fFalse_def fTrue_def fequal_def by auto
       
    81 
       
    82 lemma fAll_table:
    78 lemma fAll_table:
    83 "Ex (fComp P) \<or> fAll P = fTrue"
    79 "Ex (fComp P) \<or> fAll P = fTrue"
    84 "All P \<or> fAll P = fFalse"
    80 "All P \<or> fAll P = fFalse"
    85 unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    81 unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    86 
    82 
    87 lemma fEx_table:
    83 lemma fEx_table:
    88 "All (fComp P) \<or> fEx P = fTrue"
    84 "All (fComp P) \<or> fEx P = fTrue"
    89 "Ex P \<or> fEx P = fFalse"
    85 "Ex P \<or> fEx P = fFalse"
    90 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    86 unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
       
    87 
       
    88 lemma fequal_table:
       
    89 "fequal x x = fTrue"
       
    90 "x = y \<or> fequal x y = fFalse"
       
    91 unfolding fFalse_def fTrue_def fequal_def by auto
    91 
    92 
    92 lemma fNot_law:
    93 lemma fNot_law:
    93 "fNot P \<noteq> P"
    94 "fNot P \<noteq> P"
    94 unfolding fNot_def by auto
    95 unfolding fNot_def by auto
    95 
    96 
   112 lemma fimplies_laws:
   113 lemma fimplies_laws:
   113 "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
   114 "fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
   114 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
   115 "fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
   115 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
   116 unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
   116 
   117 
   117 lemma fequal_laws:
       
   118 "fequal x y = fequal y x"
       
   119 "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
       
   120 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
       
   121 unfolding fFalse_def fTrue_def fequal_def by auto
       
   122 
       
   123 lemma fAll_law:
   118 lemma fAll_law:
   124 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
   119 "fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
   125 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   120 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   126 
   121 
   127 lemma fEx_law:
   122 lemma fEx_law:
   128 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
   123 "fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
   129 unfolding fNot_def fComp_def fAll_def fEx_def by auto
   124 unfolding fNot_def fComp_def fAll_def fEx_def by auto
       
   125 
       
   126 lemma fequal_laws:
       
   127 "fequal x y = fequal y x"
       
   128 "fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
       
   129 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
       
   130 unfolding fFalse_def fTrue_def fequal_def by auto
       
   131 
   130 
   132 
   131 subsection {* Setup *}
   133 subsection {* Setup *}
   132 
   134 
   133 ML_file "Tools/ATP/atp_problem_generate.ML"
   135 ML_file "Tools/ATP/atp_problem_generate.ML"
   134 ML_file "Tools/ATP/atp_proof_reconstruct.ML"
   136 ML_file "Tools/ATP/atp_proof_reconstruct.ML"