(* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) theory WPC imports "WP_Pre" keywords "wpc_setup" :: thy_decl begin definition wpc_helper :: "(('a \ bool) \ 'b set) \ (('a \ bool) \ 'b set) \ bool \ bool" where "wpc_helper \ \(P, P') (Q, Q') R. ((\s. P s \ Q s) \ P' \ Q') \ R" lemma wpc_conj_process: "\ wpc_helper (P, P') (A, A') C; wpc_helper (P, P') (B, B') D \ \ wpc_helper (P, P') (\s. A s \ B s, A' \ B') (C \ D)" by (clarsimp simp add: wpc_helper_def) lemma wpc_all_process: "\ \x. wpc_helper (P, P') (Q x, Q' x) (R x) \ \ wpc_helper (P, P') (\s. \x. Q x s, {s. \x. s \ Q' x}) (\x. R x)" by (clarsimp simp: wpc_helper_def subset_iff) lemma wpc_all_process_very_weak: "\ \x. wpc_helper (P, P') (Q, Q') (R x) \ \ wpc_helper (P, P') (Q, Q') (\x. R x)" by (clarsimp simp: wpc_helper_def) lemma wpc_imp_process: "\ Q \ wpc_helper (P, P') (R, R') S \ \ wpc_helper (P, P') (\s. Q \ R s, {s. Q \ s \ R'}) (Q \ S)" by (clarsimp simp add: wpc_helper_def subset_iff) lemma wpc_imp_process_weak: "\ wpc_helper (P, P') (R, R') S \ \ wpc_helper (P, P') (R, R') (Q \ S)" by (clarsimp simp add: wpc_helper_def) lemmas wpc_processors = wpc_conj_process wpc_all_process wpc_imp_process lemmas wpc_weak_processors = wpc_conj_process wpc_all_process wpc_imp_process_weak lemmas wpc_vweak_processors = wpc_conj_process wpc_all_process_very_weak wpc_imp_process_weak lemma wpc_helperI: "wpc_helper (P, P') (P, P') Q \ Q" by (simp add: wpc_helper_def) lemma wpc_foo: "\ undefined x; False \ \ P x" by simp lemma foo: assumes foo_elim: "\P Q h. \ foo Q h; \s. P s \ Q s \ \ foo P h" shows "\ \x. foo (Q x) (f x); foo R g \ \ foo (\s. (\x. Q x s) \ (y = None \ R s)) (case y of Some x \ f x | None \ g)" by (auto split: option.split intro: foo_elim) ML \ signature WPC = sig exception WPCFailed of string * term list * thm list; val foo_thm: thm; val iffd2_thm: thm; val wpc_helperI: thm; val instantiate_concl_pred: Proof.context -> cterm -> thm -> thm; val detect_term: Proof.context -> int -> thm -> cterm -> (cterm * term) list; val detect_terms: Proof.context -> (term -> cterm -> thm -> int -> tactic) -> int -> tactic; val split_term: thm list -> Proof.context -> term -> cterm -> thm -> int -> tactic; val wp_cases_tac: thm list -> Proof.context -> int -> tactic; val wp_debug_tac: thm list -> Proof.context -> int -> tactic; val wp_cases_method: thm list -> (Proof.context -> Method.method) context_parser; end; 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 fun inxs x = exists (fn y => x aconv y) tms val ys' = filter (not o inxs o Thm.term_of o fst) ys in xs @ ys' end end); structure WeakestPreCases : WPC = struct exception WPCFailed of string * term list * thm list; val iffd2_thm = @{thm "iffD2"}; val wpc_helperI = @{thm "wpc_helperI"}; 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 \ ?'b *) fun instantiate_concl_pred ctxt pred thm = let 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 = domain_type o Thm.typ_of o Thm.ctyp_of_cterm; val thm_pred = get_concl_predC thm; 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_pred = Term.dest_Var (get_concl_pred thm2); in Thm.instantiate ([], [(thm2_pred, pred)]) thm2 end; fun detect_term ctxt n thm tm = let val foo_thm_tm = instantiate_concl_pred ctxt tm foo_thm; val matches = resolve_tac ctxt [foo_thm_tm] n 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 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 ctxt tactic2 n thm = let val pfs = WPCPredicateAndFinals.get (Proof_Context.theory_of ctxt); val detects = map (fn (tm, rl) => (detect_term ctxt n 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]) | ((d3, fin) :: _) => (hd d3, fin) in tactic2 arg pred fin n thm end; (* give each rule in the list one possible resolution outcome *) fun resolve_each_once_tac ctxt thms i = fold (curry (APPEND')) (map (DETERM oo resolve_tac ctxt o single) thms) (K no_tac) i fun resolve_single_tac ctxt rules n thm = case Seq.chop 2 (resolve_each_once_tac ctxt rules n thm) of ([], _) => raise WPCFailed ("resolve_single_tac: no rules could apply", [], thm :: rules) | (_ :: _ :: _, _) => raise WPCFailed ("resolve_single_tac: multiple rules applied", [], thm :: rules) | ([x], _) => Seq.single x; fun split_term processors ctxt target pred fin = let val hdTarget = head_of target; val (constNm, _) = dest_Const hdTarget handle TERM (_, tms) => raise WPCFailed ("split_term: couldn't dest_Const", tms, []); val split = case (Ctr_Sugar.ctr_sugar_of_case ctxt constNm) of SOME sugar => #split sugar | _ => raise WPCFailed ("split_term: not a case", [hdTarget], []); val subst = split RS iffd2_thm; val subst2 = instantiate_concl_pred ctxt pred subst; in (resolve_tac ctxt [subst2]) THEN' (resolve_tac ctxt [wpc_helperI]) THEN' (REPEAT_ALL_NEW (resolve_tac ctxt processors) THEN_ALL_NEW resolve_single_tac ctxt [fin]) 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 n thm = detect_terms ctxt (split_term processors ctxt) n thm |> Seq.list_of |> Seq.of_list handle WPCFailed _ => no_tac thm; fun wp_debug_tac processors ctxt n thm = detect_terms ctxt (split_term processors ctxt) n thm |> Seq.list_of |> Seq.of_list handle WPCFailed e => (warning (@{make_string} (WPCFailed e)); no_tac thm); 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 lthy = let val ctxt = Local_Theory.target_of 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)) lthy end; val _ = Outer_Syntax.command @{command_keyword "wpc_setup"} "Add wpc stuff" (P.term -- P.name >> (fn (tm, thm) => Toplevel.local_theory NONE NONE (add_wpc tm thm))) end; end; \ ML \ val wp_cases_tactic_weak = WeakestPreCases.wp_cases_tac @{thms wpc_weak_processors}; val wp_cases_method_strong = WeakestPreCases.wp_cases_method @{thms wpc_processors}; val wp_cases_method_weak = WeakestPreCases.wp_cases_method @{thms wpc_weak_processors}; val wp_cases_method_vweak = WeakestPreCases.wp_cases_method @{thms wpc_vweak_processors}; \ method_setup wpc0 = \wp_cases_method_strong\ "case splitter for weakest-precondition proofs" method_setup wpcw0 = \wp_cases_method_weak\ "weak-form case splitter for weakest-precondition proofs" method wpc = (wp_pre, wpc0) method wpcw = (wp_pre, wpcw0) definition wpc_test :: "'a set \ ('a \ 'b) set \ 'b set \ bool" where "wpc_test P R S \ (R `` P) \ S" lemma wpc_test_weaken: "\ wpc_test Q R S; P \ Q \ \ wpc_test P R S" by (simp add: wpc_test_def, blast) lemma wpc_helper_validF: "wpc_test Q' R S \ wpc_helper (P, P') (Q, Q') (wpc_test P' R S)" by (simp add: wpc_test_def wpc_helper_def, blast) setup \ let val tm = Thm.cterm_of @{context} (Logic.varify_global @{term "\R. wpc_test P R S"}); val thm = @{thm wpc_helper_validF}; in WPCPredicateAndFinals.map (fn xs => (tm, thm) :: xs) end \ lemma set_conj_Int_simp: "{s \ S. P s} = S \ {s. P s}" by auto lemma case_options_weak_wp: "\ wpc_test P R S; \x. wpc_test P' (R' x) S \ \ wpc_test (P \ P') (case opt of None \ R | Some x \ R' x) S" apply (rule wpc_test_weaken) apply wpcw apply assumption apply assumption apply simp done end