Tune Lem pretty-printing

In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.

2 files changed, 50 insertions, 7 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index 56aa6e87..84f3333e 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -4,6 +4,11 @@ theory Prompt_monad_lemmas
     Sail_values_lemmas
 begin
 
+notation bind (infixr "\<bind>" 54)
+
+abbreviation seq :: "('rv,unit,'e)monad \<Rightarrow> ('rv,'b,'e)monad \<Rightarrow>('rv,'b,'e)monad" (infixr "\<then>" 54) where
+  "m \<then> n \<equiv> m \<bind> (\<lambda>_. n)"
+
 lemma All_bind_dom: "bind_dom (m, f)"
   by (induction m) (auto intro: bind.domintros)
 
diff --git a/lib/isabelle/Sail_values_lemmas.thy b/lib/isabelle/Sail_values_lemmas.thy
index df2fc808..256e76d0 100644
--- a/lib/isabelle/Sail_values_lemmas.thy
+++ b/lib/isabelle/Sail_values_lemmas.thy
@@ -44,7 +44,7 @@ abbreviation "BC_bitU_list \<equiv> instance_Sail_values_Bitvector_list_dict ins
 lemmas BC_bitU_list_def = instance_Sail_values_Bitvector_list_dict_def instance_Sail_values_BitU_Sail_values_bitU_dict_def
 abbreviation "BC_mword \<equiv> instance_Sail_values_Bitvector_Machine_word_mword_dict"
 lemmas BC_mword_defs = instance_Sail_values_Bitvector_Machine_word_mword_dict_def
-  length_mword_def access_mword_def access_mword_inc_def access_mword_dec_def
+  access_mword_def access_mword_inc_def access_mword_dec_def
   (*update_mword_def update_mword_inc_def update_mword_dec_def*)
   subrange_list_def subrange_list_inc_def subrange_list_dec_def
   update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def
@@ -60,7 +60,8 @@ lemma nat_of_bits_aux_bl_to_bin_aux:
   by (induction acc bs rule: nat_of_bools_aux.induct)
      (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits)
 
-lemma nat_of_bits_bl_to_bin[simp]: "nat_of_bools bs = nat (bl_to_bin bs)"
+lemma nat_of_bits_bl_to_bin[simp]:
+  "nat_of_bools bs = nat (bl_to_bin bs)"
   by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux)
 
 lemma unsigned_bits_of_mword[simp]:
@@ -72,18 +73,55 @@ lemma bits_of_bitU_list[simp]:
   "of_bits_method BC_bitU_list v = Some v"
   by (auto simp: BC_bitU_list_def)
 
+lemma subrange_list_inc_drop_take:
+  "subrange_list_inc xs i j = drop (nat i) (take (nat (j + 1)) xs)"
+  by (auto simp: subrange_list_inc_def split_at_def)
+
+lemma subrange_list_dec_drop_take:
+  assumes "i \<ge> 0" and "j \<ge> 0"
+  shows "subrange_list_dec xs i j = drop (length xs - nat (i + 1)) (take (length xs - nat j) xs)"
+  using assms unfolding subrange_list_dec_def
+  by (auto simp: subrange_list_inc_drop_take add.commute diff_diff_add nat_minus_as_int)
+
+lemma update_subrange_list_inc_drop_take:
+  assumes "i \<ge> 0" and "j \<ge> i"
+  shows "update_subrange_list_inc xs i j xs' = take (nat i) xs @ xs' @ drop (nat (j + 1)) xs"
+  using assms unfolding update_subrange_list_inc_def
+  by (auto simp: split_at_def min_def)
+
+lemma update_subrange_list_dec_drop_take:
+  assumes "j \<ge> 0" and "i \<ge> j"
+  shows "update_subrange_list_dec xs i j xs' = take (length xs - nat (i + 1)) xs @ xs' @ drop (length xs - nat j) xs"
+  using assms unfolding update_subrange_list_dec_def update_subrange_list_inc_def
+  by (auto simp: split_at_def min_def Let_def add.commute diff_diff_add nat_minus_as_int)
+
+declare access_list_inc_def[simp]
+
+lemma access_list_dec_nth:
+  assumes "0 \<le> i"
+  shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))"
+  using assms
+  by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int)
+
 lemma access_list_dec_rev_nth:
-  assumes "0 \<le> i" and "nat i < size xs"
+  assumes "0 \<le> i" and "nat i < length xs"
   shows "access_list_dec xs i = rev xs ! (nat i)"
   using assms
-  by (auto simp: access_list_dec_def access_list_inc_def length_list_def rev_nth
-           intro!: arg_cong2[where f = List.nth])
+  by (auto simp: access_list_dec_def rev_nth intro!: arg_cong2[where f = List.nth])
 
 lemma access_bv_dec_mword[simp]:
   fixes w :: "('a::len) word"
   assumes "0 \<le> n" and "nat n < LENGTH('a)"
   shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))"
-  using assms
-  by (auto simp: access_bv_dec_def access_list_def access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl word_size)
+  using assms unfolding access_bv_dec_def access_list_def
+  by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl word_size)
+
+lemma update_list_inc_update[simp]:
+  "update_list_inc xs n x = xs[nat n := x]"
+  by (auto simp: update_list_inc_def)
+
+lemma update_list_dec_update:
+  "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]"
+  by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int)
 
 end