# HG changeset patch
# User wenzelm
# Date 1213191693 -7200
# Node ID 123377499a8ed43cee884ec86d59f8bc80f4c882
# Parent  5b78e50adc4902d64d1520af3f57c705fff47d60
converted ML proofs from simpdata.ML;
tuned;

diff -r 5b78e50adc49 -r 123377499a8e src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Wed Jun 11 15:41:08 2008 +0200
+++ b/src/Sequents/LK.thy	Wed Jun 11 15:41:33 2008 +0200
@@ -18,13 +18,231 @@
 uses ("simpdata.ML")
 begin
 
-axioms
-
-  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
+axiomatization where
+  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
 
   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
                ==> (P, $H |- $F) == (P', $H' |- $F')"
 
+
+subsection {* Rewrite rules *}
+
+lemma conj_simps:
+  "|- P & True <-> P"
+  "|- True & P <-> P"
+  "|- P & False <-> False"
+  "|- False & P <-> False"
+  "|- P & P <-> P"
+  "|- P & P & Q <-> P & Q"
+  "|- P & ~P <-> False"
+  "|- ~P & P <-> False"
+  "|- (P & Q) & R <-> P & (Q & R)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma disj_simps:
+  "|- P | True <-> True"
+  "|- True | P <-> True"
+  "|- P | False <-> P"
+  "|- False | P <-> P"
+  "|- P | P <-> P"
+  "|- P | P | Q <-> P | Q"
+  "|- (P | Q) | R <-> P | (Q | R)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma not_simps:
+  "|- ~ False <-> True"
+  "|- ~ True <-> False"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma imp_simps:
+  "|- (P --> False) <-> ~P"
+  "|- (P --> True) <-> True"
+  "|- (False --> P) <-> True"
+  "|- (True --> P) <-> P"
+  "|- (P --> P) <-> True"
+  "|- (P --> ~P) <-> ~P"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma iff_simps:
+  "|- (True <-> P) <-> P"
+  "|- (P <-> True) <-> P"
+  "|- (P <-> P) <-> True"
+  "|- (False <-> P) <-> ~P"
+  "|- (P <-> False) <-> ~P"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma quant_simps:
+  "!!P. |- (ALL x. P) <-> P"
+  "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
+  "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
+  "!!P. |- (EX x. P) <-> P"
+  "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
+  "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+
+subsection {* Miniscoping: pushing quantifiers in *}
+
+text {*
+  We do NOT distribute of ALL over &, or dually that of EX over |
+  Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
+  show that this step can increase proof length!
+*}
+
+text {*existential miniscoping*}
+lemma ex_simps:
+  "!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
+  "!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
+  "!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
+  "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+  "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
+  "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+text {*universal miniscoping*}
+lemma all_simps:
+  "!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
+  "!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
+  "!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
+  "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
+  "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
+  "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+text {*These are NOT supplied by default!*}
+lemma distrib_simps:
+  "|- P & (Q | R) <-> P&Q | P&R"
+  "|- (Q | R) & P <-> Q&P | R&P"
+  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
+  apply (erule thinR [THEN cut])
+  apply (tactic {* fast_tac LK_pack 1 *})
+  done
+
+lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
+
+lemma P_iff_T: "|- P ==> |- (P <-> True)"
+  apply (erule thinR [THEN cut])
+  apply (tactic {* fast_tac LK_pack 1 *})
+  done
+
+lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
+
+
+lemma LK_extra_simps:
+  "|- P | ~P"
+  "|- ~P | P"
+  "|- ~ ~ P <-> P"
+  "|- (~P --> P) <-> P"
+  "|- (~P <-> ~Q) <-> (P<->Q)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+
+subsection {* Named rewrite rules *}
+
+lemma conj_commute: "|- P&Q <-> Q&P"
+  and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemmas conj_comms = conj_commute conj_left_commute
+
+lemma disj_commute: "|- P|Q <-> Q|P"
+  and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemmas disj_comms = disj_commute disj_left_commute
+
+lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
+  and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
+
+  and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
+  and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
+
+  and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
+  and imp_conj: "|- ((P&Q)-->R)   <-> (P --> (Q --> R))"
+  and imp_disj: "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)"
+
+  and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
+  and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
+
+  and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
+  and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
+
+  and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
+  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
+  done
+
+lemma imp_cong:
+  assumes p1: "|- P <-> P'"
+    and p2: "|- P' ==> |- Q <-> Q'"
+  shows "|- (P-->Q) <-> (P'-->Q')"
+  apply (tactic {* lemma_tac @{thm p1} 1 *})
+  apply (tactic {* safe_tac LK_pack 1 *})
+   apply (tactic {*
+     REPEAT (rtac @{thm cut} 1 THEN
+       DEPTH_SOLVE_1
+         (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
+           safe_tac LK_pack 1) *})
+  done
+
+lemma conj_cong:
+  assumes p1: "|- P <-> P'"
+    and p2: "|- P' ==> |- Q <-> Q'"
+  shows "|- (P&Q) <-> (P'&Q')"
+  apply (tactic {* lemma_tac @{thm p1} 1 *})
+  apply (tactic {* safe_tac LK_pack 1 *})
+   apply (tactic {*
+     REPEAT (rtac @{thm cut} 1 THEN
+       DEPTH_SOLVE_1
+         (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
+           safe_tac LK_pack 1) *})
+  done
+
+lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
+  apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
+  done
+
 use "simpdata.ML"
 
+
+text {* To create substition rules *}
+
+lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
+  apply (tactic {* asm_simp_tac LK_basic_ss 1 *})
+  done
+
+lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
+  apply (rule_tac P = Q in cut)
+   apply (tactic {* simp_tac (simpset () addsimps @{thms if_P}) 2 *})
+  apply (rule_tac P = "~Q" in cut)
+   apply (tactic {* simp_tac (simpset() addsimps @{thms if_not_P}) 2 *})
+  apply (tactic {* fast_tac LK_pack 1 *})
+  done
+
+lemma if_cancel: "|- (if P then x else x) = x"
+  apply (tactic {* lemma_tac @{thm split_if} 1 *})
+  apply (tactic {* fast_tac LK_pack 1 *})
+  done
+
+lemma if_eq_cancel: "|- (if x=y then y else x) = x"
+  apply (tactic {* lemma_tac @{thm split_if} 1 *})
+  apply (tactic {* safe_tac LK_pack 1 *})
+  apply (rule symL)
+  apply (rule basic)
+  done
+
 end
diff -r 5b78e50adc49 -r 123377499a8e src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Wed Jun 11 15:41:08 2008 +0200
+++ b/src/Sequents/simpdata.ML	Wed Jun 11 15:41:33 2008 +0200
@@ -3,83 +3,11 @@
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
 
-Instantiation of the generic simplifier for LK
+Instantiation of the generic simplifier for LK.
 
 Borrows from the DC simplifier of Soren Heilmann.
 *)
 
-(*** Rewrite rules ***)
-
-fun prove_fun s =
- (writeln s;
-  prove_goal (the_context ()) s
-   (fn prems => [ (cut_facts_tac prems 1),
-                  (fast_tac (LK_pack add_safes @{thms subst}) 1) ]));
-
-val conj_simps = map prove_fun
- ["|- P & True <-> P",      "|- True & P <-> P",
-  "|- P & False <-> False", "|- False & P <-> False",
-  "|- P & P <-> P", "        |- P & P & Q <-> P & Q",
-  "|- P & ~P <-> False",    "|- ~P & P <-> False",
-  "|- (P & Q) & R <-> P & (Q & R)"];
-
-val disj_simps = map prove_fun
- ["|- P | True <-> True",  "|- True | P <-> True",
-  "|- P | False <-> P",    "|- False | P <-> P",
-  "|- P | P <-> P",        "|- P | P | Q <-> P | Q",
-  "|- (P | Q) | R <-> P | (Q | R)"];
-
-val not_simps = map prove_fun
- ["|- ~ False <-> True",   "|- ~ True <-> False"];
-
-val imp_simps = map prove_fun
- ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
-  "|- (False --> P) <-> True",     "|- (True --> P) <-> P",
-  "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
-
-val iff_simps = map prove_fun
- ["|- (True <-> P) <-> P",         "|- (P <-> True) <-> P",
-  "|- (P <-> P) <-> True",
-  "|- (False <-> P) <-> ~P",       "|- (P <-> False) <-> ~P"];
-
-
-val quant_simps = map prove_fun
- ["|- (ALL x. P) <-> P",
-  "|- (ALL x. x=t --> P(x)) <-> P(t)",
-  "|- (ALL x. t=x --> P(x)) <-> P(t)",
-  "|- (EX x. P) <-> P",
-  "|- (EX x. x=t & P(x)) <-> P(t)",
-  "|- (EX x. t=x & P(x)) <-> P(t)"];
-
-(*** Miniscoping: pushing quantifiers in
-     We do NOT distribute of ALL over &, or dually that of EX over |
-     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
-     show that this step can increase proof length!
-***)
-
-(*existential miniscoping*)
-val ex_simps = map prove_fun
-                   ["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
-                    "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
-                    "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
-                    "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
-                    "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
-                    "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
-
-(*universal miniscoping*)
-val all_simps = map prove_fun
-                    ["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
-                     "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
-                     "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
-                     "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
-                     "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
-                     "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
-
-(*These are NOT supplied by default!*)
-val distrib_simps  = map prove_fun
- ["|- P & (Q | R) <-> P&Q | P&R",
-  "|- (Q | R) & P <-> Q&P | R&P",
-  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
 
 (** Conversion into rewrite rules **)
 
@@ -100,20 +28,6 @@
       | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
  | _ => [r];
 
-Goal "|- ~P ==> |- (P <-> False)";
-by (etac (@{thm thinR} RS @{thm cut}) 1);
-by (fast_tac LK_pack 1);
-qed "P_iff_F";
-
-bind_thm ("iff_reflection_F", P_iff_F RS @{thm iff_reflection});
-
-Goal "|- P ==> |- (P <-> True)";
-by (etac (@{thm thinR} RS @{thm cut}) 1);
-by (fast_tac LK_pack 1);
-qed "P_iff_T";
-
-bind_thm ("iff_reflection_T", P_iff_T RS @{thm iff_reflection});
-
 (*Make meta-equalities.*)
 fun mk_meta_eq th = case concl_of th of
     Const("==",_)$_$_           => th
@@ -123,8 +37,8 @@
                  (case p of
                       (Const("equal",_)$_$_)   => th RS @{thm eq_reflection}
                     | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
-                    | (Const("Not",_)$_)      => th RS iff_reflection_F
-                    | _                       => th RS iff_reflection_T)
+                    | (Const("Not",_)$_)      => th RS @{thm iff_reflection_F}
+                    | _                       => th RS @{thm iff_reflection_T})
            | _ => error ("addsimps: unable to use theorem\n" ^
                          Display.string_of_thm th));
 
@@ -140,77 +54,17 @@
   error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 
-(*** Named rewrite rules ***)
-
-fun prove nm thm  = qed_goal nm (the_context ()) thm
-    (fn prems => [ (cut_facts_tac prems 1),
-                   (fast_tac LK_pack 1) ]);
-
-prove "conj_commute" "|- P&Q <-> Q&P";
-prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)";
-val conj_comms = [conj_commute, conj_left_commute];
-
-prove "disj_commute" "|- P|Q <-> Q|P";
-prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)";
-val disj_comms = [disj_commute, disj_left_commute];
-
-prove "conj_disj_distribL" "|- P&(Q|R) <-> (P&Q | P&R)";
-prove "conj_disj_distribR" "|- (P|Q)&R <-> (P&R | Q&R)";
-
-prove "disj_conj_distribL" "|- P|(Q&R) <-> (P|Q) & (P|R)";
-prove "disj_conj_distribR" "|- (P&Q)|R <-> (P|R) & (Q|R)";
-
-prove "imp_conj_distrib" "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)";
-prove "imp_conj"         "|- ((P&Q)-->R)   <-> (P --> (Q --> R))";
-prove "imp_disj"         "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)";
-
-prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)";
-prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)";
-
-prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)";
-prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)";
-
-prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
-
-
-val [p1,p2] = Goal
-    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
-by (lemma_tac p1 1);
-by (safe_tac LK_pack 1);
-by (REPEAT (rtac @{thm cut} 1
-            THEN
-            DEPTH_SOLVE_1 (resolve_tac [@{thm thinL}, @{thm thinR}, p2 COMP @{thm monotonic}] 1)
-            THEN
-            safe_tac LK_pack 1));
-qed "imp_cong";
-
-val [p1,p2] = Goal
-    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
-by (lemma_tac p1 1);
-by (safe_tac LK_pack 1);
-by (REPEAT (rtac @{thm cut} 1
-            THEN
-            DEPTH_SOLVE_1 (resolve_tac [@{thm thinL}, @{thm thinR}, p2 COMP @{thm monotonic}] 1)
-            THEN
-            safe_tac LK_pack 1));
-qed "conj_cong";
-
-Goal "|- (x=y) <-> (y=x)";
-by (fast_tac (LK_pack add_safes @{thms subst}) 1);
-qed "eq_sym_conv";
-
-
-
 (*** Standard simpsets ***)
 
