src/HOL/Metis.thy
changeset 41140 9c68004b8c9d
parent 41042 8275f52ac991
child 42349 721e85fd2db3
     1.1 --- a/src/HOL/Metis.thy	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Metis.thy	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -15,17 +15,26 @@
     1.4       ("Tools/try.ML")
     1.5  begin
     1.6  
     1.7 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
     1.8 -"fequal X Y \<longleftrightarrow> (X = Y)"
     1.9 +definition fFalse :: bool where [no_atp]:
    1.10 +"fFalse \<longleftrightarrow> False"
    1.11  
    1.12 -lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
    1.13 -by (simp add: fequal_def)
    1.14 +definition fTrue :: bool where [no_atp]:
    1.15 +"fTrue \<longleftrightarrow> True"
    1.16 +
    1.17 +definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    1.18 +"fNot P \<longleftrightarrow> \<not> P"
    1.19  
    1.20 -lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
    1.21 -by (simp add: fequal_def)
    1.22 +definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.23 +"fconj P Q \<longleftrightarrow> P \<and> Q"
    1.24 +
    1.25 +definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.26 +"fdisj P Q \<longleftrightarrow> P \<or> Q"
    1.27  
    1.28 -lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
    1.29 -by auto
    1.30 +definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.31 +"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    1.32 +
    1.33 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.34 +"fequal x y \<longleftrightarrow> (x = y)"
    1.35  
    1.36  use "Tools/Metis/metis_translate.ML"
    1.37  use "Tools/Metis/metis_reconstruct.ML"
    1.38 @@ -36,8 +45,9 @@
    1.39    #> Metis_Tactics.setup
    1.40  *}
    1.41  
    1.42 -hide_const (open) fequal
    1.43 -hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    1.44 +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
    1.45 +hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.46 +                 fequal_def
    1.47  
    1.48  subsection {* Try *}
    1.49