isabelle-2021: update Lib
This includes the removal of the theory Extend_Locale, which was an (unused) experiment. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein
Gerwin Klein
parent
d61cffcf61
commit
f2fc2345fe
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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+
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -717,17 +717,19 @@ lemma bind_spec_ev:
|
|||
shows "spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> 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:
|
||||
|
|
|
|||
|
|
@ -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 \<open>
|
||||
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;
|
||||
\<close>
|
||||
|
||||
ML \<open>
|
||||
|
||||
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)
|
||||
)));
|
||||
|
||||
\<close>
|
||||
|
||||
locale Internal begin
|
||||
definition "internal_const1 = True"
|
||||
definition "internal_const2 = False"
|
||||
end
|
||||
|
||||
locale Generic
|
||||
begin
|
||||
|
||||
definition "generic_const = ((\<forall>x :: nat. x \<noteq> x))"
|
||||
|
||||
extend_locale
|
||||
assumes asm_1: "Internal.internal_const1 = (\<forall>x :: nat. x = x)"
|
||||
|
||||
lemma generic_lemma_1: "Internal.internal_const1"
|
||||
apply (insert asm_1)
|
||||
apply simp
|
||||
done
|
||||
|
||||
extend_locale
|
||||
assumes asm_2: "\<not> 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 \<noteq> 0"
|
||||
by (simp add: asm_3)
|
||||
|
||||
extend_locale
|
||||
assumes asm_4: "\<not> 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 \<Longrightarrow> y > x \<Longrightarrow> y > 1"
|
||||
|
||||
|
||||
end
|
||||
|
||||
context Internal begin
|
||||
|
||||
lemma internal_lemma1: "internal_const1 = (\<forall>x :: nat. x = x)" by (simp add: internal_const1_def)
|
||||
|
||||
lemma internal_lemma2: "\<not> internal_const2" by (simp add: internal_const2_def)
|
||||
|
||||
lemma internal_lemma3: "\<not> 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 \<Longrightarrow> y > x \<Longrightarrow> 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 \<noteq> 0"
|
||||
by (rule generic_lemma_3)
|
||||
|
||||
end
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -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 \<Rightarrow> nat \<Rightarrow> 'a"
|
||||
fixes shiftR :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
|
||||
fixes bitSize :: "'a \<Rightarrow> nat"
|
||||
|
|
@ -236,7 +236,7 @@ instance ..
|
|||
|
||||
end
|
||||
|
||||
class finiteBit = bit_operations +
|
||||
class finiteBit = ring_bit_operations +
|
||||
fixes finiteBitSize :: "'a \<Rightarrow> 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 \<Rightarrow> nat) = id"
|
||||
by (simp add: fromIntegral_def fromInteger_nat toInteger_nat)
|
||||
|
|
@ -318,9 +313,7 @@ lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id
|
|||
definition
|
||||
infix_apply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("_ `~_~` _" [81, 100, 80] 80) where
|
||||
infix_apply_def[simp]:
|
||||
"infix_apply a f b \<equiv> f a b"
|
||||
|
||||
term "return $ a `~b~` c d"
|
||||
"a `~f~` b \<equiv> f a b"
|
||||
|
||||
definition
|
||||
zip3 :: "'a list \<Rightarrow> 'b list \<Rightarrow> 'c list \<Rightarrow> ('a \<times> 'b \<times> 'c) list" where
|
||||
|
|
|
|||
|
|
@ -496,13 +496,14 @@ lemma not_emptyI:
|
|||
lemma add_mask_lower_bits2:
|
||||
"\<lbrakk>is_aligned (x :: 'a :: len word) n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> 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 \<or> Q then x else y)" by simp
|
||||
"(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
|
||||
by (rule z3_rule)
|
||||
|
||||
lemma inter_UNIV_minus[simp]:
|
||||
"x \<inter> (UNIV - y) = x-y" by blast
|
||||
|
|
|
|||
|
|
@ -22,8 +22,6 @@ imports
|
|||
"Word_Lib.WordSetup"
|
||||
begin
|
||||
|
||||
typ "32 word"
|
||||
|
||||
(* FIXME: eliminate *)
|
||||
abbreviation (input)
|
||||
split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
|
||||
|
|
|
|||
|
|
@ -369,7 +369,6 @@ proof -
|
|||
apply (drule use_validNF [OF _ inv_holds])
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply blast
|
||||
done
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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 \<le> m \<Longrightarrow> ((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 \<Longrightarrow> \<forall>i \<ge> n. \<not> 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) = (\<forall>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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
1
lib/ROOT
1
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
|
||||
|
|
|
|||
|
|
@ -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 \<Longrightarrow>
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
|
||||
theory Setup_Locale
|
||||
imports "Lib.Qualify" "Lib.Requalify" "Lib.Extend_Locale"
|
||||
imports "Lib.Qualify" "Lib.Requalify"
|
||||
begin
|
||||
|
||||
(*
|
||||
|
|
|
|||
Loading…
Reference in New Issue