-val triv_rls = [thm "FalseL", thm "TrueR", thm "basic", thm "refl",
-  thm "iff_refl", reflexive_thm];
+val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
+  @{thm iff_refl}, reflexive_thm];
 
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
-                                 assume_tac];
+fun unsafe_solver prems =
+  FIRST' [resolve_tac (triv_rls @ prems), assume_tac];
+
 (*No premature instantiation of variables during simplification*)
-fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
-                                 eq_assume_tac];
+fun safe_solver prems =
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), eq_assume_tac];
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
@@ -223,48 +77,16 @@
 
 val LK_simps =
    [triv_forall_equality, (* prunes params *)
-    @{thm refl} RS P_iff_T] @
-    conj_simps @ disj_simps @ not_simps @
-    imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
-    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
-    map prove_fun
-     ["|- P | ~P",             "|- ~P | P",
-      "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
-      "|- (~P <-> ~Q) <-> (P<->Q)"];
+    @{thm refl} RS @{thm P_iff_T}] @
+    @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
+    @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
+    @{thms all_simps} @ @{thms ex_simps} @
+    [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @
+    @{thms LK_extra_simps};
 
 val LK_ss =
   LK_basic_ss addsimps LK_simps
-  addeqcongs [thm "left_cong"]
-  addcongs [imp_cong];
+  addeqcongs [@{thm left_cong}]
+  addcongs [@{thm imp_cong}];
 
 change_simpset (fn _ => LK_ss);
-
-
-(* To create substition rules *)
-
-qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
-  (fn prems =>
-   [cut_facts_tac prems 1,
-    asm_simp_tac LK_basic_ss 1]);
-
-Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
-by (res_inst_tac [ ("P","Q") ] (thm "cut") 1);
-by (simp_tac (simpset() addsimps [thm "if_P"]) 2);
-by (res_inst_tac [ ("P","~Q") ] (thm "cut") 1);
-by (simp_tac (simpset() addsimps [thm "if_not_P"]) 2);
-by (fast_tac LK_pack 1);
-qed "split_if";
-
-Goal "|- (if P then x else x) = x";
-by (lemma_tac split_if 1);
-by (fast_tac LK_pack 1);
-qed "if_cancel";
-
-Goal "|- (if x=y then y else x) = x";
-by (lemma_tac split_if 1);
-by (safe_tac LK_pack 1);
-by (rtac (thm "symL") 1);
-by (rtac (thm "basic") 1);
-qed "if_eq_cancel";
-
-(*Putting in automatic case splits seems to require a lot of work.*)