Update Isabelle snapshots

Except RISC-V duopod, which doesn't seem to build for me at the moment

1 files changed, 76 insertions, 79 deletions

diff --git a/snapshots/isabelle/cheri/Mips_extras.thy b/snapshots/isabelle/cheri/Mips_extras.thy
index c0379d3a..387b5ea7 100644
--- a/snapshots/isabelle/cheri/Mips_extras.thy
+++ b/snapshots/isabelle/cheri/Mips_extras.thy
@@ -1,4 +1,4 @@
-chapter \<open>Generated by Lem from /auto/homes/tb592/REMS/rems/sail/mips/mips_extras.lem.\<close>
+chapter \<open>Generated by Lem from /tmp/sail/mips/mips_extras.lem.\<close>
 
 theory "Mips_extras" 
 
@@ -6,21 +6,21 @@ imports
  	 Main
 	 "Lem_pervasives" 
 	 "Lem_pervasives_extra" 
-	 "Sail_instr_kinds" 
-	 "Sail_values" 
-	 "Prompt_monad" 
-	 "Prompt" 
-	 "Sail_operators" 
+	 "Sail2_instr_kinds" 
+	 "Sail2_values" 
+	 "Sail2_prompt_monad" 
+	 "Sail2_prompt" 
+	 "Sail2_operators" 
 
 begin 
 
 (*open import Pervasives*)
 (*open import Pervasives_extra*)
-(*open import Sail_instr_kinds*)
-(*open import Sail_values*)
-(*open import Sail_operators*)
-(*open import Prompt_monad*)
-(*open import Prompt*)
+(*open import Sail2_instr_kinds*)
+(*open import Sail2_values*)
+(*open import Sail2_operators*)
+(*open import Sail2_prompt_monad*)
+(*open import Sail2_prompt*)
 
 (*val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
 (*val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
@@ -28,39 +28,39 @@ begin
 (*val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e*)
 
 definition MEMr  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad "              where 
-     " MEMr dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1             = ( read_mem 
-  dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 )"
+     " MEMr dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1             = ( read_mem 
+  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 )"
 
 definition MEMr_reserve  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad "      where 
-     " MEMr_reserve dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1     = ( read_mem 
-  dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_reserve addr size1 )"
+     " MEMr_reserve dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1     = ( read_mem 
+  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_reserve addr size1 )"
 
 
 (*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*)
 definition read_tag_bool  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow>('regval,(bool),'e)monad "  where 
-     " read_tag_bool dict_Sail_values_Bitvector_a addr = (
-  read_tag dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t . 
+     " read_tag_bool dict_Sail2_values_Bitvector_a addr = (
+  read_tag dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
   maybe_fail (''read_tag_bool'') (bool_of_bitU t)))"
 
 
 (*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*)
 definition write_tag_bool  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow>('regval,(unit),'e)monad "  where 
-     " write_tag_bool dict_Sail_values_Bitvector_a addr t = ( write_tag 
-  dict_Sail_values_Bitvector_a addr (bitU_of_bool t) \<bind>  
+     " write_tag_bool dict_Sail2_values_Bitvector_a addr t = ( write_tag 
+  dict_Sail2_values_Bitvector_a addr (bitU_of_bool t) \<bind>  
   (\<lambda>x .  (case  x of _ => return ()  )) )"
 
 
 definition MEMr_tag  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad "  where 
-     " MEMr_tag dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = (
-  read_mem dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
-  read_tag_bool dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t . 
+     " MEMr_tag dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
+  read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
+  read_tag_bool dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
   return (t, v))))"
 
 
 definition MEMr_tag_reserve  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad "  where 
-     " MEMr_tag_reserve dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = (
-  read_mem dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
-  read_tag_bool dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t . 
+     " MEMr_tag_reserve dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
+  read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
+  read_tag_bool dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
   return (t, v))))"
 
 
@@ -71,21 +71,21 @@ definition MEMr_tag_reserve  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_
 (*val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
 
 definition MEMea  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "                  where 
-     " MEMea dict_Sail_values_Bitvector_a addr size1                 = ( write_mem_ea 
-  dict_Sail_values_Bitvector_a Write_plain addr size1 )"
+     " MEMea dict_Sail2_values_Bitvector_a addr size1                 = ( write_mem_ea 
+  dict_Sail2_values_Bitvector_a Write_plain addr size1 )"
 
 definition MEMea_conditional  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "      where 
-     " MEMea_conditional dict_Sail_values_Bitvector_a addr size1     = ( write_mem_ea 
-  dict_Sail_values_Bitvector_a Write_conditional addr size1 )"
+     " MEMea_conditional dict_Sail2_values_Bitvector_a addr size1     = ( write_mem_ea 
+  dict_Sail2_values_Bitvector_a Write_conditional addr size1 )"
 
 
 definition MEMea_tag  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "              where 
-     " MEMea_tag dict_Sail_values_Bitvector_a addr size1             = ( write_mem_ea 
-  dict_Sail_values_Bitvector_a Write_plain addr size1 )"
+     " MEMea_tag dict_Sail2_values_Bitvector_a addr size1             = ( write_mem_ea 
+  dict_Sail2_values_Bitvector_a Write_plain addr size1 )"
 
 definition MEMea_tag_conditional  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "  where 
-     " MEMea_tag_conditional dict_Sail_values_Bitvector_a addr size1 = ( write_mem_ea 
-  dict_Sail_values_Bitvector_a Write_conditional addr size1 )"
+     " MEMea_tag_conditional dict_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea 
+  dict_Sail2_values_Bitvector_a Write_conditional addr size1 )"
 
 
 
@@ -95,25 +95,25 @@ definition MEMea_tag_conditional  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rig
 (*val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e*)
 
 definition MEMval  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad "                       where 
-     " MEMval dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 v                      = ( write_mem_val 
-  dict_Sail_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of _ => return ()  )) )"
+     " MEMval dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v                      = ( write_mem_val 
+  dict_Sail2_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of _ => return ()  )) )"
 
 definition MEMval_conditional  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad "           where 
-     " MEMval_conditional dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 v          = ( write_mem_val 
-  dict_Sail_values_Bitvector_b v \<bind> (\<lambda> b .  return (if b then True else False)))"
+     " MEMval_conditional dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v          = ( write_mem_val 
+  dict_Sail2_values_Bitvector_b v \<bind> (\<lambda> b .  return (if b then True else False)))"
 
 definition MEMval_tag  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad "              where 
-     " MEMval_tag dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 t v             = ( write_mem_val 
-  dict_Sail_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of
-                    _ => write_tag_bool dict_Sail_values_Bitvector_a addr t
+     " MEMval_tag dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v             = ( write_mem_val 
+  dict_Sail2_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of
+                    _ => write_tag_bool dict_Sail2_values_Bitvector_a addr t
                            \<bind>
                            (\<lambda>x .  (case  x of _ => return ()  ))
                 )) )"
 
 definition MEMval_tag_conditional  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad "  where 
-     " MEMval_tag_conditional dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 t v = ( write_mem_val 
-  dict_Sail_values_Bitvector_b v \<bind> (\<lambda> b .  write_tag_bool 
-  dict_Sail_values_Bitvector_a addr t \<bind>  (\<lambda>x .  (case  x of _ => return (if b then True else False) ))))"
+     " MEMval_tag_conditional dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v = ( write_mem_val 
+  dict_Sail2_values_Bitvector_b v \<bind> (\<lambda> b .  write_tag_bool 
+  dict_Sail2_values_Bitvector_a addr t \<bind>  (\<lambda>x .  (case  x of _ => return (if b then True else False) ))))"
 
 
 (*val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e*)
@@ -135,62 +135,45 @@ definition get_slice_int_bl  :: " int \<Rightarrow> int \<Rightarrow> int \<Righ
 
 (*val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
 definition get_slice_int0  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a "  where 
-     " get_slice_int0 dict_Sail_values_Bitvector_a len n lo = (
-  (of_bools_method   dict_Sail_values_Bitvector_a) (get_slice_int_bl len n lo))"
+     " get_slice_int0 dict_Sail2_values_Bitvector_a len n lo = (
+  (of_bools_method   dict_Sail2_values_Bitvector_a) (get_slice_int_bl len n lo))"
 
 
 definition write_ram  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>('d,(unit),'c)monad "  where 
-     " write_ram dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 _ addr data = (
-  MEMea dict_Sail_values_Bitvector_b addr size1 \<then>
-  MEMval dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a addr size1 data )"
+     " write_ram dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 _ addr data = (
+  MEMea dict_Sail2_values_Bitvector_b addr size1 \<then>
+  MEMval dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a addr size1 data )"
 
 
 definition read_ram  :: " 'a Bitvector_class \<Rightarrow> 'c Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'a \<Rightarrow>('d,'c,'b)monad "  where 
-     " read_ram dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_c _ size1 _ addr = ( MEMr 
-  dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_c addr size1 )"
+     " read_ram dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c _ size1 _ addr = ( MEMr 
+  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c addr size1 )"
 
 
-definition string_of_bits  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> string "  where 
-     " string_of_bits dict_Sail_values_Bitvector_a bs = ( string_of_bv 
-  (instance_Sail_values_Bitvector_list_dict
-     instance_Sail_values_BitU_Sail_values_bitU_dict) ((bits_of_method   dict_Sail_values_Bitvector_a) bs))"
-
 definition string_of_int  :: " 'a Show_class \<Rightarrow> 'a \<Rightarrow> string "  where 
      " string_of_int dict_Show_Show_a = ((show_method   dict_Show_Show_a))"
 
 
