Theory Autoref_Misc

(* TODO: Integrate into Misc*)
theory Autoref_Misc

(* Refine-Basic *)
(* TODO: Move to Refine_Basic *)
lemma nofail_RES_conv: "nofail m  (M. m=RES M)" by (cases m) auto

(* TODO: Move, near SPEC_nofail  *)
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)

(* TODO: Move *)
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  xX"
  by (simp add: refine_pw_simps)

lemma nf_inres_SPEC[simp]: "nf_inres (SPEC Φ) x  Φ x"
  by (simp add: refine_pw_simps)

(* TODO: Move *)
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)Rnres_rel  a R b"
  by (auto simp: nres_rel_def)

lemma inf_RETURN_RES:
  "inf (RETURN x) (RES X) = (if xX then RETURN x else SUCCEED)"
  "inf (RES X) (RETURN x) = (if xX then RETURN x else SUCCEED)"
  by (auto simp: pw_eq_iff refine_pw_simps)

(* TODO: MOve, test as default simp-rule *)
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 {xa; 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)"
  ― ‹Lift assertion over refinement relation›
  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

(* TODO: Replace original lemma *)
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"
  ― ‹Ghost tag to mark ghost variables in let-expressions›
  where [simp]: "GHOST  λx. x"
lemma GHOST_elim_Let: ― ‹Unfold rule to inline GHOST-Lets›
  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. xX  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 {xm; 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 "xX"
  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)  (xX. nofail (f x))"
  "inres (RES X  f) y  (xX. inres (f x) y)"
  by (auto simp: refine_pw_simps)

(* TODO: Move to Refine_Basic: Convenience*)
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)"
  ― ‹Strengthen SPEC by adding trivial upper bound for result›
  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')Rnres_rel"
  shows "(op_nres_ASSERT_bnd Φ m, op_nres_ASSERT_bnd Φ' m')  Rnres_rel"
  using assms
  by (auto simp: pw_le_iff refine_pw_simps nres_rel_def)

declare autoref_FAIL[param]

(* Refine_Transfer *)
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)

(* TODO: Move *)
lemma nres_of_transfer[refine_transfer]: "nres_of x  nres_of x" by simp

(* Refine_Foreach  *)
(* TODO: Change in Refine_Foreach(?)! *)
declare FOREACH_patterns[autoref_op_pat_def]

(* Refine_Recursion  *)

(* Refine_While  *)
context begin interpretation autoref_syn .
(* TODO: Change in Refine_While *)
lemma [autoref_op_pat_def]:
  by auto

(* Relators *)
lemma set_relD: "(s,s')Rset_rel  xs  x's'. (x,x')R"
  unfolding set_rel_def by blast

lemma set_relE[consumes 2]:
  assumes "(s,s')Rset_rel" "xs"
  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)

(* Parametricity-HOL *)

lemma dropWhile_param[param]:
  "(dropWhile, dropWhile)  (a  bool_rel)  alist_rel  alist_rel"
  unfolding dropWhile_def by parametricity

term takeWhile
lemma takeWhile_param[param]:
  "(takeWhile, takeWhile)  (a  bool_rel)  alist_rel  alist_rel"
  unfolding takeWhile_def by parametricity

(* Autoref-HOL  *)
lemmas [autoref_rules] = dropWhile_param takeWhile_param

(* Autoref-Tool *)

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)

(* Autoref_Monadic  *)

(* TODO: Replace! *)
text ‹Default setup of the autoref-tool for the monadic framework.›

lemma autoref_monadicI1:
  assumes "(b,a)Rnres_rel"
  assumes "RETURN c  b"
  shows "(RETURN c, a)Rnres_rel" "RETURN c R a"
  using assms
  unfolding nres_rel_def
  by simp_all

lemma autoref_monadicI2:
  assumes "(b,a)Rnres_rel"
  assumes "nres_of c  b"
  shows "(nres_of c, a)Rnres_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}

      resolve_tac ctxt @{thms autoref_monadicI}
      IF_SOLVED (Autoref_Phases.all_phases_tac ctxt)
        (RefineG_Transfer.post_transfer_tac trans_thms ctxt)
        (K all_tac) (* Autoref failed *)


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

    parse_paren_lists autoref_flags
    ( fn _ => fn ctxt => SIMPLE_METHOD' (
        val ctxt = Config.put Autoref_Phases.cfg_keep_goal true ctxt
      in autoref_monadic_tac ctxt end

 "Automatic Refinement and Determinization for the Monadic Refinement Framework"

(* Move to Refine Transfer *)
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

(* TODO: Move *)
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)"
  val _ = ()
