Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default



Oops! I realized that I forgot to attach the patches.

On Fri, Nov 21, 2014 at 5:09 PM, Josh Tilles <merelyapseudonym at gmail.com>
wrote:

> I've come across a few errors that are blocking my progress. I'm not sure
> what to do besides trying to become familiar with *all* of Isabelle's
> internals, so I'd appreciate any advice/direction—particularly on the two
> specific errors I present below.
>
> Thank you,
> --Josh Tilles
>
>
>
> These errors have arisen because I've returned to a task that I last
> attempted a year or so ago: adapting HOL to make it possible to selectively
> "opt-in" to classical logic. I've thought of a few approaches that would
> work as initial proof-of-concepts. My intuition is that any of the below
> *should* be possible, but one might be more tractable than the others.
>
>
> Extract HOL.True_or_False into a locale.
>
>    - seems like the ideal solution
>    - Ultimately, I think the locale *should* be named classical *but*
>    I've currently named it NonIntuitionistic because there's a lemma that's
>    also named classical and an ML structure named Classical. So if I
>    wanted the locale usage to stand out in these prototypes, I needed a
>    different name.
>    - The problem is that the elim rules break:
>       - on the line "declare NonIntuitionistic.iffCE [elim!]" we see the
>       message:
>       exception THM 1 raised (line 332 of "drule.ML"):
>
>       RSN: no unifiers
>       PROP NonIntuitionistic ⟹ ?P = ?Q ⟹ (?P ⟹ ?Q ⟹ ?R) ⟹ (¬ ?P ⟹ ¬ ?Q ⟹
>       ?R) ⟹ ?R
>       PROP NonIntuitionistic ⟹ (¬ ?P ⟹ ?P) ⟹ ?P
>
>
> Extract non-classical code into IHOL.thy, which the normal/classical
> HOL.thy subsequently imports.
>
>    - Took a lot of time the last time I tried it a year ago, so I don't
>    have a demonstration patch (yet)
>    - A major problem is that all future theories will need to be split
>    similarly
>       - For example, IOrderings.thy for all of the lemmas and theorems
>       that work in an intuitionistic context, and Orderings.thy as the
>       theory that contains everything in IOrderings.thy *plus* any
>       lemmas/theories that actually depend on classical logic.
>
>
> Replace the global HOL.True_or_False axiomatization with many local
> assumptions/dependencies on the individual lemmas and theorems.
>
>    - probably the least amount of broad structural change (effectively,
>    we're just adding one more assumption to any classical lemmas)
>    - but tedious to make lots of minor changes to make to the proofs of
>    the lemmas
>       - you can see examples of this in my attached patch
>       - I totally acknowledge that my updated proofs are super-hacky at
>       the moment.
>    - needed to move the declarations of a bunch of lemmas as elimination
>    rules *before* the Hypsubst and Classical structures, otherwise I get
>    an error:
>    - on the line "declare iffCE [elim!]" we see the message:
>       exception Option raised (line 81 of "General/basics.ML")
>       - but if those particular errors go away if I relocate the
>       declarations
>    - unfortunately, anything elim-related fails with the same error
>
>
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
index 6dfd9a3..46659b2 100644
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -168,8 +168,10 @@ axiomatization where
   impI: "(P ==> Q) ==> P-->Q" and
   mp: "[| P-->Q;  P |] ==> Q" and
 
-  iff: "(P-->Q) --> (Q-->P) --> (P=Q)" and
-  True_or_False: "(P=True) | (P=False)"
+  iff: "(P-->Q) --> (Q-->P) --> (P=Q)"
+
+locale NonIntuitionistic =
+  assumes True_or_False: "(P=True) | (P=False)"
 
 defs
   True_def:     "True      == ((%x::bool. x) = (%x. x))"
@@ -471,6 +473,8 @@ by (iprover intro: minorP minorQ impI
 
 subsubsection {*Classical logic*}
 
+context NonIntuitionistic begin
+
 lemma classical:
   assumes prem: "~P ==> P"
   shows "P"
@@ -505,7 +509,7 @@ lemma contrapos_pp:
       and p2: "~P ==> ~Q"
   shows "P"
 by (iprover intro: classical p1 p2 notE)
-
+end
 
 subsubsection {*Unique existence*}
 
@@ -595,7 +599,7 @@ done
 
 
 subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
-
+context NonIntuitionistic begin
 lemma disjCI:
   assumes "~Q ==> P" shows "P|Q"
 apply (rule classical)
@@ -653,7 +657,7 @@ lemma exCI:
 apply (rule ccontr)
 apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 done
-
+end
 
 subsubsection {* Intuitionistic Reasoning *}
 
@@ -803,10 +807,10 @@ setup {* No_ATPs.setup *}
 
 subsubsection {* Classical Reasoner setup *}
 
-lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+lemma (in NonIntuitionistic) imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
   by (rule classical) iprover
 
-lemma swap: "~ P ==> (~ R ==> P) ==> R"
+lemma (in NonIntuitionistic) swap: "~ P ==> (~ R ==> P) ==> R"
   by (rule classical) iprover
 
 lemma thin_refl:
@@ -830,10 +834,10 @@ open Hypsubst;
 
 structure Classical = Classical
 (
-  val imp_elim = @{thm imp_elim}
+  val imp_elim = @{thm NonIntuitionistic.imp_elim}
   val not_elim = @{thm notE}
-  val swap = @{thm swap}
-  val classical = @{thm classical}
+  val swap = @{thm NonIntuitionistic.swap}
+  val classical = @{thm NonIntuitionistic.classical}
   val sizef = Drule.size_of_thm
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 );
@@ -863,16 +867,18 @@ end
 declare iffI [intro!]
   and notI [intro!]
   and impI [intro!]
-  and disjCI [intro!]
+  and NonIntuitionistic.disjCI [intro!]
   and conjI [intro!]
   and TrueI [intro!]
   and refl [intro!]
 
-declare iffCE [elim!]
+declare NonIntuitionistic.iffCE [elim!]
+(*
   and FalseE [elim!]
   and impCE [elim!]
   and disjE [elim!]
   and conjE [elim!]
+*)
 
 declare ex_ex1I [intro!]
   and allI [intro!]
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
index 46659b2..ad58984 100644
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -875,30 +875,33 @@ declare iffI [intro!]
 declare NonIntuitionistic.iffCE [elim!]
 (*
   and FalseE [elim!]
-  and impCE [elim!]
+  and NonIntuitionistic.impCE [elim!]
   and disjE [elim!]
   and conjE [elim!]
 *)
 
 declare ex_ex1I [intro!]
   and allI [intro!]
+(*
   and the_equality [intro]
   and exI [intro]
 
 declare exE [elim!]
   allE [elim]
+*)
 
 ML {* val HOL_cs = claset_of @{context} *}
 
-lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
+lemma (in NonIntuitionistic) contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
   apply (erule swap)
   apply (erule (1) meta_mp)
   done
-
+(*
 declare ex_ex1I [rule del, intro! 2]
   and ex1I [intro]
 
 declare ext [intro]
+*)
 
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
@@ -914,6 +917,7 @@ apply (tactic {* ares_tac @{thms allI} 1 *})+
 apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
 apply iprover
 done
+oops
 
 ML {*
   structure Blast = Blast
@@ -923,7 +927,7 @@ ML {*
     val equality_name = @{const_name HOL.eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
-    val ccontr = @{thm ccontr}
+    val ccontr = @{thm NonIntuitionistic.ccontr}
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   );
   val blast_tac = Blast.blast_tac;
@@ -968,24 +972,25 @@ lemma simp_thms:
     "!!P. (EX x. t=x & P(x)) = P(t)"
     "!!P. (ALL x. x=t --> P(x)) = P(t)"
     "!!P. (ALL x. t=x --> P(x)) = P(t)"
-  by (blast, blast, blast, blast, blast, iprover+)
+(*  by (blast, blast, blast, blast, blast, iprover+) *)
+sorry
 
-lemma disj_absorb: "(A | A) = A"
+lemma disj_absorb: "(A | A) = A" (* 33 *)
   by blast
 
-lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
+lemma disj_left_absorb: "(A | (A | B)) = (A | B)" (* 34 *)
   by blast
 
-lemma conj_absorb: "(A & A) = A"
+lemma conj_absorb: "(A & A) = A" (* 25 *)
   by blast
 
-lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
+lemma conj_left_absorb: "(A & (A & B)) = (A & B)" (* 26 *)
   by blast
 
 lemma eq_ac:
   shows eq_commute: "a = b \<longleftrightarrow> b = a"
     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
-    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
+    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" (* by (iprover, blast+) *) sorry
 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
 
 lemma conj_comms:
@@ -1013,23 +1018,23 @@ lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
 lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
 
 text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
-lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
-lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
+lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" (* by blast *) sorry
+lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" (* by blast *) sorry
 
-lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
-lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
+lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" (* by blast *) sorry
+lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" (* by blast *) sorry
 
 lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
   by iprover
 
 lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
-lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
-lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
-lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
-lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
+lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" (* by blast *) sorry
+lemma not_imp: "(~(P --> Q)) = (P & ~Q)" (* by blast *) sorry
+lemma not_iff: "(P~=Q) = (P = (~Q))" (* by blast *) sorry
+lemma disj_not1: "(~P | Q) = (P --> Q)" (* by blast *) sorry
 lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
-  by blast
-lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
+   (* by blast *) sorry
+lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)"  (* by blast *) sorry
 
 lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 
@@ -1037,13 +1042,13 @@ lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
   -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
   -- {* cases boil down to the same thing. *}
-  by blast
+   (* by blast *) sorry
 
-lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
-lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
+lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" (* by blast *) sorry
+lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" (* by blast *) sorry
 lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
 lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
-lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
+lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" (* by blast *) sorry
 
 declare All_def [no_atp]
 
@@ -1066,31 +1071,31 @@ text {* The @{text "|"} congruence rule: not included by default! *}
 
 lemma disj_cong:
     "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
-  by blast
+ (* by blast *) sorry
 
 
 text {* \medskip if-then-else rules *}
 
 lemma if_True [code]: "(if True then x else y) = x"
-  by (unfold If_def) blast
+  by (unfold If_def) (* by blast *) sorry
 
 lemma if_False [code]: "(if False then x else y) = y"
-  by (unfold If_def) blast
+  by (unfold If_def) (* by blast *) sorry
 
 lemma if_P: "P ==> (if P then x else y) = x"
-  by (unfold If_def) blast
+  by (unfold If_def) (* by blast *) sorry
 
 lemma if_not_P: "~P ==> (if P then x else y) = y"
-  by (unfold If_def) blast
+  by (unfold If_def) (* by blast *) sorry
 
 lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
   apply (rule case_split [of Q])
    apply (simplesubst if_P)
     prefer 3 apply (simplesubst if_not_P, blast+)
-  done
+  (* done *) sorry
 
 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
-by (simplesubst split_if, blast)
+(* by (simplesubst split_if, blast) *) sorry
 
 lemmas if_splits [no_atp] = split_if split_if_asm
 
@@ -1108,7 +1113,9 @@ lemma if_bool_eq_conj:
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
   apply (simplesubst split_if, blast)
+(*
   done
+*) sorry
 
 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
@@ -1467,7 +1474,7 @@ text {* Method setup. *}
 ML {*
 structure Induct = Induct
 (
-  val cases_default = @{thm case_split}
+  val cases_default = @{thm NonIntuitionistic.case_split}
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
index 828f48f..dd0a700 100644
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -181,8 +181,7 @@ axiomatization where
   impI: "(P ==> Q) ==> P-->Q" and
   mp: "[| P-->Q;  P |] ==> Q" and
 
-  iff: "(P-->Q) --> (Q-->P) --> (P=Q)" and
-  True_or_False: "(P=True) | (P=False)"
+  iff: "(P-->Q) --> (Q-->P) --> (P=Q)"
 
 defs
   True_def:     "True      == ((%x::bool. x) = (%x. x))"
@@ -485,6 +484,7 @@ by (iprover intro: minorP minorQ impI
 subsubsection {*Classical logic*}
 
 lemma classical:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes prem: "~P ==> P"
   shows "P"
 apply (rule True_or_False [THEN disjE, THEN eqTrueE])
@@ -494,30 +494,44 @@ apply (erule subst)
 apply assumption
 done
 
-lemmas ccontr = FalseE [THEN classical]
+lemma ccontr:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
+  assumes "(\<not>P \<Longrightarrow> False)" shows P
+proof (rule classical)
+  fix Y show "Y = True \<or> Y = False" by (rule True_or_False)
+next
+  assume "\<not>P"
+  with assms(2) have False .
+  thus P by (rule FalseE)
+qed
 
 (*notE with premises exchanged; it discharges ~R so that it can be used to
   make elimination rules*)
 lemma rev_notE:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes premp: "P"
       and premnot: "~R ==> ~P"
   shows "R"
-apply (rule ccontr)
-apply (erule notE [OF premnot premp])
-done
+proof (rule ccontr)
+  fix Y show "(Y=True) | (Y=False)" by (rule True_or_False)
+next
+  assume "\<not>R" thus False by (rule notE [OF premnot premp])
+qed
 
 (*Double negation law*)
-lemma notnotD: "~~P ==> P"
+lemma notnotD: "(\<And>X. (X=True)|(X=False)) \<Longrightarrow> ~~P ==> P"
 apply (rule classical)
+apply assumption
 apply (erule notE)
 apply assumption
 done
 
 lemma contrapos_pp:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes p1: "Q"
       and p2: "~P ==> ~Q"
   shows "P"
-by (iprover intro: classical p1 p2 notE)
+by (iprover intro: True_or_False classical p1 p2 notE)
 
 
 subsubsection {*Unique existence*}
@@ -610,33 +624,46 @@ done
 subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
 
 lemma disjCI:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes "~Q ==> P" shows "P|Q"
-apply (rule classical)
-apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
-done
+proof (rule classical)
+  fix Y show "(Y=True) | (Y=False)" by (rule True_or_False)
+next
+  assume "\<not>(P \<or> Q)" thus "P \<or> Q" by (iprover intro: `\<not>Q \<Longrightarrow> P` disjI1 disjI2 notI elim: notE)
+qed
 
-lemma excluded_middle: "~P | P"
-by (iprover intro: disjCI)
+lemma excluded_middle:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
+  shows "~P | P"
+proof (rule disjCI)
+  fix Y show "(Y=True) | (Y=False)" by (rule True_or_False)
+next
+  assume "\<not>P" thus "\<not>P" .
+qed
 
 text {*
   case distinction as a natural deduction rule.
   Note that @{term "~P"} is the second case, not the first
 *}
 lemma case_split [case_names True False]:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes prem1: "P ==> Q"
       and prem2: "~P ==> Q"
   shows "Q"
 apply (rule excluded_middle [THEN disjE])
+apply (rule True_or_False)
 apply (erule prem2)
 apply (erule prem1)
 done
 
 (*Classical implies (-->) elimination. *)
 lemma impCE:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes major: "P-->Q"
       and minor: "~P ==> R" "Q ==> R"
   shows "R"
 apply (rule excluded_middle [of P, THEN disjE])
+apply (rule True_or_False)
 apply (iprover intro: minor major [THEN mp])+
 done
 
@@ -644,26 +671,52 @@ done
   those cases in which P holds "almost everywhere".  Can't install as
   default: would break old proofs.*)
 lemma impCE':
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes major: "P-->Q"
       and minor: "Q ==> R" "~P ==> R"
   shows "R"
 apply (rule excluded_middle [of P, THEN disjE])
+apply (rule True_or_False)
 apply (iprover intro: minor major [THEN mp])+
 done
 
 (*Classical <-> elimination. *)
 lemma iffCE:
+  assumes True_or_False: "\<And>X. (X=True) | (X=False)"
   assumes major: "P=Q"
       and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
   shows "R"
-apply (rule major [THEN iffE])
-apply (iprover intro: minor elim: impCE notE)
-done
+proof (rule impCE)
+  fix Y show "(Y=True) | (Y=False)" by (rule True_or_False)
+next
+  show "P \<longrightarrow> Q" by (iprover intro: impI major elim: rev_iffD1)
+(*
+  proof (rule impI)
+    assume "P"
+    thus "Q" using major by (rule rev_iffD1)
+  qed
+*)
+next
+  from major have "Q=P" by (rule sym)
+  assume "\<not>P"
+  hence "P \<longrightarrow> False" by (unfold not_def)
+  with `Q=P` have "Q \<longrightarrow> False" by (rule ssubst)
+  hence "\<not>Q" by (unfold not_def)
+  with `\<not>P` show R by (rule minor)
+next
+  from major have "Q=P" by (rule sym)
+  assume Q
+  hence P using `Q=P` by (rule back_subst)
+  from `P` and `Q` show R by (rule minor)
+qed
+
 
 lemma exCI:
+  assumes True_or_False: "\<And>X. (X=True)|(X=False)"
   assumes "ALL x. ~P(x) ==> P(a)"
   shows "EX x. P(x)"
 apply (rule ccontr)
+apply (rule True_or_False)
 apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
 done
 
@@ -806,11 +859,17 @@ named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
 
 subsubsection {* Classical Reasoner setup *}
 
-lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
-  by (rule classical) iprover
+lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> (\<And>X. (X=True)|(X=False)) ==> R"
+  apply (rule classical)
+  apply assumption
+  apply iprover
+  done
 
-lemma swap: "~ P ==> (~ R ==> P) ==> R"
-  by (rule classical) iprover
+lemma swap: " ~ P ==> (~ R ==> P) ==> (\<And>X. (X=True)|(X=False)) ==> R"
+  apply (rule classical)
+  apply assumption
+  apply iprover
+  done
 
 lemma thin_refl:
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
diff --git a/src/HOL/HOL.thy b/src/HOL/HOL.thy
index dd0a700..c36b28a3 100644
--- a/src/HOL/HOL.thy
+++ b/src/HOL/HOL.thy
@@ -874,6 +874,25 @@ lemma swap: " ~ P ==> (~ R ==> P) ==> (\<And>X. (X=True)|(X=False)) ==> R"
 lemma thin_refl:
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
+declare iffCE [elim!]
+  and FalseE [elim!]
+  and impCE [elim!]
+  and disjE [elim!]
+  and conjE [elim!]
+
+
+
+
+declare ex_ex1I [intro!]
+  and allI [intro!]
+  and the_equality [intro]
+  and exI [intro]
+
+
+declare exE [elim!]
+  allE [elim]
+
+
 ML {*
 structure Hypsubst = Hypsubst
 (
@@ -943,21 +962,23 @@ declare exE [elim!]
 
 ML {* val HOL_cs = claset_of @{context} *}
 
-lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
-  apply (erule swap)
-  apply (erule (1) meta_mp)
-  done
+lemma contrapos_np: "(\<And>X. (X=True)|(X=False)) ==> ~ Q ==> (~ P ==> Q) ==> P"
+  by (erule swap)
 
+(*
 declare ex_ex1I [rule del, intro! 2]
   and ex1I [intro]
+*)
 
+(*
 declare ext [intro]
+*)
 
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
-lemma alt_ex1E [elim!]:
+lemma alt_ex1E (* [elim!] *):
   assumes major: "\<exists>!x. P x"
       and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
   shows R
@@ -987,13 +1008,21 @@ subsubsection {* Simplifier *}
 
 lemma eta_contract_eq: "(%s. f s) = f" ..
 
+lemma intuitionistic_simp_thms:
+  shows "(x = x) = True"
+by blast
+
+lemma classical_simp_thms:
+  assumes True_or_False: "\<And>X. (X=True)|(X=False)"
+  shows not_not: "(\<not> \<not> P) = P"
+  and "(P \<or> \<not>P) = True" and "(\<not>P \<or> P) = True"
+sorry
+
+
 lemma simp_thms:
-  shows not_not: "(~ ~ P) = P"
-  and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
+  shows Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
   and
     "(P ~= Q) = (P = (~Q))"
-    "(P | ~P) = True"    "(~P | P) = True"
-    "(x = x) = True"
   and not_True_eq_False [code]: "(\<not> True) = False"
   and not_False_eq_True [code]: "(\<not> False) = True"
   and
@@ -1019,24 +1048,25 @@ lemma simp_thms:
     "!!P. (EX x. t=x & P(x)) = P(t)"
     "!!P. (ALL x. x=t --> P(x)) = P(t)"
     "!!P. (ALL x. t=x --> P(x)) = P(t)"
-  by (blast, blast, blast, blast, blast, iprover+)
+sorry
+(*  by (blast, blast, blast, blast, blast, iprover) *)
 
 lemma disj_absorb: "(A | A) = A"
-  by blast
+  sorry (*  by blast *)
 
 lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
-  by blast
+  sorry (*  by blast *)
 
 lemma conj_absorb: "(A & A) = A"
-  by blast
+  sorry (*  by blast *)
 
 lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
-  by blast
+  sorry (*  by blast *)
 
 lemma eq_ac:
   shows eq_commute: "a = b \<longleftrightarrow> b = a"
     and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
-    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
+    and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" sorry (* by (iprover, blast) *)
 lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
 
 lemma conj_comms:
@@ -1064,23 +1094,23 @@ lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
 lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
 
 text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
-lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
-lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast
+lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" sorry (* by blast *)
+lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" sorry (* by blast *)
 
-lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
-lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
+lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" sorry (* by blast *)
+lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" sorry (* by blast *)
 
 lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
   by iprover
 
 lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
-lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
-lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
-lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
-lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
+lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" sorry (* by blast *)
+lemma not_imp: "(~(P --> Q)) = (P & ~Q)" sorry (* by blast *)
+lemma not_iff: "(P~=Q) = (P = (~Q))" sorry (* by blast *)
+lemma disj_not1: "(~P | Q) = (P --> Q)" sorry (* by blast *)
 lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
-  by blast
-lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
+   sorry (* by blast *)
+lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)"  sorry (* by blast *)
 
 lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 
@@ -1088,13 +1118,13 @@ lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
   -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
   -- {* cases boil down to the same thing. *}
-  by blast
+   sorry (* by blast *)
 
-lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
-lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
+lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))"  sorry (* by blast *)
+lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)"  sorry (* by blast *)
 lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
 lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
-lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
+lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"  sorry (* by blast *)
 
 declare All_def [no_atp]
 
@@ -1117,31 +1147,37 @@ text {* The @{text "|"} congruence rule: not included by default! *}
 
 lemma disj_cong:
     "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
-  by blast
+   sorry (* by blast *)
 
 
 text {* \medskip if-then-else rules *}
 
 lemma if_True [code]: "(if True then x else y) = x"
-  by (unfold If_def) blast
+sorry (*
+  by (unfold If_def) blast *)
 
 lemma if_False [code]: "(if False then x else y) = y"
-  by (unfold If_def) blast
+sorry (*
+  by (unfold If_def) blast *)
 
 lemma if_P: "P ==> (if P then x else y) = x"
-  by (unfold If_def) blast
+sorry (*
+  by (unfold If_def) blast *)
 
 lemma if_not_P: "~P ==> (if P then x else y) = y"
-  by (unfold If_def) blast
+sorry (*
+  by (unfold If_def) blast *)
 
 lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
+sorry (*
   apply (rule case_split [of Q])
    apply (simplesubst if_P)
     prefer 3 apply (simplesubst if_not_P, blast+)
   done
+*)
 
 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
-by (simplesubst split_if, blast)
+sorry (* by (simplesubst split_if, blast) *)
 
 lemmas if_splits [no_atp] = split_if split_if_asm
 
@@ -1158,8 +1194,8 @@ lemma if_bool_eq_conj:
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
-  apply (simplesubst split_if, blast)
-  done
+  sorry (* apply (simplesubst split_if, blast)
+  done *)
 
 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
@@ -1222,25 +1258,25 @@ qed
 lemma uncurry:
   assumes "P \<longrightarrow> Q \<longrightarrow> R"
   shows "P \<and> Q \<longrightarrow> R"
-  using assms by blast
+  using assms by iprover
 
 lemma iff_allI:
   assumes "\<And>x. P x = Q x"
   shows "(\<forall>x. P x) = (\<forall>x. Q x)"
-  using assms by blast
+  using assms by iprover
 
 lemma iff_exI:
   assumes "\<And>x. P x = Q x"
   shows "(\<exists>x. P x) = (\<exists>x. Q x)"
-  using assms by blast
+  using assms by iprover
 
 lemma all_comm:
   "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
-  by blast
+  by iprover
 
 lemma ex_comm:
   "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
-  by blast
+  by iprover
 
 ML_file "Tools/simpdata.ML"
 ML {* open Simpdata *}
@@ -1351,7 +1387,8 @@ lemma ex_simps:
   "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
   "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
   -- {* Miniscoping: pushing in existential quantifiers. *}
-  by (iprover | blast)+
+sorry
+(*   by (iprover | blast)+ *)
 
 lemma all_simps:
   "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
@@ -1361,7 +1398,8 @@ lemma all_simps:
   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
   -- {* Miniscoping: pushing in universal quantifiers. *}
-  by (iprover | blast)+
+sorry
+(*  by (iprover | blast)+ *)
 
 lemmas [simp] =
   triv_forall_equality (*prunes params*)
@@ -1392,6 +1430,8 @@ lemmas [simp] =
   ex_simps
   all_simps
   simp_thms
+  classical_simp_thms
+  intuitionistic_simp_thms
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = split_if
@@ -1432,7 +1472,7 @@ lemma if_distrib:
 text{*As a simplification rule, it replaces all function equalities by
   first-order equalities.*}
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
-  by auto
+sorry (*  by auto *)
 
 
 subsubsection {* Generic cases and induction *}
@@ -1603,7 +1643,7 @@ lemma [induct_simp]: "induct_implies induct_true P == P"
   by (simp add: induct_implies_def induct_true_def)
 
 lemma [induct_simp]: "(x = x) = True"
-  by (rule simp_thms)
+  by (rule intuitionistic_simp_thms)
 
 hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
 
@@ -1662,9 +1702,12 @@ end;
 subsection {* Other simple lemmas and lemma duplicates *}
 
 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
+sorry (*
   by blast+
+*)
 
 lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
+sorry (*
   apply (rule iffI)
   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
   apply (fast dest!: theI')
@@ -1679,6 +1722,7 @@ lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
   apply (case_tac "xa = x")
   apply (drule_tac [3] x = x in fun_cong, simp_all)
   done
+*)
 
 lemmas eq_sym_conv = eq_commute
 
@@ -1686,7 +1730,9 @@ lemma nnf_simps:
   "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
   "(\<not> \<not>(P)) = P"
+sorry (*
 by blast+
+*)
 
 subsection {* Basic ML bindings *}
 
@@ -1741,7 +1787,10 @@ val sym = @{thm sym}
 val trans = @{thm trans}
 *}
 
+
+(*
 ML_file "Tools/cnf.ML"
+*)
 
 
 section {* @{text NO_MATCH} simproc *}
@@ -1848,7 +1897,7 @@ text {* More about @{typ prop} *}
 lemma [code nbe]:
   shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
-    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
+    and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" sorry (* by (auto intro!: equal_intr_rule) *)
 
 lemma Trueprop_code [code]:
   "Trueprop True \<equiv> Code_Generator.holds"
@@ -1858,7 +1907,9 @@ declare Trueprop_code [symmetric, code_post]
 
 text {* Equality *}
 
+(*
 declare simp_thms(6) [code nbe]
+*)
 
 instantiation itself :: (type) equal
 begin


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.