--- a/src/HOL/Word/Tools/smt_word.ML Mon Mar 20 21:01:47 2017 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML Mon Mar 20 21:53:37 2017 +0100
@@ -99,30 +99,30 @@
val setup_builtins =
SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
fold (add_word_fun if_fixed_all) [
- (@{term "uminus :: 'a::len word => _"}, "bvneg"),
- (@{term "plus :: 'a::len word => _"}, "bvadd"),
- (@{term "minus :: 'a::len word => _"}, "bvsub"),
- (@{term "times :: 'a::len word => _"}, "bvmul"),
- (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
- (@{term "bitAND :: 'a::len word => _"}, "bvand"),
- (@{term "bitOR :: 'a::len word => _"}, "bvor"),
- (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
- (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
+ (@{term "uminus :: 'a::len word \<Rightarrow> _"}, "bvneg"),
+ (@{term "plus :: 'a::len word \<Rightarrow> _"}, "bvadd"),
+ (@{term "minus :: 'a::len word \<Rightarrow> _"}, "bvsub"),
+ (@{term "times :: 'a::len word \<Rightarrow> _"}, "bvmul"),
+ (@{term "bitNOT :: 'a::len word \<Rightarrow> _"}, "bvnot"),
+ (@{term "bitAND :: 'a::len word \<Rightarrow> _"}, "bvand"),
+ (@{term "bitOR :: 'a::len word \<Rightarrow> _"}, "bvor"),
+ (@{term "bitXOR :: 'a::len word \<Rightarrow> _"}, "bvxor"),
+ (@{term "word_cat :: 'a::len word \<Rightarrow> _"}, "concat") ] #>
fold (add_word_fun shift) [
- (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
- (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
- (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
+ (@{term "shiftl :: 'a::len word \<Rightarrow> _ "}, "bvshl"),
+ (@{term "shiftr :: 'a::len word \<Rightarrow> _"}, "bvlshr"),
+ (@{term "sshiftr :: 'a::len word \<Rightarrow> _"}, "bvashr") ] #>
add_word_fun extract
- (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
+ (@{term "slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _"}, "extract") #>
fold (add_word_fun extend) [
- (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
- (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
+ (@{term "ucast :: 'a::len word \<Rightarrow> _"}, "zero_extend"),
+ (@{term "scast :: 'a::len word \<Rightarrow> _"}, "sign_extend") ] #>
fold (add_word_fun rotate) [
(@{term word_rotl}, "rotate_left"),
(@{term word_rotr}, "rotate_right") ] #>
fold (add_word_fun if_fixed_args) [
- (@{term "less :: 'a::len word => _"}, "bvult"),
- (@{term "less_eq :: 'a::len word => _"}, "bvule"),
+ (@{term "less :: 'a::len word \<Rightarrow> _"}, "bvult"),
+ (@{term "less_eq :: 'a::len word \<Rightarrow> _"}, "bvule"),
(@{term word_sless}, "bvslt"),
(@{term word_sle}, "bvsle") ]
--- a/src/HOL/Word/Word.thy Mon Mar 20 21:01:47 2017 +0100
+++ b/src/HOL/Word/Word.thy Mon Mar 20 21:53:37 2017 +0100
@@ -3315,25 +3315,21 @@
apply (simp add: word_size)
done
-lemma nth_slice:
- "(slice n w :: 'a::len0 word) !! m =
- (w !! (m + n) & m < len_of TYPE('a))"
- unfolding slice_shiftr
- by (simp add : nth_ucast nth_shiftr)
+lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
+ by (simp add: slice_shiftr nth_ucast nth_shiftr)
lemma slice1_down_alt':
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
to_bl sl = takefill False fs (drop k (to_bl w))"
- unfolding slice1_def word_size of_bl_def uint_bl
- by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
+ by (auto simp: slice1_def word_size of_bl_def uint_bl
+ word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
lemma slice1_up_alt':
"sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
apply (unfold slice1_def word_size of_bl_def uint_bl)
- apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
- takefill_append [symmetric])
- apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
+ apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
+ apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
(replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
apply arith
done
@@ -3346,42 +3342,40 @@
le_add_diff_inverse2 [symmetric, THEN su1]
lemma ucast_slice1: "ucast w = slice1 (size w) w"
- unfolding slice1_def ucast_bl
- by (simp add : takefill_same' word_size)
+ by (simp add: slice1_def ucast_bl takefill_same' word_size)
lemma ucast_slice: "ucast w = slice 0 w"
- unfolding slice_def by (simp add : ucast_slice1)
+ by (simp add: slice_def ucast_slice1)
lemma slice_id: "slice 0 t = t"
by (simp only: ucast_slice [symmetric] ucast_id)
-lemma revcast_slice1 [OF refl]:
- "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
- unfolding slice1_def revcast_def' by (simp add : word_size)
+lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
+ by (simp add: slice1_def revcast_def' word_size)
lemma slice1_tf_tf':
"to_bl (slice1 n w :: 'a::len0 word) =
- rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
+ rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
unfolding slice1_def by (rule word_rev_tf)
lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
lemma rev_slice1:
"n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
- slice1 n (word_reverse w :: 'b::len0 word) =
- word_reverse (slice1 k w :: 'a::len0 word)"
+ slice1 n (word_reverse w :: 'b::len0 word) =
+ word_reverse (slice1 k w :: 'a::len0 word)"
apply (unfold word_reverse_def slice1_tf_tf)
apply (rule word_bl.Rep_inverse')
apply (rule rev_swap [THEN iffD1])
apply (rule trans [symmetric])
- apply (rule tf_rev)
+ apply (rule tf_rev)
apply (simp add: word_bl.Abs_inverse)
apply (simp add: word_bl.Abs_inverse)
done
lemma rev_slice:
"n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
- slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
+ slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
apply (unfold slice_def word_size)
apply (rule rev_slice1)
apply arith
@@ -3394,8 +3388,9 @@
criterion for overflow of addition of signed integers\<close>
lemma sofl_test:
- "(sint (x :: 'a::len word) + sint y = sint (x + y)) =
- ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
+ "(sint x + sint y = sint (x + y)) =
+ ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
+ for x y :: "'a::len word"
apply (unfold word_size)
apply (cases "len_of TYPE('a)", simp)
apply (subst msb_shift [THEN sym_notr])
@@ -3406,19 +3401,19 @@
apply (unfold sint_word_ariths)
apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
apply safe
- apply (insert sint_range' [where x=x])
- apply (insert sint_range' [where x=y])
- defer
+ apply (insert sint_range' [where x=x])
+ apply (insert sint_range' [where x=y])
+ defer
+ apply (simp (no_asm), arith)
apply (simp (no_asm), arith)
+ defer
+ defer
apply (simp (no_asm), arith)
- defer
- defer
apply (simp (no_asm), arith)
- apply (simp (no_asm), arith)
- apply (rule notI [THEN notnotD],
- drule leI not_le_imp_less,
- drule sbintrunc_inc sbintrunc_dec,
- simp)+
+ apply (rule notI [THEN notnotD],
+ drule leI not_le_imp_less,
+ drule sbintrunc_inc sbintrunc_dec,
+ simp)+
done
@@ -3431,57 +3426,49 @@
"(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
map word_of_int (bin_rsplit (len_of TYPE('a::len))
(len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
- unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
+ by (simp add: word_rsplit_def word_ubin.eq_norm)
lemmas word_rsplit_no_cl [simp] = word_rsplit_no
[unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
lemma test_bit_cat:
- "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
+ "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
(if n < size b then b !! n else a !! (n - size b)))"
- apply (unfold word_cat_bin' test_bit_bin)
- apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
+ apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
apply (erule bin_nth_uint_imp)
done
lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
- apply (unfold of_bl_def to_bl_def word_cat_bin')
- apply (simp add: bl_to_bin_app_cat)
- done
+ by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
lemma of_bl_append:
"(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
- apply (unfold of_bl_def)
- apply (simp add: bl_to_bin_app_cat bin_cat_num)
+ apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
done
-lemma of_bl_False [simp]:
- "of_bl (False#xs) = of_bl xs"
- by (rule word_eqI)
- (auto simp add: test_bit_of_bl nth_append)
-
-lemma of_bl_True [simp]:
- "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
- by (subst of_bl_append [where xs="[True]", simplified])
- (simp add: word_1_bl)
-
-lemma of_bl_Cons:
- "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
+lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
+ by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
+
+lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
+ by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
+
+lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
by (cases x) simp_all
-lemma split_uint_lem: "bin_split n (uint (w :: 'a::len0 word)) = (a, b) \<Longrightarrow>
- a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
+lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
+ a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
+ for w :: "'a::len0 word"
apply (frule word_ubin.norm_Rep [THEN ssubst])
apply (drule bin_split_trunc1)
apply (drule sym [THEN trans])
- apply assumption
+ apply assumption
apply safe
done
lemma word_split_bl':
"std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
- (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
+ (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
apply (unfold word_split_bin')
apply safe
defer
@@ -3489,12 +3476,12 @@
apply hypsubst_thin
apply (drule word_ubin.norm_Rep [THEN ssubst])
apply (drule split_bintrunc)
- apply (simp add : of_bl_def bl2bin_drop word_size
- word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
+ apply (simp add: of_bl_def bl2bin_drop word_size
+ word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
apply (clarsimp split: prod.splits)
apply (frule split_uint_lem [THEN conjunct1])
apply (unfold word_size)
- apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
+ apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
defer
apply simp
apply (simp add : of_bl_def to_bl_def)
@@ -3508,30 +3495,33 @@
done
lemma word_split_bl: "std = size c - size b \<Longrightarrow>
- (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
+ (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
word_split c = (a, b)"
apply (rule iffI)
defer
apply (erule (1) word_split_bl')
apply (case_tac "word_split c")
- apply (auto simp add : word_size)
+ apply (auto simp add: word_size)
apply (frule word_split_bl' [rotated])
- apply (auto simp add : word_size)
+ apply (auto simp add: word_size)
done
lemma word_split_bl_eq:
- "(word_split (c::'a::len word) :: ('c::len0 word * 'd::len0 word)) =
- (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
- of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
+ "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
+ (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
+ of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
+ for c :: "'a::len word"
apply (rule word_split_bl [THEN iffD1])
- apply (unfold word_size)
- apply (rule refl conjI)+
+ apply (unfold word_size)
+ apply (rule refl conjI)+
done
\<comment> "keep quantifiers for use in simplification"
lemma test_bit_split':
- "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
- a !! m = (m < size a & c !! (m + size b)))"
+ "word_split c = (a, b) \<longrightarrow>
+ (\<forall>n m.
+ b !! n = (n < size b \<and> c !! n) \<and>
+ a !! m = (m < size a \<and> c !! (m + size b)))"
apply (unfold word_split_bin' test_bit_bin)
apply (clarify)
apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
@@ -3543,12 +3533,14 @@
lemma test_bit_split:
"word_split c = (a, b) \<Longrightarrow>
- (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
+ (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
+ (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
by (simp add: test_bit_split')
-lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow>
- ((ALL n::nat. b !! n = (n < size b & c !! n)) &
- (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
+lemma test_bit_split_eq:
+ "word_split c = (a, b) \<longleftrightarrow>
+ ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
+ (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
apply (rule_tac iffI)
apply (rule_tac conjI)
apply (erule test_bit_split [THEN conjunct1])
@@ -3556,28 +3548,24 @@
apply (case_tac "word_split c")
apply (frule test_bit_split)
apply (erule trans)
- apply (fastforce intro ! : word_eqI simp add : word_size)
+ apply (fastforce intro!: word_eqI simp add: word_size)
done
\<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
result to the length given by the result type\<close>
lemma word_cat_id: "word_cat a b = b"
- unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
+ by (simp add: word_cat_bin' word_ubin.inverse_norm)
\<comment> "limited hom result"
lemma word_cat_hom:
- "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE('c::len0)
- \<Longrightarrow>
- (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
- word_of_int (bin_cat w (size b) (uint b))"
- apply (unfold word_cat_def word_size)
- apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
+ "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
+ (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
+ word_of_int (bin_cat w (size b) (uint b))"
+ by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
word_ubin.eq_norm bintr_cat min.absorb1)
- done
-
-lemma word_cat_split_alt:
- "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
+
+lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
apply (rule word_eqI)
apply (drule test_bit_split)
apply (clarsimp simp add : test_bit_cat word_size)
@@ -3590,8 +3578,7 @@
subsubsection \<open>Split and slice\<close>
-lemma split_slices:
- "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
+lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
apply (drule test_bit_split)
apply (rule conjI)
apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
@@ -3617,7 +3604,7 @@
done
lemma word_split_cat_alt:
- "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
+ "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
apply (case_tac "word_split w")
apply (rule trans, assumption)
apply (drule test_bit_split)
@@ -3626,31 +3613,30 @@
done
lemmas word_cat_bl_no_bin [simp] =
- word_cat_bl [where a="numeral a" and b="numeral b",
- unfolded to_bl_numeral]
+ word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
for a b (* FIXME: negative numerals, 0 and 1 *)
lemmas word_split_bl_no_bin [simp] =
word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
-text \<open>this odd result arises from the fact that the statement of the
- result implies that the decoded words are of the same type,
- and therefore of the same length, as the original word\<close>
+text \<open>
+ This odd result arises from the fact that the statement of the
+ result implies that the decoded words are of the same type,
+ and therefore of the same length, as the original word.\<close>
lemma word_rsplit_same: "word_rsplit w = [w]"
- unfolding word_rsplit_def by (simp add : bin_rsplit_all)
-
-lemma word_rsplit_empty_iff_size:
- "(word_rsplit w = []) = (size w = 0)"
- unfolding word_rsplit_def bin_rsplit_def word_size
- by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
+ by (simp add: word_rsplit_def bin_rsplit_all)
+
+lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
+ by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
+ split: prod.split)
lemma test_bit_rsplit:
"sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
- apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
+ apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
apply (rule nth_map [symmetric])
apply simp
apply (rule bin_nth_rsplit)
@@ -3665,12 +3651,10 @@
done
lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
- unfolding word_rcat_def to_bl_def' of_bl_def
- by (clarsimp simp add : bin_rcat_bl)
-
-lemma size_rcat_lem':
- "size (concat (map to_bl wl)) = length wl * size (hd wl)"
- unfolding word_size by (induct wl) auto
+ by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
+
+lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
+ by (induct wl) (auto simp: word_size)
lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
@@ -3680,7 +3664,7 @@
"n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
rev (concat (map to_bl wl)) ! n =
rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
- apply (induct "wl")
+ apply (induct wl)
apply clarsimp
apply (clarsimp simp add : nth_append size_rcat_lem)
apply (simp (no_asm_use) only: mult_Suc [symmetric]
@@ -3690,18 +3674,16 @@
lemma test_bit_rcat:
"sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
- (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
+ (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
apply (unfold word_rcat_bl word_size)
- apply (clarsimp simp add :
- test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
+ apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
apply safe
- apply (auto simp add :
- test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
+ apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
done
-lemma foldl_eq_foldr:
- "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
- by (induct xs arbitrary: x) (auto simp add : add.assoc)
+lemma foldl_eq_foldr: "foldl op + x xs = foldr op + (x # xs) 0"
+ for x :: "'a::comm_monoid_add"
+ by (induct xs arbitrary: x) (auto simp: add.assoc)
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
@@ -3713,16 +3695,12 @@
lemma word_rsplit_len_indep [OF refl refl refl refl]:
"[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
word_rsplit v = sv \<Longrightarrow> length su = length sv"
- apply (unfold word_rsplit_def)
- apply (auto simp add : bin_rsplit_len_indep)
- done
+ by (auto simp: word_rsplit_def bin_rsplit_len_indep)
lemma length_word_rsplit_size:
"n = len_of TYPE('a::len) \<Longrightarrow>
- (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
- apply (unfold word_rsplit_def word_size)
- apply (clarsimp simp add : bin_rsplit_len_le)
- done
+ length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
+ by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
lemmas length_word_rsplit_lt_size =
length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
@@ -3730,12 +3708,12 @@
lemma length_word_rsplit_exp_size:
"n = len_of TYPE('a::len) \<Longrightarrow>
length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
- unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
+ by (auto simp: word_rsplit_def word_size bin_rsplit_len)
lemma length_word_rsplit_even_size:
"n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
length (word_rsplit w :: 'a word list) = m"
- by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
+ by (auto simp: length_word_rsplit_exp_size given_quot_alt)
lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
@@ -3745,7 +3723,7 @@
lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
apply (rule word_eqI)
- apply (clarsimp simp add : test_bit_rcat word_size)
+ apply (clarsimp simp: test_bit_rcat word_size)
apply (subst refl [THEN test_bit_rsplit])
apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
@@ -3754,22 +3732,23 @@
done
lemma size_word_rsplit_rcat_size:
- "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
- size frcw = length ws * len_of TYPE('a)\<rbrakk>
+ "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
\<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
- apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
+ for ws :: "'a::len word list" and frcw :: "'b::len0 word"
+ apply (clarsimp simp: word_size length_word_rsplit_exp_size')
apply (fast intro: given_quot_alt)
done
lemma msrevs:
- fixes n::nat
- shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
- and "(k * n + m) mod n = m mod n"
+ "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
+ "(k * n + m) mod n = m mod n"
+ for n :: nat
by (auto simp: add.commute)
lemma word_rsplit_rcat_size [OF refl]:
- "word_rcat (ws :: 'a::len word list) = frcw \<Longrightarrow>
+ "word_rcat ws = frcw \<Longrightarrow>
size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
+ for ws :: "'a::len word list"
apply (frule size_word_rsplit_rcat_size, assumption)
apply (clarsimp simp add : word_size)
apply (rule nth_equalityI, assumption)
@@ -3779,7 +3758,7 @@
apply (rule test_bit_rsplit_alt)
apply (clarsimp simp: word_size)+
apply (rule trans)
- apply (rule test_bit_rcat [OF refl refl])
+ apply (rule test_bit_rcat [OF refl refl])
apply (simp add: word_size)
apply (subst nth_rev)
apply arith
@@ -3787,8 +3766,8 @@
apply safe
apply (simp add: diff_mult_distrib)
apply (rule mpl_lem)
- apply (cases "size ws")
- apply simp_all
+ apply (cases "size ws")
+ apply simp_all
done
@@ -3798,8 +3777,7 @@
lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
-lemma rotate_eq_mod:
- "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
+lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
apply (rule box_equals)
defer
apply (rule rotate_conv_mod [symmetric])+
@@ -3817,47 +3795,42 @@
subsubsection \<open>Rotation of list to right\<close>
lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
- unfolding rotater1_def by (cases l) auto
+ by (cases l) (auto simp: rotater1_def)
lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
apply (unfold rotater1_def)
apply (cases "l")
- apply (case_tac [2] "list")
- apply auto
+ apply (case_tac [2] "list")
+ apply auto
done
lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
- unfolding rotater1_def by (cases l) auto
+ by (cases l) (auto simp: rotater1_def)
lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
- apply (cases "xs")
- apply (simp add : rotater1_def)
- apply (simp add : rotate1_rl')
- done
+ by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
- unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
+ by (induct n) (auto simp: rotater_def intro: rotater1_rev')
lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
using rotater_rev' [where xs = "rev ys"] by simp
lemma rotater_drop_take:
"rotater n xs =
- drop (length xs - n mod length xs) xs @
- take (length xs - n mod length xs) xs"
- by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
-
-lemma rotater_Suc [simp] :
- "rotater (Suc n) xs = rotater1 (rotater n xs)"
+ drop (length xs - n mod length xs) xs @
+ take (length xs - n mod length xs) xs"
+ by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
+
+lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
unfolding rotater_def by auto
lemma rotate_inv_plus [rule_format] :
- "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
- rotate k (rotater n xs) = rotate m xs &
- rotater n (rotate k xs) = rotate m xs &
+ "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
+ rotate k (rotater n xs) = rotate m xs \<and>
+ rotater n (rotate k xs) = rotate m xs \<and>
rotate n (rotater k xs) = rotater m xs"
- unfolding rotater_def rotate_def
- by (induct n) (auto intro: funpow_swap1 [THEN trans])
+ by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
@@ -3866,20 +3839,17 @@
lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
-lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
+lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
by auto
-lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
+lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
by auto
-lemma length_rotater [simp]:
- "length (rotater n xs) = length xs"
+lemma length_rotater [simp]: "length (rotater n xs) = length xs"
by (simp add : rotater_rev)
-lemma restrict_to_left:
- assumes "x = y"
- shows "(x = z) = (y = z)"
- using assms by simp
+lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
+ by simp
lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
@@ -3891,34 +3861,30 @@
subsubsection \<open>map, map2, commuting with rotate(r)\<close>
-lemma butlast_map:
- "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
+lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
by (induct xs) auto
lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
- unfolding rotater1_def
- by (cases xs) (auto simp add: last_map butlast_map)
-
-lemma rotater_map:
- "rotater n (map f xs) = map f (rotater n xs)"
- unfolding rotater_def
- by (induct n) (auto simp add : rotater1_map)
+ by (cases xs) (auto simp: rotater1_def last_map butlast_map)
+
+lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
+ by (induct n) (auto simp: rotater_def rotater1_map)
lemma but_last_zip [rule_format] :
- "ALL ys. length xs = length ys --> xs ~= [] -->
- last (zip xs ys) = (last xs, last ys) &
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (zip xs ys) = (last xs, last ys) \<and>
butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
- apply (induct "xs")
- apply auto
+ apply (induct xs)
+ apply auto
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
done
lemma but_last_map2 [rule_format] :
- "ALL ys. length xs = length ys --> xs ~= [] -->
- last (map2 f xs ys) = f (last xs) (last ys) &
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (map2 f xs ys) = f (last xs) (last ys) \<and>
butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
- apply (induct "xs")
- apply auto
+ apply (induct xs)
+ apply auto
apply (unfold map2_def)
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
done
@@ -3927,7 +3893,7 @@
"length xs = length ys \<Longrightarrow>
rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
apply (unfold rotater1_def)
- apply (cases "xs")
+ apply (cases xs)
apply auto
apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
done
@@ -3935,7 +3901,7 @@
lemma rotater1_map2:
"length xs = length ys \<Longrightarrow>
rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
- unfolding map2_def by (simp add: rotater1_map rotater1_zip)
+ by (simp add: map2_def rotater1_map rotater1_zip)
lemmas lrth =
box_equals [OF asm_rl length_rotater [symmetric]
@@ -3950,10 +3916,7 @@
lemma rotate1_map2:
"length xs = length ys \<Longrightarrow>
rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
- apply (unfold map2_def)
- apply (cases xs)
- apply (cases ys, auto)+
- done
+ by (cases xs; cases ys) (auto simp: map2_def)
lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
length_rotate [symmetric], THEN rotate1_map2]
@@ -3966,8 +3929,7 @@
\<comment> "corresponding equalities for word rotation"
-lemma to_bl_rotl:
- "to_bl (word_rotl n w) = rotate n (to_bl w)"
+lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
by (simp add: word_bl.Abs_inverse' word_rotl_def)
lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
@@ -3975,8 +3937,7 @@
lemmas word_rotl_eqs =
blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
-lemma to_bl_rotr:
- "to_bl (word_rotr n w) = rotater n (to_bl w)"
+lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
by (simp add: word_bl.Abs_inverse' word_rotr_def)
lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
@@ -3987,40 +3948,28 @@
declare word_rotr_eqs (1) [simp]
declare word_rotl_eqs (1) [simp]
-lemma
- word_rot_rl [simp]:
- "word_rotl k (word_rotr k v) = v" and
- word_rot_lr [simp]:
- "word_rotr k (word_rotl k v) = v"
+lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
+ and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
-lemma
- word_rot_gal:
- "(word_rotr n v = w) = (word_rotl n w = v)" and
- word_rot_gal':
- "(w = word_rotr n v) = (v = word_rotl n w)"
- by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
- dest: sym)
-
-lemma word_rotr_rev:
- "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
- by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
- to_bl_rotr to_bl_rotl rotater_rev)
+lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
+ and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
+ by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
+
+lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
+ by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
lemma word_roti_0 [simp]: "word_roti 0 w = w"
- by (unfold word_rot_defs) auto
+ by (auto simp: word_rot_defs)
lemmas abl_cong = arg_cong [where f = "of_bl"]
-lemma word_roti_add:
- "word_roti (m + n) w = word_roti m (word_roti n w)"
+lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
proof -
- have rotater_eq_lem:
- "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
+ have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
by auto
- have rotate_eq_lem:
- "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
+ have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
by auto
note rpts [symmetric] =
@@ -4033,17 +3982,17 @@
note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
show ?thesis
- apply (unfold word_rot_defs)
- apply (simp only: split: if_split)
- apply (safe intro!: abl_cong)
- apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
- to_bl_rotl
- to_bl_rotr [THEN word_bl.Rep_inverse']
- to_bl_rotr)
- apply (rule rrp rrrp rpts,
- simp add: nat_add_distrib [symmetric]
- nat_diff_distrib [symmetric])+
- done
+ apply (unfold word_rot_defs)
+ apply (simp only: split: if_split)
+ apply (safe intro!: abl_cong)
+ apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
+ to_bl_rotl
+ to_bl_rotr [THEN word_bl.Rep_inverse']
+ to_bl_rotr)
+ apply (rule rrp rrrp rpts,
+ simp add: nat_add_distrib [symmetric]
+ nat_diff_distrib [symmetric])+
+ done
qed
lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
@@ -4129,11 +4078,11 @@
lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
-lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
- by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
+lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
+ by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
lemma word_roti_0' [simp] : "word_roti n 0 = 0"
- unfolding word_roti_def by auto
+ by (auto simp: word_roti_def)
lemmas word_rotr_dt_no_bin' [simp] =
word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
@@ -4149,11 +4098,13 @@
subsection \<open>Maximum machine word\<close>
lemma word_int_cases:
- obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
+ fixes x :: "'a::len0 word"
+ obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
lemma word_nat_cases [cases type: word]:
- obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
+ fixes x :: "'a::len word"
+ obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
@@ -4166,62 +4117,55 @@
lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
by (subst word_uint.Abs_norm [symmetric]) simp
-lemma word_pow_0:
- "(2::'a::len word) ^ len_of TYPE('a) = 0"
+lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
proof -
have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
by (rule word_of_int_2p_len)
- thus ?thesis by (simp add: word_of_int_2p)
+ then show ?thesis by (simp add: word_of_int_2p)
qed
lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
apply (simp add: max_word_eq)
apply uint_arith
- apply auto
- apply (simp add: word_pow_0)
+ apply (auto simp: word_pow_0)
done
-lemma max_word_minus:
- "max_word = (-1::'a::len word)"
+lemma max_word_minus: "max_word = (-1::'a::len word)"
proof -
- have "-1 + 1 = (0::'a word)" by simp
- thus ?thesis by (rule max_word_wrap [symmetric])
+ have "-1 + 1 = (0::'a word)"
+ by simp
+ then show ?thesis
+ by (rule max_word_wrap [symmetric])
qed
-lemma max_word_bl [simp]:
- "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
+lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
by (subst max_word_minus to_bl_n1)+ simp
-lemma max_test_bit [simp]:
- "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
- by (auto simp add: test_bit_bl word_size)
-
-lemma word_and_max [simp]:
- "x AND max_word = x"
+lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
+ by (auto simp: test_bit_bl word_size)
+
+lemma word_and_max [simp]: "x AND max_word = x"
by (rule word_eqI) (simp add: word_ops_nth_size word_size)
-lemma word_or_max [simp]:
- "x OR max_word = max_word"
+lemma word_or_max [simp]: "x OR max_word = max_word"
by (rule word_eqI) (simp add: word_ops_nth_size word_size)
-lemma word_ao_dist2:
- "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
+lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
+ for x y z :: "'a::len0 word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-lemma word_oa_dist2:
- "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
+lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)"
+ for x y z :: "'a::len0 word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-lemma word_and_not [simp]:
- "x AND NOT x = (0::'a::len0 word)"
+lemma word_and_not [simp]: "x AND NOT x = 0"
+ for x :: "'a::len0 word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-lemma word_or_not [simp]:
- "x OR NOT x = max_word"
+lemma word_or_not [simp]: "x OR NOT x = max_word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-lemma word_boolean:
- "boolean (op AND) (op OR) bitNOT 0 max_word"
+lemma word_boolean: "boolean (op AND) (op OR) bitNOT 0 max_word"
apply (rule boolean.intro)
apply (rule word_bw_assocs)
apply (rule word_bw_assocs)
@@ -4235,48 +4179,42 @@
apply (rule word_or_not)
done
-interpretation word_bool_alg:
- boolean "op AND" "op OR" bitNOT 0 max_word
+interpretation word_bool_alg: boolean "op AND" "op OR" bitNOT 0 max_word
by (rule word_boolean)
-lemma word_xor_and_or:
- "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
+lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
+ for x y :: "'a::len0 word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-interpretation word_bool_alg:
- boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
+interpretation word_bool_alg: boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
apply (rule boolean_xor.intro)
apply (rule word_boolean)
apply (rule boolean_xor_axioms.intro)
apply (rule word_xor_and_or)
done
-lemma shiftr_x_0 [iff]:
- "(x::'a::len0 word) >> 0 = x"
+lemma shiftr_x_0 [iff]: "x >> 0 = x"
+ for x :: "'a::len0 word"
by (simp add: shiftr_bl)
-lemma shiftl_x_0 [simp]:
- "(x :: 'a::len word) << 0 = x"
+lemma shiftl_x_0 [simp]: "x << 0 = x"
+ for x :: "'a::len word"
by (simp add: shiftl_t2n)
-lemma shiftl_1 [simp]:
- "(1::'a::len word) << n = 2^n"
+lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
by (simp add: shiftl_t2n)
-lemma uint_lt_0 [simp]:
- "uint x < 0 = False"
+lemma uint_lt_0 [simp]: "uint x < 0 = False"
by (simp add: linorder_not_less)
-lemma shiftr1_1 [simp]:
- "shiftr1 (1::'a::len word) = 0"
+lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0"
unfolding shiftr1_def by simp
-lemma shiftr_1[simp]:
- "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
+lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
by (induct n) (auto simp: shiftr_def)
-lemma word_less_1 [simp]:
- "((x::'a::len word) < 1) = (x = 0)"
+lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0"
+ for x :: "'a::len word"
by (simp add: word_less_nat_alt unat_0_iff)
lemma to_bl_mask:
@@ -4287,33 +4225,29 @@
lemma map_replicate_True:
"n = length xs \<Longrightarrow>
- map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
+ map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
by (induct xs arbitrary: n) auto
lemma map_replicate_False:
- "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
+ "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
(zip xs (replicate n False)) = replicate n False"
by (induct xs arbitrary: n) auto
lemma bl_and_mask:
fixes w :: "'a::len word"
- fixes n
+ and n :: nat
defines "n' \<equiv> len_of TYPE('a) - n"
- shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
+ shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
proof -
note [simp] = map_replicate_True map_replicate_False
- have "to_bl (w AND mask n) =
- map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
+ have "to_bl (w AND mask n) = map2 op \<and> (to_bl w) (to_bl (mask n::'a::len word))"
by (simp add: bl_word_and)
- also
- have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
- also
- have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
- replicate n' False @ drop n' (to_bl w)"
- unfolding to_bl_mask n'_def map2_def
- by (subst zip_append) auto
- finally
- show ?thesis .
+ also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
+ by simp
+ also have "map2 op \<and> \<dots> (to_bl (mask n::'a::len word)) =
+ replicate n' False @ drop n' (to_bl w)"
+ unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
+ finally show ?thesis .
qed
lemma drop_rev_takefill:
@@ -4321,61 +4255,53 @@
drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
by (simp add: takefill_alt rev_take)
-lemma map_nth_0 [simp]:
- "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
+lemma map_nth_0 [simp]: "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
by (induct xs) auto
lemma uint_plus_if_size:
"uint (x + y) =
- (if uint x + uint y < 2^size x then
- uint x + uint y
- else
- uint x + uint y - 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_add_if_z
- word_size)
+ (if uint x + uint y < 2^size x
+ then uint x + uint y
+ else uint x + uint y - 2^size x)"
+ by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
lemma unat_plus_if_size:
"unat (x + (y::'a::len word)) =
- (if unat x + unat y < 2^size x then
- unat x + unat y
- else
- unat x + unat y - 2^size x)"
+ (if unat x + unat y < 2^size x
+ then unat x + unat y
+ else unat x + unat y - 2^size x)"
apply (subst word_arith_nat_defs)
apply (subst unat_of_nat)
apply (simp add: mod_nat_add word_size)
done
-lemma word_neq_0_conv:
- fixes w :: "'a::len word"
- shows "(w \<noteq> 0) = (0 < w)"
- unfolding word_gt_0 by simp
-
-lemma max_lt:
- "unat (max a b div c) = unat (max a b) div unat (c:: 'a::len word)"
+lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
+ for w :: "'a::len word"
+ by (simp add: word_gt_0)
+
+lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
+ for c :: "'a::len word"
by (fact unat_div)
lemma uint_sub_if_size:
"uint (x - y) =
- (if uint y \<le> uint x then
- uint x - uint y
- else
- uint x - uint y + 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_sub_if_z
- word_size)
-
-lemma unat_sub:
- "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
+ (if uint y \<le> uint x
+ then uint x - uint y
+ else uint x - uint y + 2^size x)"
+ by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
+
+lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
-lemma word_of_int_minus:
- "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
+lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
proof -
- have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
+ have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
+ by simp
show ?thesis
- apply (subst x)
+ apply (subst *)
apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
apply simp
done
@@ -4384,35 +4310,37 @@
lemmas word_of_int_inj =
word_uint.Abs_inject [unfolded uints_num, simplified]
-lemma word_le_less_eq:
- "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
+lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
+ for x y :: "'z::len word"
by (auto simp add: order_class.le_less)
lemma mod_plus_cong:
- assumes 1: "(b::int) = b'"
- and 2: "x mod b' = x' mod b'"
- and 3: "y mod b' = y' mod b'"
- and 4: "x' + y' = z'"
+ fixes b b' :: int
+ assumes 1: "b = b'"
+ and 2: "x mod b' = x' mod b'"
+ and 3: "y mod b' = y' mod b'"
+ and 4: "x' + y' = z'"
shows "(x + y) mod b = z' mod b'"
proof -
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
by (simp add: mod_add_eq)
also have "\<dots> = (x' + y') mod b'"
by (simp add: mod_add_eq)
- finally show ?thesis by (simp add: 4)
+ finally show ?thesis
+ by (simp add: 4)
qed
lemma mod_minus_cong:
- assumes 1: "(b::int) = b'"
- and 2: "x mod b' = x' mod b'"
- and 3: "y mod b' = y' mod b'"
- and 4: "x' - y' = z'"
+ fixes b b' :: int
+ assumes "b = b'"
+ and "x mod b' = x' mod b'"
+ and "y mod b' = y' mod b'"
+ and "x' - y' = z'"
shows "(x - y) mod b = z' mod b'"
- using 1 2 3 4 [symmetric]
- by (auto intro: mod_diff_cong)
-
-lemma word_induct_less:
- "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+ using assms [symmetric] by (auto intro: mod_diff_cong)
+
+lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+ for P :: "'a::len word \<Rightarrow> bool"
apply (cases m)
apply atomize
apply (erule rev_mp)+
@@ -4434,22 +4362,23 @@
apply simp
done
-lemma word_induct:
- "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
- by (erule word_induct_less, simp)
-
-lemma word_induct2 [induct type]:
- "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
- apply (rule word_induct, simp)
- apply (case_tac "1+n = 0", auto)
+lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+ for P :: "'a::len word \<Rightarrow> bool"
+ by (erule word_induct_less) simp
+
+lemma word_induct2 [induct type]: "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P n"
+ for P :: "'b::len word \<Rightarrow> bool"
+ apply (rule word_induct)
+ apply simp
+ apply (case_tac "1 + n = 0")
+ apply auto
done
subsection \<open>Recursion combinator for words\<close>
definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
-where
- "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
+ where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
lemma word_rec_0: "word_rec z s 0 = z"
by (simp add: word_rec_def)
@@ -4471,79 +4400,75 @@
apply simp
done
-lemma word_rec_in:
- "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
+lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
-lemma word_rec_in2:
- "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
+lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
lemma word_rec_twice:
"m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
-apply (erule rev_mp)
-apply (rule_tac x=z in spec)
-apply (rule_tac x=f in spec)
-apply (induct n)
- apply (simp add: word_rec_0)
-apply clarsimp
-apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
- apply simp
-apply (case_tac "1 + (n - m) = 0")
- apply (simp add: word_rec_0)
- apply (rule_tac f = "word_rec a b" for a b in arg_cong)
- apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
+ apply (erule rev_mp)
+ apply (rule_tac x=z in spec)
+ apply (rule_tac x=f in spec)
+ apply (induct n)
+ apply (simp add: word_rec_0)
+ apply clarsimp
+ apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
+ apply simp
+ apply (case_tac "1 + (n - m) = 0")
+ apply (simp add: word_rec_0)
+ apply (rule_tac f = "word_rec a b" for a b in arg_cong)
+ apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
+ apply simp
+ apply (simp (no_asm_use))
+ apply (simp add: word_rec_Suc word_rec_in2)
+ apply (erule impE)
+ apply uint_arith
+ apply (drule_tac x="x \<circ> op + 1" in spec)
+ apply (drule_tac x="x 0 xa" in spec)
apply simp
- apply (simp (no_asm_use))
-apply (simp add: word_rec_Suc word_rec_in2)
-apply (erule impE)
- apply uint_arith
-apply (drule_tac x="x \<circ> op + 1" in spec)
-apply (drule_tac x="x 0 xa" in spec)
-apply simp
-apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
- in subst)
- apply (clarsimp simp add: fun_eq_iff)
- apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
- apply simp
- apply (rule refl)
-apply (rule refl)
-done
+ apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
+ apply (clarsimp simp add: fun_eq_iff)
+ apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
+ apply simp
+ apply (rule refl)
+ apply (rule refl)
+ done
lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
-apply (erule rev_mp)
-apply (induct n)
- apply (auto simp add: word_rec_0 word_rec_Suc)
- apply (drule spec, erule mp)
- apply uint_arith
-apply (drule_tac x=n in spec, erule impE)
- apply uint_arith
-apply simp
-done
+ apply (erule rev_mp)
+ apply (induct n)
+ apply (auto simp add: word_rec_0 word_rec_Suc)
+ apply (drule spec, erule mp)
+ apply uint_arith
+ apply (drule_tac x=n in spec, erule impE)
+ apply uint_arith
+ apply simp
+ done
lemma word_rec_max:
"\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
-apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
- apply simp
-apply simp
-apply (rule word_rec_id_eq)
-apply clarsimp
-apply (drule spec, rule mp, erule mp)
- apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
- prefer 2
- apply assumption
- apply simp
-apply (erule contrapos_pn)
-apply simp
-apply (drule arg_cong[where f="\<lambda>x. x - n"])
-apply simp
-done
-
-lemma unatSuc:
- "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+ apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
+ apply simp
+ apply simp
+ apply (rule word_rec_id_eq)
+ apply clarsimp
+ apply (drule spec, rule mp, erule mp)
+ apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
+ prefer 2
+ apply assumption
+ apply simp
+ apply (erule contrapos_pn)
+ apply simp
+ apply (drule arg_cong[where f="\<lambda>x. x - n"])
+ apply simp
+ done
+
+lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
by unat_arith
declare bin_to_bl_def [simp]
--- a/src/Pure/General/symbol.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/General/symbol.scala Mon Mar 20 21:53:37 2017 +0100
@@ -198,6 +198,25 @@
case class Id(id: Document_ID.Generic) extends Name
case class File(name: String) extends Name
+ val encode_name: XML.Encode.T[Name] =
+ {
+ import XML.Encode._
+ variant(List(
+ { case Default => (Nil, Nil) },
+ { case Id(a) => (List(long_atom(a)), Nil) },
+ { case File(a) => (List(a), Nil) }))
+ }
+
+ val decode_name: XML.Decode.T[Name] =
+ {
+ import XML.Decode._
+ variant(List(
+ { case (Nil, Nil) => Default },
+ { case (List(a), Nil) => Id(long_atom(a)) },
+ { case (List(a), Nil) => File(a) }))
+ }
+
+
def apply(text: CharSequence): Text_Chunk =
new Text_Chunk(Text.Range(0, text.length), Index(text))
}
--- a/src/Pure/Isar/token.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/Isar/token.scala Mon Mar 20 21:53:37 2017 +0100
@@ -218,6 +218,22 @@
def reader(tokens: List[Token], start: Token.Pos): Reader =
new Token_Reader(tokens, start)
+
+
+ /* XML data representation */
+
+ val encode: XML.Encode.T[Token] = (tok: Token) =>
+ {
+ import XML.Encode._
+ pair(int, string)(tok.kind.id, tok.source)
+ }
+
+ val decode: XML.Decode.T[Token] = (body: XML.Body) =>
+ {
+ import XML.Decode._
+ val (k, s) = pair(int, string)(body)
+ Token(Kind(k), s)
+ }
}
--- a/src/Pure/PIDE/command.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/command.scala Mon Mar 20 21:53:37 2017 +0100
@@ -31,6 +31,15 @@
val empty = new Results(SortedMap.empty)
def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
+
+
+ /* XML data representation */
+
+ val encode: XML.Encode.T[Results] = (results: Results) =>
+ { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
+
+ val decode: XML.Decode.T[Results] = (body: XML.Body) =>
+ { import XML.Decode._; make(list(pair(long, tree))(body)) }
}
final class Results private(private val rep: SortedMap[Long, XML.Tree])
@@ -71,9 +80,37 @@
object Markups
{
val empty: Markups = new Markups(Map.empty)
+ def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
+ def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
- def init(markup: Markup_Tree): Markups =
- new Markups(Map(Markup_Index.markup -> markup))
+
+ /* XML data representation */
+
+ def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
+ {
+ import XML.Encode._
+
+ val markup_index: T[Markup_Index] = (index: Markup_Index) =>
+ pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
+
+ val markup_tree: T[Markup_Tree] =
+ _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
+
+ list(pair(markup_index, markup_tree))(markups.rep.toList)
+ }
+
+ val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
+ {
+ import XML.Decode._
+
+ val markup_index: T[Markup_Index] = (body: XML.Body) =>
+ {
+ val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
+ Markup_Index(status, chunk_name)
+ }
+
+ (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
+ }
}
final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
@@ -86,6 +123,17 @@
def add(index: Markup_Index, markup: Text.Markup): Markups =
new Markups(rep + (index -> (this(index) + markup)))
+ def + (entry: (Markup_Index, Markup_Tree)): Markups =
+ {
+ val (index, tree) = entry
+ new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
+ }
+
+ def ++ (other: Markups): Markups =
+ if (this eq other) this
+ else if (rep.isEmpty) other
+ else (this /: other.rep.iterator)(_ + _)
+
def redirection_iterator: Iterator[Document_ID.Generic] =
for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
yield id
@@ -114,12 +162,49 @@
object State
{
- def merge_results(states: List[State]): Command.Results =
+ def merge_results(states: List[State]): Results =
Results.merge(states.map(_.results))
+ def merge_markups(states: List[State]): Markups =
+ Markups.merge(states.map(_.markups))
+
def merge_markup(states: List[State], index: Markup_Index,
range: Text.Range, elements: Markup.Elements): Markup_Tree =
Markup_Tree.merge(states.map(_.markup(index)), range, elements)
+
+ def merge(command: Command, states: List[State]): State =
+ State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
+
+
+ /* XML data representation */
+
+ val encode: XML.Encode.T[State] = (st: State) =>
+ {
+ import XML.Encode._
+
+ val command = st.command
+ val blobs_names = command.blobs_names.map(_.node)
+ val blobs_index = command.blobs_index
+ require(command.blobs_ok)
+
+ pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
+ pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
+ (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
+ (st.status, (st.results, st.markups)))))))
+ }
+
+ def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
+ {
+ import XML.Decode._
+ val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
+ pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
+ pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
+
+ val blobs_info: Blobs_Info =
+ (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
+ val command = Command(id, node_name(node), blobs_info, span)
+ State(command, status, results, markups)
+ }
}
sealed case class State(
@@ -404,6 +489,9 @@
def blobs: List[Command.Blob] = blobs_info._1
def blobs_index: Int = blobs_info._2
+ def blobs_ok: Boolean =
+ blobs.forall({ case Exn.Res(_) => true case _ => false })
+
def blobs_names: List[Document.Node.Name] =
for (Exn.Res((name, _)) <- blobs) yield name
--- a/src/Pure/PIDE/command_span.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/command_span.scala Mon Mar 20 21:53:37 2017 +0100
@@ -56,4 +56,30 @@
def unparsed(source: String): Span =
Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+
+
+ /* XML data representation */
+
+ def encode: XML.Encode.T[Span] = (span: Span) =>
+ {
+ import XML.Encode._
+ val kind: T[Kind] =
+ variant(List(
+ { case Command_Span(a, b) => (List(a), properties(b)) },
+ { case Ignored_Span => (Nil, Nil) },
+ { case Malformed_Span => (Nil, Nil) }))
+ pair(kind, list(Token.encode))((span.kind, span.content))
+ }
+
+ def decode: XML.Decode.T[Span] = (body: XML.Body) =>
+ {
+ import XML.Decode._
+ val kind: T[Kind] =
+ variant(List(
+ { case (List(a), b) => Command_Span(a, properties(b)) },
+ { case (Nil, Nil) => Ignored_Span },
+ { case (Nil, Nil) => Malformed_Span }))
+ val (k, toks) = pair(kind, list(Token.decode))(body)
+ Span(k, toks)
+ }
}
--- a/src/Pure/PIDE/document.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/document.scala Mon Mar 20 21:53:37 2017 +0100
@@ -449,7 +449,6 @@
def node: Node
def commands_loading: List[Command]
def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
- def command_results(command: Command): Command.Results
def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
def find_command(id: Document_ID.Generic): Option[(Node, Command)]
@@ -468,6 +467,9 @@
elements: Markup.Elements,
result: List[Command.State] => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]]
+
+ def command_results(range: Text.Range): Command.Results
+ def command_results(command: Command): Command.Results
}
@@ -827,9 +829,6 @@
start <- node.command_start(cmd)
} yield convert(cmd.proper_range + start)).toList
- def command_results(command: Command): Command.Results =
- state.command_results(version, command)
-
def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
if (other_node_name.is_theory) {
val other_node = version.nodes(other_node_name)
@@ -919,6 +918,17 @@
}
+ /* command results */
+
+ def command_results(range: Text.Range): Command.Results =
+ Command.State.merge_results(
+ select[List[Command.State]](range, Markup.Elements.full, command_states =>
+ { case _ => Some(command_states) }).flatMap(_.info))
+
+ def command_results(command: Command): Command.Results =
+ state.command_results(version, command)
+
+
/* output */
override def toString: String =
--- a/src/Pure/PIDE/markup.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Mar 20 21:53:37 2017 +0100
@@ -607,6 +607,22 @@
case _ => None
}
}
+
+
+ /* XML data representation */
+
+ def encode: XML.Encode.T[Markup] = (markup: Markup) =>
+ {
+ import XML.Encode._
+ pair(string, properties)((markup.name, markup.properties))
+ }
+
+ def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
+ {
+ import XML.Decode._
+ val (name, props) = pair(string, properties)(body)
+ Markup(name, props)
+ }
}
--- a/src/Pure/PIDE/xml.ML Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/xml.ML Mon Mar 20 21:53:37 2017 +0100
@@ -52,8 +52,16 @@
val parse: string -> tree
exception XML_ATOM of string
exception XML_BODY of body
- structure Encode: XML_DATA_OPS
- structure Decode: XML_DATA_OPS
+ structure Encode:
+ sig
+ include XML_DATA_OPS
+ val tree: tree T
+ end
+ structure Decode:
+ sig
+ include XML_DATA_OPS
+ val tree: tree T
+ end
end;
structure XML: XML =
@@ -302,6 +310,8 @@
(* representation of standard types *)
+fun tree (t: tree) = [t];
+
fun properties props = [Elem ((":", props), [])];
fun string "" = []
@@ -364,6 +374,9 @@
(* representation of standard types *)
+fun tree [t] = t
+ | tree ts = raise XML_BODY ts;
+
fun properties [Elem ((":", props), [])] = props
| properties ts = raise XML_BODY ts;
--- a/src/Pure/PIDE/xml.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Mar 20 21:53:37 2017 +0100
@@ -214,6 +214,7 @@
object Encode
{
type T[A] = A => XML.Body
+ type V[A] = PartialFunction[A, (List[String], XML.Body)]
/* atomic values */
@@ -240,6 +241,8 @@
/* representation of standard types */
+ val tree: T[XML.Tree] = (t => List(t))
+
val properties: T[Properties.T] =
(props => List(XML.Elem(Markup(":", props), Nil)))
@@ -268,7 +271,7 @@
case Some(x) => List(node(f(x)))
}
- def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
+ def variant[A](fs: List[V[A]]): T[A] =
{
case x =>
val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
@@ -322,6 +325,12 @@
/* representation of standard types */
+ val tree: T[XML.Tree] =
+ {
+ case List(t) => t
+ case ts => throw new XML_Body(ts)
+ }
+
val properties: T[Properties.T] =
{
case List(XML.Elem(Markup(":", props), Nil)) => props
--- a/src/Tools/jEdit/src/document_view.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Mar 20 21:53:37 2017 +0100
@@ -213,7 +213,6 @@
val snapshot = model.snapshot()
if (changed.assignment ||
- snapshot.commands_loading.exists(changed.commands.contains) ||
(changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
text_overview.invoke()
--- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Mar 20 21:53:37 2017 +0100
@@ -353,11 +353,6 @@
else Some(Text.Info(snapshot.convert(info_range), elem))
}).headOption.map(_.info)
- def command_results(range: Text.Range): Command.Results =
- Command.State.merge_results(
- snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
- { case _ => Some(command_states) }).flatMap(_.info))
-
/* tooltips */
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 20 21:01:47 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 20 21:53:37 2017 +0100
@@ -271,7 +271,7 @@
case Some(tip) =>
val painter = text_area.getPainter
val loc = new Point(x, y + painter.getLineHeight / 2)
- val results = rendering.command_results(tip.range)
+ val results = snapshot.command_results(tip.range)
Pretty_Tooltip(view, painter, loc, rendering, results, tip)
}
}