# Theory Separation_Logic_Imperative_HOL.Automation

section ‹Automation›
theory Automation
imports Hoare_Triple (*"../Lib/Refine_Util"*)
begin

text ‹
In this theory, we provide a set of tactics and a simplifier setup for easy
reasoning with our separation logic.
›

subsection ‹Normalization of Assertions›
text ‹
In this section, we provide a set of lemmas and a simplifier
setup to bring assertions to a normal form. We provide a simproc that
detects pure parts of assertions and duplicate pointers. Moreover,
we provide ac-rules for assertions. See Section~\ref{sec:auto:overview}
for a short overview of the available proof methods.
›

lemmas assn_aci =
inf_aci[where 'a=assn]
sup_aci[where 'a=assn]
mult.left_ac[where 'a=assn]

lemmas star_assoc = mult.assoc[where 'a=assn]
lemmas assn_assoc =
mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn]

lemma merge_true_star_ctx: "true * (true * P) = true * P"
by (simp add: mult.left_ac)

lemmas star_aci =
mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn]
assn_one_left mult_1_right[where 'a=assn]
merge_true_star merge_true_star_ctx

text ‹Move existential quantifiers to the front of assertions›
lemma ex_assn_move_out[simp]:
"⋀Q R. (∃⇩Ax. Q x) * R = (∃⇩Ax. (Q x * R))"
"⋀Q R. R * (∃⇩Ax. Q x) = (∃⇩Ax. (R * Q x))"

"⋀P Q. (∃⇩Ax. Q x) ∧⇩A P = (∃⇩Ax. (Q x ∧⇩A P)) "
"⋀P Q. Q ∧⇩A (∃⇩Ax. P x) = (∃⇩Ax. (Q ∧⇩A P x))"

"⋀P Q. (∃⇩Ax. Q x) ∨⇩A P = (∃⇩Ax. (Q x ∨⇩A P))"
"⋀P Q. Q ∨⇩A (∃⇩Ax. P x) = (∃⇩Ax. (Q ∨⇩A P x))"
apply -
apply (simp add: ex_distrib_star)
apply (subst mult.commute)
apply (subst (2) mult.commute)
apply (simp add: ex_distrib_star)

apply (simp add: ex_distrib_and)
apply (subst inf_commute)
apply (subst (2) inf_commute)
apply (simp add: ex_distrib_and)

apply (simp add: ex_distrib_or)
apply (subst sup_commute)
apply (subst (2) sup_commute)
apply (simp add: ex_distrib_or)
done

text ‹Extract pure assertions from and-clauses›
lemma and_extract_pure_left_iff[simp]: "↑b ∧⇩A Q = (emp∧⇩AQ)*↑b"
by (cases b) auto

lemma and_extract_pure_left_ctx_iff[simp]: "P*↑b ∧⇩A Q = (P∧⇩AQ)*↑b"
by (cases b) auto

lemma and_extract_pure_right_iff[simp]: "P ∧⇩A ↑b = (emp∧⇩AP)*↑b"
by (cases b) (auto simp: assn_aci)

lemma and_extract_pure_right_ctx_iff[simp]: "P ∧⇩A Q*↑b = (P∧⇩AQ)*↑b"
by (cases b) auto

lemmas and_extract_pure_iff =
and_extract_pure_left_iff and_extract_pure_left_ctx_iff
and_extract_pure_right_iff and_extract_pure_right_ctx_iff

lemmas norm_assertion_simps =
(* Neutral elements *)
mult_1[where 'a=assn] mult_1_right[where 'a=assn]
inf_top_left[where 'a=assn] inf_top_right[where 'a=assn]
sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn]

(* Zero elements *)
star_false_left star_false_right
inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn]
sup_top_left[where 'a=assn] sup_top_right[where 'a=assn]

(* Associativity *)
mult.left_assoc[where 'a=assn]
inf_assoc[where 'a=assn]
sup_assoc[where 'a=assn]

(* Existential Quantifiers *)
ex_assn_move_out ex_assn_const

(* Extract pure assertions from conjunctions *)
and_extract_pure_iff

(* Merging *)
merge_pure_star merge_pure_and merge_pure_or
merge_true_star
inf_idem[where 'a=assn] sup_idem[where 'a=assn]

(* Duplicated References *)
sngr_same_false snga_same_false

subsubsection ‹Simplifier Setup Fine-Tuning›
text ‹Imperative HOL likes to simplify pointer inequations to this strange
operator. We do some additional simplifier setup here›
lemma not_same_noteqr[simp]: "¬ a=!=a"
by (metis Ref.unequal)
declare Ref.noteq_irrefl[dest!]

lemma not_same_noteqa[simp]: "¬ a=!!=a"
by (metis Array.unequal)
declare Array.noteq_irrefl[dest!]

text ‹However, it is safest to disable this rewriting, as there is
a working standard simplifier setup for ‹(≠)›
›
declare Ref.unequal[simp del]
declare Array.unequal[simp del]

subsection ‹Normalization of Entailments›

text ‹Used by existential quantifier extraction tactic›
lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *)
"(⋀x. Z x ⟶ (P ⟹⇩A Q x)) ⟹ (∃x. Z x) ⟶ (P ⟹⇩A (∃⇩Ax. Q x))"
by (metis ent_ex_postI)

text ‹Example of how to build an extraction lemma.›
thm enorm_exI'[OF enorm_exI'[OF imp_refl]]

lemmas ent_triv = ent_true ent_false

text ‹Dummy rule to detect Hoare triple goal›
lemma is_hoare_triple: "<P> c <Q> ⟹ <P> c <Q>" .
text ‹Dummy rule to detect entailment goal›
lemma is_entails: "P⟹⇩AQ ⟹ P ⟹⇩AQ" .

subsection ‹Frame Matcher›
text ‹Given star-lists P,Q and a frame F, this method tries to match
all elements of Q with corresponding elements of P. The result is a
partial match, that contains matching pairs and the unmatched content.›

text ‹The frame-matcher internally uses syntactic lists separated by
star, and delimited by the special symbol ‹SLN›, which is defined
to be ‹emp›.›
definition [simp]: "SLN ≡ emp"
lemma SLN_left: "SLN * P = P" by simp
lemma SLN_right: "P * SLN = P" by simp

lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn]
lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn]

