src/Sequents/LK.thy

 
   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
                ==> (P, $H |- $F) == (P', $H' |- $F')"
 
 
-subsection {* Rewrite rules *}
+subsection \<open>Rewrite rules\<close>
 
 lemma conj_simps:
   "|- P & True <-> P"
   "|- True & P <-> P"
   "|- P & False <-> False"

   "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
   "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
   by (fast add!: subst)+
 
 
-subsection {* Miniscoping: pushing quantifiers in *}
-
-text {*
+subsection \<open>Miniscoping: pushing quantifiers in\<close>
+
+text \<open>
   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*}
+\<close>
+
+text \<open>existential miniscoping\<close>
 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))"
   by (fast add!: subst)+
 
-text {*universal miniscoping*}
+text \<open>universal miniscoping\<close>
 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))"
   by (fast add!: subst)+
 
-text {*These are NOT supplied by default!*}
+text \<open>These are NOT supplied by default!\<close>
 lemma distrib_simps:
   "|- P & (Q | R) <-> P&Q | P&R"
   "|- (Q | R) & P <-> Q&P | R&P"
   "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
   by (fast add!: subst)+

   "|- (~P --> P) <-> P"
   "|- (~P <-> ~Q) <-> (P<->Q)"
   by (fast add!: subst)+
 
 
-subsection {* Named rewrite rules *}
+subsection \<open>Named rewrite rules\<close>
 
 lemma conj_commute: "|- P&Q <-> Q&P"
   and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
   by (fast add!: subst)+
 

   assumes p1: "|- P <-> P'"
     and p2: "|- P' ==> |- Q <-> Q'"
   shows "|- (P-->Q) <-> (P'-->Q')"
   apply (lem p1)
   apply safe
-   apply (tactic {*
+   apply (tactic \<open>
      REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
        DEPTH_SOLVE_1
          (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
-           Cla.safe_tac @{context} 1) *})
+           Cla.safe_tac @{context} 1)\<close>)
   done
 
 lemma conj_cong:
   assumes p1: "|- P <-> P'"
     and p2: "|- P' ==> |- Q <-> Q'"
   shows "|- (P&Q) <-> (P'&Q')"
   apply (lem p1)
   apply safe
-   apply (tactic {*
+   apply (tactic \<open>
      REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
        DEPTH_SOLVE_1
          (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
-           Cla.safe_tac @{context} 1) *})
+           Cla.safe_tac @{context} 1)\<close>)
   done
 
 lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
   by (fast add!: subst)
 
 ML_file "simpdata.ML"
-setup {* map_theory_simpset (put_simpset LK_ss) *}
-setup {* Simplifier.method_setup [] *}
-
-
-text {* To create substition rules *}
+setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
+setup \<open>Simplifier.method_setup []\<close>
+
+
+text \<open>To create substition rules\<close>
 
 lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   by simp
 
 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"