diff --git a/lib/AutoLevity_Base.thy b/lib/AutoLevity_Base.thy index fb9b879bb..969edf2a0 100644 --- a/lib/AutoLevity_Base.thy +++ b/lib/AutoLevity_Base.thy @@ -214,9 +214,6 @@ end This is needed to perform localized attribute tests (e.g.. is this locale assumption marked as simp?) *) -(* TODO: extend_locale breaks this naming scheme by adding the "chunk" qualifier. This can - probably just be handled as a special case *) - fun most_local_fact_of ctxt xnm prop = let val local_name = xnm |> try (Long_Name.explode #> tl #> tl #> Long_Name.implode) diff --git a/lib/Bisim_UL.thy b/lib/Bisim_UL.thy index 369e22119..a4d72b61e 100644 --- a/lib/Bisim_UL.thy +++ b/lib/Bisim_UL.thy @@ -534,13 +534,8 @@ lemma bisim_splitE_req: apply simp apply assumption+ apply (frule (1) use_valid [OF _ v1 [unfolded validE_R_def validE_def]]) - apply clarsimp - apply (case_tac x) - apply (clarsimp simp: in_monad) - apply (rule_tac x = "(Inl y', t')" in bexI) - apply fastforce - apply (fastforce simp: in_monad) - apply clarsimp + apply (clarsimp split: sum.splits) + apply (fastforce simp: in_monad bind_def throwError_def return_def split: sum.splits prod.splits) apply (rule bisim_underlyingE1 [OF bd]) apply simp apply assumption+ @@ -548,19 +543,14 @@ lemma bisim_splitE_req: apply (rule_tac x = "(r'', t'')" in bexI) apply clarsimp apply (fastforce simp: in_monad) - apply (clarsimp simp: in_monad split_def) apply (erule bisim_underlyingE2) apply simp apply assumption+ apply (frule (1) use_valid [OF _ v1 [unfolded validE_R_def validE_def]]) apply clarsimp - apply (case_tac r) - apply (clarsimp simp: in_monad) - apply (rule_tac x = "(Inl aa, s'')" in bexI) - apply fastforce - apply (fastforce simp: in_monad) - apply clarsimp + apply (clarsimp split: sum.splits) + apply (fastforce simp: in_monad bind_def throwError_def return_def split: sum.splits prod.splits) apply (rule bisim_underlyingE2 [OF bd]) apply simp apply assumption+ diff --git a/lib/CorresK/CorresK_Lemmas.thy b/lib/CorresK/CorresK_Lemmas.thy index aee808693..1588afd6b 100644 --- a/lib/CorresK/CorresK_Lemmas.thy +++ b/lib/CorresK/CorresK_Lemmas.thy @@ -108,7 +108,6 @@ lemma F_all2_eq: apply (intro conjI impI allI) apply (drule list_all2_conjD) apply (simp add: list.rel_eq) - apply clarsimp apply (simp add: list_all2_to_list_all list_all_mem_subset) apply (rule list.rel_refl_strong;simp) done diff --git a/lib/EquivValid.thy b/lib/EquivValid.thy index 27bb032b6..78256d01d 100644 --- a/lib/EquivValid.thy +++ b/lib/EquivValid.thy @@ -717,17 +717,19 @@ lemma bind_spec_ev: shows "spec_equiv_valid_inv s' I A (\s. P' s \ P'' s) (f >>= g)" using reads_res_1 apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def valid_def bind_def split_def) + apply (rename_tac t a b aa ba ab bb ac bc) apply (erule_tac x=t in allE) apply clarsimp apply (erule_tac x="(a, b)" in ballE) - apply (erule_tac x="(ab, bb)" in ballE) - apply clarsimp - apply (cut_tac rv="ab" and s''="b" in reads_res_2) - apply assumption - apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) - apply(erule_tac x=bb in allE) - using hoare - apply (fastforce simp: valid_def)+ + apply (erule_tac x="(ab, bb)" in ballE) + apply clarsimp + apply (cut_tac reads_res_2) + prefer 2 + apply assumption + apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) + apply(erule_tac x=bb in allE) + using hoare + apply (fastforce simp: valid_def)+ done lemma bindE_spec_ev: diff --git a/lib/Extend_Locale.thy b/lib/Extend_Locale.thy deleted file mode 100644 index fc1c24486..000000000 --- a/lib/Extend_Locale.thy +++ /dev/null @@ -1,166 +0,0 @@ -(* - * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) - * - * SPDX-License-Identifier: BSD-2-Clause - *) - -(* - * Extend a locale by seamlessly generating sublocales. - *) - -theory Extend_Locale -imports Main Defs -keywords "extend_locale" :: thy_decl -begin - -ML \ -fun note_new_facts prev_lthy (lthy : local_theory) = -let - val facts = Proof_Context.facts_of lthy; - - val local_facts = Facts.dest_static false [Proof_Context.facts_of prev_lthy] facts; - - val space = Facts.space_of (Proof_Context.facts_of lthy); - - fun make_binding (long_name, pos) = - let val (qualifier, name) = split_last (Long_Name.explode long_name) - in fold (Binding.qualify true) qualifier (Binding.make (name, pos)) end; - - fun add_entry (nm, thms) lthy = - let - val extern_nm = Name_Space.extern_shortest lthy space nm; - val {pos, ...} = Name_Space.the_entry space nm; - val b = make_binding (extern_nm, pos); - val (_, lthy') = Local_Theory.note ((b,[]),thms) lthy; - in lthy' end - -in fold add_entry local_facts lthy end; -\ - -ML \ - -val _ = - Outer_Syntax.command @{command_keyword extend_locale} "extend current locale" - (Parse.opt_target -- (Scan.repeat1 Parse_Spec.context_element) >> (fn (target, (elems)) => - (Toplevel.local_theory NONE target (fn lthy => - let - val locale_name = case Named_Target.locale_of lthy of SOME x => x | NONE => error "Not in a locale!" - val binding = Binding.make (Long_Name.base_name locale_name, Position.none) - - val chunkN = "extchunk_" - - val last_chunk = - case Long_Name.explode locale_name of - [_, chunk, _] => (unprefix chunkN chunk |> Int.fromString |> the) - | [_, _] => 0 - | _ => raise Fail ("Unexpected locale naming scheme:" ^ locale_name) - - val chunk = Int.toString (last_chunk + 1) - - - val (next_locale_name, lthy') = lthy - |> Local_Theory.map_background_naming - (Name_Space.parent_path #> Name_Space.add_path (chunkN ^ chunk)) - |> Local_Theory.background_theory_result - (Expression.add_locale_cmd binding binding - ([((locale_name,Position.none), (("#",false), (Expression.Positional [],[])))], []) elems - ##> Local_Theory.exit_global) - ||> Local_Theory.restore_background_naming lthy - - - val lthy'' = lthy' - |> Local_Theory.exit_global - |> Named_Target.init next_locale_name - - in lthy'' end) - ))); - -\ - -locale Internal begin - definition "internal_const1 = True" - definition "internal_const2 = False" -end - -locale Generic -begin - -definition "generic_const = ((\x :: nat. x \ x))" - -extend_locale - assumes asm_1: "Internal.internal_const1 = (\x :: nat. x = x)" - -lemma generic_lemma_1: "Internal.internal_const1" - apply (insert asm_1) - apply simp - done - -extend_locale - assumes asm_2: "\ Internal.internal_const2" - -lemma generic_lemma_2: "generic_const = Internal.internal_const2" - by (simp add: asm_2 generic_const_def) - -extend_locale - fixes param_const_1 :: nat - assumes asm_3: "param_const_1 > 0" - -lemma generic_lemma_3: "param_const_1 \ 0" - by (simp add: asm_3) - -extend_locale - assumes asm_4: "\ generic_const" - -lemma generic_lemma_4: "generic_const = Internal.internal_const2" - by (simp add: asm_4 asm_2 generic_lemma_2) - -extend_locale - assumes asm_4: "x = param_const_1 \ y > x \ y > 1" - - -end - -context Internal begin - -lemma internal_lemma1: "internal_const1 = (\x :: nat. x = x)" by (simp add: internal_const1_def) - -lemma internal_lemma2: "\ internal_const2" by (simp add: internal_const2_def) - -lemma internal_lemma3: "\ Generic.generic_const" by (simp add: Generic.generic_const_def) - -definition "internal_const3 = (1 :: nat)" - -lemma internal_lemma4: "internal_const3 > 0" by (simp add: internal_const3_def) - -lemma asm_4: "x = internal_const3 \ y > x \ y > 1" - by (simp add: internal_const3_def) - -end - -interpretation Generic - where param_const_1 = Internal.internal_const3 - subgoal - proof - - interpret Internal . - show ?thesis - (* annoyingly, the proof method "fact" no longer has access to facts produced by "interpret" *) - apply (intro_locales; unfold_locales) - apply (rule internal_lemma1) - apply (rule internal_lemma2) - apply (rule internal_lemma4) - apply (rule internal_lemma3) - apply (erule (1) asm_4) - done - qed - done - -context Internal begin - -lemma internal_lemma5: - "internal_const3 \ 0" - by (rule generic_lemma_3) - -end - - -end diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index 24b32c645..71c716585 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -200,7 +200,7 @@ lemma either_simp[simp]: "either = case_sum" apply (simp add: either_def) done -class HS_bit = bit_operations + +class HS_bit = semiring_bit_operations + fixes shiftL :: "'a \ nat \ 'a" fixes shiftR :: "'a \ nat \ 'a" fixes bitSize :: "'a \ nat" @@ -236,7 +236,7 @@ instance .. end -class finiteBit = bit_operations + +class finiteBit = ring_bit_operations + fixes finiteBitSize :: "'a \ nat" instantiation word :: (len) finiteBit @@ -305,12 +305,7 @@ lemma fromIntegral_simp2[simp]: "fromIntegral = unat" by (simp add: fromIntegral_def fromInteger_nat toInteger_word) lemma fromIntegral_simp3[simp]: "fromIntegral = ucast" - apply (simp add: fromIntegral_def fromInteger_word toInteger_word) - apply (rule ext) - apply (simp add: ucast_def) - apply (subst word_of_nat) - apply (simp add: unat_def) - done + unfolding fromIntegral_def fromInteger_word toInteger_word by force lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \ nat) = id" by (simp add: fromIntegral_def fromInteger_nat toInteger_nat) @@ -318,9 +313,7 @@ lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \ nat) = id definition infix_apply :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("_ `~_~` _" [81, 100, 80] 80) where infix_apply_def[simp]: - "infix_apply a f b \ f a b" - -term "return $ a `~b~` c d" + "a `~f~` b \ f a b" definition zip3 :: "'a list \ 'b list \ 'c list \ ('a \ 'b \ 'c) list" where diff --git a/lib/LemmaBucket.thy b/lib/LemmaBucket.thy index e1727d265..a9733c834 100644 --- a/lib/LemmaBucket.thy +++ b/lib/LemmaBucket.thy @@ -496,13 +496,14 @@ lemma not_emptyI: lemma add_mask_lower_bits2: "\is_aligned (x :: 'a :: len word) n; p && ~~ mask n = 0\ \ x + p && ~~ mask n = x" apply (subst word_plus_and_or_coroll) - apply (simp add: aligned_mask_disjoint and_mask_0_iff_le_mask) - apply (clarsimp simp: word_bool_alg.conj_disj_distrib2) + apply (simp add: aligned_mask_disjoint and_mask_0_iff_le_mask) + apply (clarsimp simp: bit.conj_disj_distrib2) done (* FIXME: move to GenericLib *) lemma if3_fold2: - "(if P then x else if Q then x else y) = (if P \ Q then x else y)" by simp + "(if P then x else if Q then x else y) = (if P \ Q then x else y)" + by (rule z3_rule) lemma inter_UNIV_minus[simp]: "x \ (UNIV - y) = x-y" by blast diff --git a/lib/Lib.thy b/lib/Lib.thy index 35fd339ca..a8c25f1d9 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -22,8 +22,6 @@ imports "Word_Lib.WordSetup" begin -typ "32 word" - (* FIXME: eliminate *) abbreviation (input) split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" diff --git a/lib/Monad_WP/WhileLoopRules.thy b/lib/Monad_WP/WhileLoopRules.thy index 8bc34cda2..abd2b8d52 100644 --- a/lib/Monad_WP/WhileLoopRules.thy +++ b/lib/Monad_WP/WhileLoopRules.thy @@ -369,7 +369,6 @@ proof - apply (drule use_validNF [OF _ inv_holds]) apply simp apply clarsimp - apply blast done } diff --git a/lib/NatBitwise.thy b/lib/NatBitwise.thy index 16ff1e1ac..88cb798fa 100644 --- a/lib/NatBitwise.thy +++ b/lib/NatBitwise.thy @@ -11,53 +11,70 @@ imports Lib begin -instantiation nat :: bit_operations +instantiation nat :: semiring_bit_syntax begin +instance .. +end -definition - "shiftl x y = nat (shiftl (int x) y)" - -definition - "shiftr x y = nat (shiftr (int x) y)" - -definition - "test_bit x y = test_bit (int x) y" +instantiation nat :: lsb +begin definition "lsb x = lsb (int x)" -definition - "msb x = msb (int x)" +instance + by intro_classes (meson even_of_nat lsb_nat_def lsb_odd) + +end + +instantiation nat :: msb +begin definition - "set_bit x y z = nat (set_bit (int x) y z)" + "msb x = msb (int x)" instance .. end +instantiation nat :: set_bit +begin + +definition + "set_bit x y z = nat (set_bit (int x) y z)" + +instance + by intro_classes + (simp add: set_bit_nat_def bit_nat_iff set_bit_int_def bin_nth_sc_gen bin_sc_pos + bit_of_nat_iff_bit) + +end + + lemma nat_2p_eq_shiftl: "(2::nat)^x = 1 << x" - by (simp add: shiftl_nat_def int_2p_eq_shiftl) + by (simp add: shiftl_eq_push_bit) lemma shiftl_nat_alt_def: "(x::nat) << n = x * 2^n" - by (simp add: shiftl_nat_def shiftl_int_def nat_int_mul) + by (simp add: push_bit_nat_def shiftl_eq_push_bit) + +lemma shiftl_nat_def: + "(x::nat) << y = nat (int x << y)" + by (simp add: nat_int_mul shiftl_int_def shiftl_nat_alt_def) lemma nat_shiftl_less_cancel: "n \ m \ ((x :: nat) << n < y << m) = (x < y << (m - n))" by (simp add: nat_int_comparison(2) shiftl_nat_def int_shiftl_less_cancel) + lemma nat_shiftl_lt_2p_bits: "(x::nat) < 1 << n \ \i \ n. \ x !! i" - apply (clarsimp simp: shiftl_nat_def test_bit_nat_def zless_nat_eq_int_zless shiftl_eq_push_bit - push_bit_of_1 bit_def power_add zdiv_zmult2_eq dest!: le_Suc_ex) - done + apply (clarsimp simp: shiftl_nat_def zless_nat_eq_int_zless shiftl_eq_push_bit push_bit_of_1 + dest!: le_Suc_ex) + by (metis bit_take_bit_iff not_add_less1 take_bit_nat_eq_self_iff test_bit_eq_bit) -lemma nat_eq_test_bit: - "((x :: nat) = y) = (\i. test_bit x i = test_bit y i)" - apply (simp add: test_bit_nat_def bit_eq_iff) - done -lemmas nat_eq_test_bitI = nat_eq_test_bit[THEN iffD2, rule_format] +lemmas nat_eq_test_bit = bit_eq_iff +lemmas nat_eq_test_bitI = bit_eq_iff[THEN iffD2, rule_format] end \ No newline at end of file diff --git a/lib/Qualify.thy b/lib/Qualify.thy index 40b56c1b8..52fc026b4 100644 --- a/lib/Qualify.thy +++ b/lib/Qualify.thy @@ -141,7 +141,7 @@ fun end_global_qualify thy = |> (fn thy => fold (Sign.hide_const false o snd) consts thy) |> (fn thy => fold (Sign.hide_type false o snd) types thy); - val lthy = Named_Target.begin (#target_name args, Position.none) thy'' + val lthy = Target_Context.context_begin_named_cmd [] (#target_name args, Position.none) thy'' |> Local_Theory.map_background_naming (Name_Space.parent_path #> Name_Space.mandatory_path nm); val lthy' = lthy diff --git a/lib/ROOT b/lib/ROOT index 66d9cb8da..ae4409006 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -35,7 +35,6 @@ session Lib (lib) = Word_Lib + HaskellLib_H Eval_Bool Bisim_UL - Extend_Locale Solves_Tac Crunch Crunch_Instances_NonDet diff --git a/lib/RangeMap.thy b/lib/RangeMap.thy index 29b92dfd3..ac6bb5e59 100644 --- a/lib/RangeMap.thy +++ b/lib/RangeMap.thy @@ -546,12 +546,10 @@ lemma combine_contiguous_ranges_rev_head_helper: apply (clarsimp simp del: combine_contiguous_ranges_rev.simps) apply (drule_tac x="(start', end') # map fst kvs" in meta_spec) apply (drule_tac x="start'" in meta_spec) - apply (drule_tac x="end'" in meta_spec) apply (clarsimp simp del: combine_contiguous_ranges_rev.simps) apply (simp only: combine_contiguous_ranges_rev.simps(1)[where xs = "_#_"]) apply (fastforce dest: monotonic_ranges_each_valid split: list.splits if_splits) - apply auto - done + by auto lemma combine_contiguous_ranges_rev_correct: "monotonic_key_ranges xs \ diff --git a/spec/machine/Setup_Locale.thy b/spec/machine/Setup_Locale.thy index abd874c7f..8c963000c 100644 --- a/spec/machine/Setup_Locale.thy +++ b/spec/machine/Setup_Locale.thy @@ -6,7 +6,7 @@ theory Setup_Locale -imports "Lib.Qualify" "Lib.Requalify" "Lib.Extend_Locale" +imports "Lib.Qualify" "Lib.Requalify" begin (*