src/HOL/HOL.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 66893 ced164fe3bbd
child 67091 1393c2340eec
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/HOL.thy
     2     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     3 *)
     4 
     5 section \<open>The basis of Higher-Order Logic\<close>
     6 
     7 theory HOL
     8 imports Pure "~~/src/Tools/Code_Generator"
     9 keywords
    10   "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
    11     "print_induct_rules" :: diag and
    12   "quickcheck_params" :: thy_decl
    13 begin
    14 
    15 ML_file "~~/src/Tools/misc_legacy.ML"
    16 ML_file "~~/src/Tools/try.ML"
    17 ML_file "~~/src/Tools/quickcheck.ML"
    18 ML_file "~~/src/Tools/solve_direct.ML"
    19 ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
    20 ML_file "~~/src/Tools/IsaPlanner/isand.ML"
    21 ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
    22 ML_file "~~/src/Provers/hypsubst.ML"
    23 ML_file "~~/src/Provers/splitter.ML"
    24 ML_file "~~/src/Provers/classical.ML"
    25 ML_file "~~/src/Provers/blast.ML"
    26 ML_file "~~/src/Provers/clasimp.ML"
    27 ML_file "~~/src/Tools/eqsubst.ML"
    28 ML_file "~~/src/Provers/quantifier1.ML"
    29 ML_file "~~/src/Tools/atomize_elim.ML"
    30 ML_file "~~/src/Tools/cong_tac.ML"
    31 ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
    32 ML_file "~~/src/Tools/project_rule.ML"
    33 ML_file "~~/src/Tools/subtyping.ML"
    34 ML_file "~~/src/Tools/case_product.ML"
    35 
    36 
    37 ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
    38 
    39 ML \<open>
    40   Plugin_Name.declare_setup @{binding quickcheck_random};
    41   Plugin_Name.declare_setup @{binding quickcheck_exhaustive};
    42   Plugin_Name.declare_setup @{binding quickcheck_bounded_forall};
    43   Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive};
    44   Plugin_Name.declare_setup @{binding quickcheck_narrowing};
    45 \<close>
    46 ML \<open>
    47   Plugin_Name.define_setup @{binding quickcheck}
    48    [@{plugin quickcheck_exhaustive},
    49     @{plugin quickcheck_random},
    50     @{plugin quickcheck_bounded_forall},
    51     @{plugin quickcheck_full_exhaustive},
    52     @{plugin quickcheck_narrowing}]
    53 \<close>
    54 
    55 
    56 subsection \<open>Primitive logic\<close>
    57 
    58 text \<open>
    59 The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that
    60 describes the first implementation of HOL. However, there are a number of differences.
    61 In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
    62 only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
    63 axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
    64 line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
    65 \<close>
    66 
    67 subsubsection \<open>Core syntax\<close>
    68 
    69 setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
    70 default_sort type
    71 setup \<open>Object_Logic.add_base_sort @{sort type}\<close>
    72 
    73 axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
    74 instance "fun" :: (type, type) type by (rule fun_arity)
    75 
    76 axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
    77 instance itself :: (type) type by (rule itself_arity)
    78 
    79 typedecl bool
    80 
    81 judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
    82 
    83 axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
    84   and eq :: "['a, 'a] \<Rightarrow> bool"  (infixl "=" 50)
    85   and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    86 
    87 
    88 subsubsection \<open>Defined connectives and quantifiers\<close>
    89 
    90 definition True :: bool
    91   where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
    92 
    93 definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
    94   where "All P \<equiv> (P = (\<lambda>x. True))"
    95 
    96 definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
    97   where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
    98 
    99 definition False :: bool
   100   where "False \<equiv> (\<forall>P. P)"
   101 
   102 definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
   103   where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
   104 
   105 definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
   106   where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
   107 
   108 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   109   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
   110 
   111 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   112   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
   113 
   114 
   115 subsubsection \<open>Additional concrete syntax\<close>
   116 
   117 syntax (ASCII)
   118   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
   119 syntax (input)
   120   "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
   121 syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
   122 translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
   123 
   124 print_translation \<open>
   125  [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Ex1} @{syntax_const "_Ex1"}]
   126 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
   127 
   128 
   129 syntax
   130   "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
   131   "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
   132 translations
   133   "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
   134   "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
   135 
   136 
   137 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
   138   where "x \<noteq> y \<equiv> \<not> (x = y)"
   139 
   140 notation (output)
   141   eq  (infix "=" 50) and
   142   not_equal  (infix "\<noteq>" 50)
   143 
   144 notation (ASCII output)
   145   not_equal  (infix "~=" 50)
   146 
   147 notation (ASCII)
   148   Not  ("~ _" [40] 40) and
   149   conj  (infixr "&" 35) and
   150   disj  (infixr "|" 30) and
   151   implies  (infixr "-->" 25) and
   152   not_equal  (infixl "~=" 50)
   153 
   154 abbreviation (iff)
   155   iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
   156   where "A \<longleftrightarrow> B \<equiv> A = B"
   157 
   158 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
   159 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
   160 print_translation \<open>
   161   [(@{const_syntax The}, fn _ => fn [Abs abs] =>
   162       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
   163       in Syntax.const @{syntax_const "_The"} $ x $ t end)]
   164 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
   165 
   166 nonterminal letbinds and letbind
   167 syntax
   168   "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              ("(2_ =/ _)" 10)
   169   ""            :: "letbind \<Rightarrow> letbinds"                 ("_")
   170   "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     ("_;/ _")
   171   "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                ("(let (_)/ in (_))" [0, 10] 10)
   172 
   173 nonterminal case_syn and cases_syn
   174 syntax
   175   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
   176   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
   177   "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
   178   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
   179 syntax (ASCII)
   180   "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
   181 
   182 notation (ASCII)
   183   All  (binder "ALL " 10) and
   184   Ex  (binder "EX " 10)
   185 
   186 notation (input)
   187   All  (binder "! " 10) and
   188   Ex  (binder "? " 10)
   189 
   190 
   191 subsubsection \<open>Axioms and basic definitions\<close>
   192 
   193 axiomatization where
   194   refl: "t = (t::'a)" and
   195   subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
   196   ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
   197     \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses
   198          a related property.  It is an eta-expanded version of the traditional
   199          rule, and similar to the ABS rule of HOL\<close> and
   200 
   201   the_eq_trivial: "(THE x. x = a) = (a::'a)"
   202 
   203 axiomatization where
   204   impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
   205   mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
   206 
   207   True_or_False: "(P = True) \<or> (P = False)"
   208 
   209 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
   210   where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
   211 
   212 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   213   where "Let s f \<equiv> f s"
   214 
   215 translations
   216   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   217   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
   218 
   219 axiomatization undefined :: 'a
   220 
   221 class default = fixes default :: 'a
   222 
   223 
   224 subsection \<open>Fundamental rules\<close>
   225 
   226 subsubsection \<open>Equality\<close>
   227 
   228 lemma sym: "s = t \<Longrightarrow> t = s"
   229   by (erule subst) (rule refl)
   230 
   231 lemma ssubst: "t = s \<Longrightarrow> P s \<Longrightarrow> P t"
   232   by (drule sym) (erule subst)
   233 
   234 lemma trans: "\<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t"
   235   by (erule subst)
   236 
   237 lemma trans_sym [Pure.elim?]: "r = s \<Longrightarrow> t = s \<Longrightarrow> r = t"
   238   by (rule trans [OF _ sym])
   239 
   240 lemma meta_eq_to_obj_eq:
   241   assumes "A \<equiv> B"
   242   shows "A = B"
   243   unfolding assms by (rule refl)
   244 
   245 text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
   246      (* a = b
   247         |   |
   248         c = d   *)
   249 lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
   250   apply (rule trans)
   251    apply (rule trans)
   252     apply (rule sym)
   253     apply assumption+
   254   done
   255 
   256 text \<open>For calculational reasoning:\<close>
   257 
   258 lemma forw_subst: "a = b \<Longrightarrow> P b \<Longrightarrow> P a"
   259   by (rule ssubst)
   260 
   261 lemma back_subst: "P a \<Longrightarrow> a = b \<Longrightarrow> P b"
   262   by (rule subst)
   263 
   264 
   265 subsubsection \<open>Congruence rules for application\<close>
   266 
   267 text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
   268 lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
   269   apply (erule subst)
   270   apply (rule refl)
   271   done
   272 
   273 text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
   274 lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
   275   apply (erule subst)
   276   apply (rule refl)
   277   done
   278 
   279 lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
   280   apply (erule ssubst)+
   281   apply (rule refl)
   282   done
   283 
   284 lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
   285   apply (erule subst)+
   286   apply (rule refl)
   287   done
   288 
   289 ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
   290 
   291 
   292 subsubsection \<open>Equality of booleans -- iff\<close>
   293 
   294 lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
   295   by (erule ssubst)
   296 
   297 lemma rev_iffD2: "\<lbrakk>Q; P = Q\<rbrakk> \<Longrightarrow> P"
   298   by (erule iffD2)
   299 
   300 lemma iffD1: "Q = P \<Longrightarrow> Q \<Longrightarrow> P"
   301   by (drule sym) (rule iffD2)
   302 
   303 lemma rev_iffD1: "Q \<Longrightarrow> Q = P \<Longrightarrow> P"
   304   by (drule sym) (rule rev_iffD2)
   305 
   306 lemma iffE:
   307   assumes major: "P = Q"
   308     and minor: "\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R"
   309   shows R
   310   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
   311 
   312 
   313 subsubsection \<open>True (1)\<close>
   314 
   315 lemma TrueI: True
   316   unfolding True_def by (rule refl)
   317 
   318 lemma eqTrueE: "P = True \<Longrightarrow> P"
   319   by (erule iffD2) (rule TrueI)
   320 
   321 
   322 subsubsection \<open>Universal quantifier (1)\<close>
   323 
   324 lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
   325   apply (unfold All_def)
   326   apply (rule eqTrueE)
   327   apply (erule fun_cong)
   328   done
   329 
   330 lemma allE:
   331   assumes major: "\<forall>x. P x"
   332     and minor: "P x \<Longrightarrow> R"
   333   shows R
   334   by (iprover intro: minor major [THEN spec])
   335 
   336 lemma all_dupE:
   337   assumes major: "\<forall>x. P x"
   338     and minor: "\<lbrakk>P x; \<forall>x. P x\<rbrakk> \<Longrightarrow> R"
   339   shows R
   340   by (iprover intro: minor major major [THEN spec])
   341 
   342 
   343 subsubsection \<open>False\<close>
   344 
   345 text \<open>
   346   Depends upon \<open>spec\<close>; it is impossible to do propositional
   347   logic before quantifiers!
   348 \<close>
   349 
   350 lemma FalseE: "False \<Longrightarrow> P"
   351   apply (unfold False_def)
   352   apply (erule spec)
   353   done
   354 
   355 lemma False_neq_True: "False = True \<Longrightarrow> P"
   356   by (erule eqTrueE [THEN FalseE])
   357 
   358 
   359 subsubsection \<open>Negation\<close>
   360 
   361 lemma notI:
   362   assumes "P \<Longrightarrow> False"
   363   shows "\<not> P"
   364   apply (unfold not_def)
   365   apply (iprover intro: impI assms)
   366   done
   367 
   368 lemma False_not_True: "False \<noteq> True"
   369   apply (rule notI)
   370   apply (erule False_neq_True)
   371   done
   372 
   373 lemma True_not_False: "True \<noteq> False"
   374   apply (rule notI)
   375   apply (drule sym)
   376   apply (erule False_neq_True)
   377   done
   378 
   379 lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R"
   380   apply (unfold not_def)
   381   apply (erule mp [THEN FalseE])
   382   apply assumption
   383   done
   384 
   385 lemma notI2: "(P \<Longrightarrow> \<not> Pa) \<Longrightarrow> (P \<Longrightarrow> Pa) \<Longrightarrow> \<not> P"
   386   by (erule notE [THEN notI]) (erule meta_mp)
   387 
   388 
   389 subsubsection \<open>Implication\<close>
   390 
   391 lemma impE:
   392   assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
   393   shows R
   394   by (iprover intro: assms mp)
   395 
   396 text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
   397 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   398   by (iprover intro: mp)
   399 
   400 lemma contrapos_nn:
   401   assumes major: "\<not> Q"
   402     and minor: "P \<Longrightarrow> Q"
   403   shows "\<not> P"
   404   by (iprover intro: notI minor major [THEN notE])
   405 
   406 text \<open>Not used at all, but we already have the other 3 combinations.\<close>
   407 lemma contrapos_pn:
   408   assumes major: "Q"
   409     and minor: "P \<Longrightarrow> \<not> Q"
   410   shows "\<not> P"
   411   by (iprover intro: notI minor major notE)
   412 
   413 lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
   414   by (erule contrapos_nn) (erule sym)
   415 
   416 lemma eq_neq_eq_imp_neq: "\<lbrakk>x = a; a \<noteq> b; b = y\<rbrakk> \<Longrightarrow> x \<noteq> y"
   417   by (erule subst, erule ssubst, assumption)
   418 
   419 
   420 subsubsection \<open>Disjunction (1)\<close>
   421 
   422 lemma disjE:
   423   assumes major: "P \<or> Q"
   424     and minorP: "P \<Longrightarrow> R"
   425     and minorQ: "Q \<Longrightarrow> R"
   426   shows R
   427   by (iprover intro: minorP minorQ impI
   428       major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   429 
   430 
   431 subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
   432 
   433 text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
   434 
   435 lemma iffI:
   436   assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
   437   shows "P = Q"
   438 proof (rule disjE[OF True_or_False[of P]])
   439   assume 1: "P = True"
   440   note Q = assms(1)[OF eqTrueE[OF this]]
   441   from 1 show ?thesis
   442   proof (rule ssubst)
   443     from True_or_False[of Q] show "True = Q"
   444     proof (rule disjE)
   445       assume "Q = True"
   446       thus ?thesis by(rule sym)
   447     next
   448       assume "Q = False"
   449       with Q have False by (rule rev_iffD1)
   450       thus ?thesis by (rule FalseE)
   451     qed
   452   qed
   453 next
   454   assume 2: "P = False"
   455   thus ?thesis
   456   proof (rule ssubst)
   457     from True_or_False[of Q] show "False = Q"
   458     proof (rule disjE)
   459       assume "Q = True"
   460       from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
   461       thus ?thesis by (rule FalseE)
   462     next
   463       assume "Q = False"
   464       thus ?thesis by(rule sym)
   465     qed
   466   qed
   467 qed
   468 
   469 
   470 subsubsection \<open>True (2)\<close>
   471 
   472 lemma eqTrueI: "P \<Longrightarrow> P = True"
   473   by (iprover intro: iffI TrueI)
   474 
   475 
   476 subsubsection \<open>Universal quantifier (2)\<close>
   477 
   478 lemma allI:
   479   assumes "\<And>x::'a. P x"
   480   shows "\<forall>x. P x"
   481   unfolding All_def by (iprover intro: ext eqTrueI assms)
   482 
   483 
   484 subsubsection \<open>Existential quantifier\<close>
   485 
   486 lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   487   unfolding Ex_def by (iprover intro: allI allE impI mp)
   488 
   489 lemma exE:
   490   assumes major: "\<exists>x::'a. P x"
   491     and minor: "\<And>x. P x \<Longrightarrow> Q"
   492   shows "Q"
   493   by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
   494 
   495 
   496 subsubsection \<open>Conjunction\<close>
   497 
   498 lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
   499   unfolding and_def by (iprover intro: impI [THEN allI] mp)
   500 
   501 lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
   502   unfolding and_def by (iprover intro: impI dest: spec mp)
   503 
   504 lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
   505   unfolding and_def by (iprover intro: impI dest: spec mp)
   506 
   507 lemma conjE:
   508   assumes major: "P \<and> Q"
   509     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   510   shows R
   511   apply (rule minor)
   512    apply (rule major [THEN conjunct1])
   513   apply (rule major [THEN conjunct2])
   514   done
   515 
   516 lemma context_conjI:
   517   assumes P "P \<Longrightarrow> Q"
   518   shows "P \<and> Q"
   519   by (iprover intro: conjI assms)
   520 
   521 
   522 subsubsection \<open>Disjunction (2)\<close>
   523 
   524 lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   525   unfolding or_def by (iprover intro: allI impI mp)
   526 
   527 lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   528   unfolding or_def by (iprover intro: allI impI mp)
   529 
   530 
   531 subsubsection \<open>Classical logic\<close>
   532 
   533 lemma classical:
   534   assumes prem: "\<not> P \<Longrightarrow> P"
   535   shows P
   536   apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   537    apply assumption
   538   apply (rule notI [THEN prem, THEN eqTrueI])
   539   apply (erule subst)
   540   apply assumption
   541   done
   542 
   543 lemmas ccontr = FalseE [THEN classical]
   544 
   545 text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
   546   make elimination rules.\<close>
   547 lemma rev_notE:
   548   assumes premp: P
   549     and premnot: "\<not> R \<Longrightarrow> \<not> P"
   550   shows R
   551   apply (rule ccontr)
   552   apply (erule notE [OF premnot premp])
   553   done
   554 
   555 text \<open>Double negation law.\<close>
   556 lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
   557   apply (rule classical)
   558   apply (erule notE)
   559   apply assumption
   560   done
   561 
   562 lemma contrapos_pp:
   563   assumes p1: Q
   564     and p2: "\<not> P \<Longrightarrow> \<not> Q"
   565   shows P
   566   by (iprover intro: classical p1 p2 notE)
   567 
   568 
   569 subsubsection \<open>Unique existence\<close>
   570 
   571 lemma ex1I:
   572   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
   573   shows "\<exists>!x. P x"
   574   unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
   575 
   576 text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
   577 lemma ex_ex1I:
   578   assumes ex_prem: "\<exists>x. P x"
   579     and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
   580   shows "\<exists>!x. P x"
   581   by (iprover intro: ex_prem [THEN exE] ex1I eq)
   582 
   583 lemma ex1E:
   584   assumes major: "\<exists>!x. P x"
   585     and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
   586   shows R
   587   apply (rule major [unfolded Ex1_def, THEN exE])
   588   apply (erule conjE)
   589   apply (iprover intro: minor)
   590   done
   591 
   592 lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
   593   apply (erule ex1E)
   594   apply (rule exI)
   595   apply assumption
   596   done
   597 
   598 
   599 subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
   600 
   601 lemma disjCI:
   602   assumes "\<not> Q \<Longrightarrow> P"
   603   shows "P \<or> Q"
   604   by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
   605 
   606 lemma excluded_middle: "\<not> P \<or> P"
   607   by (iprover intro: disjCI)
   608 
   609 text \<open>
   610   case distinction as a natural deduction rule.
   611   Note that \<open>\<not> P\<close> is the second case, not the first.
   612 \<close>
   613 lemma case_split [case_names True False]:
   614   assumes prem1: "P \<Longrightarrow> Q"
   615     and prem2: "\<not> P \<Longrightarrow> Q"
   616   shows Q
   617   apply (rule excluded_middle [THEN disjE])
   618    apply (erule prem2)
   619   apply (erule prem1)
   620   done
   621 
   622 text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
   623 lemma impCE:
   624   assumes major: "P \<longrightarrow> Q"
   625     and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
   626   shows R
   627   apply (rule excluded_middle [of P, THEN disjE])
   628    apply (iprover intro: minor major [THEN mp])+
   629   done
   630 
   631 text \<open>
   632   This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>.  It works best for
   633   those cases in which \<open>P\<close> holds "almost everywhere".  Can't install as
   634   default: would break old proofs.
   635 \<close>
   636 lemma impCE':
   637   assumes major: "P \<longrightarrow> Q"
   638     and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
   639   shows R
   640   apply (rule excluded_middle [of P, THEN disjE])
   641    apply (iprover intro: minor major [THEN mp])+
   642   done
   643 
   644 text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
   645 lemma iffCE:
   646   assumes major: "P = Q"
   647     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   648   shows R
   649   by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
   650 
   651 lemma exCI:
   652   assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
   653   shows "\<exists>x. P x"
   654   by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
   655 
   656 
   657 subsubsection \<open>Intuitionistic Reasoning\<close>
   658 
   659 lemma impE':
   660   assumes 1: "P \<longrightarrow> Q"
   661     and 2: "Q \<Longrightarrow> R"
   662     and 3: "P \<longrightarrow> Q \<Longrightarrow> P"
   663   shows R
   664 proof -
   665   from 3 and 1 have P .
   666   with 1 have Q by (rule impE)
   667   with 2 show R .
   668 qed
   669 
   670 lemma allE':
   671   assumes 1: "\<forall>x. P x"
   672     and 2: "P x \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q"
   673   shows Q
   674 proof -
   675   from 1 have "P x" by (rule spec)
   676   from this and 1 show Q by (rule 2)
   677 qed
   678 
   679 lemma notE':
   680   assumes 1: "\<not> P"
   681     and 2: "\<not> P \<Longrightarrow> P"
   682   shows R
   683 proof -
   684   from 2 and 1 have P .
   685   with 1 show R by (rule notE)
   686 qed
   687 
   688 lemma TrueE: "True \<Longrightarrow> P \<Longrightarrow> P" .
   689 lemma notFalseE: "\<not> False \<Longrightarrow> P \<Longrightarrow> P" .
   690 
   691 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE
   692   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   693   and [Pure.elim 2] = allE notE' impE'
   694   and [Pure.intro] = exI disjI2 disjI1
   695 
   696 lemmas [trans] = trans
   697   and [sym] = sym not_sym
   698   and [Pure.elim?] = iffD1 iffD2 impE
   699 
   700 
   701 subsubsection \<open>Atomizing meta-level connectives\<close>
   702 
   703 axiomatization where
   704   eq_reflection: "x = y \<Longrightarrow> x \<equiv> y"  \<comment> \<open>admissible axiom\<close>
   705 
   706 lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
   707 proof
   708   assume "\<And>x. P x"
   709   then show "\<forall>x. P x" ..
   710 next
   711   assume "\<forall>x. P x"
   712   then show "\<And>x. P x" by (rule allE)
   713 qed
   714 
   715 lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
   716 proof
   717   assume r: "A \<Longrightarrow> B"
   718   show "A \<longrightarrow> B" by (rule impI) (rule r)
   719 next
   720   assume "A \<longrightarrow> B" and A
   721   then show B by (rule mp)
   722 qed
   723 
   724 lemma atomize_not: "(A \<Longrightarrow> False) \<equiv> Trueprop (\<not> A)"
   725 proof
   726   assume r: "A \<Longrightarrow> False"
   727   show "\<not> A" by (rule notI) (rule r)
   728 next
   729   assume "\<not> A" and A
   730   then show False by (rule notE)
   731 qed
   732 
   733 lemma atomize_eq [atomize, code]: "(x \<equiv> y) \<equiv> Trueprop (x = y)"
   734 proof
   735   assume "x \<equiv> y"
   736   show "x = y" by (unfold \<open>x \<equiv> y\<close>) (rule refl)
   737 next
   738   assume "x = y"
   739   then show "x \<equiv> y" by (rule eq_reflection)
   740 qed
   741 
   742 lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)"
   743 proof
   744   assume conj: "A &&& B"
   745   show "A \<and> B"
   746   proof (rule conjI)
   747     from conj show A by (rule conjunctionD1)
   748     from conj show B by (rule conjunctionD2)
   749   qed
   750 next
   751   assume conj: "A \<and> B"
   752   show "A &&& B"
   753   proof -
   754     from conj show A ..
   755     from conj show B ..
   756   qed
   757 qed
   758 
   759 lemmas [symmetric, rulify] = atomize_all atomize_imp
   760   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
   761 
   762 
   763 subsubsection \<open>Atomizing elimination rules\<close>
   764 
   765 lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)"
   766   by rule iprover+
   767 
   768 lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
   769   by rule iprover+
   770 
   771 lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
   772   by rule iprover+
   773 
   774 lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" ..
   775 
   776 
   777 subsection \<open>Package setup\<close>
   778 
   779 ML_file "Tools/hologic.ML"
   780 
   781 
   782 subsubsection \<open>Sledgehammer setup\<close>
   783 
   784 text \<open>
   785   Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
   786   that are prolific (match too many equality or membership literals) and relate to
   787   seldom-used facts. Some duplicate other rules.
   788 \<close>
   789 
   790 named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
   791 
   792 
   793 subsubsection \<open>Classical Reasoner setup\<close>
   794 
   795 lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   796   by (rule classical) iprover
   797 
   798 lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   799   by (rule classical) iprover
   800 
   801 lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
   802 
   803 ML \<open>
   804 structure Hypsubst = Hypsubst
   805 (
   806   val dest_eq = HOLogic.dest_eq
   807   val dest_Trueprop = HOLogic.dest_Trueprop
   808   val dest_imp = HOLogic.dest_imp
   809   val eq_reflection = @{thm eq_reflection}
   810   val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
   811   val imp_intr = @{thm impI}
   812   val rev_mp = @{thm rev_mp}
   813   val subst = @{thm subst}
   814   val sym = @{thm sym}
   815   val thin_refl = @{thm thin_refl};
   816 );
   817 open Hypsubst;
   818 
   819 structure Classical = Classical
   820 (
   821   val imp_elim = @{thm imp_elim}
   822   val not_elim = @{thm notE}
   823   val swap = @{thm swap}
   824   val classical = @{thm classical}
   825   val sizef = Drule.size_of_thm
   826   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
   827 );
   828 
   829 structure Basic_Classical: BASIC_CLASSICAL = Classical;
   830 open Basic_Classical;
   831 \<close>
   832 
   833 setup \<open>
   834   (*prevent substitution on bool*)
   835   let
   836     fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
   837       | non_bool_eq _ = false;
   838     fun hyp_subst_tac' ctxt =
   839       SUBGOAL (fn (goal, i) =>
   840         if Term.exists_Const non_bool_eq goal
   841         then Hypsubst.hyp_subst_tac ctxt i
   842         else no_tac);
   843   in
   844     Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
   845   end
   846 \<close>
   847 
   848 declare iffI [intro!]
   849   and notI [intro!]
   850   and impI [intro!]
   851   and disjCI [intro!]
   852   and conjI [intro!]
   853   and TrueI [intro!]
   854   and refl [intro!]
   855 
   856 declare iffCE [elim!]
   857   and FalseE [elim!]
   858   and impCE [elim!]
   859   and disjE [elim!]
   860   and conjE [elim!]
   861 
   862 declare ex_ex1I [intro!]
   863   and allI [intro!]
   864   and exI [intro]
   865 
   866 declare exE [elim!]
   867   allE [elim]
   868 
   869 ML \<open>val HOL_cs = claset_of @{context}\<close>
   870 
   871 lemma contrapos_np: "\<not> Q \<Longrightarrow> (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P"
   872   apply (erule swap)
   873   apply (erule (1) meta_mp)
   874   done
   875 
   876 declare ex_ex1I [rule del, intro! 2]
   877   and ex1I [intro]
   878 
   879 declare ext [intro]
   880 
   881 lemmas [intro?] = ext
   882   and [elim?] = ex1_implies_ex
   883 
   884 text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
   885 lemma alt_ex1E [elim!]:
   886   assumes major: "\<exists>!x. P x"
   887     and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   888   shows R
   889   apply (rule ex1E [OF major])
   890   apply (rule prem)
   891    apply assumption
   892   apply (rule allI)+
   893   apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
   894   apply iprover
   895   done
   896 
   897 ML \<open>
   898   structure Blast = Blast
   899   (
   900     structure Classical = Classical
   901     val Trueprop_const = dest_Const @{const Trueprop}
   902     val equality_name = @{const_name HOL.eq}
   903     val not_name = @{const_name Not}
   904     val notE = @{thm notE}
   905     val ccontr = @{thm ccontr}
   906     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   907   );
   908   val blast_tac = Blast.blast_tac;
   909 \<close>
   910 
   911 
   912 subsubsection \<open>THE: definite description operator\<close>
   913 
   914 lemma the_equality [intro]:
   915   assumes "P a"
   916     and "\<And>x. P x \<Longrightarrow> x = a"
   917   shows "(THE x. P x) = a"
   918   by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
   919 
   920 lemma theI:
   921   assumes "P a"
   922     and "\<And>x. P x \<Longrightarrow> x = a"
   923   shows "P (THE x. P x)"
   924   by (iprover intro: assms the_equality [THEN ssubst])
   925 
   926 lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
   927   by (blast intro: theI)
   928 
   929 text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
   930 lemma theI2:
   931   assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
   932   shows "Q (THE x. P x)"
   933   by (iprover intro: assms theI)
   934 
   935 lemma the1I2:
   936   assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   937   shows "Q (THE x. P x)"
   938   by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
   939 
   940 lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
   941   by blast
   942 
   943 lemma the_sym_eq_trivial: "(THE y. x = y) = x"
   944   by blast
   945 
   946 
   947 subsubsection \<open>Simplifier\<close>
   948 
   949 lemma eta_contract_eq: "(\<lambda>s. f s) = f" ..
   950 
   951 lemma simp_thms:
   952   shows not_not: "(\<not> \<not> P) = P"
   953   and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)"
   954   and
   955     "(P \<noteq> Q) = (P = (\<not> Q))"
   956     "(P \<or> \<not>P) = True"    "(\<not> P \<or> P) = True"
   957     "(x = x) = True"
   958   and not_True_eq_False [code]: "(\<not> True) = False"
   959   and not_False_eq_True [code]: "(\<not> False) = True"
   960   and
   961     "(\<not> P) \<noteq> P"  "P \<noteq> (\<not> P)"
   962     "(True = P) = P"
   963   and eq_True: "(P = True) = P"
   964   and "(False = P) = (\<not> P)"
   965   and eq_False: "(P = False) = (\<not> P)"
   966   and
   967     "(True \<longrightarrow> P) = P"  "(False \<longrightarrow> P) = True"
   968     "(P \<longrightarrow> True) = True"  "(P \<longrightarrow> P) = True"
   969     "(P \<longrightarrow> False) = (\<not> P)"  "(P \<longrightarrow> \<not> P) = (\<not> P)"
   970     "(P \<and> True) = P"  "(True \<and> P) = P"
   971     "(P \<and> False) = False"  "(False \<and> P) = False"
   972     "(P \<and> P) = P"  "(P \<and> (P \<and> Q)) = (P \<and> Q)"
   973     "(P \<and> \<not> P) = False"    "(\<not> P \<and> P) = False"
   974     "(P \<or> True) = True"  "(True \<or> P) = True"
   975     "(P \<or> False) = P"  "(False \<or> P) = P"
   976     "(P \<or> P) = P"  "(P \<or> (P \<or> Q)) = (P \<or> Q)" and
   977     "(\<forall>x. P) = P"  "(\<exists>x. P) = P"  "\<exists>x. x = t"  "\<exists>x. t = x"
   978   and
   979     "\<And>P. (\<exists>x. x = t \<and> P x) = P t"
   980     "\<And>P. (\<exists>x. t = x \<and> P x) = P t"
   981     "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
   982     "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
   983     "(\<forall>x. x \<noteq> t) = False"  "(\<forall>x. t \<noteq> x) = False"
   984   by (blast, blast, blast, blast, blast, iprover+)
   985 
   986 lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
   987   by blast
   988 
   989 lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
   990   by blast
   991 
   992 lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
   993   by blast
   994 
   995 lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
   996   by blast
   997 
   998 lemma eq_ac:
   999   shows eq_commute: "a = b \<longleftrightarrow> b = a"
  1000     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
  1001     and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
  1002   by (iprover, blast+)
  1003 
  1004 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
  1005 
  1006 lemma conj_comms:
  1007   shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
  1008     and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
  1009 lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
  1010 
  1011 lemmas conj_ac = conj_commute conj_left_commute conj_assoc
  1012 
  1013 lemma disj_comms:
  1014   shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
  1015     and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
  1016 lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
  1017 
  1018 lemmas disj_ac = disj_commute disj_left_commute disj_assoc
  1019 
  1020 lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
  1021 lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
  1022 
  1023 lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
  1024 lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
  1025 
  1026 lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
  1027 lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
  1028 lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
  1029 
  1030 text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
  1031 lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
  1032 lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
  1033 
  1034 lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
  1035 lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
  1036 
  1037 lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
  1038   by iprover
  1039 
  1040 lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
  1041 lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
  1042 lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
  1043 lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
  1044 lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
  1045 lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast  \<comment> \<open>changes orientation :-(\<close>
  1046 lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
  1047 lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
  1048 
  1049 lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
  1050 
  1051 
  1052 lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
  1053   \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
  1054   \<comment> \<open>cases boil down to the same thing.\<close>
  1055   by blast
  1056 
  1057 lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
  1058 lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
  1059 lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
  1060 lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
  1061 lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
  1062 
  1063 declare All_def [no_atp]
  1064 
  1065 lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
  1066 lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
  1067 
  1068 text \<open>
  1069   \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
  1070   May slow rewrite proofs down by as much as 50\%\<close>
  1071 
  1072 lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
  1073   by iprover
  1074 
  1075 lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
  1076   by iprover
  1077 
  1078 text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
  1079 
  1080 lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
  1081   by blast
  1082 
  1083 
  1084 text \<open>\<^medskip> if-then-else rules\<close>
  1085 
  1086 lemma if_True [code]: "(if True then x else y) = x"
  1087   unfolding If_def by blast
  1088 
  1089 lemma if_False [code]: "(if False then x else y) = y"
  1090   unfolding If_def by blast
  1091 
  1092 lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
  1093   unfolding If_def by blast
  1094 
  1095 lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
  1096   unfolding If_def by blast
  1097 
  1098 lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
  1099   apply (rule case_split [of Q])
  1100    apply (simplesubst if_P)
  1101     prefer 3
  1102     apply (simplesubst if_not_P)
  1103      apply blast+
  1104   done
  1105 
  1106 lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
  1107   by (simplesubst if_split) blast
  1108 
  1109 lemmas if_splits [no_atp] = if_split if_split_asm
  1110 
  1111 lemma if_cancel: "(if c then x else x) = x"
  1112   by (simplesubst if_split) blast
  1113 
  1114 lemma if_eq_cancel: "(if x = y then y else x) = x"
  1115   by (simplesubst if_split) blast
  1116 
  1117 lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
  1118   \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
  1119   by (rule if_split)
  1120 
  1121 lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
  1122   \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
  1123   by (simplesubst if_split) blast
  1124 
  1125 lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
  1126 lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
  1127 
  1128 text \<open>\<^medskip> let rules for simproc\<close>
  1129 
  1130 lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
  1131   by (unfold Let_def)
  1132 
  1133 lemma Let_unfold: "f x \<equiv> g \<Longrightarrow> Let x f \<equiv> g"
  1134   by (unfold Let_def)
  1135 
  1136 text \<open>
  1137   The following copy of the implication operator is useful for
  1138   fine-tuning congruence rules.  It instructs the simplifier to simplify
  1139   its premise.
  1140 \<close>
  1141 
  1142 definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop"  (infixr "=simp=>" 1)
  1143   where "simp_implies \<equiv> op \<Longrightarrow>"
  1144 
  1145 lemma simp_impliesI:
  1146   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
  1147   shows "PROP P =simp=> PROP Q"
  1148   apply (unfold simp_implies_def)
  1149   apply (rule PQ)
  1150   apply assumption
  1151   done
  1152 
  1153 lemma simp_impliesE:
  1154   assumes PQ: "PROP P =simp=> PROP Q"
  1155     and P: "PROP P"
  1156     and QR: "PROP Q \<Longrightarrow> PROP R"
  1157   shows "PROP R"
  1158   apply (rule QR)
  1159   apply (rule PQ [unfolded simp_implies_def])
  1160   apply (rule P)
  1161   done
  1162 
  1163 lemma simp_implies_cong:
  1164   assumes PP' :"PROP P \<equiv> PROP P'"
  1165     and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
  1166   shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
  1167   unfolding simp_implies_def
  1168 proof (rule equal_intr_rule)
  1169   assume PQ: "PROP P \<Longrightarrow> PROP Q"
  1170     and P': "PROP P'"
  1171   from PP' [symmetric] and P' have "PROP P"
  1172     by (rule equal_elim_rule1)
  1173   then have "PROP Q" by (rule PQ)
  1174   with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
  1175 next
  1176   assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
  1177     and P: "PROP P"
  1178   from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
  1179   then have "PROP Q'" by (rule P'Q')
  1180   with P'QQ' [OF P', symmetric] show "PROP Q"
  1181     by (rule equal_elim_rule1)
  1182 qed
  1183 
  1184 lemma uncurry:
  1185   assumes "P \<longrightarrow> Q \<longrightarrow> R"
  1186   shows "P \<and> Q \<longrightarrow> R"
  1187   using assms by blast
  1188 
  1189 lemma iff_allI:
  1190   assumes "\<And>x. P x = Q x"
  1191   shows "(\<forall>x. P x) = (\<forall>x. Q x)"
  1192   using assms by blast
  1193 
  1194 lemma iff_exI:
  1195   assumes "\<And>x. P x = Q x"
  1196   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
  1197   using assms by blast
  1198 
  1199 lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
  1200   by blast
  1201 
  1202 lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
  1203   by blast
  1204 
  1205 ML_file "Tools/simpdata.ML"
  1206 ML \<open>open Simpdata\<close>
  1207 
  1208 setup \<open>
  1209   map_theory_simpset (put_simpset HOL_basic_ss) #>
  1210   Simplifier.method_setup Splitter.split_modifiers
  1211 \<close>
  1212 
  1213 simproc_setup defined_Ex ("\<exists>x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
  1214 simproc_setup defined_All ("\<forall>x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
  1215 
  1216 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
  1217 
  1218 simproc_setup neq ("x = y") = \<open>fn _ =>
  1219   let
  1220     val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
  1221     fun is_neq eq lhs rhs thm =
  1222       (case Thm.prop_of thm of
  1223         _ $ (Not $ (eq' $ l' $ r')) =>
  1224           Not = HOLogic.Not andalso eq' = eq andalso
  1225           r' aconv lhs andalso l' aconv rhs
  1226       | _ => false);
  1227     fun proc ss ct =
  1228       (case Thm.term_of ct of
  1229         eq $ lhs $ rhs =>
  1230           (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
  1231             SOME thm => SOME (thm RS neq_to_EQ_False)
  1232           | NONE => NONE)
  1233        | _ => NONE);
  1234   in proc end;
  1235 \<close>
  1236 
  1237 simproc_setup let_simp ("Let x f") = \<open>
  1238   let
  1239     fun count_loose (Bound i) k = if i >= k then 1 else 0
  1240       | count_loose (s $ t) k = count_loose s k + count_loose t k
  1241       | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
  1242       | count_loose _ _ = 0;
  1243     fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
  1244       (case t of
  1245         Abs (_, _, t') => count_loose t' 0 <= 1
  1246       | _ => true);
  1247   in
  1248     fn _ => fn ctxt => fn ct =>
  1249       if is_trivial_let (Thm.term_of ct)
  1250       then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
  1251       else
  1252         let (*Norbert Schirmer's case*)
  1253           val t = Thm.term_of ct;
  1254           val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
  1255         in
  1256           Option.map (hd o Variable.export ctxt' ctxt o single)
  1257             (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
  1258               if is_Free x orelse is_Bound x orelse is_Const x
  1259               then SOME @{thm Let_def}
  1260               else
  1261                 let
  1262                   val n = case f of (Abs (x, _, _)) => x | _ => "x";
  1263                   val cx = Thm.cterm_of ctxt x;
  1264                   val xT = Thm.typ_of_cterm cx;
  1265                   val cf = Thm.cterm_of ctxt f;
  1266                   val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
  1267                   val (_ $ _ $ g) = Thm.prop_of fx_g;
  1268                   val g' = abstract_over (x, g);
  1269                   val abs_g'= Abs (n, xT, g');
  1270                 in
  1271                   if g aconv g' then
  1272                     let
  1273                       val rl =
  1274                         infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
  1275                     in SOME (rl OF [fx_g]) end
  1276                   else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
  1277                   then NONE (*avoid identity conversion*)
  1278                   else
  1279                     let
  1280                       val g'x = abs_g' $ x;
  1281                       val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
  1282                       val rl =
  1283                         @{thm Let_folded} |> infer_instantiate ctxt
  1284                           [(("f", 0), Thm.cterm_of ctxt f),
  1285                            (("x", 0), cx),
  1286                            (("g", 0), Thm.cterm_of ctxt abs_g')];
  1287                     in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
  1288                 end
  1289             | _ => NONE)
  1290         end
  1291   end
  1292 \<close>
  1293 
  1294 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
  1295 proof
  1296   assume "True \<Longrightarrow> PROP P"
  1297   from this [OF TrueI] show "PROP P" .
  1298 next
  1299   assume "PROP P"
  1300   then show "PROP P" .
  1301 qed
  1302 
  1303 lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
  1304   by standard (intro TrueI)
  1305 
  1306 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
  1307   by standard simp_all
  1308 
  1309 (* This is not made a simp rule because it does not improve any proofs
  1310    but slows some AFP entries down by 5% (cpu time). May 2015 *)
  1311 lemma implies_False_swap:
  1312   "NO_MATCH (Trueprop False) P \<Longrightarrow>
  1313     (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
  1314   by (rule swap_prems_eq)
  1315 
  1316 lemma ex_simps:
  1317   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
  1318   "\<And>P Q. (\<exists>x. P \<and> Q x)   = (P \<and> (\<exists>x. Q x))"
  1319   "\<And>P Q. (\<exists>x. P x \<or> Q)   = ((\<exists>x. P x) \<or> Q)"
  1320   "\<And>P Q. (\<exists>x. P \<or> Q x)   = (P \<or> (\<exists>x. Q x))"
  1321   "\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
  1322   "\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))"
  1323   \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close>
  1324   by (iprover | blast)+
  1325 
  1326 lemma all_simps:
  1327   "\<And>P Q. (\<forall>x. P x \<and> Q)   = ((\<forall>x. P x) \<and> Q)"
  1328   "\<And>P Q. (\<forall>x. P \<and> Q x)   = (P \<and> (\<forall>x. Q x))"
  1329   "\<And>P Q. (\<forall>x. P x \<or> Q)   = ((\<forall>x. P x) \<or> Q)"
  1330   "\<And>P Q. (\<forall>x. P \<or> Q x)   = (P \<or> (\<forall>x. Q x))"
  1331   "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
  1332   "\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))"
  1333   \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close>
  1334   by (iprover | blast)+
  1335 
  1336 lemmas [simp] =
  1337   triv_forall_equality  \<comment> \<open>prunes params\<close>
  1338   True_implies_equals implies_True_equals  \<comment> \<open>prune \<open>True\<close> in asms\<close>
  1339   False_implies_equals  \<comment> \<open>prune \<open>False\<close> in asms\<close>
  1340   if_True
  1341   if_False
  1342   if_cancel
  1343   if_eq_cancel
  1344   imp_disjL \<comment>
  1345    \<open>In general it seems wrong to add distributive laws by default: they
  1346     might cause exponential blow-up.  But \<open>imp_disjL\<close> has been in for a while
  1347     and cannot be removed without affecting existing proofs.  Moreover,
  1348     rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
  1349     grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
  1350   conj_assoc
  1351   disj_assoc
  1352   de_Morgan_conj
  1353   de_Morgan_disj
  1354   imp_disj1
  1355   imp_disj2
  1356   not_imp
  1357   disj_not1
  1358   not_all
  1359   not_ex
  1360   cases_simp
  1361   the_eq_trivial
  1362   the_sym_eq_trivial
  1363   ex_simps
  1364   all_simps
  1365   simp_thms
  1366 
  1367 lemmas [cong] = imp_cong simp_implies_cong
  1368 lemmas [split] = if_split
  1369 
  1370 ML \<open>val HOL_ss = simpset_of @{context}\<close>
  1371 
  1372 text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
  1373 lemma if_cong:
  1374   assumes "b = c"
  1375     and "c \<Longrightarrow> x = u"
  1376     and "\<not> c \<Longrightarrow> y = v"
  1377   shows "(if b then x else y) = (if c then u else v)"
  1378   using assms by simp
  1379 
  1380 text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
  1381   faster and allows the execution of functional programs.\<close>
  1382 lemma if_weak_cong [cong]:
  1383   assumes "b = c"
  1384   shows "(if b then x else y) = (if c then x else y)"
  1385   using assms by (rule arg_cong)
  1386 
  1387 text \<open>Prevents simplification of t: much faster\<close>
  1388 lemma let_weak_cong:
  1389   assumes "a = b"
  1390   shows "(let x = a in t x) = (let x = b in t x)"
  1391   using assms by (rule arg_cong)
  1392 
  1393 text \<open>To tidy up the result of a simproc.  Only the RHS will be simplified.\<close>
  1394 lemma eq_cong2:
  1395   assumes "u = u'"
  1396   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
  1397   using assms by simp
  1398 
  1399 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
  1400   by simp
  1401 
  1402 text \<open>As a simplification rule, it replaces all function equalities by
  1403   first-order equalities.\<close>
  1404 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
  1405   by auto
  1406 
  1407 
  1408 subsubsection \<open>Generic cases and induction\<close>
  1409 
  1410 text \<open>Rule projections:\<close>
  1411 ML \<open>
  1412 structure Project_Rule = Project_Rule
  1413 (
  1414   val conjunct1 = @{thm conjunct1}
  1415   val conjunct2 = @{thm conjunct2}
  1416   val mp = @{thm mp}
  1417 );
  1418 \<close>
  1419 
  1420 context
  1421 begin
  1422 
  1423 qualified definition "induct_forall P \<equiv> \<forall>x. P x"
  1424 qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
  1425 qualified definition "induct_equal x y \<equiv> x = y"
  1426 qualified definition "induct_conj A B \<equiv> A \<and> B"
  1427 qualified definition "induct_true \<equiv> True"
  1428 qualified definition "induct_false \<equiv> False"
  1429 
  1430 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
  1431   by (unfold atomize_all induct_forall_def)
  1432 
  1433 lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
  1434   by (unfold atomize_imp induct_implies_def)
  1435 
  1436 lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
  1437   by (unfold atomize_eq induct_equal_def)
  1438 
  1439 lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
  1440   by (unfold atomize_conj induct_conj_def)
  1441 
  1442 lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
  1443 lemmas induct_atomize = induct_atomize' induct_equal_eq
  1444 lemmas induct_rulify' [symmetric] = induct_atomize'
  1445 lemmas induct_rulify [symmetric] = induct_atomize
  1446 lemmas induct_rulify_fallback =
  1447   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
  1448   induct_true_def induct_false_def
  1449 
  1450 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
  1451     induct_conj (induct_forall A) (induct_forall B)"
  1452   by (unfold induct_forall_def induct_conj_def) iprover
  1453 
  1454 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
  1455     induct_conj (induct_implies C A) (induct_implies C B)"
  1456   by (unfold induct_implies_def induct_conj_def) iprover
  1457 
  1458 lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
  1459 proof
  1460   assume r: "induct_conj A B \<Longrightarrow> PROP C"
  1461   assume ab: A B
  1462   show "PROP C" by (rule r) (simp add: induct_conj_def ab)
  1463 next
  1464   assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
  1465   assume ab: "induct_conj A B"
  1466   show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
  1467 qed
  1468 
  1469 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
  1470 
  1471 lemma induct_trueI: "induct_true"
  1472   by (simp add: induct_true_def)
  1473 
  1474 text \<open>Method setup.\<close>
  1475 
  1476 ML_file "~~/src/Tools/induct.ML"
  1477 ML \<open>
  1478 structure Induct = Induct
  1479 (
  1480   val cases_default = @{thm case_split}
  1481   val atomize = @{thms induct_atomize}
  1482   val rulify = @{thms induct_rulify'}
  1483   val rulify_fallback = @{thms induct_rulify_fallback}
  1484   val equal_def = @{thm induct_equal_def}
  1485   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
  1486     | dest_def _ = NONE
  1487   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
  1488 )
  1489 \<close>
  1490 
  1491 ML_file "~~/src/Tools/induction.ML"
  1492 
  1493 declaration \<open>
  1494   fn _ => Induct.map_simpset (fn ss => ss
  1495     addsimprocs
  1496       [Simplifier.make_simproc @{context} "swap_induct_false"
  1497         {lhss = [@{term "induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"}],
  1498          proc = fn _ => fn _ => fn ct =>
  1499           (case Thm.term_of ct of
  1500             _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
  1501               if P <> Q then SOME Drule.swap_prems_eq else NONE
  1502           | _ => NONE)},
  1503        Simplifier.make_simproc @{context} "induct_equal_conj_curry"
  1504         {lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
  1505          proc = fn _ => fn _ => fn ct =>
  1506           (case Thm.term_of ct of
  1507             _ $ (_ $ P) $ _ =>
  1508               let
  1509                 fun is_conj (@{const induct_conj} $ P $ Q) =
  1510                       is_conj P andalso is_conj Q
  1511                   | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true
  1512                   | is_conj @{const induct_true} = true
  1513                   | is_conj @{const induct_false} = true
  1514                   | is_conj _ = false
  1515               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
  1516             | _ => NONE)}]
  1517     |> Simplifier.set_mksimps (fn ctxt =>
  1518         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
  1519         map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
  1520 \<close>
  1521 
  1522 text \<open>Pre-simplification of induction and cases rules\<close>
  1523 
  1524 lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
  1525   unfolding induct_equal_def
  1526 proof
  1527   assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
  1528   show "PROP P t" by (rule r [OF refl])
  1529 next
  1530   fix x
  1531   assume "PROP P t" "x = t"
  1532   then show "PROP P x" by simp
  1533 qed
  1534 
  1535 lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
  1536   unfolding induct_equal_def
  1537 proof
  1538   assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
  1539   show "PROP P t" by (rule r [OF refl])
  1540 next
  1541   fix x
  1542   assume "PROP P t" "t = x"
  1543   then show "PROP P x" by simp
  1544 qed
  1545 
  1546 lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
  1547   unfolding induct_false_def induct_true_def
  1548   by (iprover intro: equal_intr_rule)
  1549 
  1550 lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
  1551   unfolding induct_true_def
  1552 proof
  1553   assume "True \<Longrightarrow> PROP P"
  1554   then show "PROP P" using TrueI .
  1555 next
  1556   assume "PROP P"
  1557   then show "PROP P" .
  1558 qed
  1559 
  1560 lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
  1561   unfolding induct_true_def
  1562   by (iprover intro: equal_intr_rule)
  1563 
  1564 lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
  1565   unfolding induct_true_def
  1566   by (iprover intro: equal_intr_rule)
  1567 
  1568 lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
  1569   by (simp add: induct_implies_def induct_true_def)
  1570 
  1571 lemma [induct_simp]: "x = x \<longleftrightarrow> True"
  1572   by (rule simp_thms)
  1573 
  1574 end
  1575 
  1576 ML_file "~~/src/Tools/induct_tacs.ML"
  1577 
  1578 
  1579 subsubsection \<open>Coherent logic\<close>
  1580 
  1581 ML_file "~~/src/Tools/coherent.ML"
  1582 ML \<open>
  1583 structure Coherent = Coherent
  1584 (
  1585   val atomize_elimL = @{thm atomize_elimL};
  1586   val atomize_exL = @{thm atomize_exL};
  1587   val atomize_conjL = @{thm atomize_conjL};
  1588   val atomize_disjL = @{thm atomize_disjL};
  1589   val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
  1590 );
  1591 \<close>
  1592 
  1593 
  1594 subsubsection \<open>Reorienting equalities\<close>
  1595 
  1596 ML \<open>
  1597 signature REORIENT_PROC =
  1598 sig
  1599   val add : (term -> bool) -> theory -> theory
  1600   val proc : morphism -> Proof.context -> cterm -> thm option
  1601 end;
  1602 
  1603 structure Reorient_Proc : REORIENT_PROC =
  1604 struct
  1605   structure Data = Theory_Data
  1606   (
  1607     type T = ((term -> bool) * stamp) list;
  1608     val empty = [];
  1609     val extend = I;
  1610     fun merge data : T = Library.merge (eq_snd op =) data;
  1611   );
  1612   fun add m = Data.map (cons (m, stamp ()));
  1613   fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
  1614 
  1615   val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
  1616   fun proc phi ctxt ct =
  1617     let
  1618       val thy = Proof_Context.theory_of ctxt;
  1619     in
  1620       case Thm.term_of ct of
  1621         (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
  1622       | _ => NONE
  1623     end;
  1624 end;
  1625 \<close>
  1626 
  1627 
  1628 subsection \<open>Other simple lemmas and lemma duplicates\<close>
  1629 
  1630 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  1631     (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
  1632   by auto
  1633 
  1634 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
  1635     (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
  1636   by auto
  1637 
  1638 lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
  1639   by blast+
  1640 
  1641 lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))"
  1642   apply (rule iffI)
  1643    apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
  1644     apply (fast dest!: theI')
  1645    apply (fast intro: the1_equality [symmetric])
  1646   apply (erule ex1E)
  1647   apply (rule allI)
  1648   apply (rule ex1I)
  1649    apply (erule spec)
  1650   apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE)
  1651   apply (erule impE)
  1652    apply (rule allI)
  1653    apply (case_tac "xa = x")
  1654     apply (drule_tac [3] x = x in fun_cong)
  1655     apply simp_all
  1656   done
  1657 
  1658 lemmas eq_sym_conv = eq_commute
  1659 
  1660 lemma nnf_simps:
  1661   "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
  1662   "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
  1663   "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
  1664   "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
  1665   "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
  1666   "(\<not> \<not> P) = P"
  1667   by blast+
  1668 
  1669 
  1670 subsection \<open>Basic ML bindings\<close>
  1671 
  1672 ML \<open>
  1673 val FalseE = @{thm FalseE}
  1674 val Let_def = @{thm Let_def}
  1675 val TrueI = @{thm TrueI}
  1676 val allE = @{thm allE}
  1677 val allI = @{thm allI}
  1678 val all_dupE = @{thm all_dupE}
  1679 val arg_cong = @{thm arg_cong}
  1680 val box_equals = @{thm box_equals}
  1681 val ccontr = @{thm ccontr}
  1682 val classical = @{thm classical}
  1683 val conjE = @{thm conjE}
  1684 val conjI = @{thm conjI}
  1685 val conjunct1 = @{thm conjunct1}
  1686 val conjunct2 = @{thm conjunct2}
  1687 val disjCI = @{thm disjCI}
  1688 val disjE = @{thm disjE}
  1689 val disjI1 = @{thm disjI1}
  1690 val disjI2 = @{thm disjI2}
  1691 val eq_reflection = @{thm eq_reflection}
  1692 val ex1E = @{thm ex1E}
  1693 val ex1I = @{thm ex1I}
  1694 val ex1_implies_ex = @{thm ex1_implies_ex}
  1695 val exE = @{thm exE}
  1696 val exI = @{thm exI}
  1697 val excluded_middle = @{thm excluded_middle}
  1698 val ext = @{thm ext}
  1699 val fun_cong = @{thm fun_cong}
  1700 val iffD1 = @{thm iffD1}
  1701 val iffD2 = @{thm iffD2}
  1702 val iffI = @{thm iffI}
  1703 val impE = @{thm impE}
  1704 val impI = @{thm impI}
  1705 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
  1706 val mp = @{thm mp}
  1707 val notE = @{thm notE}
  1708 val notI = @{thm notI}
  1709 val not_all = @{thm not_all}
  1710 val not_ex = @{thm not_ex}
  1711 val not_iff = @{thm not_iff}
  1712 val not_not = @{thm not_not}
  1713 val not_sym = @{thm not_sym}
  1714 val refl = @{thm refl}
  1715 val rev_mp = @{thm rev_mp}
  1716 val spec = @{thm spec}
  1717 val ssubst = @{thm ssubst}
  1718 val subst = @{thm subst}
  1719 val sym = @{thm sym}
  1720 val trans = @{thm trans}
  1721 \<close>
  1722 
  1723 ML_file "Tools/cnf.ML"
  1724 
  1725 
  1726 section \<open>\<open>NO_MATCH\<close> simproc\<close>
  1727 
  1728 text \<open>
  1729   The simplification procedure can be used to avoid simplification of terms
  1730   of a certain form.
  1731 \<close>
  1732 
  1733 definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  1734   where "NO_MATCH pat val \<equiv> True"
  1735 
  1736 lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
  1737   by (rule refl)
  1738 
  1739 declare [[coercion_args NO_MATCH - -]]
  1740 
  1741 simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
  1742   let
  1743     val thy = Proof_Context.theory_of ctxt
  1744     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
  1745     val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
  1746   in if m then NONE else SOME @{thm NO_MATCH_def} end
  1747 \<close>
  1748 
  1749 text \<open>
  1750   This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
  1751   is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
  1752 \<close>
  1753 
  1754 
  1755 text\<open>
  1756   Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
  1757   not to simplify the argument and to solve it by an assumption.
  1758 \<close>
  1759 
  1760 definition ASSUMPTION :: "bool \<Rightarrow> bool"
  1761   where "ASSUMPTION A \<equiv> A"
  1762 
  1763 lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
  1764   by (rule refl)
  1765 
  1766 lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
  1767   by (simp add: ASSUMPTION_def)
  1768 
  1769 lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
  1770   by (simp add: ASSUMPTION_def)
  1771 
  1772 setup \<open>
  1773 let
  1774   val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
  1775     resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
  1776     resolve_tac ctxt (Simplifier.prems_of ctxt))
  1777 in
  1778   map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
  1779 end
  1780 \<close>
  1781 
  1782 
  1783 subsection \<open>Code generator setup\<close>
  1784 
  1785 subsubsection \<open>Generic code generator preprocessor setup\<close>
  1786 
  1787 lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
  1788   by (fact arg_cong)
  1789 
  1790 lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
  1791   by (fact arg_cong)
  1792 
  1793 setup \<open>
  1794   Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
  1795   Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
  1796   Code_Simp.map_ss (put_simpset HOL_basic_ss #>
  1797   Simplifier.add_cong @{thm conj_left_cong} #>
  1798   Simplifier.add_cong @{thm disj_left_cong})
  1799 \<close>
  1800 
  1801 
  1802 subsubsection \<open>Equality\<close>
  1803 
  1804 class equal =
  1805   fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  1806   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
  1807 begin
  1808 
  1809 lemma equal: "equal = (op =)"
  1810   by (rule ext equal_eq)+
  1811 
  1812 lemma equal_refl: "equal x x \<longleftrightarrow> True"
  1813   unfolding equal by rule+
  1814 
  1815 lemma eq_equal: "(op =) \<equiv> equal"
  1816   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
  1817 
  1818 end
  1819 
  1820 declare eq_equal [symmetric, code_post]
  1821 declare eq_equal [code]
  1822 
  1823 setup \<open>
  1824   Code_Preproc.map_pre (fn ctxt =>
  1825     ctxt addsimprocs
  1826       [Simplifier.make_simproc @{context} "equal"
  1827         {lhss = [@{term HOL.eq}],
  1828          proc = fn _ => fn _ => fn ct =>
  1829           (case Thm.term_of ct of
  1830             Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
  1831           | _ => NONE)}])
  1832 \<close>
  1833 
  1834 
  1835 subsubsection \<open>Generic code generator foundation\<close>
  1836 
  1837 text \<open>Datatype @{typ bool}\<close>
  1838 
  1839 code_datatype True False
  1840 
  1841 lemma [code]:
  1842   shows "False \<and> P \<longleftrightarrow> False"
  1843     and "True \<and> P \<longleftrightarrow> P"
  1844     and "P \<and> False \<longleftrightarrow> False"
  1845     and "P \<and> True \<longleftrightarrow> P"
  1846   by simp_all
  1847 
  1848 lemma [code]:
  1849   shows "False \<or> P \<longleftrightarrow> P"
  1850     and "True \<or> P \<longleftrightarrow> True"
  1851     and "P \<or> False \<longleftrightarrow> P"
  1852     and "P \<or> True \<longleftrightarrow> True"
  1853   by simp_all
  1854 
  1855 lemma [code]:
  1856   shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
  1857     and "(True \<longrightarrow> P) \<longleftrightarrow> P"
  1858     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
  1859     and "(P \<longrightarrow> True) \<longleftrightarrow> True"
  1860   by simp_all
  1861 
  1862 text \<open>More about @{typ prop}\<close>
  1863 
  1864 lemma [code nbe]:
  1865   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
  1866     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
  1867     and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
  1868   by (auto intro!: equal_intr_rule)
  1869 
  1870 lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
  1871   by (auto intro!: equal_intr_rule holds)
  1872 
  1873 declare Trueprop_code [symmetric, code_post]
  1874 
  1875 text \<open>Equality\<close>
  1876 
  1877 declare simp_thms(6) [code nbe]
  1878 
  1879 instantiation itself :: (type) equal
  1880 begin
  1881 
  1882 definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
  1883   where "equal_itself x y \<longleftrightarrow> x = y"
  1884 
  1885 instance
  1886   by standard (fact equal_itself_def)
  1887 
  1888 end
  1889 
  1890 lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
  1891   by (simp add: equal)
  1892 
  1893 setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
  1894 
  1895 lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
  1896   (is "?ofclass \<equiv> ?equal")
  1897 proof
  1898   assume "PROP ?ofclass"
  1899   show "PROP ?equal"
  1900     by (tactic \<open>ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}])\<close>)
  1901       (fact \<open>PROP ?ofclass\<close>)
  1902 next
  1903   assume "PROP ?equal"
  1904   show "PROP ?ofclass" proof
  1905   qed (simp add: \<open>PROP ?equal\<close>)
  1906 qed
  1907 
  1908 setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::equal \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
  1909 
  1910 setup \<open>Nbe.add_const_alias @{thm equal_alias_cert}\<close>
  1911 
  1912 text \<open>Cases\<close>
  1913 
  1914 lemma Let_case_cert:
  1915   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
  1916   shows "CASE x \<equiv> f x"
  1917   using assms by simp_all
  1918 
  1919 setup \<open>
  1920   Code.declare_case_global @{thm Let_case_cert} #>
  1921   Code.declare_undefined_global @{const_name undefined}
  1922 \<close>
  1923 
  1924 declare [[code abort: undefined]]
  1925 
  1926 
  1927 subsubsection \<open>Generic code generator target languages\<close>
  1928 
  1929 text \<open>type @{typ bool}\<close>
  1930 
  1931 code_printing
  1932   type_constructor bool \<rightharpoonup>
  1933     (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
  1934 | constant True \<rightharpoonup>
  1935     (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
  1936 | constant False \<rightharpoonup>
  1937     (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
  1938 
  1939 code_reserved SML
  1940   bool true false
  1941 
  1942 code_reserved OCaml
  1943   bool
  1944 
  1945 code_reserved Scala
  1946   Boolean
  1947 
  1948 code_printing
  1949   constant Not \<rightharpoonup>
  1950     (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
  1951 | constant HOL.conj \<rightharpoonup>
  1952     (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
  1953 | constant HOL.disj \<rightharpoonup>
  1954     (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
  1955 | constant HOL.implies \<rightharpoonup>
  1956     (SML) "!(if (_)/ then (_)/ else true)"
  1957     and (OCaml) "!(if (_)/ then (_)/ else true)"
  1958     and (Haskell) "!(if (_)/ then (_)/ else True)"
  1959     and (Scala) "!(if ((_))/ (_)/ else true)"
  1960 | constant If \<rightharpoonup>
  1961     (SML) "!(if (_)/ then (_)/ else (_))"
  1962     and (OCaml) "!(if (_)/ then (_)/ else (_))"
  1963     and (Haskell) "!(if (_)/ then (_)/ else (_))"
  1964     and (Scala) "!(if ((_))/ (_)/ else (_))"
  1965 
  1966 code_reserved SML
  1967   not
  1968 
  1969 code_reserved OCaml
  1970   not
  1971 
  1972 code_identifier
  1973   code_module Pure \<rightharpoonup>
  1974     (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
  1975 
  1976 text \<open>Using built-in Haskell equality.\<close>
  1977 code_printing
  1978   type_class equal \<rightharpoonup> (Haskell) "Eq"
  1979 | constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
  1980 | constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
  1981 
  1982 text \<open>\<open>undefined\<close>\<close>
  1983 code_printing
  1984   constant undefined \<rightharpoonup>
  1985     (SML) "!(raise/ Fail/ \"undefined\")"
  1986     and (OCaml) "failwith/ \"undefined\""
  1987     and (Haskell) "error/ \"undefined\""
  1988     and (Scala) "!sys.error(\"undefined\")"
  1989 
  1990 
  1991 subsubsection \<open>Evaluation and normalization by evaluation\<close>
  1992 
  1993 method_setup eval = \<open>
  1994   let
  1995     fun eval_tac ctxt =
  1996       let val conv = Code_Runtime.dynamic_holds_conv ctxt
  1997       in
  1998         CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
  1999         resolve_tac ctxt [TrueI]
  2000       end
  2001   in
  2002     Scan.succeed (SIMPLE_METHOD' o eval_tac)
  2003   end
  2004 \<close> "solve goal by evaluation"
  2005 
  2006 method_setup normalization = \<open>
  2007   Scan.succeed (fn ctxt =>
  2008     SIMPLE_METHOD'
  2009       (CHANGED_PROP o
  2010         (CONVERSION (Nbe.dynamic_conv ctxt)
  2011           THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
  2012 \<close> "solve goal by normalization"
  2013 
  2014 
  2015 subsection \<open>Counterexample Search Units\<close>
  2016 
  2017 subsubsection \<open>Quickcheck\<close>
  2018 
  2019 quickcheck_params [size = 5, iterations = 50]
  2020 
  2021 
  2022 subsubsection \<open>Nitpick setup\<close>
  2023 
  2024 named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
  2025   and nitpick_simp "equational specification of constants as needed by Nitpick"
  2026   and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
  2027   and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
  2028 
  2029 declare if_bool_eq_conj [nitpick_unfold, no_atp]
  2030   and if_bool_eq_disj [no_atp]
  2031 
  2032 
  2033 subsection \<open>Preprocessing for the predicate compiler\<close>
  2034 
  2035 named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
  2036   and code_pred_inline "inlining definitions for the Predicate Compiler"
  2037   and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
  2038 
  2039 
  2040 subsection \<open>Legacy tactics and ML bindings\<close>
  2041 
  2042 ML \<open>
  2043   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
  2044   local
  2045     fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
  2046       | wrong_prem (Bound _) = true
  2047       | wrong_prem _ = false;
  2048     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
  2049     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
  2050   in
  2051     fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
  2052   end;
  2053 
  2054   local
  2055     val nnf_ss =
  2056       simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
  2057   in
  2058     fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
  2059   end
  2060 \<close>
  2061 
  2062 hide_const (open) eq equal
  2063 
  2064 end