x64: configure arch-specific array types
This commit is contained in:
Matthew Brecknell
parent
ce748b7522
commit
2f4b822da9
|
|
@ -845,15 +845,15 @@ lemma heap_update_Array_element'':
|
|||
lemmas heap_update_Array_element'
|
||||
= heap_update_Array_element''[simplified array_ptr_index_simps]
|
||||
|
||||
lemma fourthousand_size:
|
||||
"CARD('b :: fourthousand_count) * size_of TYPE('a :: oneMB_size) < 2 ^ 32"
|
||||
using oneMB_size_ax[where 'a='a] fourthousand_count_ax[where 'a='b]
|
||||
lemma array_count_size:
|
||||
"CARD('b :: array_max_count) * size_of TYPE('a :: array_outer_max_size) < 2 ^ 32"
|
||||
using array_outer_max_size_ax[where 'a='a] array_max_count_ax[where 'a='b]
|
||||
apply (clarsimp dest!: nat_le_Suc_less_imp)
|
||||
apply (drule(1) mult_mono, simp+)
|
||||
done
|
||||
|
||||
lemmas heap_update_Array_element
|
||||
= heap_update_Array_element'[OF refl _ fourthousand_size]
|
||||
= heap_update_Array_element'[OF refl _ array_count_size]
|
||||
|
||||
lemma typ_slice_list_cut:
|
||||
"\<lbrakk> (\<forall>x \<in> set xs. size_td (dt_fst x) = m); m \<noteq> 0; n < (length xs * m) \<rbrakk>
|
||||
|
|
|
|||
|
|
@ -412,7 +412,7 @@ lemma c_guard_array_c_guard:
|
|||
lemma c_guard_array_field:
|
||||
assumes parent_cguard: "c_guard (p :: 'a :: mem_type ptr)"
|
||||
and subfield: "field_ti TYPE('a :: mem_type) f = Some t"
|
||||
and type_match: "export_uinfo t = export_uinfo (typ_info_t TYPE(('b :: oneMB_size, 'c :: fourthousand_count) array))"
|
||||
and type_match: "export_uinfo t = export_uinfo (typ_info_t TYPE(('b :: array_outer_max_size, 'c :: array_max_count) array))"
|
||||
shows "c_guard (Ptr &(p\<rightarrow>f) :: 'b ptr)"
|
||||
by (metis c_guard_array_c_guard c_guard_field parent_cguard ptr_coerce.simps subfield type_match)
|
||||
|
||||
|
|
|
|||
|
|
@ -32,9 +32,9 @@ lemma globals_update_eq_iff:
|
|||
apply (rule state.fold_congs, simp+)
|
||||
done
|
||||
|
||||
instance ptr :: (c_type)oneMB_packed ..
|
||||
instance tcb_queue_C :: oneMB_packed ..
|
||||
instance region_C :: oneMB_packed ..
|
||||
instance ptr :: (c_type)array_outer_packed ..
|
||||
instance tcb_queue_C :: array_outer_packed ..
|
||||
instance region_C :: array_outer_packed ..
|
||||
|
||||
locale graph_refine_locale = kernel_all_substitute
|
||||
+ assumes globals_list_distinct:
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ begin
|
|||
|
||||
declare word_neq_0_conv [simp del]
|
||||
|
||||
instance cte_C :: oneMB_size
|
||||
instance cte_C :: array_outer_max_size
|
||||
by intro_classes simp
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
|
|
|||
|
|
@ -674,11 +674,11 @@ lemma struct_rewrite_guard_c_guard_field [heap_abs]:
|
|||
(\<lambda>s. c_guard (Ptr (field_lvalue (p s :: 'a ptr) field_name) :: 'f ptr))"
|
||||
by (simp add: valid_struct_field_def struct_rewrite_expr_def struct_rewrite_guard_def)
|
||||
|
||||
lemma align_of_array: "align_of TYPE(('a :: oneMB_size)['b' :: fourthousand_count]) = align_of TYPE('a)"
|
||||
lemma align_of_array: "align_of TYPE(('a :: array_outer_max_size)['b' :: array_max_count]) = align_of TYPE('a)"
|
||||
by (simp add: align_of_def align_td_array)
|
||||
|
||||
lemma c_guard_array:
|
||||
"\<lbrakk> 0 \<le> k; nat k < CARD('b); c_guard (p :: (('a::oneMB_size)['b::fourthousand_count]) ptr) \<rbrakk>
|
||||
"\<lbrakk> 0 \<le> k; nat k < CARD('b); c_guard (p :: (('a::array_outer_max_size)['b::array_max_count]) ptr) \<rbrakk>
|
||||
\<Longrightarrow> c_guard (ptr_coerce p +\<^sub>p k :: 'a ptr)"
|
||||
apply (clarsimp simp: ptr_add_def c_guard_def c_null_guard_def)
|
||||
apply (rule conjI[rotated])
|
||||
|
|
@ -698,7 +698,7 @@ lemma c_guard_array:
|
|||
done
|
||||
|
||||
lemma struct_rewrite_guard_c_guard_Array_field [heap_abs]:
|
||||
"\<lbrakk> valid_struct_field st field_name (field_getter :: ('a :: packed_type) \<Rightarrow> ('f::oneMB_packed ['n::fourthousand_count])) field_setter t_hrs t_hrs_update;
|
||||
"\<lbrakk> valid_struct_field st field_name (field_getter :: ('a :: packed_type) \<Rightarrow> ('f::array_outer_packed ['n::array_max_count])) field_setter t_hrs t_hrs_update;
|
||||
struct_rewrite_expr P p' p;
|
||||
struct_rewrite_guard Q (\<lambda>s. c_guard (p' s)) \<rbrakk> \<Longrightarrow>
|
||||
struct_rewrite_guard (\<lambda>s. P s \<and> Q s \<and> 0 \<le> k \<and> nat k < CARD('n))
|
||||
|
|
@ -764,7 +764,7 @@ lemma struct_rewrite_expr_field [heap_abs]:
|
|||
(* Descend into struct fields that are themselves arrays. *)
|
||||
lemma struct_rewrite_expr_Array_field [heap_abs]:
|
||||
"\<lbrakk> valid_struct_field st field_name
|
||||
(field_getter :: ('a :: packed_type) \<Rightarrow> 'f::oneMB_packed ['n::fourthousand_count])
|
||||
(field_getter :: ('a :: packed_type) \<Rightarrow> 'f::array_outer_packed ['n::array_max_count])
|
||||
field_setter t_hrs t_hrs_update;
|
||||
struct_rewrite_expr P p' p;
|
||||
struct_rewrite_expr Q a (\<lambda>s. h_val (hrs_mem (t_hrs s)) (p' s)) \<rbrakk>
|
||||
|
|
@ -819,9 +819,9 @@ lemma heap_update_field_unpacked:
|
|||
|
||||
(* \<approx> heap_update_Array_element. Would want this for struct_rewrite_modifies_Array_field. *)
|
||||
lemma heap_update_Array_element_unpacked:
|
||||
"n < CARD('b::fourthousand_count) \<Longrightarrow>
|
||||
"n < CARD('b::array_max_count) \<Longrightarrow>
|
||||
heap_update (ptr_coerce p' +\<^sub>p int n) w hp =
|
||||
heap_update (p'::('a::oneMB_size['b::fourthousand_count]) ptr)
|
||||
heap_update (p'::('a::array_outer_max_size['b::array_max_count]) ptr)
|
||||
(Arrays.update (h_val hp p') n w) hp"
|
||||
oops
|
||||
|
||||
|
|
@ -918,7 +918,7 @@ lemma struct_rewrite_modifies_field__unused:
|
|||
done
|
||||
|
||||
lemma struct_rewrite_modifies_Array_field__unused:
|
||||
"\<lbrakk> valid_struct_field (st :: 's \<Rightarrow> 't) field_name (field_getter :: ('a::packed_type) \<Rightarrow> (('f::oneMB_packed)['n::fourthousand_count])) field_setter t_hrs t_hrs_update;
|
||||
"\<lbrakk> valid_struct_field (st :: 's \<Rightarrow> 't) field_name (field_getter :: ('a::packed_type) \<Rightarrow> (('f::array_outer_packed)['n::array_max_count])) field_setter t_hrs t_hrs_update;
|
||||
struct_rewrite_expr P p' p;
|
||||
struct_rewrite_expr Q f' f;
|
||||
struct_rewrite_modifies R
|
||||
|
|
@ -1021,7 +1021,7 @@ lemma struct_rewrite_modifies_field [heap_abs]:
|
|||
|
||||
(* FIXME: this is nearly a duplicate. Would a standalone array rule work instead? *)
|
||||
lemma struct_rewrite_modifies_Array_field [heap_abs]:
|
||||
"\<lbrakk> valid_struct_field (st :: 's \<Rightarrow> 't) field_name (field_getter :: ('a::packed_type) \<Rightarrow> (('f::oneMB_packed)['n::fourthousand_count])) field_setter t_hrs t_hrs_update;
|
||||
"\<lbrakk> valid_struct_field (st :: 's \<Rightarrow> 't) field_name (field_getter :: ('a::packed_type) \<Rightarrow> (('f::array_outer_packed)['n::array_max_count])) field_setter t_hrs t_hrs_update;
|
||||
struct_rewrite_expr P p' p;
|
||||
struct_rewrite_expr Q f' f;
|
||||
\<And>s. heap_lift__wrap_h_val (h_val_p' s) (h_val (hrs_mem (t_hrs s)) (p' s));
|
||||
|
|
@ -1385,7 +1385,7 @@ lemma heap_abs_expr_c_guard_array [heap_abs]:
|
|||
abs_expr st P x' (\<lambda>s. ptr_coerce (x s) :: 'a ptr) \<rbrakk> \<Longrightarrow>
|
||||
abs_guard st
|
||||
(\<lambda>s. P s \<and> (\<forall>a \<in> set (array_addrs (x' s) CARD('b)). vgetter s a))
|
||||
(\<lambda>s. c_guard (x s :: ('a::oneMB_size, 'b::fourthousand_count) array ptr))"
|
||||
(\<lambda>s. c_guard (x s :: ('a::array_outer_max_size, 'b::array_max_count) array ptr))"
|
||||
apply (clarsimp simp: abs_expr_def abs_guard_def simple_lift_def heap_ptr_valid_def)
|
||||
apply (subgoal_tac "\<forall>a\<in>set (array_addrs (x' (st s)) CARD('b)). c_guard a")
|
||||
apply (erule allE, erule (1) impE)
|
||||
|
|
@ -1521,9 +1521,9 @@ lemma concat_nth_chunk:
|
|||
done
|
||||
|
||||
lemma array_update_split:
|
||||
"\<lbrakk> valid_typ_heap st (getter :: 's \<Rightarrow> ('a::oneMB_size) ptr \<Rightarrow> 'a) setter
|
||||
"\<lbrakk> valid_typ_heap st (getter :: 's \<Rightarrow> ('a::array_outer_max_size) ptr \<Rightarrow> 'a) setter
|
||||
vgetter vsetter t_hrs t_hrs_update;
|
||||
\<forall>x \<in> set (array_addrs (ptr_coerce p) CARD('b::fourthousand_count)).
|
||||
\<forall>x \<in> set (array_addrs (ptr_coerce p) CARD('b::array_max_count)).
|
||||
vgetter (st s) x
|
||||
\<rbrakk> \<Longrightarrow> st (t_hrs_update (hrs_mem_update (heap_update p (arr :: 'a['b]))) s) =
|
||||
fold (\<lambda>i. setter (\<lambda>x. x(ptr_coerce p +\<^sub>p int i := index arr i)))
|
||||
|
|
@ -1561,7 +1561,7 @@ lemma array_update_split:
|
|||
apply simp
|
||||
|
||||
(* remove false dependency *)
|
||||
apply (subst fold_heap_update_list[OF fourthousand_size])
|
||||
apply (subst fold_heap_update_list[OF array_count_size])
|
||||
apply (rule fold_cong[OF refl refl])
|
||||
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
|
|
@ -1620,10 +1620,10 @@ lemma fold_update_id:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma fourthousand_index:
|
||||
"\<lbrakk> i < CARD('b::fourthousand_count); j < CARD('b) \<rbrakk>
|
||||
lemma array_count_index:
|
||||
"\<lbrakk> i < CARD('b::array_max_count); j < CARD('b) \<rbrakk>
|
||||
\<Longrightarrow> (i = j) =
|
||||
((of_nat (i * size_of TYPE('a::oneMB_size)) :: word32)
|
||||
((of_nat (i * size_of TYPE('a::array_outer_max_size)) :: word32)
|
||||
= of_nat (j * size_of TYPE('a)))"
|
||||
apply (rule_tac t = "i = j" and s = "i * size_of TYPE('a) = j * size_of TYPE('a)" in subst)
|
||||
apply clarsimp
|
||||
|
|
@ -1635,7 +1635,7 @@ lemma fourthousand_index:
|
|||
rule less_trans,
|
||||
erule_tac b = "CARD('b)" in mult_strict_right_mono,
|
||||
rule sz_nzero,
|
||||
rule fourthousand_size)+
|
||||
rule array_count_size)+
|
||||
done
|
||||
|
||||
(* end machinery for heap_abs_array_update *)
|
||||
|
|
@ -1652,7 +1652,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
(\<lambda>s. setter (\<lambda>v. v(ptr_coerce (b' s) +\<^sub>p int (n' s) := v' s)) s)
|
||||
(\<lambda>s. t_hrs_update (hrs_mem_update (
|
||||
heap_update (b s) (Arrays.update ((h_val (hrs_mem (t_hrs s)) (b s))
|
||||
:: ('a::oneMB_size)['b::fourthousand_count]) (n s) (v s)))) s)"
|
||||
:: ('a::array_outer_max_size)['b::array_max_count]) (n s) (v s)))) s)"
|
||||
apply (clarsimp simp: abs_modifies_def abs_expr_def)
|
||||
(* rewrite heap_update of array *)
|
||||
apply (subst array_update_split
|
||||
|
|
@ -1687,7 +1687,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
apply assumption
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (subst of_nat_mult[symmetric])+
|
||||
apply (rule fourthousand_index)
|
||||
apply (rule array_count_index)
|
||||
apply (erule less_trans, assumption)+
|
||||
apply clarsimp
|
||||
|
||||
|
|
@ -1696,7 +1696,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
apply assumption
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (subst of_nat_mult[symmetric])+
|
||||
apply (erule fourthousand_index)
|
||||
apply (erule array_count_index)
|
||||
apply assumption
|
||||
apply clarsimp
|
||||
(* index n is disjoint *)
|
||||
|
|
@ -1705,7 +1705,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (subgoal_tac "of_nat (i * size_of TYPE('a)) \<noteq> of_nat (n s * size_of TYPE('a))")
|
||||
apply force
|
||||
apply (subst fourthousand_index[symmetric])
|
||||
apply (subst array_count_index[symmetric])
|
||||
apply assumption
|
||||
apply simp
|
||||
apply simp
|
||||
|
|
|
|||
|
|
@ -16,8 +16,8 @@ theory nested_struct imports "../../AutoCorres" begin
|
|||
|
||||
install_C_file "nested_struct.c"
|
||||
(* Nested struct translation currently only works for packed_type types. *)
|
||||
instance s1_C :: oneMB_packed by intro_classes auto
|
||||
instance s3_C :: oneMB_packed by intro_classes auto
|
||||
instance s1_C :: array_outer_packed by intro_classes auto
|
||||
instance s3_C :: array_outer_packed by intro_classes auto
|
||||
autocorres "nested_struct.c"
|
||||
|
||||
context nested_struct begin
|
||||
|
|
@ -57,4 +57,4 @@ lemma "\<lbrace> \<lambda>h. is_valid_s4_C h s \<and>
|
|||
|
||||
end
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -114,6 +114,7 @@ ML_file "program_analysis.ML"
|
|||
ML_file "heapstatetype.ML"
|
||||
ML_file "MemoryModelExtras-sig.ML"
|
||||
ML_file "MemoryModelExtras.ML"
|
||||
ML_file "$L4V_ARCH/calculate_state_arch.ML"
|
||||
ML_file "calculate_state.ML"
|
||||
ML_file "syntax_transforms.ML"
|
||||
ML_file "expression_translation.ML"
|
||||
|
|
|
|||
|
|
@ -656,22 +656,19 @@ end
|
|||
|
||||
text {* Arrays of packed types are in turn packed *}
|
||||
|
||||
class oneMB_packed = packed_type + oneMB_size
|
||||
class twoToSix_packed = oneMB_packed + twoToSix_size
|
||||
class array_outer_packed = packed_type + array_outer_max_size
|
||||
class array_inner_packed = array_outer_packed + array_inner_max_size
|
||||
|
||||
instance word :: (len8)oneMB_packed ..
|
||||
instance word :: (len8)twoToSix_packed ..
|
||||
instance word :: (len8)array_outer_packed ..
|
||||
instance word :: (len8)array_inner_packed ..
|
||||
|
||||
instantiation array :: (oneMB_packed, fourthousand_count) packed_type
|
||||
begin
|
||||
instance
|
||||
apply(intro_classes)
|
||||
instance array :: (array_outer_packed, array_max_count) packed_type
|
||||
apply(intro_classes)
|
||||
apply (simp add: td_fafu_idem_intro_simps)
|
||||
apply (simp add: td_fa_hi_intro_simps)
|
||||
done
|
||||
end
|
||||
|
||||
instance array :: (twoToSix_packed, fourthousand_count) oneMB_packed ..
|
||||
instance array :: (array_inner_packed, array_max_count) array_outer_packed ..
|
||||
|
||||
section {* Theorems about packed types *}
|
||||
|
||||
|
|
|
|||
|
|
@ -596,7 +596,7 @@ end
|
|||
|
||||
|
||||
(* prove that the new type is an instance of the class finite *)
|
||||
(* prove that the new type is an instance of the class fourthousand_count *)
|
||||
(* prove that the new type is an instance of the class array_max_count *)
|
||||
fun umm_array_calculation el_ty n st thy = let
|
||||
val _ = Feedback.informStr (0, "Proving that an array of "^Int.toString n^" "^
|
||||
Syntax.string_of_typ (thy2ctxt thy) el_ty ^" is a mem_type")
|
||||
|
|
@ -611,19 +611,19 @@ fun umm_array_calculation el_ty n st thy = let
|
|||
This is done exploiting the fact that we have the following instance
|
||||
in our context already
|
||||
|
||||
instance array :: (oneMB_size, fourthousand_count) mem_type
|
||||
instance array :: (array_outer_max_size, array_max_count) mem_type
|
||||
|
||||
Thanks to the neat instance declarations in ArraysMemInstance.thy
|
||||
(all those classes with names lt<n>), the fourthousand_count for
|
||||
Thanks to the neat instance declarations in ArchArraysMemInstance.thy
|
||||
(all those classes with names lt<n>), the array_max_count for
|
||||
the array size will be handled automatically by type-checking.
|
||||
|
||||
This means that we just need to do one independent instance proofs,
|
||||
for el_ty :: oneMB_size
|
||||
for el_ty :: array_outer_max_size
|
||||
|
||||
Even that may be done automatically, for certain element types. For
|
||||
example all the word types have this happen through
|
||||
|
||||
instance word :: (len8) oneMB_size
|
||||
instance word :: (len8) array_outer_max_size
|
||||
instance word_length8 :: len8
|
||||
instance word_length16 :: len8
|
||||
instance word_length32 :: len8
|
||||
|
|
@ -633,7 +633,7 @@ fun umm_array_calculation el_ty n st thy = let
|
|||
|
||||
Arrays get to use the
|
||||
|
||||
instance array :: (twoToSix_size, fourthousand_count) oneMB_size
|
||||
instance array :: (array_inner_max_size, array_max_count) array_outer_max_size
|
||||
|
||||
information.
|
||||
|
||||
|
|
@ -647,7 +647,7 @@ in
|
|||
val (st,thy) =
|
||||
case args of
|
||||
[] => (* will be a record type *)
|
||||
prove_type_in_szclass (st, thy) el_ty "ArraysMemInstance.oneMB_size"
|
||||
prove_type_in_szclass (st, thy) el_ty "ArchArraysMemInstance.array_outer_max_size"
|
||||
| [_] => (* can compute sizes for words and ptrs *)
|
||||
if tyname = @{type_name "Word.word"} then (st, thy)
|
||||
else if tyname = @{type_name "CTypesBase.ptr"} then (st, thy)
|
||||
|
|
@ -655,12 +655,12 @@ in
|
|||
| [a,_] => let
|
||||
val _ = tyname = @{type_name "array"} orelse
|
||||
error "Binary type operator is not array."
|
||||
(* a is an element type and must be in twoToSix_size *)
|
||||
(* a is an element type and must be in array_inner_max_size *)
|
||||
val (atyname, aargs) = case a of Type p => p
|
||||
| _ => error "Array eltype is not Type"
|
||||
in
|
||||
case aargs of
|
||||
[] => prove_type_in_szclass (st,thy) a "ArraysMemInstance.twoToSix_size"
|
||||
[] => prove_type_in_szclass (st,thy) a "ArchArraysMemInstance.array_inner_max_size"
|
||||
| [_] => if atyname = @{type_name "word"} orelse
|
||||
atyname = @{type_name "ptr"}
|
||||
then (st, thy)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,21 @@
|
|||
(*
|
||||
* Copyright 2017, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*)
|
||||
|
||||
signature CALCULATE_STATE_ARCH = sig
|
||||
val mk_array_size_type : int -> typ
|
||||
end;
|
||||
|
||||
structure CalculateStateArch : CALCULATE_STATE_ARCH = struct
|
||||
open TermsTypes
|
||||
fun mk_array_size_type sz =
|
||||
if sz = 1048576
|
||||
then @{typ "ty1048576"}
|
||||
else mk_numeral_type sz
|
||||
end
|
||||
|
|
@ -227,6 +227,7 @@ in
|
|||
end
|
||||
|
||||
fun isa_type_to_typ ctxt (ity : isa_type) = let
|
||||
open CalculateStateArch
|
||||
fun m s = let
|
||||
val thy = Proof_Context.theory_of ctxt
|
||||
val known = (Syntax.parse_typ ctxt s; true) handle ERROR _ => false
|
||||
|
|
@ -234,16 +235,13 @@ fun isa_type_to_typ ctxt (ity : isa_type) = let
|
|||
in
|
||||
f s
|
||||
end
|
||||
fun mk_numeral_type' sz =
|
||||
if sz = 8192 then @{typ "ty8192"}
|
||||
else mk_numeral_type sz
|
||||
in
|
||||
case ity of
|
||||
refty (NONE, _) => mk_ptr_ty unit
|
||||
| refty (SOME ity0, _) => mk_ptr_ty (isa_type_to_typ ctxt ity0)
|
||||
| recd (s, _) => Type (m s, [])
|
||||
| array (ity, sz, _) =>
|
||||
Type("Arrays.array", [isa_type_to_typ ctxt ity, mk_numeral_type' sz])
|
||||
Type("Arrays.array", [isa_type_to_typ ctxt ity, mk_array_size_type sz])
|
||||
| existing (ty, _) => ty
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
theory ArrayAssertion
|
||||
|
||||
imports
|
||||
"ArraysMemInstance"
|
||||
"$L4V_ARCH/ArchArraysMemInstance"
|
||||
"StructSupport"
|
||||
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -28,10 +28,7 @@ definition
|
|||
array_tag :: "('a::c_type,'b::finite) array itself \<Rightarrow> ('a,'b) array typ_info" where
|
||||
"array_tag t \<equiv> array_tag_n (CARD('b))"
|
||||
|
||||
instantiation array :: (c_type,finite) c_type
|
||||
begin
|
||||
instance ..
|
||||
end
|
||||
instance array :: (c_type,finite) c_type ..
|
||||
|
||||
overloading typ_info_array \<equiv> typ_info_t begin
|
||||
definition
|
||||
|
|
@ -205,10 +202,7 @@ apply(subgoal_tac "align_of TYPE('a) dvd size_of TYPE('a)")
|
|||
apply(rule align_size_of)
|
||||
done
|
||||
|
||||
instantiation array :: (mem_type,finite) mem_type_sans_size
|
||||
begin
|
||||
|
||||
instance
|
||||
instance array :: (mem_type,finite) mem_type_sans_size
|
||||
apply intro_classes
|
||||
apply(simp_all add: typ_info_array array_tag_def size_of_def
|
||||
norm_bytes_def)
|
||||
|
|
@ -229,8 +223,6 @@ apply(rule dvd_trans)
|
|||
apply(simp add: size_of_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
declare atn_base [simp del]
|
||||
declare atn_rec [simp del]
|
||||
|
||||
|
|
@ -249,299 +241,4 @@ apply(subst align_td_array_tag)
|
|||
apply simp+
|
||||
done
|
||||
|
||||
(* Showing arrays are in mem_type requires maximum sizes for objects,
|
||||
and maximum counts for elements *)
|
||||
class oneMB_size = mem_type +
|
||||
assumes oneMB_size_ax: "size_of TYPE('a::c_type) < 2 ^ 19"
|
||||
|
||||
class fourthousand_count = finite +
|
||||
assumes fourthousand_count_ax: "CARD ('a) <= 2 ^ 13"
|
||||
|
||||
instantiation array :: (oneMB_size, fourthousand_count) mem_type
|
||||
begin
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply simp
|
||||
apply (subgoal_tac "addr_card = 2 ^ (addr_bitsize - 19) * 2 ^ 19")
|
||||
apply (erule ssubst)
|
||||
apply (rule less_le_trans[where y = "card (UNIV::'b set) * 2 ^ 19"])
|
||||
apply (rule mult_less_mono2)
|
||||
apply (rule oneMB_size_ax)
|
||||
apply simp
|
||||
apply (rule mult_le_mono1)
|
||||
apply (rule le_trans[where j = "2 ^ 13"])
|
||||
apply (rule fourthousand_count_ax)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp add: addr_card)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
class twoToSix_size = oneMB_size +
|
||||
assumes twoToSix_size_ax: "size_of TYPE('a::c_type) < 2 ^ 6"
|
||||
|
||||
instantiation array :: (twoToSix_size, fourthousand_count) oneMB_size
|
||||
begin
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply simp
|
||||
apply (rule order_less_le_trans)
|
||||
apply (rule mult_le_less_imp_less)
|
||||
apply (rule fourthousand_count_ax)
|
||||
apply (rule twoToSix_size_ax)
|
||||
apply simp
|
||||
apply simp
|
||||
apply simp
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
instantiation word :: (len8) oneMB_size
|
||||
begin
|
||||
instance
|
||||
apply intro_classes
|
||||
apply(simp add: size_of_def)
|
||||
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
|
||||
apply simp
|
||||
apply(rule len8_width)
|
||||
done
|
||||
end
|
||||
|
||||
instantiation word :: (len8) twoToSix_size
|
||||
begin
|
||||
instance
|
||||
apply intro_classes
|
||||
apply(simp add: size_of_def)
|
||||
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
|
||||
apply simp
|
||||
apply(rule len8_width)
|
||||
done
|
||||
end
|
||||
|
||||
instantiation ptr :: (c_type) oneMB_size
|
||||
begin
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (simp add: size_of_def)
|
||||
done
|
||||
end
|
||||
|
||||
instantiation ptr :: (c_type) twoToSix_size
|
||||
begin
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (simp add: size_of_def)
|
||||
done
|
||||
end
|
||||
|
||||
class lt12 = finite +
|
||||
assumes lt12_ax: "CARD ('a) < 2 ^ 12"
|
||||
class lt11 = lt12 +
|
||||
assumes lt11_ax: "CARD ('a) < 2 ^ 11"
|
||||
class lt10 = lt11 +
|
||||
assumes lt10_ax: "CARD ('a) < 2 ^ 10"
|
||||
class lt9 = lt10 +
|
||||
assumes lt9_ax: "CARD ('a) < 2 ^ 9"
|
||||
class lt8 = lt9 +
|
||||
assumes lt8_ax: "CARD ('a) < 2 ^ 8"
|
||||
class lt7 = lt8 +
|
||||
assumes lt7_ax: "CARD ('a) < 2 ^ 7"
|
||||
class lt6 = lt7 +
|
||||
assumes lt6_ax: "CARD ('a) < 2 ^ 6"
|
||||
class lt5 = lt6 +
|
||||
assumes lt5_ax: "CARD ('a) < 2 ^ 5"
|
||||
class lt4 = lt5 +
|
||||
assumes lt4_ax: "CARD ('a) < 2 ^ 4"
|
||||
class lt3 = lt4 +
|
||||
assumes lt3_ax: "CARD ('a) < 2 ^ 3"
|
||||
class lt2 = lt3 +
|
||||
assumes lt2_ax: "CARD ('a) < 2 ^ 2"
|
||||
class lt1 = lt2 +
|
||||
assumes lt1_ax: "CARD ('a) < 2 ^ 1"
|
||||
|
||||
instantiation bit0 :: (lt12) fourthousand_count
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt12_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt12) fourthousand_count
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt12_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt11) lt12
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt11_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt11) lt12
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt11_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt10) lt11
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt10_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt10) lt11
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt10_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt9) lt10
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt9_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt9) lt10
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt9_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt8) lt9
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt8_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt8) lt9
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt8_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt7) lt8
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt7_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt7) lt8
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt7_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt6) lt7
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt6_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt6) lt7
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt6_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt5) lt6
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt5_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt5) lt6
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt5_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt4) lt5
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt4_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt4) lt5
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt4_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt3) lt4
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt3_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt3) lt4
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt3_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt2) lt3
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt2_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt2) lt3
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt2_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit0 :: (lt1) lt2
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt1_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation bit1 :: (lt1) lt2
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, insert lt1_ax[where 'a = 'a], simp)
|
||||
end
|
||||
|
||||
instantiation num1 :: lt1
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, simp_all)
|
||||
end
|
||||
|
||||
(* don't understand why this also seems to be necessary *)
|
||||
instantiation num1 :: fourthousand_count
|
||||
begin
|
||||
instance
|
||||
by (intro_classes, simp)
|
||||
end
|
||||
|
||||
(* introduce hackish handling of 8192 type by making a copy of the type
|
||||
under a constructor, and then manually showing that it is an instance of
|
||||
fourthousand_count *)
|
||||
datatype ty8192 = ty8192 "8192"
|
||||
|
||||
lemma univ8192: "(UNIV::ty8192 set) = image ty8192 (UNIV::8192 set)"
|
||||
apply (simp add: set_eq_iff image_iff)
|
||||
apply (rule_tac allI)
|
||||
apply (rule_tac ty8192.induct)
|
||||
apply simp
|
||||
done
|
||||
|
||||
instance "ty8192" :: finite
|
||||
apply intro_classes
|
||||
apply (simp add: univ8192)
|
||||
done
|
||||
|
||||
lemma card8192[simp]: "CARD(ty8192) = CARD(8192)"
|
||||
apply (simp add: univ8192 card_image inj_on_def)
|
||||
done
|
||||
|
||||
instance "ty8192" :: fourthousand_count
|
||||
by intro_classes simp
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
theory TypHeap
|
||||
imports
|
||||
Vanilla32
|
||||
ArraysMemInstance
|
||||
"$L4V_ARCH/ArchArraysMemInstance"
|
||||
HeapRawState
|
||||
MapExtraTrans
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -0,0 +1,265 @@
|
|||
(*
|
||||
* Copyright 2017, NICTA
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_BSD)
|
||||
*)
|
||||
|
||||
theory ArchArraysMemInstance
|
||||
imports "../ArraysMemInstance"
|
||||
begin
|
||||
|
||||
(* Showing arrays are in mem_type requires maximum sizes for objects,
|
||||
and maximum counts for elements *)
|
||||
class array_outer_max_size = mem_type +
|
||||
assumes array_outer_max_size_ax: "size_of TYPE('a::c_type) < 2 ^ 26"
|
||||
|
||||
class array_max_count = finite +
|
||||
assumes array_max_count_ax: "CARD ('a) <= 2 ^ 20"
|
||||
|
||||
instance array :: (array_outer_max_size, array_max_count) mem_type
|
||||
apply intro_classes
|
||||
apply simp
|
||||
apply (subgoal_tac "addr_card = 2 ^ (addr_bitsize - 26) * 2 ^ 26")
|
||||
apply (erule ssubst)
|
||||
apply (rule less_le_trans[where y = "card (UNIV::'b set) * 2 ^ 26"])
|
||||
apply (rule mult_less_mono2)
|
||||
apply (rule array_outer_max_size_ax)
|
||||
apply simp
|
||||
apply (rule mult_le_mono1)
|
||||
apply (rule le_trans[where j = "2 ^ 20"])
|
||||
apply (rule array_max_count_ax)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp add: addr_card)
|
||||
done
|
||||
|
||||
class array_inner_max_size = array_outer_max_size +
|
||||
assumes array_inner_max_size_ax: "size_of TYPE('a::c_type) < 2 ^ 6"
|
||||
|
||||
instance array :: (array_inner_max_size, array_max_count) array_outer_max_size
|
||||
apply intro_classes
|
||||
apply simp
|
||||
apply (rule order_less_le_trans)
|
||||
apply (rule mult_le_less_imp_less)
|
||||
apply (rule array_max_count_ax)
|
||||
apply (rule array_inner_max_size_ax)
|
||||
apply simp
|
||||
apply simp
|
||||
apply simp
|
||||
done
|
||||
|
||||
instance word :: (len8) array_outer_max_size
|
||||
apply intro_classes
|
||||
apply(simp add: size_of_def)
|
||||
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
|
||||
apply simp
|
||||
apply(rule len8_width)
|
||||
done
|
||||
|
||||
instance word :: (len8) array_inner_max_size
|
||||
apply intro_classes
|
||||
apply(simp add: size_of_def)
|
||||
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
|
||||
apply simp
|
||||
apply(rule len8_width)
|
||||
done
|
||||
|
||||
instance ptr :: (c_type) array_outer_max_size
|
||||
apply intro_classes
|
||||
apply (simp add: size_of_def)
|
||||
done
|
||||
|
||||
instance ptr :: (c_type) array_inner_max_size
|
||||
apply intro_classes
|
||||
apply (simp add: size_of_def)
|
||||
done
|
||||
|
||||
class lt19 = finite +
|
||||
assumes lt19_ax: "CARD ('a) < 2 ^ 19"
|
||||
class lt18 = lt19 +
|
||||
assumes lt18_ax: "CARD ('a) < 2 ^ 18"
|
||||
class lt17 = lt18 +
|
||||
assumes lt17_ax: "CARD ('a) < 2 ^ 17"
|
||||
class lt16 = lt17 +
|
||||
assumes lt16_ax: "CARD ('a) < 2 ^ 16"
|
||||
class lt15 = lt16 +
|
||||
assumes lt15_ax: "CARD ('a) < 2 ^ 15"
|
||||
class lt14 = lt15 +
|
||||
assumes lt14_ax: "CARD ('a) < 2 ^ 14"
|
||||
class lt13 = lt14 +
|
||||
assumes lt13_ax: "CARD ('a) < 2 ^ 13"
|
||||
class lt12 = lt13 +
|
||||
assumes lt12_ax: "CARD ('a) < 2 ^ 12"
|
||||
class lt11 = lt12 +
|
||||
assumes lt11_ax: "CARD ('a) < 2 ^ 11"
|
||||
class lt10 = lt11 +
|
||||
assumes lt10_ax: "CARD ('a) < 2 ^ 10"
|
||||
class lt9 = lt10 +
|
||||
assumes lt9_ax: "CARD ('a) < 2 ^ 9"
|
||||
class lt8 = lt9 +
|
||||
assumes lt8_ax: "CARD ('a) < 2 ^ 8"
|
||||
class lt7 = lt8 +
|
||||
assumes lt7_ax: "CARD ('a) < 2 ^ 7"
|
||||
class lt6 = lt7 +
|
||||
assumes lt6_ax: "CARD ('a) < 2 ^ 6"
|
||||
class lt5 = lt6 +
|
||||
assumes lt5_ax: "CARD ('a) < 2 ^ 5"
|
||||
class lt4 = lt5 +
|
||||
assumes lt4_ax: "CARD ('a) < 2 ^ 4"
|
||||
class lt3 = lt4 +
|
||||
assumes lt3_ax: "CARD ('a) < 2 ^ 3"
|
||||
class lt2 = lt3 +
|
||||
assumes lt2_ax: "CARD ('a) < 2 ^ 2"
|
||||
class lt1 = lt2 +
|
||||
assumes lt1_ax: "CARD ('a) < 2 ^ 1"
|
||||
|
||||
instance bit0 :: (lt19) array_max_count
|
||||
using lt19_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt19) array_max_count
|
||||
using lt19_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt18) lt19
|
||||
using lt18_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt18) lt19
|
||||
using lt18_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt17) lt18
|
||||
using lt17_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt17) lt18
|
||||
using lt17_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt16) lt17
|
||||
using lt16_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt16) lt17
|
||||
using lt16_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt15) lt16
|
||||
using lt15_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt15) lt16
|
||||
using lt15_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt14) lt15
|
||||
using lt14_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt14) lt15
|
||||
using lt14_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt13) lt14
|
||||
using lt13_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt13) lt14
|
||||
using lt13_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt12) lt13
|
||||
using lt12_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt12) lt13
|
||||
using lt12_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt11) lt12
|
||||
using lt11_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt11) lt12
|
||||
using lt11_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt10) lt11
|
||||
using lt10_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt10) lt11
|
||||
using lt10_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt9) lt10
|
||||
using lt9_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt9) lt10
|
||||
using lt9_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt8) lt9
|
||||
using lt8_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt8) lt9
|
||||
using lt8_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt7) lt8
|
||||
using lt7_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt7) lt8
|
||||
using lt7_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt6) lt7
|
||||
using lt6_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt6) lt7
|
||||
using lt6_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt5) lt6
|
||||
using lt5_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt5) lt6
|
||||
using lt5_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt4) lt5
|
||||
using lt4_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt4) lt5
|
||||
using lt4_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt3) lt4
|
||||
using lt3_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt3) lt4
|
||||
using lt3_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt2) lt3
|
||||
using lt2_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt2) lt3
|
||||
using lt2_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit0 :: (lt1) lt2
|
||||
using lt1_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance bit1 :: (lt1) lt2
|
||||
using lt1_ax[where 'a='a] by intro_classes simp
|
||||
|
||||
instance num1 :: lt1
|
||||
by (intro_classes, simp_all)
|
||||
|
||||
(* don't understand why this also seems to be necessary *)
|
||||
instance num1 :: array_max_count
|
||||
by (intro_classes, simp)
|
||||
|
||||
(* introduce hackish handling of 8192 type by making a copy of the type
|
||||
under a constructor, and then manually showing that it is an instance of
|
||||
array_max_count *)
|
||||
datatype ty1048576 = ty1048576 "1048576"
|
||||
|
||||
lemma univ1048576: "(UNIV::ty1048576 set) = image ty1048576 (UNIV::1048576 set)"
|
||||
apply (simp add: set_eq_iff image_iff)
|
||||
apply (rule_tac allI)
|
||||
apply (rule_tac ty1048576.induct)
|
||||
apply simp
|
||||
done
|
||||
|
||||
instance "ty1048576" :: finite
|
||||
apply intro_classes
|
||||
apply (simp add: univ1048576)
|
||||
done
|
||||
|
||||
lemma card8192[simp]: "CARD(ty1048576) = CARD(1048576)"
|
||||
apply (simp add: univ1048576 card_image inj_on_def)
|
||||
done
|
||||
|
||||
instance "ty1048576" :: array_max_count
|
||||
by intro_classes simp
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue