src/HOL/HOL.thy
changeset 20944 34b2c1bb7178
parent 20833 4fcf8ddb54f5
child 20973 0b8e436ed071
equal deleted inserted replaced
20943:cf19faf11bbd 20944:34b2c1bb7178
   147   the_eq_trivial: "(THE x. x = a) = (a::'a)"
   147   the_eq_trivial: "(THE x. x = a) = (a::'a)"
   148 
   148 
   149   impI:           "(P ==> Q) ==> P-->Q"
   149   impI:           "(P ==> Q) ==> P-->Q"
   150   mp:             "[| P-->Q;  P |] ==> Q"
   150   mp:             "[| P-->Q;  P |] ==> Q"
   151 
   151 
   152 
       
   153 text{*Thanks to Stephan Merz*}
       
   154 theorem subst:
       
   155   assumes eq: "s = t" and p: "P(s)"
       
   156   shows "P(t::'a)"
       
   157 proof -
       
   158   from eq have meta: "s \<equiv> t"
       
   159     by (rule eq_reflection)
       
   160   from p show ?thesis
       
   161     by (unfold meta)
       
   162 qed
       
   163 
   152 
   164 defs
   153 defs
   165   True_def:     "True      == ((%x::bool. x) = (%x. x))"
   154   True_def:     "True      == ((%x::bool. x) = (%x. x))"
   166   All_def:      "All(P)    == (P = (%x. True))"
   155   All_def:      "All(P)    == (P = (%x. True))"
   167   Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
   156   Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
   234   abs  ("\<bar>_\<bar>")
   223   abs  ("\<bar>_\<bar>")
   235 const_syntax (HTML output)
   224 const_syntax (HTML output)
   236   abs  ("\<bar>_\<bar>")
   225   abs  ("\<bar>_\<bar>")
   237 
   226 
   238 
   227 
   239 subsection {*Equality*}
   228 subsection {* Fundamental rules *}
       
   229 
       
   230 subsubsection {*Equality*}
       
   231 
       
   232 text {* Thanks to Stephan Merz *}
       
   233 lemma subst:
       
   234   assumes eq: "s = t" and p: "P s"
       
   235   shows "P t"
       
   236 proof -
       
   237   from eq have meta: "s \<equiv> t"
       
   238     by (rule eq_reflection)
       
   239   from p show ?thesis
       
   240     by (unfold meta)
       
   241 qed
   240 
   242 
   241 lemma sym: "s = t ==> t = s"
   243 lemma sym: "s = t ==> t = s"
   242   by (erule subst) (rule refl)
   244   by (erule subst) (rule refl)
   243 
   245 
   244 lemma ssubst: "t = s ==> P s ==> P t"
   246 lemma ssubst: "t = s ==> P s ==> P t"
   245   by (drule sym) (erule subst)
   247   by (drule sym) (erule subst)
   246 
   248 
   247 lemma trans: "[| r=s; s=t |] ==> r=t"
   249 lemma trans: "[| r=s; s=t |] ==> r=t"
   248   by (erule subst)
   250   by (erule subst)
   249 
   251 
   250 lemma def_imp_eq: assumes meq: "A == B" shows "A = B"
   252 lemma def_imp_eq:
       
   253   assumes meq: "A == B"
       
   254   shows "A = B"
   251   by (unfold meq) (rule refl)
   255   by (unfold meq) (rule refl)
   252 
   256 
   253 
   257 (*a mere copy*)
   254 (*Useful with eresolve_tac for proving equalties from known equalities.
   258 lemma meta_eq_to_obj_eq: 
   255         a = b
   259   assumes meq: "A == B"
       
   260   shows "A = B"
       
   261   by (unfold meq) (rule refl)
       
   262 
       
   263 text {* Useful with eresolve\_tac for proving equalties from known equalities. *}
       
   264      (* a = b
   256         |   |
   265         |   |
   257         c = d   *)
   266         c = d   *)
   258 lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
   267 lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
   259 apply (rule trans)
   268 apply (rule trans)
   260 apply (rule trans)
   269 apply (rule trans)
   269 
   278 
   270 lemma back_subst: "P a ==> a = b ==> P b"
   279 lemma back_subst: "P a ==> a = b ==> P b"
   271   by (rule subst)
   280   by (rule subst)
   272 
   281 
   273 
   282 
   274 subsection {*Congruence rules for application*}
   283 subsubsection {*Congruence rules for application*}
   275 
   284 
   276 (*similar to AP_THM in Gordon's HOL*)
   285 (*similar to AP_THM in Gordon's HOL*)
   277 lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
   286 lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
   278 apply (erule subst)
   287 apply (erule subst)
   279 apply (rule refl)
   288 apply (rule refl)
   288 lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d"
   297 lemma arg_cong2: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d"
   289 apply (erule ssubst)+
   298 apply (erule ssubst)+
   290 apply (rule refl)
   299 apply (rule refl)
   291 done
   300 done
   292 
   301 
   293 
       
   294 lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
   302 lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
   295 apply (erule subst)+
   303 apply (erule subst)+
   296 apply (rule refl)
   304 apply (rule refl)
   297 done
   305 done
   298 
   306 
   299 
   307 
   300 subsection {*Equality of booleans -- iff*}
   308 subsubsection {*Equality of booleans -- iff*}
   301 
   309 
   302 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
   310 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
   303   by (iprover intro: iff [THEN mp, THEN mp] impI prems)
   311   by (iprover intro: iff [THEN mp, THEN mp] impI prems)
   304 
   312 
   305 lemma iffD2: "[| P=Q; Q |] ==> P"
   313 lemma iffD2: "[| P=Q; Q |] ==> P"
   316       and minor: "[| P --> Q; Q --> P |] ==> R"
   324       and minor: "[| P --> Q; Q --> P |] ==> R"
   317   shows R
   325   shows R
   318   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
   326   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
   319 
   327 
   320 
   328 
   321 subsection {*True*}
   329 subsubsection {*True*}
   322 
   330 
   323 lemma TrueI: "True"
   331 lemma TrueI: "True"
   324   by (unfold True_def) (rule refl)
   332   by (unfold True_def) (rule refl)
   325 
   333 
   326 lemma eqTrueI: "P ==> P=True"
   334 lemma eqTrueI: "P ==> P=True"
   330 apply (erule iffD2)
   338 apply (erule iffD2)
   331 apply (rule TrueI)
   339 apply (rule TrueI)
   332 done
   340 done
   333 
   341 
   334 
   342 
   335 subsection {*Universal quantifier*}
   343 subsubsection {*Universal quantifier*}
   336 
   344 
   337 lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
   345 lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
   338 apply (unfold All_def)
   346 apply (unfold All_def)
   339 apply (iprover intro: ext eqTrueI p)
   347 apply (iprover intro: ext eqTrueI p)
   340 done
   348 done
   356       and minor: "[| P(x); ALL x. P(x) |] ==> R"
   364       and minor: "[| P(x); ALL x. P(x) |] ==> R"
   357   shows "R"
   365   shows "R"
   358 by (iprover intro: minor major major [THEN spec])
   366 by (iprover intro: minor major major [THEN spec])
   359 
   367 
   360 
   368 
   361 subsection {*False*}
   369 subsubsection {*False*}
   362 (*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
   370 (*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
   363 
   371 
   364 lemma FalseE: "False ==> P"
   372 lemma FalseE: "False ==> P"
   365 apply (unfold False_def)
   373 apply (unfold False_def)
   366 apply (erule spec)
   374 apply (erule spec)
   368 
   376 
   369 lemma False_neq_True: "False=True ==> P"
   377 lemma False_neq_True: "False=True ==> P"
   370 by (erule eqTrueE [THEN FalseE])
   378 by (erule eqTrueE [THEN FalseE])
   371 
   379 
   372 
   380 
   373 subsection {*Negation*}
   381 subsubsection {*Negation*}
   374 
   382 
   375 lemma notI:
   383 lemma notI:
   376   assumes p: "P ==> False"
   384   assumes p: "P ==> False"
   377   shows "~P"
   385   shows "~P"
   378 apply (unfold not_def)
   386 apply (unfold not_def)
   398 
   406 
   399 (* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
   407 (* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
   400 lemmas notI2 = notE [THEN notI, standard]
   408 lemmas notI2 = notE [THEN notI, standard]
   401 
   409 
   402 
   410 
   403 subsection {*Implication*}
   411 subsubsection {*Implication*}
   404 
   412 
   405 lemma impE:
   413 lemma impE:
   406   assumes "P-->Q" "P" "Q ==> R"
   414   assumes "P-->Q" "P" "Q ==> R"
   407   shows "R"
   415   shows "R"
   408 by (iprover intro: prems mp)
   416 by (iprover intro: prems mp)
   436   shows "~P"
   444   shows "~P"
   437 apply (rule nq [THEN contrapos_nn])
   445 apply (rule nq [THEN contrapos_nn])
   438 apply (erule pq)
   446 apply (erule pq)
   439 done
   447 done
   440 
   448 
   441 subsection {*Existential quantifier*}
   449 subsubsection {*Existential quantifier*}
   442 
   450 
   443 lemma exI: "P x ==> EX x::'a. P x"
   451 lemma exI: "P x ==> EX x::'a. P x"
   444 apply (unfold Ex_def)
   452 apply (unfold Ex_def)
   445 apply (iprover intro: allI allE impI mp)
   453 apply (iprover intro: allI allE impI mp)
   446 done
   454 done
   452 apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
   460 apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
   453 apply (iprover intro: impI [THEN allI] minor)
   461 apply (iprover intro: impI [THEN allI] minor)
   454 done
   462 done
   455 
   463 
   456 
   464 
   457 subsection {*Conjunction*}
   465 subsubsection {*Conjunction*}
   458 
   466 
   459 lemma conjI: "[| P; Q |] ==> P&Q"
   467 lemma conjI: "[| P; Q |] ==> P&Q"
   460 apply (unfold and_def)
   468 apply (unfold and_def)
   461 apply (iprover intro: impI [THEN allI] mp)
   469 apply (iprover intro: impI [THEN allI] mp)
   462 done
   470 done
   483 lemma context_conjI:
   491 lemma context_conjI:
   484   assumes prems: "P" "P ==> Q" shows "P & Q"
   492   assumes prems: "P" "P ==> Q" shows "P & Q"
   485 by (iprover intro: conjI prems)
   493 by (iprover intro: conjI prems)
   486 
   494 
   487 
   495 
   488 subsection {*Disjunction*}
   496 subsubsection {*Disjunction*}
   489 
   497 
   490 lemma disjI1: "P ==> P|Q"
   498 lemma disjI1: "P ==> P|Q"
   491 apply (unfold or_def)
   499 apply (unfold or_def)
   492 apply (iprover intro: allI impI mp)
   500 apply (iprover intro: allI impI mp)
   493 done
   501 done
   504   shows "R"
   512   shows "R"
   505 by (iprover intro: minorP minorQ impI
   513 by (iprover intro: minorP minorQ impI
   506                  major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   514                  major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   507 
   515 
   508 
   516 
   509 subsection {*Classical logic*}
   517 subsubsection {*Classical logic*}
   510 
       
   511 
   518 
   512 lemma classical:
   519 lemma classical:
   513   assumes prem: "~P ==> P"
   520   assumes prem: "~P ==> P"
   514   shows "P"
   521   shows "P"
   515 apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   522 apply (rule True_or_False [THEN disjE, THEN eqTrueE])
   543       and p2: "~P ==> ~Q"
   550       and p2: "~P ==> ~Q"
   544   shows "P"
   551   shows "P"
   545 by (iprover intro: classical p1 p2 notE)
   552 by (iprover intro: classical p1 p2 notE)
   546 
   553 
   547 
   554 
   548 subsection {*Unique existence*}
   555 subsubsection {*Unique existence*}
   549 
   556 
   550 lemma ex1I:
   557 lemma ex1I:
   551   assumes prems: "P a" "!!x. P(x) ==> x=a"
   558   assumes prems: "P a" "!!x. P(x) ==> x=a"
   552   shows "EX! x. P(x)"
   559   shows "EX! x. P(x)"
   553 by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)
   560 by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)
   573 apply (rule exI)
   580 apply (rule exI)
   574 apply assumption
   581 apply assumption
   575 done
   582 done
   576 
   583 
   577 
   584 
   578 subsection {*THE: definite description operator*}
   585 subsubsection {*THE: definite description operator*}
   579 
   586 
   580 lemma the_equality:
   587 lemma the_equality:
   581   assumes prema: "P a"
   588   assumes prema: "P a"
   582       and premx: "!!x. P x ==> x=a"
   589       and premx: "!!x. P x ==> x=a"
   583   shows "(THE x. P x) = a"
   590   shows "(THE x. P x) = a"
   626 apply (rule refl)
   633 apply (rule refl)
   627 apply (erule sym)
   634 apply (erule sym)
   628 done
   635 done
   629 
   636 
   630 
   637 
   631 subsection {*Classical intro rules for disjunction and existential quantifiers*}
   638 subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
   632 
   639 
   633 lemma disjCI:
   640 lemma disjCI:
   634   assumes "~Q ==> P" shows "P|Q"
   641   assumes "~Q ==> P" shows "P|Q"
   635 apply (rule classical)
   642 apply (rule classical)
   636 apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
   643 apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
   637 done
   644 done
   638 
   645 
   639 lemma excluded_middle: "~P | P"
   646 lemma excluded_middle: "~P | P"
   640 by (iprover intro: disjCI)
   647 by (iprover intro: disjCI)
   641 
   648 
   642 text{*case distinction as a natural deduction rule. Note that @{term "~P"}
   649 text {*
   643    is the second case, not the first.*}
   650   case distinction as a natural deduction rule.
       
   651   Note that @{term "~P"} is the second case, not the first
       
   652 *}
   644 lemma case_split_thm:
   653 lemma case_split_thm:
   645   assumes prem1: "P ==> Q"
   654   assumes prem1: "P ==> Q"
   646       and prem2: "~P ==> Q"
   655       and prem2: "~P ==> Q"
   647   shows "Q"
   656   shows "Q"
   648 apply (rule excluded_middle [THEN disjE])
   657 apply (rule excluded_middle [THEN disjE])
   649 apply (erule prem2)
   658 apply (erule prem2)
   650 apply (erule prem1)
   659 apply (erule prem1)
   651 done
   660 done
       
   661 lemmas case_split = case_split_thm [case_names True False]
   652 
   662 
   653 (*Classical implies (-->) elimination. *)
   663 (*Classical implies (-->) elimination. *)
   654 lemma impCE:
   664 lemma impCE:
   655   assumes major: "P-->Q"
   665   assumes major: "P-->Q"
   656       and minor: "~P ==> R" "Q ==> R"
   666       and minor: "~P ==> R" "Q ==> R"
   683   assumes "ALL x. ~P(x) ==> P(a)"
   693   assumes "ALL x. ~P(x) ==> P(a)"
   684   shows "EX x. P(x)"
   694   shows "EX x. P(x)"
   685 apply (rule ccontr)
   695 apply (rule ccontr)
   686 apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"])
   696 apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"])
   687 done
   697 done
   688 
       
   689 
       
   690 
       
   691 subsection {* Theory and package setup *}
       
   692 
       
   693 ML
       
   694 {*
       
   695 val eq_reflection = thm "eq_reflection"
       
   696 val refl = thm "refl"
       
   697 val subst = thm "subst"
       
   698 val ext = thm "ext"
       
   699 val impI = thm "impI"
       
   700 val mp = thm "mp"
       
   701 val True_def = thm "True_def"
       
   702 val All_def = thm "All_def"
       
   703 val Ex_def = thm "Ex_def"
       
   704 val False_def = thm "False_def"
       
   705 val not_def = thm "not_def"
       
   706 val and_def = thm "and_def"
       
   707 val or_def = thm "or_def"
       
   708 val Ex1_def = thm "Ex1_def"
       
   709 val iff = thm "iff"
       
   710 val True_or_False = thm "True_or_False"
       
   711 val Let_def = thm "Let_def"
       
   712 val if_def = thm "if_def"
       
   713 val sym = thm "sym"
       
   714 val ssubst = thm "ssubst"
       
   715 val trans = thm "trans"
       
   716 val def_imp_eq = thm "def_imp_eq"
       
   717 val box_equals = thm "box_equals"
       
   718 val fun_cong = thm "fun_cong"
       
   719 val arg_cong = thm "arg_cong"
       
   720 val cong = thm "cong"
       
   721 val iffI = thm "iffI"
       
   722 val iffD2 = thm "iffD2"
       
   723 val rev_iffD2 = thm "rev_iffD2"
       
   724 val iffD1 = thm "iffD1"
       
   725 val rev_iffD1 = thm "rev_iffD1"
       
   726 val iffE = thm "iffE"
       
   727 val TrueI = thm "TrueI"
       
   728 val eqTrueI = thm "eqTrueI"
       
   729 val eqTrueE = thm "eqTrueE"
       
   730 val allI = thm "allI"
       
   731 val spec = thm "spec"
       
   732 val allE = thm "allE"
       
   733 val all_dupE = thm "all_dupE"
       
   734 val FalseE = thm "FalseE"
       
   735 val False_neq_True = thm "False_neq_True"
       
   736 val notI = thm "notI"
       
   737 val False_not_True = thm "False_not_True"
       
   738 val True_not_False = thm "True_not_False"
       
   739 val notE = thm "notE"
       
   740 val notI2 = thm "notI2"
       
   741 val impE = thm "impE"
       
   742 val rev_mp = thm "rev_mp"
       
   743 val contrapos_nn = thm "contrapos_nn"
       
   744 val contrapos_pn = thm "contrapos_pn"
       
   745 val not_sym = thm "not_sym"
       
   746 val rev_contrapos = thm "rev_contrapos"
       
   747 val exI = thm "exI"
       
   748 val exE = thm "exE"
       
   749 val conjI = thm "conjI"
       
   750 val conjunct1 = thm "conjunct1"
       
   751 val conjunct2 = thm "conjunct2"
       
   752 val conjE = thm "conjE"
       
   753 val context_conjI = thm "context_conjI"
       
   754 val disjI1 = thm "disjI1"
       
   755 val disjI2 = thm "disjI2"
       
   756 val disjE = thm "disjE"
       
   757 val classical = thm "classical"
       
   758 val ccontr = thm "ccontr"
       
   759 val rev_notE = thm "rev_notE"
       
   760 val notnotD = thm "notnotD"
       
   761 val contrapos_pp = thm "contrapos_pp"
       
   762 val ex1I = thm "ex1I"
       
   763 val ex_ex1I = thm "ex_ex1I"
       
   764 val ex1E = thm "ex1E"
       
   765 val ex1_implies_ex = thm "ex1_implies_ex"
       
   766 val the_equality = thm "the_equality"
       
   767 val theI = thm "theI"
       
   768 val theI' = thm "theI'"
       
   769 val theI2 = thm "theI2"
       
   770 val the1_equality = thm "the1_equality"
       
   771 val the_sym_eq_trivial = thm "the_sym_eq_trivial"
       
   772 val disjCI = thm "disjCI"
       
   773 val excluded_middle = thm "excluded_middle"
       
   774 val case_split_thm = thm "case_split_thm"
       
   775 val impCE = thm "impCE"
       
   776 val impCE = thm "impCE"
       
   777 val iffCE = thm "iffCE"
       
   778 val exCI = thm "exCI"
       
   779 
       
   780 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
       
   781 local
       
   782   fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
       
   783   |   wrong_prem (Bound _) = true
       
   784   |   wrong_prem _ = false
       
   785   val filter_right = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
       
   786 in
       
   787   fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp])
       
   788   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
       
   789 end
       
   790 
       
   791 
       
   792 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i)
       
   793 
       
   794 (*Obsolete form of disjunctive case analysis*)
       
   795 fun excluded_middle_tac sP =
       
   796     res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
       
   797 
       
   798 fun case_tac a = res_inst_tac [("P",a)] case_split_thm
       
   799 *}
       
   800 
       
   801 theorems case_split = case_split_thm [case_names True False]
       
   802 
       
   803 ML {*
       
   804 structure ProjectRule = ProjectRuleFun
       
   805 (struct
       
   806   val conjunct1 = thm "conjunct1";
       
   807   val conjunct2 = thm "conjunct2";
       
   808   val mp = thm "mp";
       
   809 end)
       
   810 *}
       
   811 
   698 
   812 
   699 
   813 subsubsection {* Intuitionistic Reasoning *}
   700 subsubsection {* Intuitionistic Reasoning *}
   814 
   701 
   815 lemma impE':
   702 lemma impE':
   910 
   797 
   911 lemmas [symmetric, rulify] = atomize_all atomize_imp
   798 lemmas [symmetric, rulify] = atomize_all atomize_imp
   912   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
   799   and [symmetric, defn] = atomize_all atomize_imp atomize_eq
   913 
   800 
   914 
   801 
       
   802 subsection {* Package setup *}
       
   803 
       
   804 subsubsection {* Fundamental ML bindings *}
       
   805 
       
   806 ML {*
       
   807 structure HOL =
       
   808 struct
       
   809   (*FIXME reduce this to a minimum*)
       
   810   val eq_reflection = thm "eq_reflection";
       
   811   val def_imp_eq = thm "def_imp_eq";
       
   812   val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
       
   813   val ccontr = thm "ccontr";
       
   814   val impI = thm "impI";
       
   815   val impCE = thm "impCE";
       
   816   val notI = thm "notI";
       
   817   val notE = thm "notE";
       
   818   val iffI = thm "iffI";
       
   819   val iffCE = thm "iffCE";
       
   820   val conjI = thm "conjI";
       
   821   val conjE = thm "conjE";
       
   822   val disjCI = thm "disjCI";
       
   823   val disjE = thm "disjE";
       
   824   val TrueI = thm "TrueI";
       
   825   val FalseE = thm "FalseE";
       
   826   val allI = thm "allI";
       
   827   val allE = thm "allE";
       
   828   val exI = thm "exI";
       
   829   val exE = thm "exE";
       
   830   val ex_ex1I = thm "ex_ex1I";
       
   831   val the_equality = thm "the_equality";
       
   832   val mp = thm "mp";
       
   833   val rev_mp = thm "rev_mp"
       
   834   val classical = thm "classical";
       
   835   val subst = thm "subst";
       
   836   val refl = thm "refl";
       
   837   val sym = thm "sym";
       
   838   val trans = thm "trans";
       
   839   val arg_cong = thm "arg_cong";
       
   840   val iffD1 = thm "iffD1";
       
   841   val iffD2 = thm "iffD2";
       
   842   val disjE = thm "disjE";
       
   843   val conjE = thm "conjE";
       
   844   val exE = thm "exE";
       
   845   val contrapos_nn = thm "contrapos_nn";
       
   846   val contrapos_pp = thm "contrapos_pp";
       
   847   val notnotD = thm "notnotD";
       
   848   val conjunct1 = thm "conjunct1";
       
   849   val conjunct2 = thm "conjunct2";
       
   850   val spec = thm "spec";
       
   851   val imp_cong = thm "imp_cong";
       
   852   val the_sym_eq_trivial = thm "the_sym_eq_trivial";
       
   853   val triv_forall_equality = thm "triv_forall_equality";
       
   854   val case_split = thm "case_split_thm";
       
   855 end
       
   856 *}
       
   857 
       
   858 
   915 subsubsection {* Classical Reasoner setup *}
   859 subsubsection {* Classical Reasoner setup *}
   916 
   860 
       
   861 lemma thin_refl:
       
   862   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
       
   863 
   917 use "cladata.ML"
   864 use "cladata.ML"
   918 setup hypsubst_setup
   865 ML {* val HOL_cs = HOL.cs *}
   919 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
   866 setup Hypsubst.hypsubst_setup
       
   867 setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *}
   920 setup Classical.setup
   868 setup Classical.setup
   921 setup ResAtpset.setup
   869 setup ResAtpset.setup
   922 setup clasetup
   870 setup {* fn thy => (Classical.change_claset_of thy (K HOL.cs); thy) *}
   923 
   871 
   924 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   872 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   925   apply (erule swap)
   873   apply (erule swap)
   926   apply (erule (1) meta_mp)
   874   apply (erule (1) meta_mp)
   927   done
   875   done
   930   and ex1I [intro]
   878   and ex1I [intro]
   931 
   879 
   932 lemmas [intro?] = ext
   880 lemmas [intro?] = ext
   933   and [elim?] = ex1_implies_ex
   881   and [elim?] = ex1_implies_ex
   934 
   882 
       
   883 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
       
   884 lemma alt_ex1E:
       
   885   assumes major: "\<exists>!x. P x"
       
   886       and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
       
   887   shows R
       
   888 apply (rule ex1E [OF major])
       
   889 apply (rule prem)
       
   890 apply (tactic "ares_tac [HOL.allI] 1")+
       
   891 apply (tactic "etac (Classical.dup_elim HOL.allE) 1")
       
   892 by iprover
       
   893 
   935 use "blastdata.ML"
   894 use "blastdata.ML"
   936 setup Blast.setup
   895 setup Blast.setup
   937 
   896 
   938 
   897 ML {*
   939 subsubsection {* Simplifier setup *}
   898 structure HOL =
   940 
   899 struct
   941 lemma meta_eq_to_obj_eq: "x == y ==> x = y"
   900 
   942 proof -
   901 open HOL;
   943   assume r: "x == y"
   902 
   944   show "x = y" by (unfold r) (rule refl)
   903 fun case_tac a = res_inst_tac [("P", a)] case_split;
   945 qed
   904 
       
   905 end;
       
   906 *}
       
   907 
       
   908 
       
   909 subsubsection {* Simplifier *}
   946 
   910 
   947 lemma eta_contract_eq: "(%s. f s) = f" ..
   911 lemma eta_contract_eq: "(%s. f s) = f" ..
   948 
   912 
   949 lemma simp_thms:
   913 lemma simp_thms:
   950   shows not_not: "(~ ~ P) = P"
   914   shows not_not: "(~ ~ P) = P"
   951   and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
   915   and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
   952   and
   916   and
   953     "(P ~= Q) = (P = (~Q))"
   917     "(P ~= Q) = (P = (~Q))"
   954     "(P | ~P) = True"    "(~P | P) = True"
   918     "(P | ~P) = True"    "(~P | P) = True"
   955     "(x = x) = True"
   919     "(x = x) = True"
   956     "(~True) = False"  "(~False) = True"
   920   and not_True_eq_False: "(\<not> True) = False"
       
   921   and not_False_eq_True: "(\<not> False) = True"
       
   922   and
   957     "(~P) ~= P"  "P ~= (~P)"
   923     "(~P) ~= P"  "P ~= (~P)"
   958     "(True=P) = P"  "(P=True) = P"  "(False=P) = (~P)"  "(P=False) = (~P)"
   924     "(True=P) = P"
       
   925   and eq_True: "(P = True) = P"
       
   926   and "(False=P) = (~P)"
       
   927   and eq_False: "(P = False) = (\<not> P)"
       
   928   and
   959     "(True --> P) = P"  "(False --> P) = True"
   929     "(True --> P) = P"  "(False --> P) = True"
   960     "(P --> True) = True"  "(P --> P) = True"
   930     "(P --> True) = True"  "(P --> P) = True"
   961     "(P --> False) = (~P)"  "(P --> ~P) = (~P)"
   931     "(P --> False) = (~P)"  "(P --> ~P) = (~P)"
   962     "(P & True) = P"  "(True & P) = P"
   932     "(P & True) = P"  "(True & P) = P"
   963     "(P & False) = False"  "(False & P) = False"
   933     "(P & False) = False"  "(False & P) = False"
  1088 
  1058 
  1089 lemma disj_cong:
  1059 lemma disj_cong:
  1090     "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
  1060     "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
  1091   by blast
  1061   by blast
  1092 
  1062 
  1093 lemma eq_sym_conv: "(x = y) = (y = x)"
       
  1094   by iprover
       
  1095 
       
  1096 
  1063 
  1097 text {* \medskip if-then-else rules *}
  1064 text {* \medskip if-then-else rules *}
  1098 
  1065 
  1099 lemma if_True: "(if True then x else y) = x"
  1066 lemma if_True: "(if True then x else y) = x"
  1100   by (unfold if_def) blast
  1067   by (unfold if_def) blast
  1116 
  1083 
  1117 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
  1084 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
  1118 by (simplesubst split_if, blast)
  1085 by (simplesubst split_if, blast)
  1119 
  1086 
  1120 lemmas if_splits = split_if split_if_asm
  1087 lemmas if_splits = split_if split_if_asm
  1121 
       
  1122 lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))"
       
  1123   by (rule split_if)
       
  1124 
  1088 
  1125 lemma if_cancel: "(if c then x else x) = x"
  1089 lemma if_cancel: "(if c then x else x) = x"
  1126 by (simplesubst split_if, blast)
  1090 by (simplesubst split_if, blast)
  1127 
  1091 
  1128 lemma if_eq_cancel: "(if x = y then y else x) = x"
  1092 lemma if_eq_cancel: "(if x = y then y else x) = x"
  1197 qed
  1161 qed
  1198 
  1162 
  1199 
  1163 
  1200 text {* \medskip Actual Installation of the Simplifier. *}
  1164 text {* \medskip Actual Installation of the Simplifier. *}
  1201 
  1165 
       
  1166 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
       
  1167 proof
       
  1168   assume prem: "True \<Longrightarrow> PROP P"
       
  1169   from prem [OF TrueI] show "PROP P" . 
       
  1170 next
       
  1171   assume "PROP P"
       
  1172   show "PROP P" .
       
  1173 qed
       
  1174 
       
  1175 lemma uncurry:
       
  1176   assumes "P \<longrightarrow> Q \<longrightarrow> R"
       
  1177   shows "P \<and> Q \<longrightarrow> R"
       
  1178   using prems by blast
       
  1179 
       
  1180 lemma iff_allI:
       
  1181   assumes "\<And>x. P x = Q x"
       
  1182   shows "(\<forall>x. P x) = (\<forall>x. Q x)"
       
  1183   using prems by blast
       
  1184 
       
  1185 lemma iff_exI:
       
  1186   assumes "\<And>x. P x = Q x"
       
  1187   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
       
  1188   using prems by blast
       
  1189 
       
  1190 lemma all_comm:
       
  1191   "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
       
  1192   by blast
       
  1193 
       
  1194 lemma ex_comm:
       
  1195   "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
       
  1196   by blast
       
  1197 
  1202 use "simpdata.ML"
  1198 use "simpdata.ML"
  1203 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
  1199 setup "Simplifier.method_setup Splitter.split_modifiers"
  1204 setup Splitter.setup setup Clasimp.setup
  1200 setup simpsetup
       
  1201 setup Splitter.setup
       
  1202 setup Clasimp.setup
  1205 setup EqSubst.setup
  1203 setup EqSubst.setup
       
  1204 
       
  1205 text {* Simplifies x assuming c and y assuming ~c *}
       
  1206 lemma if_cong:
       
  1207   assumes "b = c"
       
  1208       and "c \<Longrightarrow> x = u"
       
  1209       and "\<not> c \<Longrightarrow> y = v"
       
  1210   shows "(if b then x else y) = (if c then u else v)"
       
  1211   unfolding if_def using prems by simp
       
  1212 
       
  1213 text {* Prevents simplification of x and y:
       
  1214   faster and allows the execution of functional programs. *}
       
  1215 lemma if_weak_cong [cong]:
       
  1216   assumes "b = c"
       
  1217   shows "(if b then x else y) = (if c then x else y)"
       
  1218   using prems by (rule arg_cong)
       
  1219 
       
  1220 text {* Prevents simplification of t: much faster *}
       
  1221 lemma let_weak_cong:
       
  1222   assumes "a = b"
       
  1223   shows "(let x = a in t x) = (let x = b in t x)"
       
  1224   using prems by (rule arg_cong)
       
  1225 
       
  1226 text {* To tidy up the result of a simproc.  Only the RHS will be simplified. *}
       
  1227 lemma eq_cong2:
       
  1228   assumes "u = u'"
       
  1229   shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
       
  1230   using prems by simp
       
  1231 
       
  1232 lemma if_distrib:
       
  1233   "f (if c then x else y) = (if c then f x else f y)"
       
  1234   by simp
       
  1235 
       
  1236 text {* For expand\_case\_tac *}
       
  1237 lemma expand_case:
       
  1238   assumes "P \<Longrightarrow> Q True"
       
  1239       and "~P \<Longrightarrow> Q False"
       
  1240   shows "Q P"
       
  1241 proof (tactic {* HOL.case_tac "P" 1 *})
       
  1242   assume P
       
  1243   then show "Q P" by simp
       
  1244 next
       
  1245   assume "\<not> P"
       
  1246   then have "P = False" by simp
       
  1247   with prems show "Q P" by simp
       
  1248 qed
       
  1249 
       
  1250 text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
       
  1251   side of an equality.  Used in {Integ,Real}/simproc.ML *}
       
  1252 lemma restrict_to_left:
       
  1253   assumes "x = y"
       
  1254   shows "(x = z) = (y = z)"
       
  1255   using prems by simp
       
  1256 
       
  1257 
       
  1258 subsubsection {* Generic cases and induction *}
       
  1259 
       
  1260 text {* Rule projections: *}
       
  1261 
       
  1262 ML {*
       
  1263 structure ProjectRule = ProjectRuleFun
       
  1264 (struct
       
  1265   val conjunct1 = thm "conjunct1";
       
  1266   val conjunct2 = thm "conjunct2";
       
  1267   val mp = thm "mp";
       
  1268 end)
       
  1269 *}
       
  1270 
       
  1271 constdefs
       
  1272   induct_forall where "induct_forall P == \<forall>x. P x"
       
  1273   induct_implies where "induct_implies A B == A \<longrightarrow> B"
       
  1274   induct_equal where "induct_equal x y == x = y"
       
  1275   induct_conj where "induct_conj A B == A \<and> B"
       
  1276 
       
  1277 lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
       
  1278   by (unfold atomize_all induct_forall_def)
       
  1279 
       
  1280 lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
       
  1281   by (unfold atomize_imp induct_implies_def)
       
  1282 
       
  1283 lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
       
  1284   by (unfold atomize_eq induct_equal_def)
       
  1285 
       
  1286 lemma induct_conj_eq:
       
  1287   includes meta_conjunction_syntax
       
  1288   shows "(A && B) == Trueprop (induct_conj A B)"
       
  1289   by (unfold atomize_conj induct_conj_def)
       
  1290 
       
  1291 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
       
  1292 lemmas induct_rulify [symmetric, standard] = induct_atomize
       
  1293 lemmas induct_rulify_fallback =
       
  1294   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
       
  1295 
       
  1296 
       
  1297 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
       
  1298     induct_conj (induct_forall A) (induct_forall B)"
       
  1299   by (unfold induct_forall_def induct_conj_def) iprover
       
  1300 
       
  1301 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
       
  1302     induct_conj (induct_implies C A) (induct_implies C B)"
       
  1303   by (unfold induct_implies_def induct_conj_def) iprover
       
  1304 
       
  1305 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
       
  1306 proof
       
  1307   assume r: "induct_conj A B ==> PROP C" and A B
       
  1308   show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
       
  1309 next
       
  1310   assume r: "A ==> B ==> PROP C" and "induct_conj A B"
       
  1311   show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
       
  1312 qed
       
  1313 
       
  1314 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
       
  1315 
       
  1316 hide const induct_forall induct_implies induct_equal induct_conj
       
  1317 
       
  1318 text {* Method setup. *}
       
  1319 
       
  1320 ML {*
       
  1321   structure InductMethod = InductMethodFun
       
  1322   (struct
       
  1323     val cases_default = thm "case_split"
       
  1324     val atomize = thms "induct_atomize"
       
  1325     val rulify = thms "induct_rulify"
       
  1326     val rulify_fallback = thms "induct_rulify_fallback"
       
  1327   end);
       
  1328 *}
       
  1329 
       
  1330 setup InductMethod.setup
  1206 
  1331 
  1207 
  1332 
  1208 subsubsection {* Code generator setup *}
  1333 subsubsection {* Code generator setup *}
  1209 
  1334 
  1210 types_code
  1335 types_code
  1261 
  1386 
  1262 fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
  1387 fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
  1263   (Drule.goals_conv (equal i) Codegen.evaluation_conv));
  1388   (Drule.goals_conv (equal i) Codegen.evaluation_conv));
  1264 
  1389 
  1265 val evaluation_meth =
  1390 val evaluation_meth =
  1266   Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1));
  1391   Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
  1267 
  1392 
  1268 in
  1393 in
  1269 
  1394 
  1270 Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
  1395 Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
  1271 
  1396 
  1272 end;
  1397 end;
  1273 *}
  1398 *}
  1274 
  1399 
  1275 
  1400 
  1276 subsection {* Other simple lemmas *}
  1401 text {* itself as a code generator datatype *}
  1277 
  1402 
  1278 declare disj_absorb [simp] conj_absorb [simp]
  1403 setup {*
  1279 
  1404 let fun add_itself thy =
  1280 lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
  1405   let
  1281 by blast+
  1406     val v = ("'a", []);
  1282 
  1407     val t = Logic.mk_type (TFree v);
  1283 
  1408     val Const (c, ty) = t;
  1284 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
  1409     val (_, Type (dtco, _)) = strip_type ty;
       
  1410   in
       
  1411     thy
       
  1412     |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
       
  1413   end
       
  1414 in add_itself end;
       
  1415 *} 
       
  1416 
       
  1417 text {* code generation for arbitrary as exception *}
       
  1418 
       
  1419 setup {*
       
  1420   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
       
  1421 *}
       
  1422 
       
  1423 code_const arbitrary
       
  1424   (Haskell target_atom "(error \"arbitrary\")")
       
  1425 
       
  1426 
       
  1427 subsection {* Other simple lemmas and lemma duplicates *}
       
  1428 
       
  1429 lemmas eq_sym_conv = eq_commute
       
  1430 lemmas if_def2 = if_bool_eq_conj
       
  1431 
       
  1432 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
       
  1433   by blast+
       
  1434 
       
  1435 lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
  1285   apply (rule iffI)
  1436   apply (rule iffI)
  1286   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
  1437   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
  1287   apply (fast dest!: theI')
  1438   apply (fast dest!: theI')
  1288   apply (fast intro: ext the1_equality [symmetric])
  1439   apply (fast intro: ext the1_equality [symmetric])
  1289   apply (erule ex1E)
  1440   apply (erule ex1E)
  1295   apply (rule allI)
  1446   apply (rule allI)
  1296   apply (rule_tac P = "xa = x" in case_split_thm)
  1447   apply (rule_tac P = "xa = x" in case_split_thm)
  1297   apply (drule_tac [3] x = x in fun_cong, simp_all)
  1448   apply (drule_tac [3] x = x in fun_cong, simp_all)
  1298   done
  1449   done
  1299 
  1450 
  1300 text{*Needs only HOL-lemmas:*}
  1451 text {* Needs only HOL-lemmas *}
  1301 lemma mk_left_commute:
  1452 lemma mk_left_commute:
  1302   assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and
  1453   assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and
  1303           c: "\<And>x y. f x y = f y x"
  1454           c: "\<And>x y. f x y = f y x"
  1304   shows "f x (f y z) = f y (f x z)"
  1455   shows "f x (f y z) = f y (f x z)"
  1305 by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]])
  1456   by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
  1306 
  1457 
  1307 
  1458 
  1308 subsection {* Generic cases and induction *}
  1459 subsection {* Conclude HOL structure *}
  1309 
       
  1310 constdefs
       
  1311   induct_forall where "induct_forall P == \<forall>x. P x"
       
  1312   induct_implies where "induct_implies A B == A \<longrightarrow> B"
       
  1313   induct_equal where "induct_equal x y == x = y"
       
  1314   induct_conj where "induct_conj A B == A \<and> B"
       
  1315 
       
  1316 lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
       
  1317   by (unfold atomize_all induct_forall_def)
       
  1318 
       
  1319 lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
       
  1320   by (unfold atomize_imp induct_implies_def)
       
  1321 
       
  1322 lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
       
  1323   by (unfold atomize_eq induct_equal_def)
       
  1324 
       
  1325 lemma induct_conj_eq:
       
  1326   includes meta_conjunction_syntax
       
  1327   shows "(A && B) == Trueprop (induct_conj A B)"
       
  1328   by (unfold atomize_conj induct_conj_def)
       
  1329 
       
  1330 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
       
  1331 lemmas induct_rulify [symmetric, standard] = induct_atomize
       
  1332 lemmas induct_rulify_fallback =
       
  1333   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
       
  1334 
       
  1335 
       
  1336 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
       
  1337     induct_conj (induct_forall A) (induct_forall B)"
       
  1338   by (unfold induct_forall_def induct_conj_def) iprover
       
  1339 
       
  1340 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
       
  1341     induct_conj (induct_implies C A) (induct_implies C B)"
       
  1342   by (unfold induct_implies_def induct_conj_def) iprover
       
  1343 
       
  1344 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
       
  1345 proof
       
  1346   assume r: "induct_conj A B ==> PROP C" and A B
       
  1347   show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
       
  1348 next
       
  1349   assume r: "A ==> B ==> PROP C" and "induct_conj A B"
       
  1350   show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
       
  1351 qed
       
  1352 
       
  1353 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
       
  1354 
       
  1355 hide const induct_forall induct_implies induct_equal induct_conj
       
  1356 
       
  1357 text {* Method setup. *}
       
  1358 
  1460 
  1359 ML {*
  1461 ML {*
  1360   structure InductMethod = InductMethodFun
  1462 structure HOL =
  1361   (struct
  1463 struct
  1362     val cases_default = thm "case_split"
  1464 
  1363     val atomize = thms "induct_atomize"
  1465 open HOL;
  1364     val rulify = thms "induct_rulify"
  1466 
  1365     val rulify_fallback = thms "induct_rulify_fallback"
  1467 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
  1366   end);
  1468 local
       
  1469   fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
       
  1470     | wrong_prem (Bound _) = true
       
  1471     | wrong_prem _ = false;
       
  1472   val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
       
  1473 in
       
  1474   fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
       
  1475   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
       
  1476 end;
       
  1477 
       
  1478 fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
       
  1479 
       
  1480 end;
  1367 *}
  1481 *}
  1368 
  1482 
  1369 setup InductMethod.setup
       
  1370 
       
  1371 
       
  1372 text {* itself as a code generator datatype *}
       
  1373 
       
  1374 setup {*
       
  1375 let fun add_itself thy =
       
  1376   let
       
  1377     val v = ("'a", []);
       
  1378     val t = Logic.mk_type (TFree v);
       
  1379     val Const (c, ty) = t;
       
  1380     val (_, Type (dtco, _)) = strip_type ty;
       
  1381   in
       
  1382     thy
       
  1383     |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
       
  1384   end
       
  1385 in add_itself end;
       
  1386 *} 
       
  1387 
       
  1388 text {* code generation for arbitrary as exception *}
       
  1389 
       
  1390 setup {*
       
  1391   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
       
  1392 *}
       
  1393 code_const arbitrary
       
  1394   (Haskell target_atom "(error \"arbitrary\")")
       
  1395 
       
  1396 end
  1483 end