some more lib updates for Isabelle2015
This commit is contained in:
parent
ce33a07662
commit
9c17bd32a4
|
@ -51,7 +51,7 @@ lemma is_aligned_to_bl:
|
|||
apply (erule exE)
|
||||
apply (rule_tac x=j in exI)
|
||||
apply clarsimp
|
||||
apply (thin_tac "w !! ?t")
|
||||
apply (thin_tac "w !! t" for t)
|
||||
apply (rule_tac x="i + n - len_of TYPE('a)" in exI)
|
||||
apply clarsimp
|
||||
apply arith
|
||||
|
|
|
@ -253,7 +253,7 @@ lemma map_snd_zip_prefix:
|
|||
|
||||
lemma nth_upt_0 [simp]:
|
||||
"i < length xs \<Longrightarrow> [0..<length xs] ! i = i"
|
||||
by (metis comm_monoid_add_class.add.left_neutral nth_upt)
|
||||
by simp
|
||||
|
||||
lemma take_insert_nth:
|
||||
"i < length xs\<Longrightarrow>
|
||||
|
@ -589,7 +589,7 @@ lemma distinct_sets_update:
|
|||
apply (drule (2) distinct_sets_take_nth)
|
||||
apply blast
|
||||
apply clarsimp
|
||||
apply (thin_tac "?P \<subseteq> ?Q")
|
||||
apply (thin_tac "P \<subseteq> Q" for P Q)
|
||||
apply (subst (asm) id_take_nth_drop, assumption)
|
||||
apply (drule distinct_sets_append_Cons)
|
||||
apply (erule (2) distinct_sets_append_distinct)
|
||||
|
|
|
@ -4367,21 +4367,11 @@ lemma dom_eqI:
|
|||
lemma dvd_reduce_multiple:
|
||||
fixes k :: nat
|
||||
shows "(k dvd k * m + n) = (k dvd n)"
|
||||
apply (induct m)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (subst add.assoc, subst add.commute)
|
||||
apply (subst dvd_reduce)
|
||||
apply assumption
|
||||
done
|
||||
by (induct m) (auto simp: add_ac)
|
||||
|
||||
lemma image_iff:
|
||||
"inj f \<Longrightarrow> f x \<in> f ` S = (x \<in> S)"
|
||||
apply rule
|
||||
apply (erule imageE)
|
||||
apply (simp add: inj_eq)
|
||||
apply (erule imageI)
|
||||
done
|
||||
by (rule inj_image_mem_iff)
|
||||
|
||||
lemma of_nat_power:
|
||||
shows "\<lbrakk> p < 2 ^ x; x < len_of TYPE ('a :: len) \<rbrakk> \<Longrightarrow> of_nat p < (2 :: 'a :: len word) ^ x"
|
||||
|
@ -5054,7 +5044,8 @@ lemma sint_int_max_plus_1:
|
|||
"sint (2 ^ (len_of TYPE('a) - Suc 0) :: ('a::len) word) = - (2 ^ (len_of TYPE('a) - Suc 0))"
|
||||
apply (subst word_of_int_2p [symmetric])
|
||||
apply (subst int_word_sint)
|
||||
apply (clarsimp simp: comm_semiring_1_class.normalizing_semiring_rules(27))
|
||||
apply clarsimp
|
||||
apply (metis Suc_pred int_word_uint len_gt_0 power_Suc uint_eq_0 word_of_int_2p word_pow_0)
|
||||
done
|
||||
|
||||
lemma word32_bounds:
|
||||
|
@ -5379,7 +5370,7 @@ lemma smod_int_range:
|
|||
apply (insert pos_mod_conj [where a="-a" and b=b])[1]
|
||||
apply (clarsimp simp: smod_int_alt_def sign_simps sgn_if
|
||||
abs_if not_less add1_zle_eq [simplified add.commute])
|
||||
apply (metis add_le_cancel_left comm_monoid_add_class.add.right_neutral
|
||||
apply (metis add_le_cancel_left monoid_add_class.add.right_neutral
|
||||
int_one_le_iff_zero_less less_le_trans mod_minus_right neg_less_0_iff_less
|
||||
neg_mod_conj not_less pos_mod_conj)
|
||||
apply (insert neg_mod_conj [where a=a and b="b"])[1]
|
||||
|
@ -6312,7 +6303,7 @@ lemma word_lsb_nat:"lsb w = (unat w mod 2 = 1)"
|
|||
by (metis (no_types, hide_lams) nat_mod_distrib nat_numeral not_mod_2_eq_1_eq_0 numeral_One uint_eq_0 uint_nonnegative unat_0 unat_def zero_le_numeral)
|
||||
|
||||
lemma odd_iff_lsb:"odd (unat (x::('a::len) word)) = x !! 0"
|
||||
apply (simp add:even_def)
|
||||
apply (simp add:even_iff_mod_2_eq_zero)
|
||||
apply (subst word_lsb_nat[unfolded One_nat_def, symmetric])
|
||||
apply (rule word_lsb_alt)
|
||||
done
|
||||
|
@ -6352,9 +6343,8 @@ lemma shiftr1_irrelevant_lsb:"(x::('a::len) word) !! 0 \<or> x >> 1 = (x + 1) >>
|
|||
apply clarsimp
|
||||
apply (case_tac "even (unat x)")
|
||||
apply (subgoal_tac "unat x div 2 = Suc (unat x) div 2")
|
||||
apply clarsimp
|
||||
apply metis
|
||||
apply (subst numeral_2_eq_2)+
|
||||
apply (rule even_nat_plus_one_div_two[symmetric])
|
||||
apply simp
|
||||
apply (simp add:odd_iff_lsb)
|
||||
done
|
||||
|
@ -6455,7 +6445,7 @@ lemma dvd_not_suc:"\<lbrakk> 2 ^ n dvd (p::nat); n > 0; i > 0; i < 2 ^ n; p + i
|
|||
by (metis dvd_def dvd_reduce_multiple nat_dvd_not_less)
|
||||
|
||||
lemma word32_gr0_conv_Suc:"(m::word32) > 0 \<Longrightarrow> \<exists>n. m = n + 1"
|
||||
by (metis comm_semiring_1_class.normalizing_semiring_rules(24) zadd_diff_inverse)
|
||||
by (metis add.commute add_minus_cancel)
|
||||
|
||||
lemma offset_not_aligned:
|
||||
"\<lbrakk> is_aligned (p::word32) n; i > 0; i < 2 ^ n; n < 32\<rbrakk>
|
||||
|
|
|
@ -53,7 +53,7 @@ type wp_rules = {trips: thm list * (theory -> term -> term),
|
|||
|
||||
fun accum_last_occurence' [] _ = ([], Termtab.empty)
|
||||
| accum_last_occurence' ((t, v) :: ts) tt1 = let
|
||||
val tm = prop_of t;
|
||||
val tm = Thm.prop_of t;
|
||||
val tt2 = Termtab.insert_list (K false) (tm, v) tt1;
|
||||
val (ts', tt3) = accum_last_occurence' ts tt2;
|
||||
in case Termtab.lookup tt3 tm of
|
||||
|
@ -87,9 +87,9 @@ fun add_rule_inner trip_conv t (trips, n, others) = (
|
|||
|
||||
fun del_rule_inner trip_conv t (trips, n, others) =
|
||||
case get_key trip_conv t of
|
||||
SOME k => (Net.delete_term_safe (Thm.eq_thm_prop o pairself snd)
|
||||
SOME k => (Net.delete_term_safe (Thm.eq_thm_prop o apply2 snd)
|
||||
(k, (n, t)) trips, n, others)
|
||||
| _ => (trips, n, remove (Thm.eq_thm_prop o pairself snd) (n, t) others)
|
||||
| _ => (trips, n, remove (Thm.eq_thm_prop o apply2 snd) (n, t) others)
|
||||
|
||||
val no_rules = (Net.empty, 0, []);
|
||||
|
||||
|
|
|
@ -73,16 +73,16 @@ signature WPC = sig
|
|||
val iffd2_thm: thm;
|
||||
val wpc_helperI: thm;
|
||||
|
||||
val instantiate_concl_pred: theory -> cterm -> thm -> thm;
|
||||
val instantiate_concl_pred: Proof.context -> cterm -> thm -> thm;
|
||||
|
||||
val detect_term: theory -> thm -> cterm -> (cterm * term) list;
|
||||
val detect_terms: theory -> (term -> cterm -> thm -> tactic) -> tactic;
|
||||
val detect_term: Proof.context -> thm -> cterm -> (cterm * term) list;
|
||||
val detect_terms: Proof.context -> (term -> cterm -> thm -> tactic) -> tactic;
|
||||
|
||||
val split_term: thm list -> Proof.context -> term -> cterm -> thm -> tactic;
|
||||
|
||||
val wp_cases_tac: thm list -> Proof.context -> tactic;
|
||||
val wp_debug_tac: thm list -> Proof.context -> tactic;
|
||||
val wp_cases_method: thm list -> (Proof.context -> Method.method) Parse.context_parser;
|
||||
val wp_cases_method: thm list -> (Proof.context -> Method.method) context_parser;
|
||||
|
||||
end;
|
||||
|
||||
|
@ -94,9 +94,9 @@ structure WPCPredicateAndFinals = Theory_Data
|
|||
val extend = I
|
||||
fun merge (xs, ys) =
|
||||
(* Order of predicates is important, so we can't reorder *)
|
||||
let val tms = map (term_of o fst) xs
|
||||
let val tms = map (Thm.term_of o fst) xs
|
||||
fun inxs x = exists (fn y => x aconv y) tms
|
||||
val ys' = filter (not o inxs o term_of o fst) ys
|
||||
val ys' = filter (not o inxs o Thm.term_of o fst) ys
|
||||
in
|
||||
xs @ ys'
|
||||
end
|
||||
|
@ -114,12 +114,12 @@ val foo_thm = @{thm "wpc_foo"};
|
|||
(* it looks like cterm_instantiate would do the job better,
|
||||
but this handles the case where ?'a must be instantiated
|
||||
to ?'a \<times> ?'b *)
|
||||
fun instantiate_concl_pred thy pred thm =
|
||||
fun instantiate_concl_pred ctxt pred thm =
|
||||
let
|
||||
val get_concl_pred = (fst o strip_comb o HOLogic.dest_Trueprop o concl_of);
|
||||
val get_concl_predC = (cterm_of thy o get_concl_pred);
|
||||
val get_concl_pred = (fst o strip_comb o HOLogic.dest_Trueprop o Thm.concl_of);
|
||||
val get_concl_predC = (Thm.cterm_of ctxt o get_concl_pred);
|
||||
|
||||
val get_pred_tvar = (ctyp_of thy o domain_type o typ_of o ctyp_of_term);
|
||||
val get_pred_tvar = (Thm.ctyp_of ctxt o domain_type o Thm.typ_of o Thm.ctyp_of_cterm);
|
||||
val thm_pred = get_concl_predC thm;
|
||||
val thm_pred_tvar = get_pred_tvar thm_pred;
|
||||
val pred_tvar = get_pred_tvar pred;
|
||||
|
@ -131,22 +131,22 @@ in
|
|||
Thm.instantiate ([], [(thm2_pred, pred)]) thm2
|
||||
end;
|
||||
|
||||
fun detect_term thy thm tm =
|
||||
fun detect_term ctxt thm tm =
|
||||
let
|
||||
val foo_thm_tm = instantiate_concl_pred thy tm foo_thm;
|
||||
val matches = resolve_tac [foo_thm_tm] 1 thm;
|
||||
val foo_thm_tm = instantiate_concl_pred ctxt tm foo_thm;
|
||||
val matches = resolve_tac ctxt [foo_thm_tm] 1 thm;
|
||||
val outcomes = Seq.list_of matches;
|
||||
val get_goalterm = (HOLogic.dest_Trueprop o Logic.strip_assums_concl
|
||||
o Envir.beta_eta_contract o hd o prems_of);
|
||||
o Envir.beta_eta_contract o hd o Thm.prems_of);
|
||||
val get_argument = hd o snd o strip_comb;
|
||||
in
|
||||
map (pair tm o get_argument o get_goalterm) outcomes
|
||||
end;
|
||||
|
||||
fun detect_terms (thy : theory) tactic2 thm =
|
||||
fun detect_terms ctxt tactic2 thm =
|
||||
let
|
||||
val pfs = WPCPredicateAndFinals.get thy;
|
||||
val detects = map (fn (tm, rl) => (detect_term thy thm tm, rl)) pfs;
|
||||
val pfs = WPCPredicateAndFinals.get (Proof_Context.theory_of ctxt);
|
||||
val detects = map (fn (tm, rl) => (detect_term ctxt thm tm, rl)) pfs;
|
||||
val detects2 = filter (not o null o fst) detects;
|
||||
val ((pred, arg), fin) = case detects2 of
|
||||
[] => raise WPCFailed ("detect_terms: no match", [], [thm])
|
||||
|
@ -155,8 +155,8 @@ in
|
|||
tactic2 arg pred fin thm
|
||||
end;
|
||||
|
||||
fun resolve_single_tac rules n thm =
|
||||
case Seq.chop 2 (resolve_tac rules n thm)
|
||||
fun resolve_single_tac ctxt rules n thm =
|
||||
case Seq.chop 2 (resolve_tac ctxt rules n thm)
|
||||
of ([], seq) => raise WPCFailed
|
||||
("resolve_single_tac: no rules could apply",
|
||||
[], thm :: rules)
|
||||
|
@ -174,46 +174,46 @@ let
|
|||
SOME sugar => #split sugar
|
||||
| _ => raise WPCFailed ("split_term: not a case", [hdTarget], []);
|
||||
val subst = split RS iffd2_thm;
|
||||
val subst2 = instantiate_concl_pred (Proof_Context.theory_of ctxt) pred subst;
|
||||
val subst2 = instantiate_concl_pred ctxt pred subst;
|
||||
in
|
||||
((resolve_tac [subst2] 1)
|
||||
((resolve_tac ctxt [subst2] 1)
|
||||
THEN
|
||||
(resolve_tac [wpc_helperI] 1)
|
||||
(resolve_tac ctxt [wpc_helperI] 1)
|
||||
THEN
|
||||
(REPEAT_ALL_NEW (resolve_tac processors)
|
||||
(REPEAT_ALL_NEW (resolve_tac ctxt processors)
|
||||
THEN_ALL_NEW
|
||||
resolve_single_tac [fin]) 1
|
||||
resolve_single_tac ctxt [fin]) 1
|
||||
) t
|
||||
end;
|
||||
|
||||
(* n.b. need to concretise the lazy sequence via a list to ensure exceptions
|
||||
have been raised already and catch them *)
|
||||
fun wp_cases_tac processors ctxt thm =
|
||||
detect_terms (Proof_Context.theory_of ctxt) (split_term processors ctxt) thm
|
||||
detect_terms ctxt (split_term processors ctxt) thm
|
||||
|> Seq.list_of |> Seq.of_list
|
||||
handle WPCFailed _ => no_tac thm;
|
||||
|
||||
fun wp_debug_tac processors ctxt =
|
||||
detect_terms (Proof_Context.theory_of ctxt) (split_term processors ctxt);
|
||||
detect_terms ctxt (split_term processors ctxt);
|
||||
|
||||
fun wp_cases_method processors = Scan.succeed (fn ctxt =>
|
||||
Method.SIMPLE_METHOD (wp_cases_tac processors ctxt));
|
||||
|
||||
local structure P = Parse and K = Keyword in
|
||||
|
||||
fun add_wpc tm thm ctxt = let
|
||||
val thy = Proof_Context.theory_of ctxt
|
||||
val tm' = (Syntax.read_term ctxt tm) |> cterm_of thy o Logic.varify_global
|
||||
fun add_wpc tm thm lthy = let
|
||||
val ctxt = Local_Theory.exit lthy
|
||||
val tm' = (Syntax.read_term ctxt tm) |> Thm.cterm_of ctxt o Logic.varify_global
|
||||
val thm' = Proof_Context.get_thm ctxt thm
|
||||
in
|
||||
Local_Theory.background_theory (WPCPredicateAndFinals.map (fn xs => (tm', thm') :: xs)) ctxt
|
||||
Local_Theory.background_theory (WPCPredicateAndFinals.map (fn xs => (tm', thm') :: xs)) lthy
|
||||
end;
|
||||
|
||||
val wpcP =
|
||||
Outer_Syntax.command
|
||||
@{command_spec "wpc_setup"}
|
||||
@{command_keyword "wpc_setup"}
|
||||
"Add wpc stuff"
|
||||
(P.term -- P.name >> (fn (tm, thm) => Toplevel.local_theory NONE (add_wpc tm thm)))
|
||||
(P.term -- P.name >> (fn (tm, thm) => Toplevel.local_theory NONE NONE (add_wpc tm thm)))
|
||||
|
||||
end;
|
||||
end;
|
||||
|
@ -251,7 +251,7 @@ lemma wpc_helper_validF:
|
|||
setup {*
|
||||
|
||||
let
|
||||
val tm = cterm_of @{theory} (Logic.varify_global @{term "\<lambda>R. wpc_test P R S"});
|
||||
val tm = Thm.cterm_of @{context} (Logic.varify_global @{term "\<lambda>R. wpc_test P R S"});
|
||||
val thm = @{thm wpc_helper_validF};
|
||||
in
|
||||
WPCPredicateAndFinals.map (fn xs => (tm, thm) :: xs)
|
||||
|
@ -273,4 +273,5 @@ lemma case_options_weak_wp:
|
|||
apply simp
|
||||
done
|
||||
|
||||
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue