src/HOL/Word/WordBitwise.thy

 
 imports Word
 
 begin
 
-text {* Helper constants used in defining addition *}
+text \<open>Helper constants used in defining addition\<close>
 
 definition
   xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
 where
  "xor3 a b c = (a = (b = c))"

   "xor3 False a b = (a \<noteq> b)"
   "xor3 a False b = (a \<noteq> b)"
   "xor3 a b False = (a \<noteq> b)"
   by (simp_all add: xor3_def)
 
-text {* Breaking up word equalities into equalities on their
+text \<open>Breaking up word equalities into equalities on their
 bit lists. Equalities are generated and manipulated in the
-reverse order to to_bl. *}
+reverse order to to_bl.\<close>
 
 lemma word_eq_rbl_eq:
   "(x = y) = (rev (to_bl x) = rev (to_bl y))"
   by simp
 

   fixes x :: "'a :: len word"
   shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
   using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
   by (simp add: word_size)
 
-text {* Breaking up inequalities into bitlist properties. *}
+text \<open>Breaking up inequalities into bitlist properties.\<close>
 
 definition
   "rev_bl_order F xs ys =
      (length xs = length ys \<and>
        ((xs = ys \<and> F)

    apply (cases "to_bl y", simp)
    apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
    apply auto
   done
 
-text {* Lemmas for unpacking rev (to_bl n) for numerals n and also
-for irreducible values and expressions. *}
+text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
+for irreducible values and expressions.\<close>
 
 lemma rev_bin_to_bl_simps:
   "rev (bin_to_bl 0 x) = []"
   "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
     = False # rev (bin_to_bl n (numeral nm))"

 lemma upt_eq_list_intros:
   "j <= i \<Longrightarrow> [i ..< j] = []"
   "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
   by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
 
-text {* Tactic definition *}
-
-ML {*
+text \<open>Tactic definition\<close>
+
+ML \<open>
 structure Word_Bitwise_Tac =
 struct
 
 val word_ss = simpset_of @{theory_context Word};
 

         map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
   end;
 
 end
 
-*}
+\<close>
 
 method_setup word_bitwise =
-  {* Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))  *}
+  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
   "decomposer for word equalities and inequalities into bit propositions"
 
 end