text ‹A query to the frame matcher. Contains the assertions
P and Q that shall be matched, as well as a frame F, that is not
touched.›

definition [simp]: "FI_QUERY P Q F ≡ P ⟹⇩A Q*F"

abbreviation "fi_m_fst M ≡ foldr (*) (map fst M) emp"
abbreviation "fi_m_snd M ≡ foldr (*) (map snd M) emp"
abbreviation "fi_m_match M ≡ (∀(p,q)∈set M. p ⟹⇩A q)"

text ‹A result of the frame matcher. Contains a list of matching pairs,
as well as the unmatched parts of P and Q, and the frame F.
›
definition [simp]: "FI_RESULT M UP UQ F ≡
fi_m_match M ⟶ (fi_m_fst M * UP ⟹⇩A fi_m_snd M * UQ * F)"

text ‹Internal structure used by the frame matcher:
m contains the matched pairs; p,q the assertions that still needs to be
matched; up,uq the assertions that could not be matched; and f the frame.
p and q are SLN-delimited syntactic lists.
›

definition [simp]: "FI m p q up uq f ≡
fi_m_match m ⟶ (fi_m_fst m * p * up ⟹⇩A fi_m_snd m * q * uq * f)"

text ‹Initialize processing of query›
lemma FI_init:
assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F"
shows "FI_QUERY P Q F"
using assms by simp

text ‹Construct result from internal representation›
lemma FI_finalize:
assumes "FI_RESULT m (p*up) (q*uq) f"
shows "FI m p q up uq f"
using assms by (simp add: assn_aci)

text ‹Auxiliary lemma to show that all matching pairs together form
an entailment. This is required for most applications.›
lemma fi_match_entails:
assumes "fi_m_match m"
shows "fi_m_fst m ⟹⇩A fi_m_snd m"
using assms apply (induct m)
apply (simp_all split: prod.split_asm add: ent_star_mono)
done

text ‹Internally, the frame matcher tries to match the first assertion
of q with the first assertion of p. If no match is found, the first
assertion of p is discarded. If no match for any assertion in p can be
found, the first assertion of q is discarded.›

text ‹Match›
lemma FI_match:
assumes "p ⟹⇩A q"
assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f"
shows "FI m (ps*p) (qs*q) up uq f"
using assms unfolding FI_def
by (simp add: assn_aci)

text ‹No match›
lemma FI_p_nomatch:
assumes "FI m ps (qs*q) (p*up) uq f"
shows "FI m (ps*p) (qs*q) up uq f"
using assms unfolding FI_def
by (simp add: assn_aci)

text ‹Head of q could not be matched›
lemma FI_q_nomatch:
assumes "FI m (SLN*up) qs SLN (q*uq) f"
shows "FI m SLN (qs*q) up uq f"
using assms unfolding FI_def
by (simp add: assn_aci)

subsection ‹Frame Inference›
lemma frame_inference_init:
assumes "FI_QUERY P Q F"
shows "P ⟹⇩A Q * F"
using assms by simp

lemma frame_inference_finalize:
shows "FI_RESULT M F emp F"
apply simp
apply rule
apply (drule fi_match_entails)
apply (rule ent_star_mono[OF _ ent_refl])
apply assumption
done

subsection ‹Entailment Solver›
lemma entails_solve_init:
"FI_QUERY P Q true ⟹ P ⟹⇩A Q * true"
"FI_QUERY P Q emp ⟹ P ⟹⇩A Q"
by (simp_all add: assn_aci)

lemma entails_solve_finalize:
"FI_RESULT M P emp true"
"FI_RESULT M emp emp emp"
by (auto simp add: fi_match_entails intro: ent_star_mono)

lemmas solve_ent_preprocess_simps =
ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng

subsection ‹Verification Condition Generator›

lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule

(* Originally we introduced backwards-reasoning here, via
cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons).
This only works, if the postcondition is not schematic! However, for
forward reasoning, one usually assumes a schematic postcondition!
*)
text ‹May be useful in simple, manual proofs, where the postcondition
is no schematic variable.›
lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule]

text ‹Useful frame-rule variant for manual proof:›
lemma frame_rule_left:
"<P> c <Q> ⟹ <R * P> c <λx. R * Q x>"
using frame_rule by (simp add: assn_aci)

lemmas deconstruct_rules =
bind_rule if_rule false_rule return_sp_rule let_rule
case_prod_rule case_list_rule case_option_rule case_sum_rule

lemmas heap_rules =
ref_rule
lookup_rule
update_rule
new_rule
make_rule
of_list_rule
length_rule
nth_rule
upd_rule
freeze_rule

lemma fi_rule:
assumes CMD: "<P> c <Q>"
assumes FRAME: "Ps ⟹⇩A P * F"
shows "<Ps> c <λx. Q x * F>"
apply (rule cons_pre_rule[rotated])
apply (rule frame_rule)
apply (rule CMD)
apply (rule FRAME)
done

subsection ‹ML-setup›

named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers"
named_theorems sep_eintros "Seplogic: Intro rules for entailment solver"
named_theorems sep_heap_rules "Seplogic: VCG heap rules"
named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules"

ML ‹
infix 1 THEN_IGNORE_NEWGOALS

structure Seplogic_Auto =
struct

(***********************************)
(*             Tools               *)
(***********************************)

(* Repeat tac on subgoal. Determinize each step.
Stop if tac fails or subgoal is solved. *)
fun REPEAT_DETERM' tac i st = let
val n = Thm.nprems_of st
in
REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st
end

(***********************************)
(*             Debugging           *)
(***********************************)
fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t);

(***********************************)
(*        Custom Tacticals         *)
(***********************************)

(* Apply tac1, and then tac2 with an offset such that anything left
over by tac1 is skipped.

The typical usage of this tactic is, if a theorem is instantiated
with another theorem that produces additional goals that should
be ignored first. Here, it is used in the vcg to ensure that
frame inference is done before additional premises (that may
depend on the frame) are discharged.
*)
fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let
val np = Thm.nprems_of st
in
(tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in
if np'<np then tac2 i st'
else tac2 (i+(np'-np)+1) st'
end)) st
end;

(***********************************)
(*     Assertion Normalization     *)
(***********************************)
(* Find two terms in a list whose key is equal *)
fun find_similar (key_of:term -> term) (ts:term list) = let
fun frec _ [] = NONE
| frec tab (t::ts) = let val k=key_of t in
if Termtab.defined tab k then
SOME (the (Termtab.lookup tab k),t)
else frec (Termtab.update (k,t) tab) ts
end
in
frec Termtab.empty ts
end;

(* Perform DFS over term with binary operator opN, threading through
a state. Atomic terms are transformed by tr. Supports omission of
terms from the result structure by transforming them to NONE. *)
fun dfs_opr opN (tr:'state -> term -> ('state*term option))
d (t as ((op_t as Const (fN,_))$t1$t2)) =
if fN = opN then let
val (d1,t1') = dfs_opr opN tr d t1;
val (d2,t2') = dfs_opr opN tr d1 t2;
in
case (t1',t2') of
(NONE,NONE) => (d2,NONE)
| (SOME t1',NONE) => (d2,SOME t1')
| (NONE,SOME t2') => (d2,SOME t2')
| (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2'))
end
else tr d t
| dfs_opr _ tr d t = tr d t;

(* Replace single occurrence of (atomic) ot in t by nt.
Returns new term or NONE if nothing was removed. *)
fun dfs_replace_atomic opN ot nt t = let
fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t);
val (success,SOME t') = dfs_opr opN tr false t;
in
if success then SOME t' else NONE
end;

fun assn_simproc_fun ctxt credex = let
val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt;
(*val _ = tracing (tr_term redex);*)
val export = singleton (Variable.export ctxt' ctxt)

fun mk_star t1 t2 = @{term "(*)::assn ⇒ _ ⇒ _"}$t2$t1;

fun mk_star' NONE NONE = NONE
| mk_star' (SOME t1) NONE  = SOME t1
| mk_star' NONE (SOME t2) = SOME t2
| mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2);

fun ptrs_key (_$k$_) = k;

fun remove_term pt t = case
dfs_replace_atomic @{const_name "Groups.times_class.times"} pt
@{term emp} t
of
SOME t' => t';

fun normalize t = let

fun ep_tr (has_true,ps,ptrs) t = case t of
Const (@{const_name "Assertions.pure_assn"},_)$_ => ((has_true,t::ps,ptrs),NONE) | Const (@{const_name "Assertions.sngr_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Assertions.snga_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Orderings.top_class.top"},_) => ((true,ps,ptrs),NONE) | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2 => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2)) | _ => ((has_true,ps,ptrs),SOME t); fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"} ep_tr (false,[],[]) t of ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt); fun normalize_core t = let val ((has_true,pures,ptrs),rt) = normalizer t; val similar = find_similar ptrs_key ptrs; val true_t = if has_true then SOME @{term "Assertions.top_assn"} else NONE; val pures' = case pures of [] => NONE | p::ps => SOME (fold mk_star ps p); in case similar of NONE => the (mk_star' pures' (mk_star' true_t rt)) | SOME (t1,t2) => let val t_stripped = remove_term t1 (remove_term t2 t); in mk_star t_stripped (mk_star t1 t2) end end; fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) =
exq$Abs (n,ty,skip_ex t) | skip_ex t = normalize_core t; val (bs,t') = strip_abs t; val ty = fastype_of1 (map #2 bs,t'); in if ty = @{typ assn} then Logic.rlist_abs (bs,skip_ex t') else t end; (*val _ = tracing (tr_term redex);*) val (f,terms) = strip_comb redex; val nterms = map (fn t => let (*val _ = tracing (tr_term t); *) val t'=normalize t; (*val _ = tracing (tr_term t');*) in t' end) terms; val new_form = list_comb (f,nterms); val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci}); val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps [simp_tac res_ss 1] ctxt' (redex,new_form) ); in result end handle exc => if Exn.is_interrupt exc then Exn.reraise exc else (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); NONE) (* Fail silently *); val assn_simproc = Simplifier.make_simproc @{context} "assn_simproc" {lhss = [@{term "h ⊨ P"}, @{term "P ⟹⇩A Q"}, @{term "P ⟹⇩t Q"}, @{term "Hoare_Triple.hoare_triple P c Q"}, @{term "(P::assn) = Q"}], proc = K assn_simproc_fun}; (***********************************) (* Default Simplifications *) (***********************************) (* Default simplification. MUST contain assertion normalization! Tactic must not fail! *) fun dflt_tac ctxt = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimprocs [assn_simproc] addsimps @{thms norm_assertion_simps} addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps}) |> fold Splitter.del_split @{thms if_split} ); (***********************************) (* Frame Matcher *) (***********************************) (* Do frame matching imp_solve_tac - tactic used to discharge first assumption of match-rule cf. lemma FI_match. *) fun match_frame_tac imp_solve_tac ctxt = let (* Normalize star-lists *) val norm_tac = simp_tac ( put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize}); (* Strip star-lists *) val strip_tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def}); (* Do a match step *) val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*) THEN' SOLVED' imp_solve_tac (* Solve implication *) THEN' norm_tac; (* Do a no-match step *) val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE' (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac); in resolve_tac ctxt @{thms FI_init} THEN' norm_tac THEN' REPEAT_DETERM' (FIRST' [ CHANGED o dflt_tac ctxt, (match_tac ORELSE' nomatch_tac)]) THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac end; (***********************************) (* Frame Inference *) (***********************************) fun frame_inference_tac ctxt = resolve_tac ctxt @{thms frame_inference_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms frame_inference_finalize}; (***********************************) (* Entailment Solver *) (***********************************) (* Extract existential quantifiers from entailment goal *) fun extract_ex_tac ctxt i st = let fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) = count_ex c RS @{thm HOL.mp} | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t))
= count_ex t RS @{thm enorm_exI'}
| count_ex _ = @{thm imp_refl};

val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop;
val thm = count_ex concl;
in
(TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN'
resolve_tac ctxt [thm]) i st
end;

(* Solve Entailment *)
fun solve_entails_tac ctxt = let
val preprocess_entails_tac =
dflt_tac ctxt
THEN' extract_ex_tac ctxt
THEN' simp_tac
(put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps});

