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.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.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
```