-definition sign_extend0  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b "  where 
-     " sign_extend0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b bits len = ( maybe_failwith (
-  (of_bits_method   dict_Sail_values_Bitvector_b) (exts_bv dict_Sail_values_Bitvector_a len bits)))"
-
-definition zero_extend0  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b "  where 
-     " zero_extend0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b bits len = ( maybe_failwith (
-  (of_bits_method   dict_Sail_values_Bitvector_b) (extz_bv dict_Sail_values_Bitvector_a len bits)))"
-
-
 definition shift_bits_left  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
-     " shift_bits_left dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+     " shift_bits_left dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
   (let r = (Option.bind (
-  (unsigned_method   dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail_values_Bitvector_b) (shiftl_bv dict_Sail_values_Bitvector_d v n))) in
+  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (shiftl_bv dict_Sail2_values_Bitvector_d v n))) in
   maybe_fail (''shift_bits_left'') r))"
 
 definition shift_bits_right  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
-     " shift_bits_right dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+     " shift_bits_right dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
   (let r = (Option.bind (
-  (unsigned_method   dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail_values_Bitvector_b) (shiftr_bv dict_Sail_values_Bitvector_d v n))) in
+  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (shiftr_bv dict_Sail2_values_Bitvector_d v n))) in
   maybe_fail (''shift_bits_right'') r))"
 
 definition shift_bits_right_arith  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
-     " shift_bits_right_arith dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+     " shift_bits_right_arith dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
   (let r = (Option.bind (
-  (unsigned_method   dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail_values_Bitvector_b) (arith_shiftr_bv dict_Sail_values_Bitvector_d v n))) in
+  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (arith_shiftr_bv dict_Sail2_values_Bitvector_d v n))) in
   maybe_fail (''shift_bits_right_arith'') r))"
 
 
 (* Use constants for undefined values for now *)
-definition internal_pick  :: " 'a list \<Rightarrow>('c,'a,'b)monad "  where 
-     " internal_pick vs = ( return (List.hd vs))"
-
 definition undefined_string  :: " unit \<Rightarrow>('b,(string),'a)monad "  where 
      " undefined_string _ = ( return (''''))"
 
@@ -206,13 +189,13 @@ definition undefined_vector  :: " int \<Rightarrow> 'a \<Rightarrow>('rv,('a lis
 
 (*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
 definition undefined_bitvector  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad "  where 
-     " undefined_bitvector dict_Sail_values_Bitvector_a len = ( return (
-  (of_bools_method   dict_Sail_values_Bitvector_a) (repeat [False] len)))"
+     " undefined_bitvector dict_Sail2_values_Bitvector_a len = ( return (
+  (of_bools_method   dict_Sail2_values_Bitvector_a) (repeat [False] len)))"
 
 (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
 definition undefined_bits  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad "  where 
-     " undefined_bits dict_Sail_values_Bitvector_a = ( 
-  undefined_bitvector dict_Sail_values_Bitvector_a )"
+     " undefined_bits dict_Sail2_values_Bitvector_a = ( 
+  undefined_bitvector dict_Sail2_values_Bitvector_a )"
 
 definition undefined_bit  :: " unit \<Rightarrow>('b,(bitU),'a)monad "  where 
      " undefined_bit _ = ( return B0 )"
@@ -240,12 +223,26 @@ definition elf_entry  :: " unit \<Rightarrow> int "  where
 
 
 definition print_bits  :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit "  where 
-     " print_bits dict_Sail_values_Bitvector_a msg bs = ( prerr_endline (msg @ (string_of_bits 
-  dict_Sail_values_Bitvector_a bs)))"
+     " print_bits dict_Sail2_values_Bitvector_a msg bs = ( print_endline (msg @ (string_of_bv 
+  dict_Sail2_values_Bitvector_a bs)))"
+
+definition prerr_bits  :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit "  where 
+     " prerr_bits dict_Sail2_values_Bitvector_a msg bs = ( prerr_endline (msg @ (string_of_bv 
+  dict_Sail2_values_Bitvector_a bs)))"
+
+
+(*val prerr_string : string -> unit*)
+definition prerr_string  :: " string \<Rightarrow> unit "  where 
+     " prerr_string _ = ( ()  )"
 
 
 (*val get_time_ns : unit -> integer*)
 definition get_time_ns  :: " unit \<Rightarrow> int "  where 
      " get_time_ns _ = (( 0 :: int))"
 
+
+(*val cycle_count : unit -> unit*)
+definition cycle_count  :: " unit \<Rightarrow> unit "  where 
+     " cycle_count _ = ( ()  )"
+
 end