Theory Autoref_Misc
theory Autoref_Misc
imports
Refine_Dflt_No_Comp
"HOL-Analysis.Analysis"
begin
lemma nofail_RES_conv: "nofail m ⟷ (∃M. m=RES M)" by (cases m) auto
lemma nofail_SPEC: "nofail m ⟹ m ≤ SPEC (λ_. True)"
by (simp add: pw_le_iff)
lemma nofail_SPEC_iff: "nofail m ⟷ m ≤ SPEC (λ_. True)"
by (simp add: pw_le_iff)
lemma nofail_SPEC_triv_refine: "⟦ nofail m; ⋀x. Φ x ⟧ ⟹ m ≤ SPEC Φ"
by (simp add: pw_le_iff)
lemma bind_cong:
assumes "m=m'"
assumes "⋀x. RETURN x ≤ m' ⟹ f x = f' x"
shows "bind m f = bind m' f'"
using assms
by (auto simp: refine_pw_simps pw_eq_iff pw_le_iff)
primrec the_RES where "the_RES (RES X) = X"
lemma the_RES_inv[simp]: "nofail m ⟹ RES (the_RES m) = m"
by (cases m) auto
lemma le_SPEC_UNIV_rule [refine_vcg]:
"m ≤ SPEC (λ_. True) ⟹ m ≤ RES UNIV" by auto
lemma nf_inres_RES[simp]: "nf_inres (RES X) x ⟷ x∈X"
by (simp add: refine_pw_simps)
lemma nf_inres_SPEC[simp]: "nf_inres (SPEC Φ) x ⟷ Φ x"
by (simp add: refine_pw_simps)
lemma Let_refine':
assumes "(m,m')∈R"
assumes "(m,m')∈R ⟹ f m ≤⇓S (f' m')"
shows "Let m f ≤ ⇓S (Let m' f')"
using assms by simp
lemma in_nres_rel_iff: "(a,b)∈⟨R⟩nres_rel ⟷ a ≤⇓R b"
by (auto simp: nres_rel_def)
lemma inf_RETURN_RES:
"inf (RETURN x) (RES X) = (if x∈X then RETURN x else SUCCEED)"
"inf (RES X) (RETURN x) = (if x∈X then RETURN x else SUCCEED)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma inf_RETURN_SPEC[simp]:
"inf (RETURN x) (SPEC (λy. Φ y)) = SPEC (λy. y=x ∧ Φ x)"
"inf (SPEC (λy. Φ y)) (RETURN x) = SPEC (λy. y=x ∧ Φ x)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma RES_sng_eq_RETURN: "RES {x} = RETURN x"
by simp
lemma nofail_inf_serialize:
"⟦nofail a; nofail b⟧ ⟹ inf a b = do {x←a; ASSUME (inres b x); RETURN x}"
by (auto simp: pw_eq_iff refine_pw_simps)
definition lift_assn :: "('a × 'b) set ⇒ ('b ⇒ bool) ⇒ ('a ⇒ bool)"
where "lift_assn R Φ s ≡ ∃s'. (s,s')∈R ∧ Φ s'"
lemma lift_assnI: "⟦(s,s')∈R; Φ s'⟧ ⟹ lift_assn R Φ s"
unfolding lift_assn_def by auto
lemma case_option_refine[refine]:
assumes "(x,x')∈Id"
assumes "x=None ⟹ fn ≤ ⇓R fn'"
assumes "⋀v v'. ⟦x=Some v; (v,v')∈Id⟧ ⟹ fs v ≤ ⇓R (fs' v')"
shows "case_option fn (λv. fs v) x ≤ ⇓R (case_option fn' (λv'. fs' v') x')"
using assms by (auto split: option.split)
definition GHOST :: "'a ⇒ 'a"
where [simp]: "GHOST ≡ λx. x"
lemma GHOST_elim_Let:
shows "(let x=GHOST m in f x) = f m" by simp
text ‹The following set of rules executes a step on the LHS or RHS of
a refinement proof obligation, without changing the other side.
These kind of rules is useful for performing refinements with
invisible steps.›
lemma lhs_step_If:
"⟦ b ⟹ t ≤ m; ¬b ⟹ e ≤ m ⟧ ⟹ If b t e ≤ m" by simp
lemma lhs_step_RES:
"⟦ ⋀x. x∈X ⟹ RETURN x ≤ m ⟧ ⟹ RES X ≤ m"
by (simp add: pw_le_iff)
lemma lhs_step_SPEC:
"⟦ ⋀x. Φ x ⟹ RETURN x ≤ m ⟧ ⟹ SPEC (λx. Φ x) ≤ m"
by (simp add: pw_le_iff)
lemma lhs_step_bind:
fixes m :: "'a nres" and f :: "'a ⇒ 'b nres"
assumes "nofail m' ⟹ nofail m"
assumes "⋀x. nf_inres m x ⟹ f x ≤ m'"
shows "do {x←m; f x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast
lemma rhs_step_bind_RES:
assumes "x'∈X'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (RES X' ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast
lemma rhs_step_bind_SPEC:
assumes "Φ x'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (SPEC Φ ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast
lemma RES_bind_choose:
assumes "x∈X"
assumes "m ≤ f x"
shows "m ≤ RES X ⤜ f"
using assms by (auto simp: pw_le_iff refine_pw_simps)
lemma pw_RES_bind_choose:
"nofail (RES X ⤜ f) ⟷ (∀x∈X. nofail (f x))"
"inres (RES X ⤜ f) y ⟷ (∃x∈X. inres (f x) y)"
by (auto simp: refine_pw_simps)
lemma use_spec_rule:
assumes "m ≤ SPEC Ψ"
assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤ SPEC Φ"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma strengthen_SPEC: "m ≤ SPEC Φ ⟹ m ≤ SPEC(λs. inres m s ∧ Φ s)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma weaken_SPEC:
"m ≤ SPEC Φ ⟹ (⋀x. Φ x ⟹ Ψ x) ⟹ m ≤ SPEC Ψ"
by (force elim!: order_trans)
lemma ife_FAIL_to_ASSERT_cnv:
"(if Φ then m else FAIL) = op_nres_ASSERT_bnd Φ m"
by (cases Φ, auto)
lemma param_op_nres_ASSERT_bnd[param]:
assumes "Φ' ⟹ Φ"
assumes "⟦Φ'; Φ⟧ ⟹ (m,m')∈⟨R⟩nres_rel"
shows "(op_nres_ASSERT_bnd Φ m, op_nres_ASSERT_bnd Φ' m') ∈ ⟨R⟩nres_rel"
using assms
by (auto simp: pw_le_iff refine_pw_simps nres_rel_def)
declare autoref_FAIL[param]
lemma (in transfer) transfer_sum[refine_transfer]:
assumes "⋀l. α (fl l) ≤ Fl l"
assumes "⋀r. α (fr r) ≤ Fr r"
shows "α (case_sum fl fr x) ≤ (case_sum Fl Fr x)"
using assms by (auto split: sum.split)
lemma nres_of_transfer[refine_transfer]: "nres_of x ≤ nres_of x" by simp
declare FOREACH_patterns[autoref_op_pat_def]
context begin interpretation autoref_syn .
lemma [autoref_op_pat_def]:
"WHILEIT I ≡ OP (WHILEIT I)"
"WHILEI I ≡ OP (WHILEI I)"
by auto
end
lemma set_relD: "(s,s')∈⟨R⟩set_rel ⟹ x∈s ⟹ ∃x'∈s'. (x,x')∈R"
unfolding set_rel_def by blast
lemma set_relE[consumes 2]:
assumes "(s,s')∈⟨R⟩set_rel" "x∈s"
obtains x' where "x'∈s'" "(x,x')∈R"
using set_relD[OF assms] ..
lemma param_prod': "⟦
⋀a b a' b'. ⟦p=(a,b); p'=(a',b')⟧ ⟹ (f a b,f' a' b')∈R
⟧ ⟹ (case_prod f p, case_prod f' p')∈R"
by (auto split: prod.split)
lemma dropWhile_param[param]:
"(dropWhile, dropWhile) ∈ (a → bool_rel) → ⟨a⟩list_rel → ⟨a⟩list_rel"
unfolding dropWhile_def by parametricity
term takeWhile
lemma takeWhile_param[param]:
"(takeWhile, takeWhile) ∈ (a → bool_rel) → ⟨a⟩list_rel → ⟨a⟩list_rel"
unfolding takeWhile_def by parametricity
lemmas [autoref_rules] = dropWhile_param takeWhile_param
method_setup autoref_solve_id_op = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD' (
Autoref_Id_Ops.id_tac (Config.put Autoref_Id_Ops.cfg_ss_id_op false ctxt)
))
›
text ‹Default setup of the autoref-tool for the monadic framework.›
lemma autoref_monadicI1:
assumes "(b,a)∈⟨R⟩nres_rel"
assumes "RETURN c ≤ b"
shows "(RETURN c, a)∈⟨R⟩nres_rel" "RETURN c ≤⇓R a"
using assms
unfolding nres_rel_def
by simp_all
lemma autoref_monadicI2:
assumes "(b,a)∈⟨R⟩nres_rel"
assumes "nres_of c ≤ b"
shows "(nres_of c, a)∈⟨R⟩nres_rel" "nres_of c ≤ ⇓R a"
using assms
unfolding nres_rel_def
by simp_all
lemmas autoref_monadicI = autoref_monadicI1 autoref_monadicI2
ML ‹
structure Autoref_Monadic = struct
val cfg_plain = Attrib.setup_config_bool @{binding autoref_plain} (K false)
fun autoref_monadic_tac ctxt = let
open Autoref_Tacticals
val ctxt = Autoref_Phases.init_data ctxt
val plain = Config.get ctxt cfg_plain
val trans_thms = if plain then [] else @{thms the_resI}
in
resolve_tac ctxt @{thms autoref_monadicI}
THEN'
IF_SOLVED (Autoref_Phases.all_phases_tac ctxt)
(RefineG_Transfer.post_transfer_tac trans_thms ctxt)
(K all_tac)
end
end
›
method_setup autoref_monadic = ‹let
open Refine_Util Autoref_Monadic
val autoref_flags =
parse_bool_config "trace" Autoref_Phases.cfg_trace
|| parse_bool_config "debug" Autoref_Phases.cfg_debug
|| parse_bool_config "plain" Autoref_Monadic.cfg_plain
in
parse_paren_lists autoref_flags
>>
( fn _ => fn ctxt => SIMPLE_METHOD' (
let
val ctxt = Config.put Autoref_Phases.cfg_keep_goal true ctxt
in autoref_monadic_tac ctxt end
))
end
›
"Automatic Refinement and Determinization for the Monadic Refinement Framework"
lemma dres_unit_simps[refine_transfer_post_simp]:
"dbind (dRETURN (u::unit)) f = f ()"
by auto
lemma Let_dRETURN_simp[refine_transfer_post_simp]:
"Let m dRETURN = dRETURN m" by auto
lemmas [refine_transfer_post_simp] = dres_monad_laws
subsection ‹things added by Fabian›
bundle art = [[goals_limit=1, autoref_trace, autoref_trace_failed_id, autoref_keep_goal]]
definition [simp, autoref_tag_defs]: "TRANSFER_tag P == P"
lemma TRANSFER_tagI: "P ==> TRANSFER_tag P" by simp
abbreviation "TRANSFER P ≡ PREFER_tag (TRANSFER_tag P)"
declaration
‹
let
val _ = ()
in Tagged_Solver.declare_solver @{thms TRANSFER_tagI} @{binding TRANSFER}
"transfer"
(RefineG_Transfer.post_transfer_tac [])
end›
method_setup refine_vcg =
‹Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac (add_thms @ Refine.vcg.get ctxt) ctxt THEN_ALL_NEW_FWD
(TRY o
(Method.assm_tac ctxt
ORELSE' SOLVED' (clarsimp_tac ctxt THEN_ALL_NEW Method.assm_tac ctxt)
ORELSE' Refine.post_tac ctxt))
))›
"Refinement framework: Generate refinement and verification conditions"
lemmas [autoref_rules] = autoref_rec_nat
lemma
uncurry_rec_nat: "rec_nat (λa b. fn a b) (λn rr a b. fs n rr a b) n a b =
rec_nat (λ(a,b). fn a b) (λn rr (a,b). fs n (λa b. rr (a,b)) a b) n (a,b)"
apply (induction n arbitrary: a b)
apply (auto split: prod.splits)
apply metis
done
attribute_setup refine_vcg_def =
‹Scan.succeed (Thm.declaration_attribute (fn A =>
Refine.vcg.add_thm ((A RS @{thm eq_refl}) RS @{thm order.trans})))›
definition comp2 (infixl ‹o2› 55) where "comp2 f g x y ≡ f (g x y)"
definition comp3 (infixl ‹o3› 55) where "comp3 f g x y z ≡ f (g x y z)"
definition comp4 (infixl ‹o4› 55) where "comp4 f g w x y z ≡ f (g w x y z)"
definition comp5 (infixl ‹o5› 55) where "comp5 f g w x y z a ≡ f (g w x y z a)"
definition comp6 (infixl ‹o6› 55) where "comp6 f g w x y z a b ≡ f (g w x y z a b)"
lemmas comps =
comp_def[abs_def]
comp2_def[abs_def]
comp3_def[abs_def]
comp4_def[abs_def]
comp5_def[abs_def]
comp6_def[abs_def]
locale autoref_op_pat_def = fixes x
begin
lemma [autoref_op_pat_def]: "x ≡ Autoref_Tagging.OP x"
by simp
end
bundle autoref_syntax begin
no_notation vec_nth (infixl ‹$› 90)
unbundle no funcset_syntax
notation Autoref_Tagging.APP (infixl ‹$› 900)
notation rel_ANNOT (infix ‹:::› 10)
notation ind_ANNOT (infix ‹::#› 10)
notation "Autoref_Tagging.OP" (‹OP›)
notation Autoref_Tagging.ABS (binder ‹λ''› 10)
end
definition "THE_NRES = case_option SUCCEED RETURN"
context includes autoref_syntax begin
schematic_goal THE_NRES_impl:
assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued R"
assumes [autoref_rules]: "(xi, x) ∈ ⟨R⟩option_rel"
shows "(nres_of ?x, THE_NRES $ x) ∈ ⟨R⟩nres_rel"
unfolding THE_NRES_def
by (autoref_monadic)
end
concrete_definition THE_DRES uses THE_NRES_impl
lemmas [autoref_rules] = THE_DRES.refine
lemma THE_NRES_refine[THEN order_trans, refine_vcg]:
"THE_NRES x ≤ SPEC (λr. x = Some r)"
by (auto simp: THE_NRES_def split: option.splits)
definition "CHECK f P = (if P then RETURN () else let _ = f () in SUCCEED)"
definition "CHECK_dres f P = (if P then dRETURN () else let _ = f () in dSUCCEED)"
context includes autoref_syntax begin
lemma CHECK_refine[refine_transfer]:
"nres_of (CHECK_dres f x) ≤ CHECK f x"
by (auto simp: CHECK_dres_def CHECK_def)
lemma CHECK_impl[autoref_rules]:
"(CHECK, CHECK) ∈ (unit_rel → A) → bool_rel → ⟨unit_rel⟩nres_rel"
by (auto simp add: CHECK_def nres_rel_def)
definition [simp]: "op_nres_CHECK_bnd f Φ m ≡ do {CHECK f Φ; m}"
lemma id_CHECK[autoref_op_pat_def]:
"do {CHECK f Φ; m} ≡ OP op_nres_CHECK_bnd $ f $ Φ $m"
by simp
lemma op_nres_CHECK_bnd[autoref_rules]:
"(Φ ⟹ (m', m) ∈ ⟨R⟩nres_rel) ⟹
(Φ', Φ) ∈ bool_rel ⟹
(f', f) ∈ unit_rel → A ⟹
(do {CHECK f' Φ'; m'}, op_nres_CHECK_bnd $ f $ Φ $ m) ∈ ⟨R⟩nres_rel"
by (simp add: CHECK_def nres_rel_def)
lemma CHECK_rule[refine_vcg]:
assumes "P ⟹ RETURN () ≤ R"
shows "CHECK f P ≤ R"
using assms
by (auto simp: CHECK_def)
lemma SPEC_allI:
assumes "⋀x. f ≤ SPEC (P x)"
shows "f ≤ SPEC (λr. ∀x. P x r)"
using assms
by (intro pw_leI) (auto intro!: SPEC_nofail dest!: inres_SPEC)
lemma SPEC_BallI:
assumes "nofail f"
assumes "⋀x. x ∈ X ⟹ f ≤ SPEC (P x)"
shows "f ≤ SPEC (λr. ∀x∈X. P x r)"
using assms
by (intro pw_leI) (force intro!: SPEC_nofail dest!: inres_SPEC)
lemma map_option_param[param]: "(map_option, map_option) ∈ (R → S) → ⟨R⟩option_rel → ⟨S⟩option_rel"
by (auto simp: option_rel_def fun_relD)
lemma those_param[param]: "(those, those) ∈ ⟨⟨R⟩option_rel⟩list_rel → ⟨⟨R⟩list_rel⟩option_rel"
unfolding those_def
by parametricity
lemma image_param[param]:
shows "single_valued A ⟹ single_valued B ⟹
((`), (`)) ∈ (A → B) → ⟨A⟩set_rel → ⟨B⟩set_rel"
by (force simp: set_rel_def fun_rel_def elim!: single_valued_as_brE)
end
lemma Up_Down_SPECI:
assumes a5: "single_valued R"
assumes a2: "single_valued (S¯)"
assumes "SPEC Q ≤ ⇓ (S¯ O R) (SPEC P)"
shows "⇑ R (⇓ S (SPEC Q)) ≤ SPEC P"
proof -
have "x ∈ Domain R" if a1: "(x, y) ∈ S" and a3: "Q y" for x y
proof -
obtain cc :: "('a × 'b) set ⇒ ('c × 'a) set ⇒ 'b ⇒ 'c ⇒ 'c"
and bb :: "('a × 'b) set ⇒ ('c × 'a) set ⇒ 'b ⇒ 'c ⇒ 'b"
and aa :: "('a × 'b) set ⇒ ('c × 'a) set ⇒ 'b ⇒ 'c ⇒ 'a" where
f4: "∀x0 x1 x2 x3. (∃v4 v5 v6. x3 = v4 ∧ x2 = v6 ∧ (v4, v5) ∈ x1 ∧ (v5, v6) ∈ x0) = (x3 = cc x0 x1 x2 x3 ∧ x2 = bb x0 x1 x2 x3 ∧ (cc x0 x1 x2 x3, aa x0 x1 x2 x3) ∈ x1 ∧ (aa x0 x1 x2 x3, bb x0 x1 x2 x3) ∈ x0)"
by moura
have f5: "RETURN y ≤ ⇓ (S¯ O R) (SPEC P)"
using a3 by (meson assms(3) dual_order.trans ireturn_rule)
obtain bba :: "'b set ⇒ ('c × 'b) set ⇒ 'c ⇒ 'b" where
"∀x0 x1 x2. (∃v3. v3 ∈ x0 ∧ (x2, v3) ∈ x1) = (bba x0 x1 x2 ∈ x0 ∧ (x2, bba x0 x1 x2) ∈ x1)"
by moura
then have "y = cc R (S¯) (bba (Collect P) (S¯ O R) y) y"
"bba (Collect P) (S¯ O R) y = bb R (S¯) (bba (Collect P) (S¯ O R) y) y"
"(cc R (S¯) (bba (Collect P) (S¯ O R) y) y, aa R (S¯) (bba (Collect P) (S¯ O R) y) y) ∈ S¯"
"(aa R (S¯) (bba (Collect P) (S¯ O R) y) y, bb R (S¯) (bba (Collect P) (S¯ O R) y) y) ∈ R"
using f5 f4 by (meson RETURN_RES_refine_iff relcomp.cases)+
then show ?thesis
using a2 a1 by (metis Domain.simps converse.intros single_valued_def)
qed
moreover
from assms have a1: "Collect Q ⊆ (S¯ O R)¯ `` Collect P"
by (auto simp: conc_fun_def)
have "P x" if Q: "Q z" and a3: "(y, z) ∈ S" and a4: "(y, x) ∈ R" for x y z
proof -
obtain bb :: "'b set ⇒ ('b × 'c) set ⇒ 'c ⇒ 'b" where
f7: "∀x0 x1 x2. (∃v3. (v3, x2) ∈ x1 ∧ v3 ∈ x0) = ((bb x0 x1 x2, x2) ∈ x1 ∧ bb x0 x1 x2 ∈ x0)"
by moura
have f8: "z ∈ (S¯ O R)¯ `` Collect P"
using Q a1 by fastforce
obtain cc :: "('a × 'c) set ⇒ 'a ⇒ 'c ⇒ 'c" and aa :: "('a × 'c) set ⇒ 'a ⇒ 'c ⇒ 'a" where
f9: "z = cc S y z ∧ y = aa S y z ∧ (aa S y z, cc S y z) ∈ S"
using a3 by simp
then have f10: "(bb (Collect P) ((S¯ O R)¯) (cc S y z), cc S y z) ∈ (S¯ O R)¯ ∧ bb (Collect P) ((S¯ O R)¯) (cc S y z) ∈ Collect P"
using f8 f7 by (metis (no_types) ImageE)
have "(z, y) ∈ S¯"
using a3 by force
then show ?thesis
using f10 f9 a2 a5 a4 by (metis converse.cases mem_Collect_eq relcompEpair single_valued_def)
qed
ultimately show ?thesis
by (auto simp: conc_fun_def abs_fun_def)
qed
lemma nres_rel_comp: "⟨A⟩nres_rel O ⟨B⟩nres_rel = ⟨A O B⟩ nres_rel"
unfolding nres_rel_def
apply (auto simp: nres_rel_def conc_fun_def converse_relcomp relcomp_Image split: )
apply (subst converse_relcomp)
apply (subst relcomp_Image)
apply (auto split: nres.splits)
apply (meson Image_mono RES_leof_RES_iff equalityE le_RES_nofailI leofD leof_lift leof_trans)
apply (rule relcompI)
defer apply force
apply (auto simp: converse_relcomp relcomp_Image)
done
lemma nres_rel_mono: "A ⊆ B ⟹ ⟨A⟩nres_rel ⊆ ⟨B⟩nres_rel"
apply (auto simp: nres_rel_def conc_fun_def)
apply (split nres.splits)+
apply auto
by (meson Image_mono RES_leof_RES_iff converse_mono equalityE le_RES_nofailI leofD leof_lift leof_trans)
text ‹TODO: move!!›
lemma
uncurry_rec_list: "rec_list (λa b. fn a b) (λx xs rr a b. fs x xs rr a b) xs a b =
rec_list (λ(a,b). fn a b) (λx xs rr (a,b). fs x xs (λa b. rr (a,b)) a b) xs (a,b)"
apply (induction xs arbitrary: a b)
apply (auto split: prod.splits)
apply metis
done
lemma Id_br: "Id = br (λx. x) top"
by (auto simp: br_def)
lemma br_rel_prod: "br a I ×⇩r br b J = br (λ(x, y). (a x, b y)) (λ(x, y). I x ∧ J y)"
by (auto simp: br_def)
lemma br_list_rel: "⟨br a I⟩list_rel = br (map a) (list_all I)"
apply (auto simp: br_def list_rel_def list_all_iff list_all2_iff split_beta' Ball_def
in_set_zip intro!: nth_equalityI)
apply force
by (metis in_set_conv_nth)
lemma brD: "(c,a)∈br α I ⟹ a = α c ∧ I c"
by (simp add: br_def)
primrec nres_of_nress :: "('b ⇒ bool) ⇒ 'b nres list ⇒ 'b list nres"
where "nres_of_nress P [] = RETURN []"
| "nres_of_nress P (x#xs) = do {r ← x; rs ← nres_of_nress P xs; RETURN (r#rs)}"
lemma nres_of_nress_SPEC[THEN order_trans, refine_vcg]:
assumes [refine_vcg]: "⋀x. x ∈ set xs ⟹ x ≤ SPEC P"
shows "nres_of_nress P xs ≤ SPEC (list_all P)"
using assms
apply (induction xs)
apply simp
apply (simp add:)
apply (intro refine_vcg)
subgoal for x xs
apply (rule order_trans[of _ "SPEC P"])
apply auto
apply refine_vcg
done
done
context includes autoref_syntax begin
lemma [autoref_op_pat_def]: "nres_of_nress P x ≡ (OP (nres_of_nress P) $ x)"
by auto
lemma nres_of_nress_alt_def[abs_def]:
"nres_of_nress P xs = rec_list (RETURN []) (λx xs xsa. x ⤜ (λr. xsa ⤜ (λrs. RETURN (r # rs)))) xs"
by (induction xs) auto
schematic_goal nres_of_nress_impl:
"(?r, nres_of_nress P $ x) ∈ ⟨⟨A⟩list_rel⟩nres_rel"
if [autoref_rules]: "(xi, x) ∈ ⟨⟨A⟩nres_rel⟩list_rel"
unfolding nres_of_nress_alt_def
by autoref
concrete_definition nres_of_nress_impl uses nres_of_nress_impl
lemmas [autoref_rules] = nres_of_nress_impl.refine
lemma nres_of_nress_impl_map:
"nres_of_nress_impl (map f x) =
rec_list (RETURN []) (λx xs r. do { fx ← f x; r ← r; RETURN (fx # r)}) x"
by (induction x) (auto simp: nres_of_nress_impl_def)
definition [refine_vcg_def]: "list_spec X = SPEC (λxs. set xs = X)"
end
lemma
insert_mem_set_rel_iff:
assumes "single_valued A"
shows "(insert x (set xs), XXS) ∈ ⟨A⟩set_rel ⟷ (∃X XS. (x, X) ∈ A ∧ (set xs, XS) ∈ ⟨A⟩set_rel ∧ XXS = insert X XS)"
using assms
apply (auto simp: set_rel_def single_valuedD)
subgoal for a
apply (cases "x ∈ set xs")
subgoal by (rule exI[where x=a]) auto
subgoal
apply (rule exI[where x=a])
apply auto
apply (rule exI[where x="{y∈XXS. (∃x∈set xs. (x, y) ∈ A)}"])
apply auto
subgoal by (drule bspec, assumption) auto
subgoal by (meson single_valuedD)
done
done
done
lemma image_mem_set_rel_iff:
shows "(f ` x, y) ∈ ⟨R⟩set_rel ⟷ (x, y) ∈ ⟨br f top O R⟩set_rel"
proof -
have "z ∈ Domain ({(c, a). a = f c} O R)"
if "f ` x ⊆ Domain R" "z ∈ x"
for z
proof -
have "(f z, fun_of_rel R (f z)) ∈ R"
using that
by (auto intro!: for_in_RI)
then show ?thesis
by (auto intro!: Domain.DomainI[where b="fun_of_rel R (f z)"] relcompI[where b="f z"])
qed
then show ?thesis
by (auto simp: set_rel_def relcomp.simps br_def)
qed
lemma finite_list_set_rel[autoref_rules]: "(λ_. True, finite) ∈ ⟨A⟩list_set_rel → bool_rel"
by (auto simp: list_set_rel_def br_def)
lemma list_set_rel_finiteD: "(xs, X) ∈ ⟨A⟩list_set_rel ⟹ finite X"
by (auto simp: list_set_rel_def br_def)
lemma set_rel_br: "⟨br a I⟩set_rel = br ((`) a) (λX. Ball X I)"
by (auto simp: set_rel_def br_def)
lemma set_rel_sv:
"⟨R⟩set_rel = {(S,S'). S'=R``S ∧ S⊆Domain R}"
if "single_valued R"
using that
by (auto simp: set_rel_def set_rel_br elim!: single_valued_as_brE)
(auto simp: br_def)
lemma list_ex_rec_list: "list_ex P xs = rec_list False (λx xs b. P x ∨ b) xs"
by (induct xs) simp_all
lemma list_ex_param[autoref_rules, param]:
"(list_ex, list_ex) ∈ (A → bool_rel) → ⟨A⟩list_rel → bool_rel"
unfolding list_ex_rec_list
by parametricity
lemma zip_param[autoref_rules, param]:
"(zip, zip) ∈ ⟨A⟩list_rel → ⟨A⟩list_rel → ⟨A ×⇩r A⟩list_rel"
by (rule param_zip)
lemma ex_br_conj_iff:
"(∃x. (y, x) ∈ br a I ∧ P x) ⟷ I y ∧ P (a y)"
by (auto intro!: brI dest!: brD)
setup ‹
let
fun higher_order_rl_of assms ctxt thm =
let
val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt
in
case Thm.concl_of thm' of
@{mpat "Trueprop ((_,?t)∈_)"} => let
val (f0, args0) = strip_comb t
val nargs = Thm.nprems_of thm' - length assms
val (applied, args) = chop (length args0 - nargs) args0
val f = betapplys (f0, applied)
in
if length args = 0 then
thm
else let
val cT = TVar(("'c",0), @{sort type})
val c = Var (("c",0),cT)
val R = Var (("R",0), HOLogic.mk_setT (HOLogic.mk_prodT (cT, fastype_of f)))
val goal =
HOLogic.mk_mem (HOLogic.mk_prod (c,f), R)
|> HOLogic.mk_Trueprop
|> Thm.cterm_of ctxt
val res_thm = Goal.prove_internal ctxt' (map (Thm.cprem_of thm') assms) goal (fn prems =>
REPEAT (resolve_tac ctxt' @{thms fun_relI} 1)
THEN (resolve_tac ctxt' [thm] 1)
THEN (REPEAT (resolve_tac ctxt' prems 1))
THEN (ALLGOALS (assume_tac ctxt'))
)
in
singleton (Variable.export ctxt' ctxt) res_thm
end
end
| _ => raise THM("Expected autoref rule",~1,[thm])
end
fun higher_order_rl_attr assms =
Thm.rule_attribute [] (higher_order_rl_of assms o Context.proof_of)
in
Attrib.setup @{binding autoref_higher_order_rule}
(Scan.optional (Scan.lift(Args.parens (Scan.repeat Parse.nat))) [] >>
higher_order_rl_attr) "Autoref: Convert rule to higher-order form"
end
›
end