src/HOL/HOL.thy
changeset 61799 4cf66f21b764
parent 61378 3e04c9ca001a
child 61914 16bfe0a6702d
     1.1 --- a/src/HOL/HOL.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4    [(@{const_syntax The}, fn _ => fn [Abs abs] =>
     1.5        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
     1.6        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
     1.7 -\<close>  -- \<open>To avoid eta-contraction of body\<close>
     1.8 +\<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
     1.9  
    1.10  nonterminal letbinds and letbind
    1.11  syntax
    1.12 @@ -160,7 +160,7 @@
    1.13    refl: "t = (t::'a)" and
    1.14    subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
    1.15    ext: "(\<And>x::'a. (f x ::'b) = g x) \<Longrightarrow> (\<lambda>x. f x) = (\<lambda>x. g x)"
    1.16 -    -- \<open>Extensionality is built into the meta-logic, and this rule expresses
    1.17 +    \<comment> \<open>Extensionality is built into the meta-logic, and this rule expresses
    1.18           a related property.  It is an eta-expanded version of the traditional
    1.19           rule, and similar to the ABS rule of HOL\<close> and
    1.20  
    1.21 @@ -219,7 +219,7 @@
    1.22    shows "A = B"
    1.23    by (unfold meq) (rule refl)
    1.24  
    1.25 -text \<open>Useful with @{text erule} for proving equalities from known equalities.\<close>
    1.26 +text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
    1.27       (* a = b
    1.28          |   |
    1.29          c = d   *)
    1.30 @@ -241,13 +241,13 @@
    1.31  
    1.32  subsubsection \<open>Congruence rules for application\<close>
    1.33  
    1.34 -text \<open>Similar to @{text AP_THM} in Gordon's HOL.\<close>
    1.35 +text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
    1.36  lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
    1.37  apply (erule subst)
    1.38  apply (rule refl)
    1.39  done
    1.40  
    1.41 -text \<open>Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}.\<close>
    1.42 +text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
    1.43  lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
    1.44  apply (erule subst)
    1.45  apply (rule refl)
    1.46 @@ -329,7 +329,7 @@
    1.47  subsubsection \<open>False\<close>
    1.48  
    1.49  text \<open>
    1.50 -  Depends upon @{text spec}; it is impossible to do propositional
    1.51 +  Depends upon \<open>spec\<close>; it is impossible to do propositional
    1.52    logic before quantifiers!
    1.53  \<close>
    1.54  
    1.55 @@ -968,7 +968,7 @@
    1.56  lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
    1.57  lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
    1.58  
    1.59 -text \<open>These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}.\<close>
    1.60 +text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
    1.61  lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
    1.62  lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
    1.63  
    1.64 @@ -983,7 +983,7 @@
    1.65  lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
    1.66  lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
    1.67  lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
    1.68 -lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  -- \<open>changes orientation :-(\<close>
    1.69 +lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
    1.70    by blast
    1.71  lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
    1.72  
    1.73 @@ -991,8 +991,8 @@
    1.74  
    1.75  
    1.76  lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
    1.77 -  -- \<open>Avoids duplication of subgoals after @{text split_if}, when the true and false\<close>
    1.78 -  -- \<open>cases boil down to the same thing.\<close>
    1.79 +  \<comment> \<open>Avoids duplication of subgoals after \<open>split_if\<close>, when the true and false\<close>
    1.80 +  \<comment> \<open>cases boil down to the same thing.\<close>
    1.81    by blast
    1.82  
    1.83  lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
    1.84 @@ -1007,7 +1007,7 @@
    1.85  lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
    1.86  
    1.87  text \<open>
    1.88 -  \medskip The @{text "\<and>"} congruence rule: not included by default!
    1.89 +  \medskip The \<open>\<and>\<close> congruence rule: not included by default!
    1.90    May slow rewrite proofs down by as much as 50\%\<close>
    1.91  
    1.92  lemma conj_cong:
    1.93 @@ -1018,7 +1018,7 @@
    1.94      "(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
    1.95    by iprover
    1.96  
    1.97 -text \<open>The @{text "|"} congruence rule: not included by default!\<close>
    1.98 +text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
    1.99  
   1.100  lemma disj_cong:
   1.101      "(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
   1.102 @@ -1057,11 +1057,11 @@
   1.103  by (simplesubst split_if, blast)
   1.104  
   1.105  lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
   1.106 -  -- \<open>This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "\<Longrightarrow>"} symbol.\<close>
   1.107 +  \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
   1.108    by (rule split_if)
   1.109  
   1.110  lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
   1.111 -  -- \<open>And this form is useful for expanding @{text "if"}s on the LEFT.\<close>
   1.112 +  \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
   1.113    by (simplesubst split_if) blast
   1.114  
   1.115  lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
   1.116 @@ -1156,7 +1156,7 @@
   1.117  simproc_setup defined_Ex ("\<exists>x. P x") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
   1.118  simproc_setup defined_All ("\<forall>x. P x") = \<open>fn _ => Quantifier1.rearrange_all\<close>
   1.119  
   1.120 -text \<open>Simproc for proving @{text "(y = x) \<equiv> False"} from premise @{text "\<not> (x = y)"}:\<close>
   1.121 +text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
   1.122  
   1.123  simproc_setup neq ("x = y") = \<open>fn _ =>
   1.124  let
   1.125 @@ -1261,7 +1261,7 @@
   1.126    "\<And>P Q. (\<exists>x. P \<or> Q x)   = (P \<or> (\<exists>x. Q x))"
   1.127    "\<And>P Q. (\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
   1.128    "\<And>P Q. (\<exists>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<exists>x. Q x))"
   1.129 -  -- \<open>Miniscoping: pushing in existential quantifiers.\<close>
   1.130 +  \<comment> \<open>Miniscoping: pushing in existential quantifiers.\<close>
   1.131    by (iprover | blast)+
   1.132  
   1.133  lemma all_simps:
   1.134 @@ -1271,7 +1271,7 @@
   1.135    "\<And>P Q. (\<forall>x. P \<or> Q x)   = (P \<or> (\<forall>x. Q x))"
   1.136    "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
   1.137    "\<And>P Q. (\<forall>x. P \<longrightarrow> Q x) = (P \<longrightarrow> (\<forall>x. Q x))"
   1.138 -  -- \<open>Miniscoping: pushing in universal quantifiers.\<close>
   1.139 +  \<comment> \<open>Miniscoping: pushing in universal quantifiers.\<close>
   1.140    by (iprover | blast)+
   1.141  
   1.142  lemmas [simp] =
   1.143 @@ -1654,7 +1654,7 @@
   1.144  ML_file "Tools/cnf.ML"
   1.145  
   1.146  
   1.147 -section \<open>@{text NO_MATCH} simproc\<close>
   1.148 +section \<open>\<open>NO_MATCH\<close> simproc\<close>
   1.149  
   1.150  text \<open>
   1.151   The simplification procedure can be used to avoid simplification of terms of a certain form