in Tagged_Solver.declare_solver @{thms TRANSFER_tagI} @{binding TRANSFER}
        (RefineG_Transfer.post_transfer_tac [])

(* TODO: check for usage in Autoref? *)
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 ― ‹TODO: add to Autoref›
lemma ― ‹TODO: needed  because @{thm dres.transfer_rec_nat} expects one argument,
  but functions with more arguments defined by primrec take several arguments›
  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

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 =

locale autoref_op_pat_def = fixes x
lemma [autoref_op_pat_def]: "x  Autoref_Tagging.OP x"
  by simp

bundle autoref_syntax begin
no_notation vec_nth (infixl "$" 90)
no_notation funcset (infixr "" 60)
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)

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)  Roption_rel"
  shows "(nres_of ?x, THE_NRES $ x)  Rnres_rel"
  unfolding THE_NRES_def
  by (autoref_monadic)

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_relnres_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)  Rnres_rel) 
    (Φ', Φ)  bool_rel 
    (f', f)  unit_rel  A 
    (do {CHECK f' Φ'; m'}, op_nres_CHECK_bnd $ f $ Φ $ m)  Rnres_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. xX. 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)  Roption_rel  Soption_rel"
  by (auto simp: option_rel_def fun_relD)

lemma those_param[param]: "(those, those)  Roption_rellist_rel  Rlist_reloption_rel"
  unfolding those_def
  by parametricity

lemma image_param[param]:
  shows "single_valued A  single_valued B 
    ((`), (`))  (A  B)  Aset_rel  Bset_rel"
  by (force simp: set_rel_def fun_rel_def elim!: single_valued_as_brE)


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)
  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)
  ultimately show ?thesis
    by (auto simp: conc_fun_def abs_fun_def)

lemma nres_rel_comp: "Anres_rel O Bnres_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)

lemma nres_rel_mono: "A  B  Anres_rel  Bnres_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 ― ‹TODO: needed  because @{thm dres.transfer_rec_list} expects one argument,
  but functions with more arguments defined by primrec take several arguments›
  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

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 Ilist_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
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)  Alist_relnres_rel"
  if [autoref_rules]: "(xi, x)  Anres_rellist_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)"


  assumes "single_valued A"
  shows "(insert x (set xs), XXS)  Aset_rel  (X XS. (x, X)  A  (set xs, XS)  Aset_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
      apply (rule exI[where x=a])
      apply auto
      apply (rule exI[where x="{yXXS. (xset xs. (x, y)  A)}"])
      apply auto
      subgoal by (drule bspec, assumption) auto
      subgoal by (meson single_valuedD)

lemma image_mem_set_rel_iff:
  shows "(f ` x, y)  Rset_rel  (x, y)  br f top O Rset_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"])
  then show ?thesis
    by (auto simp: set_rel_def relcomp.simps br_def)

lemma finite_list_set_rel[autoref_rules]: "(λ_. True, finite)  Alist_set_rel  bool_rel"
  by (auto simp: list_set_rel_def br_def)

lemma list_set_rel_finiteD: "(xs, X)  Alist_set_rel  finite X"
  by (auto simp: list_set_rel_def br_def)

lemma set_rel_br: "br a Iset_rel = br ((`) a) (λX. Ball X I)"
  by (auto simp: set_rel_def br_def)

lemma set_rel_sv:
  "Rset_rel = {(S,S'). S'=R``S  SDomain 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)  Alist_rel  bool_rel"
  unfolding list_ex_rec_list
  by parametricity

lemma zip_param[autoref_rules, param]:
  "(zip, zip)  Alist_rel  Alist_rel  A ×r Alist_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 =
        val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt
        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)
            if length args = 0 then
            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'))
              singleton (Variable.export ctxt' ctxt) res_thm
        | _ => raise THM("Expected autoref rule",~1,[thm])

    fun higher_order_rl_attr assms =
      Thm.rule_attribute [] (higher_order_rl_of assms o Context.proof_of)
    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"