Skip to content
Permalink
Browse files

Update for changes to HOL's Unicode settings

  • Loading branch information...
myreen committed Jul 9, 2019
1 parent c4c57f1 commit 2355372f96a49914638ab924f5f5571cc747b253
@@ -527,7 +527,7 @@ Proof
(unabbrev_all_tac \\ fs [WORD_LEFT_ADD_DISTRIB,GSYM word_add_n2w] \\ NO_TAC)
\\ fs [] \\ pop_assum kall_tac
\\ fs [store_list_def,FOUR_MUL_LSL]
\\ `(n2w i ≪ (dimindex (:α) − (c.len_size + 2) + 2) make_header c 2w 0) =
\\ `(n2w i ≪ (dimindex (:α) − (c.len_size + 2) + 2) || make_header c 2w 0) =
make_header c 2w i:'a word` by
(fs [make_header_def,WORD_MUL_LSL,word_mul_n2w,LEFT_ADD_DISTRIB]
\\ rpt (AP_TERM_TAC ORELSE AP_THM_TAC)
@@ -256,7 +256,7 @@ Proof
\\ once_rewrite_tac [multiwordTheory.mw_cmp_def] \\ fs []
\\ once_rewrite_tac [multiwordTheory.mw_cmp_def] \\ fs []
\\ qabbrev_tac `n2' = n2 ⋙ 1`
\\ qabbrev_tac `n1' = (n2 ≪ (dimindex (:α) − 1) n1 ⋙ 1)`
\\ qabbrev_tac `n1' = (n2 ≪ (dimindex (:α) − 1) || n1 ⋙ 1)`
\\ rewrite_tac [LongDiv1_code_def]
\\ fs [eq_eval,word_add_n2w]
\\ once_rewrite_tac [list_Seq_def] \\ fs [eq_eval]
@@ -723,7 +723,7 @@ val can_select_def = Define `

Theorem read_length_lemma:
can_select (n+2) 2 (n2w k :'a word) ==>
(((n + 1 -- 2) (h ≪ (2 + n) n2w k ≪ 2 3w)) = n2w k :'a word)
(((n + 1 -- 2) (h ≪ (2 + n) || n2w k ≪ 2 || 3w)) = n2w k :'a word)
Proof
full_simp_tac(srw_ss())[word_bits_eq_slice_shift,word_slice_or,can_select_def,DECIDE ``n+2-1=n+1n``]
\\ full_simp_tac(srw_ss())[DECIDE ``2+n=n+1+1n``,word_slice_lsl_eq_0,word_slice_2_3_eq_0]
@@ -5773,7 +5773,7 @@ val make_header_and_2 = Q.prove(
Theorem encode_header_tag_mask:
encode_header c (4 * tag) n = SOME (w:'a word) /\ good_dimindex (:'a) ==>
tag < dimword (:α) DIV 16 /\
(w && (tag_mask c 2w)) = n2w (16 * tag + 2)
(w && (tag_mask c || 2w)) = n2w (16 * tag + 2)
Proof
strip_tac \\ fs [encode_header_def,WORD_LEFT_AND_OVER_OR]
\\ rw [make_header_and_2]
@@ -6726,9 +6726,9 @@ Theorem memory_rel_Number_bignum_header:
~small_int (:'a) i /\ good_dimindex (:'a) ==>
?ff w x a y.
v = Word w /\ get_real_addr c st w = SOME a /\
IS_SOME ((encode_header c (w2n ((b2w (i < 0) ≪ 2 3w):'a word))
IS_SOME ((encode_header c (w2n ((b2w (i < 0) ≪ 2 || 3w):'a word))
(LENGTH (n2mw (Num (ABS i)):'a word list))):'a word option) /\
m a = Word (make_header c (b2w (i < 0) ≪ 2 3w)
m a = Word (make_header c (b2w (i < 0) ≪ 2 || 3w)
(LENGTH (n2mw (Num (ABS i)):'a word list)))
Proof
fs[memory_rel_def,word_ml_inv_def,PULL_EXISTS,abs_ml_inv_def,
@@ -8096,8 +8096,8 @@ val fix_clock_IMP = prove(

val word_is_clos_def = Define `
word_is_clos c h <=>
(h && (tag_mask c 2w)) = n2w (16 * closure_tag + 2) \/
(h && (tag_mask c 2w)) = n2w (16 * partial_app_tag + 2)`;
(h && (tag_mask c || 2w)) = n2w (16 * closure_tag + 2) \/
(h && (tag_mask c || 2w)) = n2w (16 * partial_app_tag + 2)`;

val word_eq_def = tDefine "word_eq" `
(word_eq c st dm m l w1 (w2:'a word) =
@@ -8767,7 +8767,7 @@ Proof
\\ fs [bignum_words_def,i2mw_def]
\\ rpt_drule memory_rel_Number_bignum_header
\\ strip_tac \\ fs []
\\ `(w2n (b2w (i < 0) ≪ 2 3w:'a word)) = if i < 0 then 7 else 3` by
\\ `(w2n (b2w (i < 0) ≪ 2 || 3w:'a word)) = if i < 0 then 7 else 3` by
(Cases_on `i < 0i` \\ fs [] \\ EVAL_TAC
\\ fs [good_dimindex_def,dimword_def] \\ NO_TAC)
\\ fs []
@@ -1245,21 +1245,21 @@ QED

val dimword_eq_32_imp_or_bytes = Q.prove(
`dimindex (:'a) = 32 ==>
(w2w ((w2w (x:'a word)):word8)
w2w ((w2w (x ⋙ 8)):word8) ≪ 8
w2w ((w2w (x ⋙ 16)):word8) ≪ 16
(w2w ((w2w (x:'a word)):word8) ||
w2w ((w2w (x ⋙ 8)):word8) ≪ 8 ||
w2w ((w2w (x ⋙ 16)):word8) ≪ 16 ||
w2w ((w2w (x ⋙ 24)):word8) ≪ 24) = x`,
srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] [])

val dimword_eq_64_imp_or_bytes = Q.prove(
`dimindex (:'a) = 64 ==>
(w2w ((w2w (x:'a word)):word8)
w2w ((w2w (x ⋙ 8)):word8) ≪ 8
w2w ((w2w (x ⋙ 16)):word8) ≪ 16
w2w ((w2w (x ⋙ 24)):word8) ≪ 24
w2w ((w2w (x ⋙ 32)):word8) ≪ 32
w2w ((w2w (x ⋙ 40)):word8) ≪ 40
w2w ((w2w (x ⋙ 48)):word8) ≪ 48
(w2w ((w2w (x:'a word)):word8) ||
w2w ((w2w (x ⋙ 8)):word8) ≪ 8 ||
w2w ((w2w (x ⋙ 16)):word8) ≪ 16 ||
w2w ((w2w (x ⋙ 24)):word8) ≪ 24 ||
w2w ((w2w (x ⋙ 32)):word8) ≪ 32 ||
w2w ((w2w (x ⋙ 40)):word8) ≪ 40 ||
w2w ((w2w (x ⋙ 48)):word8) ≪ 48 ||
w2w ((w2w (x ⋙ 56)):word8) ≪ 56) = x`,
srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] [])

@@ -4374,7 +4374,7 @@ val word_gen_gc_move_loop_code_thm = Q.prove(
(7,Word (-1w * pb' + pbx')) |+
(8,Word pax) |+
(5,Word (-1w * pa' + pax)) |+
(7,Word (-1w * pa' + pax -1w * pb' + pb)) ;
(7,Word (-1w * pa' + pax || -1w * pb' + pb)) ;
store := s2.store |+ (Temp 4w,Word pb) |>`
\\ `s1.mdomain = s4.mdomain /\ m' = s4.memory` by
(unabbrev_all_tac \\ fs [] \\ NO_TAC) \\ fs []

0 comments on commit 2355372

Please sign in to comment.
You can’t perform that action at this time.