diff --git a/lib/Apply_Debug.thy b/lib/Apply_Debug.thy index 50f8b0eb4..b8c75457c 100644 --- a/lib/Apply_Debug.thy +++ b/lib/Apply_Debug.thy @@ -634,17 +634,18 @@ fun continue i_opt m_opt = fun markup_def rng = (Output.report - [Markup.markup (Markup.entity "breakpoint" "" - |> Markup.properties (Position.entity_properties_of true sr - (Position.range_position rng))) ""]); + [Markup.markup ( + Position.make_entity_markup {def=true} sr "breakpoint" + ("", Position.range_position rng)) + ""]); val _ = Option.map markup_def (get_latest_range (fst st'')); val _ = Option.map markup_def (get_breakpoint_range (fst st'')); val _ = (Context_Position.report ctxt (Position.thread_data ()) - (Markup.entity "breakpoint" "" - |> Markup.properties (Position.entity_properties_of false sr Position.none))) + (Position.make_entity_markup {def=false} sr "breakpoint" + ("", Position.none))) val _ = maybe_trace (#trace (get_break_opts ctxt)) st''; diff --git a/lib/Conjuncts.thy b/lib/Conjuncts.thy index a932bfd62..3d99d901a 100644 --- a/lib/Conjuncts.thy +++ b/lib/Conjuncts.thy @@ -23,7 +23,6 @@ local ( type T = thm; val empty: T = Drule.dummy_thm; - val extend = I; val merge : T * T -> T = (K Drule.dummy_thm); ); diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy index ec4d8a3cf..25b9fa13a 100644 --- a/lib/Eisbach_Methods.thy +++ b/lib/Eisbach_Methods.thy @@ -214,7 +214,7 @@ text \ \ setup \ Method.setup \<^binding>\prop_tac\ - (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >> + (Args.goal_spec -- Scan.lift (Scan.repeat1 Parse.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (props, fixes)) => fn ctxt => (SIMPLE_METHOD'' quant (EVERY' (map (fn prop => Rule_Insts.subgoal_tac ctxt prop fixes) props) diff --git a/lib/Eval_Bool.thy b/lib/Eval_Bool.thy index f9227b058..19d3e1ba4 100644 --- a/lib/Eval_Bool.thy +++ b/lib/Eval_Bool.thy @@ -124,8 +124,6 @@ end setup \Add_Locale_Code_Defs.setup "eval_bool_test_locale"\ -setup \Add_Locale_Code_Defs.setup "eval_bool_test_locale"\ - lemma "eval_bool_test_locale.z > 150" by eval_bool diff --git a/lib/FP_Eval.thy b/lib/FP_Eval.thy index a98409483..d84d6a17f 100644 --- a/lib/FP_Eval.thy +++ b/lib/FP_Eval.thy @@ -66,14 +66,14 @@ fun then_eq_reflection thm = let in Thm.implies_elim rule thm end; fun bool_conv_True thm = - Thm.instantiate ([], [((("P", 0), @{typ bool}), - Thm.dest_arg (Thm.cprop_of thm))]) + Thm.instantiate (TVars.empty, Vars.make [((("P", 0), @{typ bool}), + Thm.dest_arg (Thm.cprop_of thm))]) @{thm FP_Eval.bool_prop_eq_True} |> (fn conv => Thm.equal_elim conv thm); fun bool_conv_False thm = - Thm.instantiate ([], [((("P", 0), @{typ bool}), - Thm.dest_arg (Thm.dest_arg (Thm.cprop_of thm)))]) + Thm.instantiate (TVars.empty, Vars.make [((("P", 0), @{typ bool}), + Thm.dest_arg (Thm.dest_arg (Thm.cprop_of thm)))]) @{thm FP_Eval.bool_prop_eq_False} |> (fn conv => Thm.equal_elim conv thm); diff --git a/lib/FastMap.thy b/lib/FastMap.thy index 5c0fe634b..95a60f2a4 100644 --- a/lib/FastMap.thy +++ b/lib/FastMap.thy @@ -201,11 +201,10 @@ lemma lookup_tree_to_list_of_: (* this big blob just does case distinctions of both subtrees and all possible lookup results within each, then solves *) (* slow 10s *) - apply (fastforce simp: apfst_def map_prod_def map_add_def - split: prod.splits option.splits if_splits - dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range - elim: lookup_tree_valid_in_range_None) - done + by (fastforce simp: apfst_def map_prod_def map_add_def + split: prod.splits option.splits if_splits + dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range + elim: lookup_tree_valid_in_range_None) (* Standard form of above *) lemma lookup_tree_to_list_of: @@ -363,22 +362,22 @@ fun conv_at skel conv ctxt ct = let fun mismatch current_skel current_ct = raise TERM ("conv_at mismatch", [current_skel, Thm.term_of current_ct, skel, Thm.term_of ct]) - fun walk (Free ("HERE", _)) ctxt ct = conv ct + fun walk (Free ("HERE", _)) _ ct = conv ct | walk (skel as skel_f $ skel_x) ctxt ct = (case Thm.term_of ct of - f $ x => Conv.combination_conv (walk skel_f ctxt) (walk skel_x ctxt) ct + _ $ _ => Conv.combination_conv (walk skel_f ctxt) (walk skel_x ctxt) ct | _ => mismatch skel ct) | walk (skel as Abs (_, _, skel_body)) ctxt ct = (case Thm.term_of ct of - Abs _ => Conv.abs_conv (fn (v, ctxt') => walk skel_body ctxt') ctxt ct + Abs _ => Conv.abs_conv (fn (_, ctxt') => walk skel_body ctxt') ctxt ct | _ => mismatch skel ct) (* Also check that Consts match the skeleton pattern *) - | walk (skel as Const (skel_name, _)) ctxt ct = + | walk (skel as Const (skel_name, _)) _ ct = if (case Thm.term_of ct of Const (name, _) => name = skel_name | _ => false) then Thm.reflexive ct else mismatch skel ct (* Default case *) - | walk _ ctxt ct = Thm.reflexive ct + | walk _ _ ct = Thm.reflexive ct in walk skel ctxt ct end fun gconv_at_tac pat conv ctxt = Conv.gconv_rule (conv_at pat conv ctxt) 1 #> Seq.succeed diff --git a/lib/LemmaBucket.thy b/lib/LemmaBucket.thy index a9733c834..b1b631274 100644 --- a/lib/LemmaBucket.thy +++ b/lib/LemmaBucket.thy @@ -314,7 +314,7 @@ lemma card_of_dom_bounded: by (simp add: assms card_mono) lemma third_in: "(a, b, c) \ S \ c \ (snd \ snd) ` S" - by (metis (erased, hide_lams) map_set_in image_comp snd_conv) + by (metis (erased, opaque_lifting) map_set_in image_comp snd_conv) lemma third_in2: "(a \ (snd \ snd) ` (set (enumerate i xs))) = (a \ snd ` (set xs))" by (metis map_map map_snd_enumerate set_map) @@ -357,7 +357,7 @@ lemma distinct_map_via_ran: "distinct (map fst xs) \ ran (map_of by (simp add: ran_distinct) lemma in_ran_in_set: "x \ ran (map_of xs) \ x \ set (map snd xs)" - by (metis (mono_tags, hide_lams) map_set_in map_of_SomeD ranE set_map snd_conv) + by (metis (mono_tags) map_set_in map_of_SomeD ranE set_map snd_conv) lemma in_ran_map_app: "x \ ran (xs ++ ys ++ zs) \ x \ ran xs \ x \ ran ys \ x \ ran zs" proof - diff --git a/lib/Lib.thy b/lib/Lib.thy index a8c25f1d9..e22c44356 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -2413,9 +2413,7 @@ lemma insert_subtract_new: "x \ S \ (insert x S - S) = {x}" by auto -lemma zip_is_empty: - "(zip xs ys = []) = (xs = [] \ ys = [])" - by (cases xs; simp) (cases ys; simp) +lemmas zip_is_empty = zip_eq_Nil_iff lemma minus_Suc_0_lt: "a \ 0 \ a - Suc 0 < a" @@ -2426,14 +2424,9 @@ lemma fst_last_zip_upt: fst (last (zip [0 ..< m] xs)) = (if length xs < m then length xs - 1 else m - 1)" apply (subst last_conv_nth, assumption) apply (simp only: One_nat_def) - apply (subst nth_zip) - apply (rule order_less_le_trans[OF minus_Suc_0_lt]) - apply (simp add: zip_is_empty) - apply simp - apply (rule order_less_le_trans[OF minus_Suc_0_lt]) - apply (simp add: zip_is_empty) - apply simp - apply (simp add: min_def zip_is_empty) + apply (subst nth_zip; simp) + apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp) + apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp) done lemma neq_into_nprefix: @@ -2582,7 +2575,7 @@ lemma nat_int_mul: lemma int_shiftl_less_cancel: "n \ m \ ((x :: int) << n < y << m) = (x < y << (m - n))" apply (drule le_Suc_ex) - apply (clarsimp simp: shiftl_int_def power_add) + apply (clarsimp simp: shiftl_def shiftl_int_def power_add) done lemma int_shiftl_lt_2p_bits: @@ -2591,11 +2584,7 @@ lemma int_shiftl_lt_2p_bits: by (metis bit_take_bit_iff not_less take_bit_int_eq_self_iff) \ \TODO: The converse should be true as well, but seems hard to prove.\ -lemma int_eq_test_bit: - "((x :: int) = y) = (\i. test_bit x i = test_bit y i)" - apply simp - apply (metis bin_eqI) - done +lemmas int_eq_test_bit = bin_eq_iff lemmas int_eq_test_bitI = int_eq_test_bit[THEN iffD2, rule_format] lemma le_nat_shrink_left: diff --git a/lib/Monad_WP/wp/WPC.thy b/lib/Monad_WP/wp/WPC.thy index cff8311d0..cd19db0e4 100644 --- a/lib/Monad_WP/wp/WPC.thy +++ b/lib/Monad_WP/wp/WPC.thy @@ -86,7 +86,6 @@ structure WPCPredicateAndFinals = Theory_Data (struct type T = (cterm * thm) list val empty = [] - val extend = I fun merge (xs, ys) = (* Order of predicates is important, so we can't reorder *) let val tms = map (Thm.term_of o fst) xs @@ -119,11 +118,11 @@ let val thm_pred_tvar = Term.dest_TVar (get_pred_tvar thm_pred); val pred_tvar = Thm.ctyp_of ctxt (get_pred_tvar pred); - val thm2 = Thm.instantiate ([(thm_pred_tvar, pred_tvar)], []) thm; + val thm2 = Thm.instantiate (TVars.make [(thm_pred_tvar, pred_tvar)], Vars.empty) thm; val thm2_pred = Term.dest_Var (get_concl_pred thm2); in - Thm.instantiate ([], [(thm2_pred, pred)]) thm2 + Thm.instantiate (TVars.empty, Vars.make [(thm2_pred, pred)]) thm2 end; fun detect_term ctxt n thm tm = diff --git a/lib/Monad_WP/wp/WPEx.thy b/lib/Monad_WP/wp/WPEx.thy index 2760e2552..d68589703 100644 --- a/lib/Monad_WP/wp/WPEx.thy +++ b/lib/Monad_WP/wp/WPEx.thy @@ -10,25 +10,15 @@ imports Strengthen begin +(* Only the wps method and wps_tac are left of this experiment: *) text \WPEx - the WP Extension Experiment\ -definition - mresults :: "('s, 'a) nondet_monad \ ('a \ 's \ 's) set" -where +definition mresults :: "('s, 'a) nondet_monad \ ('a \ 's \ 's) set" where "mresults f = {(rv, s', s). (rv, s') \ fst (f s)}" -definition - assert_value_exported :: "'x \ 's \ ('s, 'a) nondet_monad \ ('x \ ('s, 'a) nondet_monad)" -where - "assert_value_exported x f y \ - do s \ get; if x = (y, s) then f else fail od" - -syntax - "_assert_bind" :: "['a, 'b] => dobind" ("_ =<= _") - -translations - "do v =<= a; e od" == "a >>= CONST assert_value_exported v e" - "doE v =<= a; e odE" == "a >>=E CONST assert_value_exported v e" +definition assert_value_exported :: + "'x \ 's \ ('s, 'a) nondet_monad \ ('x \ ('s, 'a) nondet_monad)" where + "assert_value_exported x f y \ do s \ get; if x = (y, s) then f else fail od" lemma in_mresults_export: "(rv, s', s) \ mresults (assert_value_exported (rv', s'') f rv'') @@ -38,189 +28,32 @@ lemma in_mresults_export: lemma in_mresults_bind: "(rv, s', s) \ mresults (a >>= b) = (\rv' s''. (rv, s', s'') \ mresults (b rv') \ (rv', s'', s) \ mresults a)" - apply (simp add: mresults_def bind_def) - apply (auto elim: rev_bexI) - done + by (auto simp: mresults_def bind_def elim: rev_bexI) lemma mresults_export_bindD: - "(rv, s', s) \ mresults (a >>= assert_value_exported (rv', s'') b) - \ (rv, s', s'') \ mresults b" - "(rv, s', s) \ mresults (a >>= assert_value_exported (rv', s'') b) - \ (rv', s'', s) \ mresults a" + "(rv, s', s) \ mresults (a >>= assert_value_exported (rv', s'') b) \ (rv, s', s'') \ mresults b" + "(rv, s', s) \ mresults (a >>= assert_value_exported (rv', s'') b) \ (rv', s'', s) \ mresults a" by (simp_all add: in_mresults_export in_mresults_bind) -definition "wpex_name_for_id = id" - -definition "wpex_name_for_id_prop p \ (p :: prop)" - -lemma wpex_name_for_id_propI: - "PROP p \ PROP wpex_name_for_id_prop p" - by (simp add: wpex_name_for_id_prop_def) - -lemma wpex_name_for_id_propE: - "PROP wpex_name_for_id_prop p \ PROP p" - by (simp add: wpex_name_for_id_prop_def) - -lemma del_asm_rule: - "\ PROP P; PROP Q \ \ PROP Q" - by assumption - -ML \ - -val p_prop_var = Term.dest_Var (Logic.varify_global @{term "P :: prop"}); - -fun del_asm_tac asm = - eresolve0_tac [(Thm.instantiate ([], [(p_prop_var, asm)]) @{thm del_asm_rule})]; - -fun subgoal_asm_as_thm tac = - Subgoal.FOCUS_PARAMS (fn focus => SUBGOAL (fn (t, _) => let - val asms = Logic.strip_assums_hyp t; - val ctxt = #context focus; - fun asm_tac asm = (Subgoal.FOCUS_PREMS (fn focus => let - fun is_asm asm' = asm aconv (Thm.concl_of asm'); - val (asm' :: _) = filter is_asm (#prems focus); - in tac asm' end) (#context focus) - THEN_ALL_NEW del_asm_tac (Thm.cterm_of ctxt asm)) 1; - in - FIRST (map asm_tac asms) - end) 1); - -exception SAME; - -fun eta_flat (Abs (name, tp, (Abs a))) - = eta_flat (Abs (name, tp, eta_flat (Abs a))) - | eta_flat (Abs (_, _, t $ Bound 0)) - = if member (=) (loose_bnos t) 0 then raise SAME - else subst_bound (Bound 0, t) - | eta_flat (Abs (name, tp, t $ Abs a)) - = eta_flat (Abs (name, tp, t $ eta_flat (Abs a))) - | eta_flat _ = raise SAME; - -fun const_spine t = case strip_comb t of - (Const c, xs) => SOME (c, xs) - | (Abs v, []) => (const_spine (eta_flat (Abs v)) handle SAME => NONE) - | (Abs _, (_ :: _)) => error "const_spine: term not beta expanded" - | _ => NONE; - -fun build_annotate' t wr ps = case (const_spine t, wr) of - (SOME (bd as ("NonDetMonad.bind", _), [a, b]), - "WPEx.mresults") => let - val (a', ps') = build_annotate' a "WPEx.mresults" ps; - in case const_spine b of - SOME (ass as ("WPEx.assert_value_exported", _), [rvs, c]) - => let - val (c', ps'') = build_annotate' c "WPEx.mresults" ps' - in (Const bd $ a' $ (Const ass $ rvs $ c'), ps'') end - | _ => let - val tp = fastype_of (Const bd); - val btp = domain_type (range_type tp); - val rtp = domain_type btp; - val stp = domain_type (range_type btp); - val mtp = range_type (range_type btp); - val ass = Const ("WPEx.assert_value_exported", - HOLogic.mk_prodT (rtp, stp) --> - (stp --> mtp) --> rtp --> stp --> mtp); - val rv = Bound (length ps'); - val s = Bound (length ps' + 1); - val rvs = HOLogic.pair_const rtp stp $ rv $ s; - val b' = betapply (b, Bound (length ps')); - val borings = ["x", "y", "rv"]; - val rvnms = case b of - Abs (rvnm, _, _) => - if member (=) borings rvnm then [] - else [(rvnm, rvnm ^ "_st")] - | _ => []; - val cnms = case const_spine a' of - SOME ((cnm, _), _) => let - val cnm' = List.last (space_explode "." cnm); - in [(cnm' ^ "_rv", cnm' ^ "_st")] end - | _ => []; - val nms = hd (rvnms @ cnms @ [("rv", "s")]); - val ps'' = ps' @ [(fst nms, rtp), (snd nms, stp)]; - val (b'', ps''') = build_annotate' b' "WPEx.mresults" ps''; - in (Const bd $ a' $ (ass $ rvs $ b''), ps''') end - end - | _ => (t, ps); - -fun build_annotate asm = - case const_spine (HOLogic.dest_Trueprop (Envir.beta_norm asm)) of - SOME (memb as ("Set.member", _), [x, st]) => (case const_spine st of - SOME (mres as ("WPEx.mresults", _), [m]) => let - val (m', ps) = build_annotate' m "WPEx.mresults" []; - val _ = if null ps then raise SAME else (); - val t = Const memb $ x $ (Const mres $ m'); - fun mk_exists ((s, tp), tm) = HOLogic.exists_const tp $ Abs (s, tp, tm); - in HOLogic.mk_Trueprop (Library.foldr mk_exists (rev ps, t)) end - | _ => raise SAME) | _ => raise SAME; - - -val put_Lib_simpset = put_simpset (Simplifier.simpset_of (Proof_Context.init_global @{theory Lib})) - - -fun in_mresults_ctxt ctxt = ctxt - |> put_Lib_simpset - |> (fn ctxt => ctxt addsimps [@{thm in_mresults_export}, @{thm in_mresults_bind}]) - |> Splitter.del_split @{thm if_split} - -fun prove_qad ctxt term tac = Goal.prove ctxt [] [] term - (K (if Config.get ctxt quick_and_dirty andalso false - then ALLGOALS (Skip_Proof.cheat_tac ctxt) - else tac)); - -fun preannotate_ss ctxt = ctxt - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps [@{thm K_bind_def}]) - |> simpset_of - -fun in_mresults_ss ctxt = ctxt - |> put_Lib_simpset - |> (fn ctxt => ctxt addsimps [@{thm in_mresults_export}, @{thm in_mresults_bind}]) - |> Splitter.del_split @{thm if_split} - |> simpset_of - - -val in_mresults_cs = Classical.claset_of (Proof_Context.init_global @{theory Lib}); - -fun annotate_tac ctxt asm = let - val asm' = simplify (put_simpset (preannotate_ss ctxt) ctxt) asm; - val annotated = build_annotate (Thm.concl_of asm'); - val ctxt' = Classical.put_claset in_mresults_cs (put_simpset (in_mresults_ss ctxt) ctxt) - val thm = prove_qad ctxt (Logic.mk_implies (Thm.concl_of asm', annotated)) - (auto_tac ctxt' - THEN ALLGOALS (TRY o blast_tac ctxt')); - in - cut_facts_tac [asm' RS thm] 1 - end - handle SAME => no_tac; - -fun annotate_goal_tac ctxt - = REPEAT_DETERM1 (subgoal_asm_as_thm (annotate_tac ctxt) ctxt 1 - ORELSE (eresolve_tac ctxt [exE] 1)); - -val annotate_method = - Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (annotate_goal_tac ctxt)) - : (Proof.context -> Method.method) context_parser; - -\ - -method_setup annotate = \annotate_method\ "tries to annotate" +definition wpex_name_for_id :: "'a \ 'a" where + "wpex_name_for_id = id" lemma use_valid_mresults: "\ (rv, s', s) \ mresults f; \P\ f \Q\ \ \ P s \ Q rv s'" by (auto simp: mresults_def valid_def) -lemma mresults_validI: - "\ \rv s' s. (rv, s', s) \ mresults f \ P s \ Q rv s' \ - \ \P\ f \Q\" - by (auto simp: mresults_def valid_def) +lemma valid_strengthen_with_mresults: + "\ \s rv s'. \ (rv, s', s) \ mresults f; wpex_name_for_id (Q' s rv s') \ \ Q rv s'; + \prev_s. \P prev_s\ f \Q' prev_s\ \ + \ \\s. P s s\ f \Q\" + by (clarsimp simp: valid_def mresults_def wpex_name_for_id_def) blast + +lemma wpex_name_for_idE: "wpex_name_for_id P \ P" + by (simp add: wpex_name_for_id_def) ML \ -val use_valid_mresults = @{thm use_valid_mresults}; - -val mresults_export_bindD = @{thms mresults_export_bindD}; - -fun dest_mresults_tac t = Seq.of_list ([t] RL mresults_export_bindD); +fun dest_mresults_tac t = Seq.of_list ([t] RL @{thms mresults_export_bindD}); (* take a rule of conclusion p --> q and decide whether to use it as an introduction rule or if of form ?P x --> ?P y to use it @@ -238,7 +71,7 @@ fun get_rule_uses ctxt rule = let $ Bound (length argtps - n) $ x; val v' = fold_rev Term.abs (map (pair "x") argtps) eq; in rule - |> Thm.instantiate ([], [(Term.dest_Var v, ct v')]) + |> Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var v, ct v')]) |> simplify (put_simpset HOL_ss ctxt) end; in case (strip_comb p, strip_comb q) of @@ -254,21 +87,12 @@ fun get_wp_simps_strgs ctxt rules asms = let val wp_rules = rules @ (WeakestPre.debug_get ctxt |> #rules |> WeakestPre.dest_rules); val wp_rules' = filter (null o Thm.prems_of) wp_rules; val asms' = maps (Seq.list_of o REPEAT dest_mresults_tac) asms; - val uses = asms' RL [use_valid_mresults]; + val uses = asms' RL [@{thm use_valid_mresults}]; val wp_rules'' = wp_rules' RL uses; in apply2 flat (map_split (get_rule_uses ctxt) wp_rules'') end; -fun tac_with_wp_simps_strgs ctxt rules tac = - subgoal_asm_as_thm (fn asm => let - val (simps, strgs) = get_wp_simps_strgs ctxt rules [asm] - in - cut_facts_tac [asm] 1 THEN tac (simps, strgs) - end) ctxt; - -val mresults_validI = @{thm mresults_validI}; - fun postcond_ss ctxt = ctxt |> put_simpset HOL_basic_ss |> (fn ctxt => ctxt addsimps [@{thm pred_conj_def}]) @@ -279,82 +103,18 @@ fun wp_default_ss ctxt = ctxt |> Splitter.del_split @{thm if_split} |> simpset_of -fun raise_tac s = all_tac THEN (fn _ => error s); - -fun wpx_tac ctxt rules - = TRY (resolve_tac ctxt [mresults_validI] 1) - THEN (full_simp_tac (put_simpset (postcond_ss ctxt) ctxt) 1) - THEN TRY (annotate_goal_tac ctxt) - THEN tac_with_wp_simps_strgs ctxt rules (fn (simps, strgs) => - REPEAT_DETERM1 - (CHANGED (full_simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1) - ORELSE Strengthen.default_strengthen ctxt strgs 1) - ) 1; - -val wpx_method = Attrib.thms >> curry (fn (ts, ctxt) => - Method.SIMPLE_METHOD (wpx_tac ctxt ts)); - -\ - -method_setup wpx = \wpx_method\ "experimental wp method" - -lemma foo: - "(rv, s', s) \ mresults (do x \ get; y \ get; put (x + y :: nat); return () od) - \ s' = s + s" - apply annotate - apply wpx - done - -lemma foo2: - "(rv, s', s) \ mresults (do x \ get; y \ get; put (if z = Suc 0 then x + y else x + y + z); return () od) - \ s' = s + s + (if z = Suc 0 then 0 else z)" - apply wpx - apply simp - done - -text \Have played around with it, the issues are: - 1: Need to deal with non-linear code, known issue. - 2: Using fastforce in annotate isn't cutting the mustard, need to automate better. - Probably half the issue is that there are too many simp rules available. - 3: Related to (2), there's the question of whether you can simplify code enough - once it's been annotated. This may re-raise the specter of annotation on demand. - 4: It's hard to tell whether it's worked or not. - 5: Structural rules don't really work - rules that want to transform the whole - postcondition once we get up to a particular point. Related to 4, it's hard to - say where that point is hit. - 6: Performance problems with getting the set of available rules. -\ - -lemma valid_strengthen_with_mresults: - "\ \s rv s'. \ (rv, s', s) \ mresults f; - wpex_name_for_id (Q' s rv s') \ \ Q rv s'; - \prev_s. \P prev_s\ f \Q' prev_s\ \ - \ \\s. P s s\ f \Q\" - apply atomize - apply (clarsimp simp: valid_def mresults_def wpex_name_for_id_def) - apply blast - done - -lemma wpex_name_for_idE: "wpex_name_for_id P \ P" - by (simp add: wpex_name_for_id_def) - -ML \ - -val valid_strengthen_with_mresults = @{thm valid_strengthen_with_mresults}; -val wpex_name_for_idE = @{thm wpex_name_for_idE}; - fun wps_tac ctxt rules = let (* avoid duplicate simp rule etc warnings: *) val ctxt = Context_Position.set_visible false ctxt in - resolve_tac ctxt [valid_strengthen_with_mresults] + resolve_tac ctxt [@{thm valid_strengthen_with_mresults}] THEN' (safe_simp_tac (put_simpset (postcond_ss ctxt) ctxt)) THEN' Subgoal.FOCUS (fn focus => let val ctxt = #context focus; val (simps, _) = get_wp_simps_strgs ctxt rules (#prems focus); in CHANGED (simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1) end) ctxt - THEN' eresolve_tac ctxt [wpex_name_for_idE] + THEN' eresolve_tac ctxt [@{thm wpex_name_for_idE}] end val wps_method = Attrib.thms >> curry @@ -364,11 +124,15 @@ val wps_method = Attrib.thms >> curry method_setup wps = \wps_method\ "experimental wp simp method" -lemma foo3: - "\P\ do v \ return (Suc 0); return (Suc (Suc 0)) od \(=)\" +experiment +begin + +lemma "\P\ do v \ return (Suc 0); return (Suc (Suc 0)) od \(=)\" apply (rule hoare_pre) apply (rule hoare_seq_ext)+ apply (wps | rule hoare_vcg_prop)+ oops end + +end diff --git a/lib/Monad_WP/wp/WPI.thy b/lib/Monad_WP/wp/WPI.thy index d02d1a988..50dbd6239 100644 --- a/lib/Monad_WP/wp/WPI.thy +++ b/lib/Monad_WP/wp/WPI.thy @@ -254,7 +254,7 @@ ML \ val frees = Term.add_frees t []; val frees' = Term.add_frees t' []; in - exists (member (=) frees') frees + exists (member (op =) frees') frees end \ @@ -511,7 +511,7 @@ end notepad begin - fix f and Q P P' :: "int \ 'a \ bool" and Q' :: "'a \ bool" and a + fix f :: "'a \ ('a,'b) nondet_monad" and Q P P' :: "int \ 'a \ bool" and Q' :: "'a \ bool" and a :: 'a { assume P[wp]: "\PP x. \\s. PP (P x s)\ f a \\r s. PP (P x s)\" diff --git a/lib/NICTATools.thy b/lib/NICTATools.thy index f406304b4..411248ec6 100644 --- a/lib/NICTATools.thy +++ b/lib/NICTATools.thy @@ -76,8 +76,10 @@ in end (* Setup the tool, stealing the "auto_solve_direct" option. *) -val _ = Try.tool_setup ("unused_meta_forall", - (1, @{system_option auto_solve_direct}, detect_unused_meta_forall)) +val _ = Try.tool_setup { name = "unused_meta_forall", + weight = 1, + auto_option = \<^system_option>\auto_solve_direct\, + body = detect_unused_meta_forall } \ lemma test_unused_meta_forall: "\x. y \ \ y" diff --git a/lib/NatBitwise.thy b/lib/NatBitwise.thy index 88cb798fa..2d6ce5aed 100644 --- a/lib/NatBitwise.thy +++ b/lib/NatBitwise.thy @@ -11,11 +11,6 @@ imports Lib begin -instantiation nat :: semiring_bit_syntax -begin -instance .. -end - instantiation nat :: lsb begin @@ -45,34 +40,33 @@ definition 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) - + (metis (mono_tags) set_bit_nat_def bin_nth_sc_gen bin_sc_pos + bit_nat_iff exp_eq_0_imp_not_bit int_eq_iff) end - lemma nat_2p_eq_shiftl: "(2::nat)^x = 1 << x" - by (simp add: shiftl_eq_push_bit) + by simp lemma shiftl_nat_alt_def: "(x::nat) << n = x * 2^n" - by (simp add: push_bit_nat_def shiftl_eq_push_bit) + by (simp add: push_bit_nat_def shiftl_def) lemma shiftl_nat_def: "(x::nat) << y = nat (int x << y)" - by (simp add: nat_int_mul shiftl_int_def shiftl_nat_alt_def) + by (simp add: nat_int_mul push_bit_eq_mult shiftl_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) + apply (simp add: nat_int_comparison(2) shiftl_nat_def shiftl_def) + by (metis int_shiftl_less_cancel shiftl_def) lemma nat_shiftl_lt_2p_bits: "(x::nat) < 1 << n \ \i \ n. \ x !! i" - apply (clarsimp simp: shiftl_nat_def zless_nat_eq_int_zless shiftl_eq_push_bit push_bit_of_1 + apply (clarsimp simp: shiftl_nat_def zless_nat_eq_int_zless dest!: le_Suc_ex) - by (metis bit_take_bit_iff not_add_less1 take_bit_nat_eq_self_iff test_bit_eq_bit) + by (metis bit_take_bit_iff not_add_less1 take_bit_nat_eq_self_iff) lemmas nat_eq_test_bit = bit_eq_iff lemmas nat_eq_test_bitI = bit_eq_iff[THEN iffD2, rule_format] diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index e751d1a96..989724b42 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -1003,13 +1003,13 @@ lemma zipWithM_If_cut: apply (cases "n < m") apply (cut_tac i=0 and j=n and k="m - n" in upt_add_eq_append) apply simp - apply (simp add: min.absorb1 zipWithM_mapM) + apply (simp add: zipWithM_mapM) apply (simp add: zip_append1 mapM_append zip_take_triv2 split_def) apply (intro bind_cong bind_apply_cong refl mapM_length_cong fun_cong[OF mapM_length_cong]) apply (clarsimp simp: set_zip) apply (clarsimp simp: set_zip) - apply (simp add: min.absorb2 zipWithM_mapM mapM_Nil) + apply (simp add: zipWithM_mapM mapM_Nil) apply (intro mapM_length_cong refl) apply (clarsimp simp: set_zip) done @@ -3028,12 +3028,12 @@ proof - apply (intro conjI) apply (rule set_eqI) apply (rule iffI) - apply (clarsimp simp:Union_eq dest!: singletonD) + apply (clarsimp simp:Union_eq) apply (frule fsame) apply clarsimp apply (frule gsame) apply (metis fst_conv snd_conv) - apply (clarsimp simp:Union_eq dest!: singletonD) + apply (clarsimp simp:Union_eq) apply (frule gsame) apply clarsimp apply (frule fsame) diff --git a/lib/ProvePart.thy b/lib/ProvePart.thy index ec99432a0..5634bb177 100644 --- a/lib/ProvePart.thy +++ b/lib/ProvePart.thy @@ -128,13 +128,13 @@ ML \ structure Partial_Prove = struct fun inst_frees_tac _ Ps ct = REPEAT_DETERM o SUBGOAL (fn (t, _) => - fn thm => case Term.add_frees t [] |> filter (member (=) Ps) + fn thm => case Term.add_frees t [] |> filter (member (op =) Ps) of [] => Seq.empty | (f :: _) => let val idx = Thm.maxidx_of thm + 1 val var = ((fst f, idx), snd f) - in thm |> Thm.generalize ([], [fst f]) idx - |> Thm.instantiate ([], [(var, ct)]) + in thm |> Thm.generalize (Names.empty, Names.make_set [fst f]) idx + |> Thm.instantiate (TVars.empty, Vars.make [(var, ct)]) |> Seq.single end) @@ -172,7 +172,7 @@ fun partial_prove tactic ctxt i fun method (ctxtg, []) = (fn ctxt => Method.SIMPLE_METHOD (test_start_partial_prove ctxt 1), (ctxtg, [])) - | method args = error "Partial_Prove: still working on that" + | method _ = error "Partial_Prove: still working on that" fun fin_method () = Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (test_end_partial_prove ctxt)) diff --git a/lib/Qualify.thy b/lib/Qualify.thy index 52fc026b4..f8353cf15 100644 --- a/lib/Qualify.thy +++ b/lib/Qualify.thy @@ -25,7 +25,6 @@ structure Data = Theory_Data ( type T = (theory * qualify_args) option; val empty = NONE; - val extend = I; fun merge ((_, _) : T * T) = NONE; ); diff --git a/lib/ROOT b/lib/ROOT index 86bf2f9e0..ad05d7a67 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -97,7 +97,6 @@ session Lib (lib) = Word_Lib + "Monad_WP/wp/Eisbach_WP" "Monad_WP/wp/WPI" "Monad_WP/wp/WPC" - "Monad_WP/wp/WPEx" "Monad_WP/wp/WP_Pre" "Monad_WP/wp/WP" "Monad_WP/Datatype_Schematic" diff --git a/lib/RangeMap.thy b/lib/RangeMap.thy index ac6bb5e59..c37f8f106 100644 --- a/lib/RangeMap.thy +++ b/lib/RangeMap.thy @@ -442,7 +442,7 @@ proof (induct tree) ([((start, end), v)] @ lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x" - using lookup_range_tree_to_list.simps append_assoc + using lookup_range_tree_to_list.simps(2) append_assoc lookup_map_of_append_commute[OF treeL1_disjoint] lookup_map_of_append_cong[OF _ refl] by metis diff --git a/lib/Rule_By_Method.thy b/lib/Rule_By_Method.thy index 96b0adefe..3933fe29f 100644 --- a/lib/Rule_By_Method.thy +++ b/lib/Rule_By_Method.thy @@ -23,10 +23,10 @@ fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt); fun fix_schematics ctxt raw_st = let val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt; - fun certify_inst ctxt inst = map (apsnd (Thm.cterm_of ctxt)) (#2 inst) + fun certify_inst ((_, terms), ctxt) = (Vars.map (K (Thm.cterm_of ctxt)) terms, ctxt); val (schematic_terms, ctxt2) = Variable.import_inst true [Thm.prop_of st'] ctxt1 - |>> certify_inst ctxt1; + |> certify_inst; val schematics = (schematic_types, schematic_terms); in (Thm.instantiate schematics st', ctxt2) end @@ -60,7 +60,7 @@ let in Thm.implies_elim asm (Thm.trivial @{cprop "PROP A"}) |> Drule.implies_intr_hyps - |> Thm.generalize ([],["A"]) 1 + |> Thm.generalize (Names.empty, Names.make_set ["A"]) 1 |> Drule.zero_var_indexes end @@ -77,7 +77,7 @@ in |> Thm.implies_elim (asm' COMP Drule.equal_elim_rule2) |> Drule.implies_intr_hyps |> Thm.permute_prems 0 ~1 - |> Thm.generalize ([],["A","P"]) 1 + |> Thm.generalize (Names.empty, Names.make_set ["A","P"]) 1 |> Drule.zero_var_indexes end diff --git a/lib/SimpStrategy.thy b/lib/SimpStrategy.thy index 5c03a591b..063dbfc38 100644 --- a/lib/SimpStrategy.thy +++ b/lib/SimpStrategy.thy @@ -55,7 +55,7 @@ lemma Eq_TrueI_ByAssum: simproc_setup simp_strategy_ByAssum ("simp_strategy ByAssum b") = \K (fn ss => fn ct => let val b = Thm.dest_arg ct - val t = Thm.instantiate ([],[((("P",0),@{typ bool}), b)]) + val t = Thm.instantiate (TVars.empty, Vars.make [((("P",0),@{typ bool}), b)]) @{thm Eq_TrueI_ByAssum} val prems = Raw_Simplifier.prems_of ss in get_first (try (fn p => p RS t)) prems end)\ @@ -83,7 +83,7 @@ lemma simp_strategy_Eq_True: ML \ fun simp_strategy_True_conv ct = case Thm.term_of ct of (Const (@{const_name simp_strategy}, _) $ _ $ @{term True}) - => Thm.instantiate ([], [((("name",0), @{typ nat}), Thm.dest_arg1 ct)]) + => Thm.instantiate (TVars.empty, Vars.make [((("name",0), @{typ nat}), Thm.dest_arg1 ct)]) @{thm simp_strategy_Eq_True} | _ => Conv.all_conv ct diff --git a/lib/Trace_Schematic_Insts.thy b/lib/Trace_Schematic_Insts.thy index 1987552e2..77896b093 100644 --- a/lib/Trace_Schematic_Insts.thy +++ b/lib/Trace_Schematic_Insts.thy @@ -183,9 +183,9 @@ fun attach_proof_annotations ctxt terms st = (* FIXME: this might affect st's maxidx *) val add_eqn = Thm.instantiate - ([], - [((("P", 0), @{typ prop}), cconcl_of st), - ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)]) + (TVars.empty, + Vars.make [((("P", 0), @{typ prop}), cconcl_of st), + ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)]) @{thm proof_state_add} in rewrite_state_concl add_eqn st @@ -208,9 +208,9 @@ fun detach_proof_annotations st = |> dest_term_container val remove_eqn = Thm.instantiate - ([], - [((("P", 0), @{typ prop}), real_concl), - ((("xs", 0), @{typ bool}), ccontainer)]) + (TVars.empty, + Vars.make [((("P", 0), @{typ prop}), real_concl), + ((("xs", 0), @{typ bool}), ccontainer)]) @{thm proof_state_remove} in (terms, rewrite_state_concl remove_eqn st) @@ -227,9 +227,9 @@ fun attach_rule_annotations ctxt terms thm = (* FIXME: this might affect thm's maxidx *) val add_eqn = Thm.instantiate - ([], - [((("P", 0), @{typ prop}), Thm.cconcl_of thm), - ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)]) + (TVars.empty, + Vars.make [((("P", 0), @{typ prop}), Thm.cconcl_of thm), + ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)]) @{thm rule_add} in rewrite_state_concl add_eqn thm @@ -349,7 +349,7 @@ fun instantiate_types ctxt _ tvar_insts term = val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt) tvar_inst Vartab.empty val S = Vartab.dest tyenv val S' = map (fn (s,(t,u)) => ((s,t),u)) S - in Term_Subst.instantiateT S' typ + in Term_Subst.instantiateT (TVars.make S') typ end in fold (fn typs => Term.map_types (instantiateT typs)) tvar_insts term end diff --git a/lib/Try_Methods.thy b/lib/Try_Methods.thy index a0a3d4267..238e7a873 100644 --- a/lib/Try_Methods.thy +++ b/lib/Try_Methods.thy @@ -30,7 +30,6 @@ structure Methods = Theory_Data ( type T = Symtab.set; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge (K true); ); diff --git a/lib/ml-helpers/TermPatternAntiquote.thy b/lib/ml-helpers/TermPatternAntiquote.thy index 39e8c2260..94a9246dc 100644 --- a/lib/ml-helpers/TermPatternAntiquote.thy +++ b/lib/ml-helpers/TermPatternAntiquote.thy @@ -60,7 +60,7 @@ fun term_pattern_antiquote ctxt s = end; val _ = Context.>> (Context.map_theory ( ML_Antiquotation.inline @{binding "term_pat"} - ((Args.context -- Scan.lift Args.embedded_inner_syntax) + ((Args.context -- Scan.lift Parse.embedded_inner_syntax) >> uncurry Term_Pattern_Antiquote.term_pattern_antiquote))) \ diff --git a/lib/ml-helpers/mkterm_antiquote.ML b/lib/ml-helpers/mkterm_antiquote.ML index b5a20f758..eb51244b3 100644 --- a/lib/ml-helpers/mkterm_antiquote.ML +++ b/lib/ml-helpers/mkterm_antiquote.ML @@ -171,7 +171,7 @@ local in val _ = Context.>> (Context.map_theory ( ML_Antiquotation.inline @{binding "mk_term"} - ((Args.context -- Scan.lift Args.embedded_inner_syntax -- (Scan.optional (Scan.lift ((comma_list Args.name))) [])) + ((Args.context -- Scan.lift Parse.embedded_inner_syntax -- (Scan.optional (Scan.lift ((comma_list Args.name))) [])) >> gen_constructor))) end diff --git a/lib/subgoal_focus/Subgoal_Methods.thy b/lib/subgoal_focus/Subgoal_Methods.thy index 44e3d2d5e..8896b490d 100644 --- a/lib/subgoal_focus/Subgoal_Methods.thy +++ b/lib/subgoal_focus/Subgoal_Methods.thy @@ -45,7 +45,7 @@ fun fix_schematics ctxt raw_st = val ((_, inst), ctxt2) = Variable.import_inst true [Thm.prop_of st'] ctxt1; - val schematic_terms = map (apsnd (Thm.cterm_of ctxt2)) inst; + val schematic_terms = Vars.map (K (Thm.cterm_of ctxt2)) inst; val schematics = (schematic_types, schematic_terms); in (Thm.instantiate schematics st', ctxt2) end diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy index d91b8d0eb..78cf9866c 100644 --- a/spec/machine/MachineExports.thy +++ b/spec/machine/MachineExports.thy @@ -50,7 +50,6 @@ requalify_consts lemma Suc_unat_mask_div_obfuscated: "Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)" - unfolding word_size_bits_def by (rule Suc_unat_mask_div) lemma word_size_size_bits_nat: