Skip to content

More uniformly handle endpoint and notification queues - Haskell and Refine #986

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
michaelmcinerney wants to merge 3 commits into
base: rt
Choose a base branch
from
Open

More uniformly handle endpoint and notification queues - Haskell and Refine #986

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a955cc0
lib: make some improvements in RCorres
michaelmcinerney Apr 7, 2026
cf19f6f
rt haskell+refine: more uniformly handle endpoint and ntfn queues
michaelmcinerney Apr 9, 2026
635507f
Address some of the comments from Gerwin squash
michaelmcinerney Apr 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 32 additions & 13 deletions lib/RCorres.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ text \<open>
goal when the postcondition of the rcorres goal mentions only the return value and state from
one of the two monads. These lifting rules often require @{const no_fail} assumptions, and so when
lifting an rcorres goal with a concrete function that is a @{const Nondet_Monad.bind} of other
functions, we will immediately be required to show @{const no_fail} for the composite function
anyway. Therefore, we have chosen to keep failure separate. The section below regarding
functions, we will immediately be required to show @{const no_fail} for the composite concrete
function anyway. Therefore, we have chosen to keep failure separate. The section below regarding
interactions with @{const no_fail} includes a rule that allows us to show @{const no_fail} for
composite functions by transforming complex predicates with rcorres. The section below regarding
@{const corres_underlying} shows the relation between rcorres and @{const corres_underlying}.\<close>
Expand Down Expand Up @@ -305,11 +305,13 @@ lemmas rcorres_if_r_fwd = rcorres_if_r[where T=R and F=R for R, simplified]

section \<open>Lifting rules\<close>

named_theorems rcorres_op_lifts

text \<open>
We would like a lifting rule for conjunctions, and so a rule with assumptions including
@{const rcorres} statements for the postconditions @{term R'} and @{term Q'} separately, with
conclusion an @{term rcorres} statement for the conjunction @{term "R' \<and> Q'"}, roughly speaking.
The inclusion of the @{term det_wp} assumption in the following rule warrants some explanation.
conclusion an @{const rcorres} statement for the conjunction @{term "R' \<and> Q'"}, roughly speaking.
The inclusion of the @{const det_wp} assumption in the following rule warrants some explanation.

Noting the definition of @{const rcorres}, suppose that we have two states @{term s} and @{term s'}
which satisfy the precondition of the conclusion, as well as a pair @{term "(rv', t')"} in the
Expand All @@ -327,10 +329,10 @@ text \<open>
It does not seem possible for us to state an adequate lifting rule for conjunction for
@{const rcorres} with a nondeterministic abstract monadic function, and so in such a situation,
it may be necessary to unfold the definition of @{const rcorres}.\<close>
lemma rcorres_conj_lift:
"\<lbrakk>det_wp P f; rcorres Q f f' R'; rcorres R f f' Q'\<rbrakk>
lemma rcorres_conj_lift[rcorres_op_lifts]:
"\<lbrakk>det_wp P f; rcorres R f f' R'; rcorres Q f f' Q'\<rbrakk>
\<Longrightarrow> rcorres
(\<lambda>s s'. P s \<and> Q s s' \<and> R s s')
(\<lambda>s s'. P s \<and> R s s' \<and> Q s s')
f f' (\<lambda>rv rv' s s'. R' rv rv' s s' \<and> Q' rv rv' s s')"
by (fastforce simp: rcorres_def det_wp_def)

Expand All @@ -341,7 +343,7 @@ lemma rcorres_conj_lift_fwd:
apply (fastforce intro!: rcorres_weaken_pre[OF rcorres_conj_lift])
done

lemma rcorres_imp_lift:
lemma rcorres_imp_lift[rcorres_op_lifts]:
"\<lbrakk>rcorres P' f f' (\<lambda>rv rv' s s'. \<not> P rv rv' s s'); rcorres Q' f f' Q\<rbrakk>
\<Longrightarrow> rcorres
(\<lambda>s s'. \<not> P' s s' \<longrightarrow> Q' s s')
Expand All @@ -354,10 +356,14 @@ lemma rcorres_imp_lift_fwd:
\<Longrightarrow> rcorres R f f' (\<lambda>rv rv' s s'. A s s' \<longrightarrow> R' rv rv' s s')"
by (rule rcorres_weaken_pre, rule rcorres_imp_lift, fastforce+)

lemma rcorres_drop_imp:
"rcorres P f f' Q \<Longrightarrow> rcorres P f f' (\<lambda>rv rv' s s'. Q' rv rv' s s' \<longrightarrow> Q rv rv' s s')"
by (fastforce simp: rcorres_def)

text
\<open>As with @{thm rcorres_conj_lift}, the @{const det_wp} assumption seems necessary in order
to state an adequate lifting rule for @{const All}.\<close>
lemma rcorres_allI:
lemma rcorres_allI[rcorres_op_lifts]:
"\<lbrakk>det_wp P f; \<And>x. rcorres (\<lambda>s s'. R x s s') f f' (\<lambda>rv rv' s s'. R' x rv rv' s s')\<rbrakk>
\<Longrightarrow> rcorres (\<lambda>s s'. P s \<and> (\<forall>x. R x s s')) f f' (\<lambda>rv rv' s s'. \<forall>x. R' x rv rv' s s')"
by (fastforce simp: rcorres_def det_wp_def singleton_iff)
Expand All @@ -369,8 +375,18 @@ lemma rcorres_allI_fwd:
apply (fastforce intro!: rcorres_weaken_pre[OF rcorres_allI])
done

lemma rcorres_exI[rcorres_op_lifts]:
"rcorres R f f' (\<lambda>rv rv' s s'. R' (x rv rv' s s') rv rv' s s')
\<Longrightarrow> rcorres R f f' (\<lambda>rv rv' s s'. \<exists>x. R' x rv rv' s s')"
by (fastforce simp: rcorres_def)

lemma rcorres_exI_abs_rv:
"rcorres R f f' (\<lambda>rv rv' s s'. R' rv rv rv' s s')
\<Longrightarrow> rcorres R f f' (\<lambda>rv rv' s s'. \<exists>x. R' x rv rv' s s')"
by (rule rcorres_exI)

lemma rcorres_prop:
"\<lbrakk>no_fail (\<lambda>s. Q s) f; empty_fail f\<rbrakk> \<Longrightarrow> rcorres (\<lambda>s s'. Q s \<and> R') f f' (\<lambda>_ _ _ _. R')"
"\<lbrakk>no_fail Q f; empty_fail f\<rbrakk> \<Longrightarrow> rcorres (\<lambda>s s'. Q s \<and> R') f f' (\<lambda>_ _ _ _. R')"
by (fastforce simp: rcorres_def no_fail_def empty_fail_def)

lemma rcorres_prop_fwd:
Expand Down Expand Up @@ -476,13 +492,16 @@ method rcorres uses rcorres_del rcorres_lift_del wp simp declares rcorres rcorre

text \<open>
This method is intended to be used to solve or make progress with @{const rcorres} goals via
lifting, when the precondition is not schematic.\<close>
method rcorres_conj_lift methods solve uses rule simp wp =
lifting, when the precondition is not schematic.

The user may specify a set to the argument rule: so that side conditions such as @{const no_fail},
@{const empty_fail}, and @{const det_wp} can be solved more directly.\<close>
method rcorres_conj_lift methods solve_final_imp uses rule simp wp =
Comment on lines +497 to +499
Copy link
Copy Markdown
Member

@lsf37 lsf37 Apr 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still have the urge to rename rule, because at the use side it is not going to be clear what kind of rule and what we're solving (wp and simp are clear enough). The problem is that it's multi-purpose. Maybe we should call it at least intro, since it's always used as an intro rule even though it's not a general-purpose intro rule.

Not sure. Any other opinions?

Copy link
Copy Markdown
Contributor Author

@michaelmcinerney michaelmcinerney Apr 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't have any strong opinions on this one, except that I would hope that if someone were wanting to use the method and wanted to know how it did work, they would read the comment. Maybe a big hope. If it helps, I could make the comment a bit more explicit by saying "so that the side conditions for the abstract monad such as..." Or "abstract monadic function". I'm never sure which is correct.

Copy link
Copy Markdown
Member

@lsf37 lsf37 Apr 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not so much about wanting to use the method, but understand what is written when you see the method used (and then maybe working from example).

Copy link
Copy Markdown
Contributor Author

@michaelmcinerney michaelmcinerney Apr 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, then I'm really not so sure. This rule: bit here is for what we might call "side-conditions", so maybe we could do something a bit out of the ordinary like side: ?

Copy link
Copy Markdown
Member

@lsf37 lsf37 Apr 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As a user that still doesn't tell me in which kind of context these rules are going to be applied. Is it correct that they are all about side conditions for rcorres_lift rules? Maybe something in that direction, but we'd need to be careful to not make it sound like we're supplying the actual lifting rule there (unless we do).

Copy link
Copy Markdown
Contributor Author

@michaelmcinerney michaelmcinerney Apr 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes these will all be side conditions for rcorres_lift rules, and so will be either a det_wp, no_fail, or empty_fail rule about the abstract function in the rcorres statement. I think side: or something else unusual will be a good prompt for people to look into the details, but still not sure.

(rule rcorres_conj_lift_fwd,
(solves \<open>rule det_wp_pre, rule rule, clarsimp\<close> | solves \<open>wpsimp wp: wp simp: simp\<close>))?,
rule rcorres_weaken_pre,
(rule rcorres_lift, (solves \<open>rule rule\<close> | solves \<open>wpsimp wp: wp simp: simp\<close>)+)[1],
solves solve
solves solve_final_imp

experiment
fixes f f' :: "('s, 'r) nondet_monad"
Expand Down
8 changes: 0 additions & 8 deletions proof/refine/Bits_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,14 +276,6 @@ lemma obj_at_valid_objs':
apply simp
done

lemma tcb_in_valid_state':
"\<lbrakk> st_tcb_at' P t s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s"
apply (clarsimp simp: pred_tcb_at'_def)
apply (drule obj_at_valid_objs')
apply fastforce
apply (fastforce simp add: valid_obj'_def valid_tcb'_def)
done

lemma getCurThread_corres[corres]:
"corres (=) \<top> \<top> (gets cur_thread) getCurThread"
by (simp add: getCurThread_def curthread_relation)
Expand Down
124 changes: 68 additions & 56 deletions proof/refine/CSpace1_R.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -265,46 +265,6 @@ lemma no_fail_getCTE [wp]:
"no_fail (cte_at' p) (getCTE p)"
by (wpsimp simp: getCTE_def)

lemma tcb_cases_related:
"tcb_cap_cases ref = Some (getF, setF, restr)
\<Longrightarrow> \<exists>getF' setF'.
(\<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF'))
\<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')))"
by (clarsimp simp: tcb_relation_def cte_map_def tcb_cap_cases_def tcb_cte_cases_neqs
tcb_cte_cases_def tcb_cnode_index_def
to_bl_1
simp flip: cteSizeBits_cte_level_bits
split: if_split_asm)

lemma pspace_relation_cte_wp_at:
"\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
cte_wp_at ((=) c) (cref, oref) s; pspace_aligned' s';
pspace_distinct' s' \<rbrakk>
\<Longrightarrow> cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (cref, oref)) s'"
apply (simp add: cte_wp_at_cases)
apply (erule disjE)
apply clarsimp
apply (drule(1) pspace_relation_absD)
apply (simp add: unpleasant_helper)
apply (drule spec, drule mp, erule domI)
apply (clarsimp simp: cte_relation_def)
apply (drule(2) aligned'_distinct'_ko_at'I[where 'a=cte], simp)
apply simp
apply (drule ko_at_imp_cte_wp_at')
apply (clarsimp elim!: cte_wp_at_weakenE')
apply clarsimp
apply (drule(1) pspace_relation_absD)
apply (clarsimp simp: tcb_relation_cut_def)
apply (simp split: kernel_object.split_asm)
apply (drule(2) aligned'_distinct'_ko_at'I[where 'a=tcb], simp)
apply simp
apply (drule tcb_cases_related)
apply (clarsimp simp: obj_at'_def gen_objBits_simps)
apply (erule(2) cte_wp_at_tcbI')
apply fastforce
apply simp
done

lemma pspace_relation_ctes_ofI:
"\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
cte_wp_at ((=) c) slot s; pspace_aligned' s';
Expand Down Expand Up @@ -1486,10 +1446,6 @@ lemma cte_map_inj_eq:
apply simp
done

lemma other_obj_relation_KOCTE[simp]:
"\<not> other_obj_relation ko (KOCTE cte)"
by (simp add: other_obj_relation_def split: Structures_A.kernel_object.splits)

lemma setCTE_pspace_only:
"(rv, s') \<in> fst (setCTE p v s) \<Longrightarrow> \<exists>ps'. s' = ksPSpace_update (\<lambda>s. ps') s"
apply (clarsimp simp: setCTE_def setObject_def in_monad split_def
Expand Down Expand Up @@ -1544,6 +1500,28 @@ lemma setObject_cte_scs_of'_use_valid_ksPSpace:
using use_valid[OF step setObject_scs_of'(1)] pre
by auto

lemma setObject_cte_epQueues_of[wp]:
"setObject c (cte :: cte) \<lbrace>\<lambda>s. P' (epQueues_of s)\<rbrace>"
by setObject_easy_cases

lemma setObject_cte_epQueues_of_use_valid_ksPSpace:
assumes step: "(x, s\<lparr>ksPSpace := ps\<rparr>) \<in> fst (setObject p (cte :: cte) s)"
assumes pre: "P (epQueues_of s)"
shows "P (ps |> ep_of' ||> epQueue)"
using use_valid[OF step setObject_cte_epQueues_of] pre
by auto

lemma setObject_cte_ntfnQueues_of[wp]:
"setObject c (cte :: cte) \<lbrace>\<lambda>s. P' (ntfnQueues_of s)\<rbrace>"
by setObject_easy_cases

lemma setObject_cte_ntfnQueues_of_use_valid_ksPSpace:
assumes step: "(x, s\<lparr>ksPSpace := ps\<rparr>) \<in> fst (setObject p (cte :: cte) s)"
assumes pre: "P (ntfnQueues_of s)"
shows "P (ps |> ntfn_of' ||> ntfnQueue)"
using use_valid[OF step setObject_cte_ntfnQueues_of] pre
by auto

lemma setObject_cte_tcbSchedPrevs_of_use_valid_ksPSpace:
assumes step: "(x, s\<lparr>ksPSpace := ps\<rparr>) \<in> fst (setObject p (cte :: cte) s)"
assumes pre: "P (tcbSchedPrevs_of s)"
Expand Down Expand Up @@ -1590,6 +1568,8 @@ lemma updateCap_stuff:
(pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') \<and>
replyPrevs_of s'' = replyPrevs_of s' \<and>
scReplies_of s'' = scReplies_of s' \<and>
epQueues_of s'' = epQueues_of s' \<and>
ntfnQueues_of s'' = ntfnQueues_of s' \<and>
tcbSchedPrevs_of s'' = tcbSchedPrevs_of s' \<and>
tcbSchedNexts_of s'' = tcbSchedNexts_of s' \<and>
(\<forall>domain priority.
Expand All @@ -1607,16 +1587,18 @@ lemma updateCap_stuff:
apply (frule setCTE_pspace_only)
apply (clarsimp simp: setCTE_def)
apply (intro conjI impI)
apply (erule use_valid [OF _ setObject_aligned])
apply (clarsimp simp: updateObject_cte in_monad typeError_def
in_magnitude_check gen_objBits_simps
split: kernel_object.split_asm if_split_asm)
apply (erule use_valid [OF _ setObject_distinct])
apply (clarsimp simp: updateObject_cte in_monad typeError_def
in_magnitude_check gen_objBits_simps
split: kernel_object.split_asm if_split_asm)
apply (erule setObject_cte_replies_of'_use_valid_ksPSpace; simp)
apply (erule setObject_cte_scs_of'_use_valid_ksPSpace; simp)
apply (erule use_valid [OF _ setObject_aligned])
apply (clarsimp simp: updateObject_cte in_monad typeError_def
in_magnitude_check gen_objBits_simps
split: kernel_object.split_asm if_split_asm)
apply (erule use_valid [OF _ setObject_distinct])
apply (clarsimp simp: updateObject_cte in_monad typeError_def
in_magnitude_check gen_objBits_simps
split: kernel_object.split_asm if_split_asm)
apply (erule setObject_cte_replies_of'_use_valid_ksPSpace; simp)
apply (erule setObject_cte_scs_of'_use_valid_ksPSpace; simp)
apply (erule setObject_cte_epQueues_of_use_valid_ksPSpace; simp)
apply (erule setObject_cte_ntfnQueues_of_use_valid_ksPSpace; simp)
apply (erule setObject_cte_tcbSchedPrevs_of_use_valid_ksPSpace; simp)
apply (erule setObject_cte_tcbSchedNexts_of_use_valid_ksPSpace; simp)
apply (fastforce elim: setObject_cte_inQ_of_use_valid_ksPSpace)
Expand Down Expand Up @@ -1767,7 +1749,9 @@ lemma set_cap_not_quite_corres:
cur_time t = ksCurTime t' \<and>
cur_sc t = ksCurSc t' \<and>
reprogram_timer t = ksReprogramTimer t' \<and>
sc_replies_of t = sc_replies_of s"
sc_replies_of t = sc_replies_of s \<and>
ep_queues_of t = ep_queues_of s \<and>
ntfn_queues_of t = ntfn_queues_of s"
using cr
apply (clarsimp simp: updateCap_def in_monad)
apply (drule use_valid [OF _ getCTE_sp[where P="\<lambda>s. s2 = s" for s2], OF _ refl])
Expand All @@ -1781,6 +1765,10 @@ lemma set_cap_not_quite_corres:
apply (frule setCTE_pspace_only)
apply (prop_tac "sc_replies_of x = sc_replies_of s")
apply (erule use_valid[OF _ set_cap.valid_sched_pred], simp)
apply (prop_tac "ep_queues_of x = ep_queues_of s")
apply (erule use_valid[OF _ set_cap.valid_sched_pred], simp)
apply (prop_tac "ntfn_queues_of x = ntfn_queues_of s")
apply (erule use_valid[OF _ set_cap.valid_sched_pred], simp)
apply (clarsimp simp: set_cap_def split_def in_monad set_object_def
get_object_def)
apply (rename_tac obj ps' x' obj' kobj)
Expand Down Expand Up @@ -2029,7 +2017,7 @@ lemma updateCap_corres:
apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
subgoal by (auto elim!: modify_map_casesE del: disjE)[1]

apply (clarsimp simp: sc_replies_relation_def)
apply (clarsimp simp: sc_replies_relation_def ep_queues_relation_def ntfn_queues_relation_def)
done

end (* CSpace1_R *)
Expand Down Expand Up @@ -2085,6 +2073,10 @@ lemma updateMDB_ctes_of:
apply simp
done

crunch setCTE
for eps_of'[wp]: "\<lambda>s. P (eps_of' s)"
and ntfns_of'[wp]: "\<lambda>s. P (ntfns_of' s)"

crunch updateMDB
for replies_of'[wp]: "\<lambda>s. P (replies_of' s)"
and scs_of'[wp]: "\<lambda>s. P (scs_of' s)"
Expand All @@ -2100,6 +2092,8 @@ crunch updateMDB
and tcbSchedNexts[wp]: "\<lambda>s. P (tcbSchedNexts_of s)"
and tcbInReleaseQueue[wp]: "\<lambda>s. P (tcbInReleaseQueue |< tcbs_of' s)"
and inQ_opt_pred[wp]: "\<lambda>s. P (inQ d p |< tcbs_of' s)"
and eps_of'[wp]: "\<lambda>s. P (eps_of' s)"
and ntfns_of'[wp]: "\<lambda>s. P (ntfns_of' s)"
(wp: crunch_wps simp: crunch_simps setObject_def updateObject_cte)

(* needed to make mdb_inv_preserved work with CSpace1_R(_2?) *)
Expand Down Expand Up @@ -2944,6 +2938,8 @@ lemma updateMDB_the_lot:
ksReprogramTimer s'' = ksReprogramTimer s' \<and>
replyPrevs_of s'' = replyPrevs_of s' \<and>
scReplies_of s'' = scReplies_of s' \<and>
epQueues_of s'' = epQueues_of s' \<and>
ntfnQueues_of s'' = ntfnQueues_of s' \<and>
tcbSchedNexts_of s'' = tcbSchedNexts_of s' \<and>
tcbSchedPrevs_of s'' = tcbSchedPrevs_of s' \<and>
(tcbInReleaseQueue |< tcbs_of' s'') = (tcbInReleaseQueue |< tcbs_of' s') \<and>
Expand Down Expand Up @@ -2988,6 +2984,8 @@ lemma updateMDB_the_lot':
ksReprogramTimer s'' = ksReprogramTimer s' \<and>
replyPrevs_of s'' = replyPrevs_of s' \<and>
scReplies_of s'' = scReplies_of s' \<and>
epQueues_of s'' = epQueues_of s' \<and>
ntfnQueues_of s'' = ntfnQueues_of s' \<and>
tcbSchedNexts_of s'' = tcbSchedNexts_of s' \<and>
tcbSchedPrevs_of s'' = tcbSchedPrevs_of s' \<and>
(tcbInReleaseQueue |< tcbs_of' s'') = (tcbInReleaseQueue |< tcbs_of' s') \<and>
Expand Down Expand Up @@ -3130,6 +3128,20 @@ lemma setCTE_UntypedCap_corres:
apply (rule use_valid[OF _ setCTE_tcbInReleaseQueue], assumption)
apply clarsimp

apply (extract_conjunct \<open>match conclusion in "ep_queues_relation _ _" \<Rightarrow> -\<close>)
apply (rule use_valid[OF _ setCTE_tcbSchedPrevs_of], assumption)
apply (rule use_valid[OF _ setCTE_tcbSchedNexts_of], assumption)
apply (rule use_valid[OF _ set_cap.valid_sched_pred], assumption)
apply (rule use_valid[OF _ setCTE_eps_of'], assumption)
apply clarsimp

apply (extract_conjunct \<open>match conclusion in "ntfn_queues_relation _ _" \<Rightarrow> -\<close>)
apply (rule use_valid[OF _ setCTE_tcbSchedPrevs_of], assumption)
apply (rule use_valid[OF _ setCTE_tcbSchedNexts_of], assumption)
apply (rule use_valid[OF _ set_cap.valid_sched_pred], assumption)
apply (rule use_valid[OF _ setCTE_ntfns_of'], assumption)
apply clarsimp

apply (frule setCTE_pspace_only)
apply (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def)
apply (rename_tac obj ps' s'' obj' kobj; case_tac obj;
Expand Down
Loading
Loading