val match_entails_tac =
resolve_tac ctxt @{thms entails_solve_init}
THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
THEN' resolve_tac ctxt @{thms entails_solve_finalize};
in
preprocess_entails_tac
THEN' (TRY o
REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros}))))
THEN_ALL_NEW (dflt_tac ctxt THEN'
TRY o (match_tac ctxt @{thms ent_triv}
ORELSE' resolve_tac ctxt @{thms ent_refl}
ORELSE' match_entails_tac))
end;

(***********************************)
(* Verification Condition Generator*)
(***********************************)

fun heap_rule_tac ctxt h_thms =
resolve_tac ctxt h_thms ORELSE' (
resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS
frame_inference_tac ctxt));

fun vcg_step_tac ctxt = let
val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules});
val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules});
val heap_rule_tac = heap_rule_tac ctxt h_thms

(* Apply consequence rule if postcondition is not a schematic var *)
fun app_post_cons_tac i st =
case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of
Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt => if is_Var (head_of qt) then no_tac st else resolve_tac ctxt @{thms cons_post_rule} i st | _ => no_tac st; in CSUBGOAL (snd #> (FIRST' [ CHANGED o dflt_tac ctxt, REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}), CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac] ORELSE' (app_post_cons_tac THEN' FIRST' [resolve_tac ctxt d_thms, heap_rule_tac])) ])) end; fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt) (***********************************) (* Automatic Solver *) (***********************************) fun sep_autosolve_tac do_pre do_post ctxt = let val pre_tacs = [ CHANGED o clarsimp_tac ctxt, CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI}) ]; val main_tacs = [ match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt, match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt ]; val post_tacs = [SELECT_GOAL (auto_tac ctxt)]; val tacs = (if do_pre then pre_tacs else []) @ main_tacs @ (if do_post then post_tacs else []); in REPEAT_DETERM' (CHANGED o FIRST' tacs) end; (***********************************) (* Method Setup *) (***********************************) val dflt_simps_modifiers = [ Args.$$"dflt_simps" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) ⌂), Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) ⌂)
];
val heap_modifiers = [
Args.$$"heap" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) ⌂), Args.$$$"heap" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) ⌂) ]; val decon_modifiers = [ Args.$$"decon" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) ⌂), Args.$$$ "decon" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) ⌂)
];

val eintros_modifiers = [
Args.$$"eintros" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) ⌂), Args.$$\$ "eintros" -- Scan.option Args.del -- Args.colon
>> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) ⌂)
];

val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers;

val vcg_modifiers =
heap_modifiers @ decon_modifiers @ dflt_simps_modifiers;

val sep_auto_modifiers =
clasimp_modifiers @ vcg_modifiers @ eintros_modifiers;

end;
›

simproc_setup assn_simproc
("h⊨P" | "P⟹⇩AQ" | "P⟹⇩tQ" | "<P> c <R>" | "(P::assn) = Q")
= ‹K Seplogic_Auto.assn_simproc_fun›

method_setup assn_simp =‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.dflt_tac ctxt
)))› "Seplogic: Simplification of assertions"

method_setup frame_inference = ‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.frame_inference_tac ctxt
)))› "Seplogic: Frame inference"

method_setup solve_entails = ‹
Method.sections Seplogic_Auto.solve_entails_modifiers >>
(fn _ => fn ctxt => SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.solve_entails_tac ctxt
))› "Seplogic: Entailment Solver"

method_setup heap_rule = ‹
Attrib.thms >>
(fn thms => fn ctxt => SIMPLE_METHOD' (
let
val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules})
| _ => thms
in
CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms
end
))› "Seplogic: Apply rule with frame inference"

method_setup vcg = ‹
Scan.lift (Args.mode "ss") --
Method.sections Seplogic_Auto.vcg_modifiers >>
(fn (ss,_) => fn ctxt => SIMPLE_METHOD' (
CHANGED o (
if ss then Seplogic_Auto.vcg_step_tac ctxt
else Seplogic_Auto.vcg_tac ctxt
)
))› "Seplogic: Verification Condition Generator"

method_setup sep_auto =
‹Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain")
--| Method.sections Seplogic_Auto.sep_auto_modifiers >>
(fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' (
CHANGED o Seplogic_Auto.sep_autosolve_tac
((not nopre) andalso (not plain))
((not nopost) andalso (not plain)) ctxt
))› "Seplogic: Automatic solver"

lemmas [sep_dflt_simps] = split

declare deconstruct_rules[sep_decon_rules]
declare heap_rules[sep_heap_rules]

lemmas [sep_eintros] = impI conjI exI

subsection ‹Semi-Automatic Reasoning›
text ‹In this section, we provide some lemmas for semi-automatic reasoning›

text ‹Forward reasoning with frame. Use ‹frame_inference›-method
to discharge second assumption.›
lemma ent_frame_fwd:
assumes R: "P ⟹⇩A R"
assumes F: "Ps ⟹⇩A P*F"
assumes I: "R*F ⟹⇩A Q"
shows "Ps ⟹⇩A Q"
using assms
by (metis ent_refl ent_star_mono ent_trans)

lemma mod_frame_fwd:
assumes M: "h⊨Ps"
assumes R: "P⟹⇩AR"
assumes F: "Ps ⟹⇩A P*F"
shows "h⊨R*F"
using assms
by (metis ent_star_mono entails_def)

text ‹Apply precision rule with frame inference.›
lemma prec_frame:
assumes PREC: "precise P"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x p * F1"
assumes F2: "R2 ⟹⇩A P y p * F2"
shows "x=y"
using preciseD[OF PREC] M1 F1 F2
by (metis entailsD mod_and_dist)

lemma prec_frame_expl:
assumes PREC: "∀x y. (h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x * F1"
assumes F2: "R2 ⟹⇩A P y * F2"
shows "x=y"
using assms
by (metis entailsD mod_and_dist)

text ‹Variant that is useful within induction proofs, where induction
goes over ‹x› or ‹y››
lemma prec_frame':
assumes PREC: "(h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"
assumes M1: "h⊨(R1 ∧⇩A R2)"
assumes F1: "R1 ⟹⇩A P x * F1"
assumes F2: "R2 ⟹⇩A P y * F2"
shows "x=y"
using assms
by (metis entailsD mod_and_dist)

lemma ent_wand_frameI:
assumes "(Q -* R) * F ⟹⇩A S"
assumes "P ⟹⇩A F * X"
assumes "Q*X ⟹⇩A R"
shows "P ⟹⇩A S"
using assms
by (metis ent_frame_fwd ent_wandI mult.commute)

subsubsection ‹Manual Frame Inference›

lemma ent_true_drop:
"P⟹⇩AQ*true ⟹ P*R⟹⇩AQ*true"
"P⟹⇩AQ ⟹ P⟹⇩AQ*true"
apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
apply (metis assn_one_left ent_star_mono ent_true star_aci(2))
done

lemma fr_refl: "A⟹⇩AB ⟹ A*C ⟹⇩AB*C"
by (blast intro: ent_star_mono ent_refl)

lemma fr_rot: "(A*B ⟹⇩A C) ⟹ (B*A ⟹⇩A C)"
by (simp add: assn_aci)

lemma fr_rot_rhs: "(A ⟹⇩A B*C) ⟹ (A ⟹⇩A C*B)"
by (simp add: assn_aci)

lemma ent_star_mono_true:
assumes "A ⟹⇩A A' * true"
assumes "B ⟹⇩A B' * true"
shows "A*B*true ⟹⇩A A'*B'*true"
using ent_star_mono[OF assms] apply simp
using ent_true_drop(1) by blast

lemma ent_refl_true: "A ⟹⇩A A * true"
by (simp add: ent_true_drop(2))

lemma entt_fr_refl: "F⟹⇩tF' ⟹ F*A ⟹⇩t F'*A" by (rule entt_star_mono) auto
lemma entt_fr_drop: "F⟹⇩tF' ⟹ F*A ⟹⇩t F'"
using ent_true_drop(1) enttD enttI by blast

method_setup fr_rot = ‹
let
fun rot_tac ctxt =
resolve_tac ctxt @{thms fr_rot} THEN'
simp_tac (put_simpset HOL_basic_ss ctxt

in
Scan.lift Parse.nat >>
(fn n => fn ctxt => SIMPLE_METHOD' (
fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

end
›

method_setup fr_rot_rhs = ‹
let
fun rot_tac ctxt =
resolve_tac ctxt @{thms fr_rot_rhs} THEN'
simp_tac (put_simpset HOL_basic_ss ctxt

in
Scan.lift Parse.nat >>
(fn n => fn ctxt => SIMPLE_METHOD' (
fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

end
›

(*<*)
subsection ‹Test Cases›

lemma "⋀x. A x * true * Q x ⟹⇩A true * A x * Q x"
apply simp
done

lemma "A * (true * B) ⟹⇩A true * A * B"
apply (simp)
done

lemma "h⊨true*P*true ⟷ h⊨P*true"
by simp

lemma "A * true * ↑(b ∧ c) * true * B ⟹⇩A ↑b * ↑c * true *A * B"
by simp

lemma "∃y c. ∃⇩Ax. P x * (R x * Q y) * ↑ (b ∧ c) ⟹⇩A (∃⇩Ax. ↑b * (P x * (R x * Q y) * ↑c))"
apply simp
done

lemma "A * B * (↑c * B * C * D * ↑a * true * ↑d) * (∃⇩Ax. E x * F * ↑b) * true ⟹⇩A (∃⇩Ax. ↑ (c ∧ a ∧ d ∧ b) *
true * A * B * (true * B * C * D) * (E x * F))"
apply simp
done

lemma "<P> c <λr. Q r * true * ↑(b r) * true * ↑a>
⟷ <P> c <λr. Q r * true * ↑(b r ∧ a)>"
apply simp
done

lemma "(h⊨((A*B*↑b*true*↑c*true) ∧⇩A (↑(p=q)*P*Q)))
⟷ h ⊨ A * B * true ∧⇩A P * Q ∧ b ∧ c ∧ p = q"
apply simp
done

lemma assumes "FI_RESULT [(B, B), (A, A)] C D F"
shows "FI_QUERY (A*B*C) (D*B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(B,B), (A,A)] C emp F"
shows "FI_QUERY (A*B*C) (B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(B, B), (A, A)] emp emp F"
shows "FI_QUERY (A*B) (B*A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(A, A)] emp emp F"
shows "FI_QUERY (A) (A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

lemma
assumes "FI_RESULT [(A, A)] (B * C * D) emp F"
shows "FI_QUERY (B*C*D*A) (A) F"
apply (tactic ‹Seplogic_Auto.match_frame_tac
(resolve_tac @{context} @{thms ent_refl}) @{context} 1›)
by (rule assms)

schematic_goal
"P1 * P2 * P3 * P4 ⟹⇩A P3 * ?R1"
"P1 * (P2 * (P3 * P4)) ⟹⇩A P1 * ?R2"
"P4 * (P2 * (P1 * P3)) ⟹⇩A P1 * ?R2'"
"P1 * P2 * P3 * P4 ⟹⇩A P4 * ?R3"
"P1 * P2 ⟹⇩A P1 * ?R4"
"P1 * P2 ⟹⇩A P2 * ?R5"
"P1 ⟹⇩A P1 * ?R6"
"P1 * P2 ⟹⇩A emp * ?R7"
by frame_inference+

lemma "⟦A; B; C; b 17⟧ ⟹
Q 1 5 3 ⟹⇩A (∃⇩Ax y z. ∃⇩Aa. Q x y z * ↑(b a) * ↑(y=5))"
by solve_entails

thm nth_rule
lemma "<P * x↦⇩a[1,2,3]>
do { v←Array.nth x 1; return v }
<λr. P * x↦⇩a[1,2,3] * ↑(r=2)>"
apply sep_auto
done

(*>*)

subsection ‹Quick Overview of Proof Methods›
text_raw ‹\label{sec:auto:overview}›
text ‹
In this section, we give a quick overview of the available proof methods
and options. The most versatile proof method that we provide is
‹sep_auto›. It tries to solve the first subgoal, invoking appropriate
proof methods as required. If it cannot solve the subgoal completely, it
stops at the intermediate state that it could not handle any more.

‹sep_auto› can be configured by
section-arguments for the simplifier, the classical reasoner, and all
section-arguments for the verification condition generator and
entailment solver. Moreover, it takes an optional mode argument (mode), where
valid modes are:
\begin{description}
\item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify
and simplify the goal before the main method is invoked.
\item[(nopost)] No postprocessing of goal. The postprocessor tries to
solve or simplify goals left over by verification condition generation or
entailment solving.
\item[(plain)] Neither pre- nor postprocessing. Just applies vcg and
entailment solver.
\end{description}

\paragraph{Entailment Solver.} The entailment solver processes goals of the
form ‹P ⟹⇩A Q›. It is invoked by the method ‹solve_entails›.
It first tries to pull out pure parts of
‹P› and ‹Q›. This may introduce quantifiers, conjunction,
and implication into the goal, that are eliminated by resolving with rules
declared as ‹sep_eintros› (method argument: eintros[add/del]:).
Moreover, it simplifies with rules declared as ‹sep_dflt_simps›

Now, ‹P› and ‹Q› should have the form ‹X⇩1*…*X⇩n›.
Then, the frame-matcher is used to match all items of ‹P› with items
of ‹Q›, and thus solve the implication. Matching is currently done
syntactically, but can instantiate schematic variables.

Note that, by default, existential introduction is declared as
‹sep_eintros›-rule. This introduces schematic variables, that can
later be matched against. However, in some cases, the matching may instantiate
the schematic variables in an undesired way. In this case, the argument
‹eintros del: exI› should be passed to the entailment solver, and
the existential quantifier should be instantiated manually.

\paragraph{Frame Inference}
The method ‹frame_inference› tries to solve a goal of the
form ‹P⟹Q*?F›, by matching ‹Q› against the parts of
‹P›, and instantiating ‹?F› accordingly.
Matching is done syntactically, possibly
instantiating schematic variables. ‹P› and ‹Q› should be
assertions separated by ‹*›. Note that frame inference does no
simplification or other kinds of normalization.

The method ‹heap_rule› applies the specified heap rules, using
frame inference if necessary. If no rules are specified, the default
heap rules are used.

\paragraph{Verification Condition Generator}
The verification condition generator processes goals of the form
‹<P>c<Q>›. It is invoked by the method ‹vcg›.
First, it tries to pull out pure parts and simplifies with
the default simplification rules. Then, it tries to resolve the goal with
deconstruct rules (attribute: ‹sep_decon_rules›,
section argument: ‹decon[add/del]:›), and if this does not succeed,
it tries
to resolve the goal with heap rules (attribute: ‹sep_heap_rules›,
section argument: ‹heap[add/del]:›), using the frame rule and
frame inference.
If resolving is not possible, it also tries to apply the consequence rule to
make the postcondition a schematic variable.
›

(*<*)
subsection ‹Hiding of internal stuff›
hide_const (open) FI SLN
(*>*)

end