Theory Collections.Gen_Set

section ‹\isaheader{Generic Set Algorithms}›
theory Gen_Set
imports "../Intf/Intf_Set" "../../Iterator/Iterator"
begin

  lemma foldli_union: "det_fold_set X (λ_. True) insert a ((∪) a)"
  proof (rule, goal_cases)
    case (1 l) thus ?case
      by (induct l arbitrary: a) auto
  qed

  definition gen_union
    :: "_  ('k  's2  's2) 
         's1  's2  's2"
    where 
    "gen_union it ins A B  it A (λ_. True) ins B"

  lemma gen_union[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes INS: "GEN_OP ins Set.insert (RkRkRs2RkRs2)"
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
    shows "(gen_union (λx. foldli (tsl x)) ins,(∪)) 
     (RkRs1)  (RkRs2)  (RkRs2)"
    apply (intro fun_relI)
    apply (subst Un_commute)
    unfolding gen_union_def 
    apply (rule det_fold_set[OF 
      foldli_union IT[unfolded autoref_tag_defs]])
    using INS
    unfolding autoref_tag_defs
    apply (parametricity)+
    done

  lemma foldli_inter: "det_fold_set X (λ_. True) 
    (λx s. if xa then insert x s else s) {} (λs. sa)" 
    (is "det_fold_set _ _ ?f _ _")
  proof -
    {
      fix l s0
      have "foldli l (λ_. True) 
        (λx s. if xa then insert x s else s) s0 = s0  (set l  a)"
        by (induct l arbitrary: s0) auto
    }
    from this[of _ "{}"] show ?thesis apply - by rule simp
  qed

  definition gen_inter :: "_  
    ('k  's2  bool)  _"
    where "gen_inter it1 memb2 ins3 empty3 s1 s2 
     it1 s1 (λ_. True) 
      (λx s. if memb2 x s2 then ins3 x s else s) empty3"

  lemma gen_inter[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
    assumes MEMB:
      "GEN_OP memb2 (∈) (Rk  RkRs2  Id)"
    assumes INS: 
      "GEN_OP ins3 Set.insert (RkRkRs3RkRs3)"
    assumes EMPTY: 
      "GEN_OP empty3 {} (RkRs3)"
    shows "(gen_inter (λx. foldli (tsl x)) memb2 ins3 empty3,(∩)) 
     (RkRs1)  (RkRs2)  (RkRs3)"
    apply (intro fun_relI)
    unfolding gen_inter_def
    apply (rule det_fold_set[OF foldli_inter IT[unfolded autoref_tag_defs]])
    using MEMB INS EMPTY
    unfolding autoref_tag_defs
    apply (parametricity)+
    done
 
  lemma foldli_diff: 
    "det_fold_set X (λ_. True) (λx s. op_set_delete x s) s ((-) s)"
  proof (rule, goal_cases)
    case (1 l) thus ?case
      by (induct l arbitrary: s) auto
  qed

  definition gen_diff :: "('k's1's1)  _  's2  _ "
    where "gen_diff del1 it2 s1 s2 
     it2 s2 (λ_. True) (λx s. del1 x s) s1"

  lemma gen_diff[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes DEL:
      "GEN_OP del1 op_set_delete (Rk  RkRs1  RkRs1)"
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs2 it2)"
    shows "(gen_diff del1 (λx. foldli (it2 x)),(-)) 
       (RkRs1)  (RkRs2)  (RkRs1)"
    apply (intro fun_relI)
    unfolding gen_diff_def 
    apply (rule det_fold_set[OF foldli_diff IT[unfolded autoref_tag_defs]])
    using DEL
    unfolding autoref_tag_defs
    apply (parametricity)+
    done

  lemma foldli_ball_aux: 
    "foldli l (λx. x) (λx _. P x) b  b  Ball (set l) P"
    by (induct l arbitrary: b) auto

  lemma foldli_ball: "det_fold_set X (λx. x) (λx _. P x) True (λs. Ball s P)"
    apply rule using foldli_ball_aux[where b=True] by simp

  definition gen_ball :: "_  's  ('k  bool)  _ "
    where "gen_ball it s P  it s (λx. x) (λx _. P x) True"

  lemma gen_ball[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
    shows "(gen_ball (λx. foldli (it x)),Ball)  RkRs  (RkId)  Id"
    apply (intro fun_relI)
    unfolding gen_ball_def
    apply (rule det_fold_set[OF foldli_ball IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done

  lemma foldli_bex_aux: "foldli l (λx. ¬x) (λx _. P x) b  b  Bex (set l) P"
    by (induct l arbitrary: b) auto

  lemma foldli_bex: "det_fold_set X (λx. ¬x) (λx _. P x) False (λs. Bex s P)"
    apply rule using foldli_bex_aux[where b=False] by simp

  definition gen_bex :: "_  's  ('k  bool)  _ "
    where "gen_bex it s P  it s (λx. ¬x) (λx _. P x) False"

  lemma gen_bex[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
    shows "(gen_bex (λx. foldli (it x)),Bex)  RkRs  (RkId)  Id"
    apply (intro fun_relI)
    unfolding gen_bex_def 
    apply (rule det_fold_set[OF foldli_bex IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done

  lemma ball_subseteq:
    "(Ball s1 (λx. xs2))  s1  s2"
    by blast

  definition gen_subseteq 
    :: "('s1  ('k  bool)  bool)  ('k  's2  bool)  _" 
    where "gen_subseteq ball1 mem2 s1 s2  ball1 s1 (λx. mem2 x s2)"

  lemma gen_subseteq[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes "GEN_OP ball1 Ball (RkRs1  (RkId)  Id)"
    assumes "GEN_OP mem2 (∈) (Rk  RkRs2  Id)"
    shows "(gen_subseteq ball1 mem2,(⊆))  RkRs1  RkRs2  Id"
    apply (intro fun_relI)
    unfolding gen_subseteq_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst ball_subseteq[symmetric])
    apply parametricity
    done

  definition "gen_equal ss1 ss2 s1 s2  ss1 s1 s2  ss2 s2 s1"

  lemma gen_equal[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes "GEN_OP ss1 (⊆) (RkRs1  RkRs2  Id)"
    assumes "GEN_OP ss2 (⊆) (RkRs2  RkRs1  Id)"
    shows "(gen_equal ss1 ss2, (=))  RkRs1  RkRs2  Id"
    apply (intro fun_relI)
    unfolding gen_equal_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst set_eq_subset)
    apply (parametricity)
    done

  lemma foldli_card_aux: "distinct l  foldli l (λ_. True) 
    (λ_ n. Suc n) n = n + card (set l)"
    apply (induct l arbitrary: n) 
    apply auto
    done
  
  lemma foldli_card: "det_fold_set X (λ_. True) (λ_ n. Suc n) 0 card"
    apply rule using foldli_card_aux[where n=0] by simp

  definition gen_card where
    "gen_card it s  it s (λx. True) (λ_ n. Suc n) 0"

  lemma gen_card[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
    shows "(gen_card (λx. foldli (it x)),card)  RkRs  Id"
    apply (intro fun_relI)
    unfolding gen_card_def
    apply (rule det_fold_set[OF foldli_card IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done

  lemma fold_set: "fold Set.insert l s = s  set l"
    by (induct l arbitrary: s) auto

  definition gen_set :: "'s  ('k  's  's)  _" where
    "gen_set emp ins l = fold ins l emp"

  lemma gen_set[autoref_rules_raw]: 
    assumes PRIO_TAG_GEN_ALGO
    assumes EMPTY: 
      "GEN_OP emp {} (RkRs)"
    assumes INS: 
      "GEN_OP ins Set.insert (RkRkRsRkRs)"
    shows "(gen_set emp ins,set)Rklist_relRkRs"
    apply (intro fun_relI)
    unfolding gen_set_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst fold_set[where s="{}",simplified,symmetric])
    apply parametricity
    done
    
  lemma ball_isEmpty: "op_set_isEmpty s = (xs. False)"
    by auto

  definition gen_isEmpty :: "('s  ('k  bool)  bool)  's  bool" where
    "gen_isEmpty ball s  ball s (λ_. False)"

  lemma gen_isEmpty[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes "GEN_OP ball Ball (RkRs  (RkId)  Id)"
    shows "(gen_isEmpty ball,op_set_isEmpty)  RkRs  Id"
    apply (intro fun_relI)
    unfolding gen_isEmpty_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst ball_isEmpty)
    apply parametricity
    done
  
  lemma foldli_size_abort_aux:
    "n0m; distinct l  
      foldli l (λn. n<m) (λ_ n. Suc n) n0 = min m (n0 + card (set l))"
    apply (induct l arbitrary: n0)
    apply auto
    done

  lemma foldli_size_abort: "
    det_fold_set X (λn. n<m) (λ_ n. Suc n) 0 (op_set_size_abort m)"
    apply rule
    using foldli_size_abort_aux[where ?n0.0=0]
    by simp

  definition gen_size_abort where
    "gen_size_abort it m s  it s (λn. n<m) (λ_ n. Suc n) 0"

  lemma gen_size_abort[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
    shows "(gen_size_abort (λx. foldli (it x)),op_set_size_abort) 
     Id  RkRs  Id"
    apply (intro fun_relI)
    unfolding gen_size_abort_def 
    apply (rule det_fold_set[OF foldli_size_abort IT[unfolded autoref_tag_defs]])
    apply (parametricity)+
    done
    
  lemma size_abort_isSng: "op_set_isSng s  op_set_size_abort 2 s = 1"
    by auto 

  definition gen_isSng :: "(nat  's  nat)  _" where
    "gen_isSng sizea s  sizea 2 s = 1"

  lemma gen_isSng[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes "GEN_OP sizea op_set_size_abort (Id  (RkRs)  Id)"
    shows "(gen_isSng sizea,op_set_isSng)  RkRs  Id"
    apply (intro fun_relI)
    unfolding gen_isSng_def using assms
    unfolding autoref_tag_defs
    apply -
    apply (subst size_abort_isSng)
    apply parametricity
    done
    
  lemma foldli_disjoint_aux:
    "foldli l1 (λx. x) (λx _. ¬xs2) b  b  op_set_disjoint (set l1) s2"
    by (induct l1 arbitrary: b) auto

  lemma foldli_disjoint: 
    "det_fold_set X (λx. x) (λx _. ¬xs2) True (λs1. op_set_disjoint s1 s2)"
    apply rule using foldli_disjoint_aux[where b=True] by simp

  definition gen_disjoint 
    :: "_  ('k's2bool)  _"
    where "gen_disjoint it1 mem2 s1 s2 
     it1 s1 (λx. x) (λx _. ¬mem2 x s2) True"

  lemma gen_disjoint[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
    assumes MEM: "GEN_OP mem2 (∈) (Rk  RkRs2  Id)"
    shows "(gen_disjoint (λx. foldli (it1 x)) mem2,op_set_disjoint) 
     RkRs1  RkRs2  Id"
    apply (intro fun_relI)
    unfolding gen_disjoint_def 
    apply (rule det_fold_set[OF foldli_disjoint IT[unfolded autoref_tag_defs]])
    using MEM unfolding autoref_tag_defs
    apply (parametricity)+
    done

  lemma foldli_filter_aux:
    "foldli l (λ_. True) (λx s. if P x then insert x s else s) s0 
    = s0  op_set_filter P (set l)"
    by (induct l arbitrary: s0) auto

  lemma foldli_filter: 
    "det_fold_set X (λ_. True) (λx s. if P x then insert x s else s) {} 
      (op_set_filter P)"
    apply rule using foldli_filter_aux[where ?s0.0="{}"] by simp

  definition gen_filter
    where "gen_filter it1 emp2 ins2 P s1  
      it1 s1 (λ_. True) (λx s. if P x then ins2 x s else s) emp2"

  lemma gen_filter[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
    assumes INS: 
      "GEN_OP ins2 Set.insert (RkRkRs2RkRs2)"
    assumes EMPTY: 
      "GEN_OP empty2 {} (RkRs2)"
    shows "(gen_filter (λx. foldli (it1 x)) empty2 ins2,op_set_filter) 
     (RkId)  (RkRs1)  (RkRs2)"
    apply (intro fun_relI)
    unfolding gen_filter_def
    apply (rule det_fold_set[OF foldli_filter IT[unfolded autoref_tag_defs]])
    using INS EMPTY unfolding autoref_tag_defs
    apply (parametricity)+
    done

  lemma foldli_image_aux:
    "foldli l (λ_. True) (λx s. insert (f x) s) s0
    = s0  f`(set l)"
    by (induct l arbitrary: s0) auto

  lemma foldli_image: 
    "det_fold_set X (λ_. True) (λx s. insert (f x) s) {} 
      ((`) f)"
    apply rule using foldli_image_aux[where ?s0.0="{}"] by simp

  definition gen_image
    where "gen_image it1 emp2 ins2 f s1  
      it1 s1 (λ_. True) (λx s. ins2 (f x) s) emp2"

  lemma gen_image[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
    assumes INS: 
      "GEN_OP ins2 Set.insert (Rk'Rk'Rs2Rk'Rs2)"
    assumes EMPTY: 
      "GEN_OP empty2 {} (Rk'Rs2)"
    shows "(gen_image (λx. foldli (it1 x)) empty2 ins2,(`)) 
     (RkRk')  (RkRs1)  (Rk'Rs2)"
    apply (intro fun_relI)
    unfolding gen_image_def
    apply (rule det_fold_set[OF foldli_image IT[unfolded autoref_tag_defs]])
    using INS EMPTY unfolding autoref_tag_defs
    apply (parametricity)+
    done

  (* TODO: Also do sel! *)

  lemma foldli_pick:
    assumes "l[]" 
    obtains x where "xset l" 
    and "(foldli l (case_option True (λ_. False)) (λx _. Some x) None) = Some x"
    using assms by (cases l) auto

  definition gen_pick where
    "gen_pick it s  
      (the (it s (case_option True (λ_. False)) (λx _. Some x) None))"

context begin interpretation autoref_syn .
  lemma gen_pick[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
    assumes NE: "SIDE_PRECOND (s'{})"
    assumes SREF: "(s,s')RkRs"
    shows "(RETURN (gen_pick (λx. foldli (it x)) s), 
      (OP op_set_pick ::: RkRsRknres_rel)$s')Rknres_rel"
  proof -
    obtain tsl' where
      [param]: "(it s,tsl')  Rklist_rel" 
      and IT': "RETURN tsl'  it_to_sorted_list (λ_ _. True) s'"
      using IT[unfolded autoref_tag_defs is_set_to_list_def] SREF
      by (rule is_set_to_sorted_listE)

    from IT' NE have "tsl'[]" and [simp]: "s'=set tsl'" 
      unfolding it_to_sorted_list_def by simp_all
    then obtain x where "xs'" and
      "(foldli tsl' (case_option True (λ_. False)) (λx _. Some x) None) = Some x"
      (is "?fld = _")
      by (blast elim: foldli_pick)
    moreover 
    have "(RETURN (gen_pick (λx. foldli (it x)) s), RETURN (the ?fld)) 
       Rknres_rel"
      unfolding gen_pick_def
      apply (parametricity add: the_paramR)
      using ?fld = Some x
      by simp
    ultimately show ?thesis
      unfolding autoref_tag_defs
      apply -
      apply (drule nres_relD)
      apply (rule nres_relI)
      apply (erule ref_two_step)
      by simp
  qed
end

  definition gen_Sigma
    where "gen_Sigma it1 it2 empX insX s1 f2  
      it1 s1 (λ_. True) (λx s. 
        it2 (f2 x) (λ_. True) (λy s. insX (x,y) s) s
      ) empX
    "

  lemma foldli_Sigma_aux:
    fixes s :: "'s1_impl" and s':: "'k set"
    fixes f :: "'k_impl  's2_impl" and f':: "'k  'l set"
    fixes s0 :: "'kl_impl" and s0' :: "('k×'l) set"
    assumes IT1: "is_set_to_list Rk Rs1 it1"
    assumes IT2: "is_set_to_list Rl Rs2 it2"
    assumes INS: 
      "(insX, Set.insert)  
        (Rk,Rlprod_relRk,Rlprod_relRs3Rk,Rlprod_relRs3)"
    assumes S0R: "(s0, s0')  Rk,Rlprod_relRs3" 
    assumes SR: "(s, s')  RkRs1" 
    assumes FR: "(f, f')  Rk  RlRs2"
    shows "(foldli (it1 s) (λ_. True) (λx s. 
        foldli (it2 (f x)) (λ_. True) (λy s. insX (x,y) s) s
      ) s0,s0'  Sigma s' f') 
       Rk,Rlprod_relRs3"
  proof -
    have S: "x s f. Sigma (insert x s) f = ({x}×f x)  Sigma s f"
      by auto

    obtain l' where 
      IT1L: "(it1 s,l')Rklist_rel" 
      and SL: "s' = set l'"
      apply (rule 
        is_set_to_sorted_listE[OF IT1[unfolded is_set_to_list_def] SR])
      by (auto simp: it_to_sorted_list_def)

    show ?thesis
      unfolding SL
      using IT1L S0R
    proof (induct arbitrary: s0 s0' rule: list_rel_induct)
      case Nil thus ?case by simp
    next
      case (Cons x x' l l')

      obtain l2' where 
        IT2L: "(it2 (f x),l2')Rllist_rel" 
        and FXL: "f' x' = set l2'"
        apply (rule 
          is_set_to_sorted_listE[
            OF IT2[unfolded is_set_to_list_def], of "f x" "f' x'"
          ])
        apply (parametricity add: Cons.hyps(1) FR)
        by (auto simp: it_to_sorted_list_def)

      have "(foldli (it2 (f x)) (λ_. True) (λy. insX (x, y)) s0, 
        s0'  {x'}×f' x')  Rk,Rlprod_relRs3"
        unfolding FXL 
        using IT2L (s0, s0')  Rk, Rlprod_relRs3
        apply (induct  arbitrary: s0 s0' rule: list_rel_induct)
        apply simp
        apply simp
        apply (subst Un_insert_left[symmetric])
        apply (rprems)
        apply (parametricity add: INS (x,x')Rk)
        done

      show ?case
        apply simp
        apply (subst S)
        apply (subst Un_assoc[symmetric])
        apply (rule Cons.hyps)
        apply fact
        done
    qed
  qed


  lemma gen_Sigma[autoref_rules_raw]:
    assumes PRIO_TAG_GEN_ALGO
    assumes IT1: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
    assumes IT2: "SIDE_GEN_ALGO (is_set_to_list Rl Rs2 it2)"
    assumes EMPTY: 
      "GEN_OP empX {} (Rk,Rlprod_relRs3)"
    assumes INS: 
      "GEN_OP insX Set.insert 
         (Rk,Rlprod_relRk,Rlprod_relRs3Rk,Rlprod_relRs3)"
    shows "(gen_Sigma (λx. foldli (it1 x)) (λx. foldli (it2 x)) empX insX,Sigma) 
       (RkRs1)  (Rk  RlRs2)  Rk,Rlprod_relRs3"
    apply (intro fun_relI)
    unfolding gen_Sigma_def
    using foldli_Sigma_aux[OF 
      IT1[unfolded autoref_tag_defs]
      IT2[unfolded autoref_tag_defs]
      INS[unfolded autoref_tag_defs]
      EMPTY[unfolded autoref_tag_defs]
    ]
    by simp

lemma gen_cart:
  assumes PRIO_TAG_GEN_ALGO
  assumes [param]: "(sigma, Sigma)  (RxRsx  (Rx  RyRsy)  Rx ×r RyRsp)"
  shows "(λx y. sigma x (λ_. y), op_set_cart)  RxRsx  RyRsy  Rx ×r RyRsp"
  unfolding op_set_cart_def[abs_def]
  by parametricity
lemmas [autoref_rules] = gen_cart[OF _ GEN_OP_D]


context begin interpretation autoref_syn .

  lemma op_set_to_sorted_list_autoref[autoref_rules]:
    assumes "SIDE_GEN_ALGO (is_set_to_sorted_list ordR Rk Rs tsl)"
    shows "(λsi. RETURN (tsl si),  OP (op_set_to_sorted_list ordR)) 
       RkRs  Rklist_relnres_rel"
    using assms
    apply (intro fun_relI nres_relI)
    apply simp
    apply (rule RETURN_SPEC_refine)
    apply (auto simp: is_set_to_sorted_list_def it_to_sorted_list_def)
    done

  lemma op_set_to_list_autoref[autoref_rules]:
    assumes "SIDE_GEN_ALGO (is_set_to_sorted_list ordR Rk Rs tsl)"
    shows "(λsi. RETURN (tsl si), op_set_to_list) 
       RkRs  Rklist_relnres_rel"
    using assms
    apply (intro fun_relI nres_relI)
    apply simp
    apply (rule RETURN_SPEC_refine)
    apply (auto simp: is_set_to_sorted_list_def it_to_sorted_list_def)
    done

end

lemma foldli_Union: "det_fold_set X (λ_. True) (∪) {} Union"
proof (rule, goal_cases)
  case (1 l)
  have "a. foldli l (λ_. True) (∪) a = a  (set l)"
    by (induct l) auto
  thus ?case by auto
qed

definition gen_Union
  :: "_  's3  ('s2  's3  's3) 
       's1  's3"
  where 
  "gen_Union it emp un X  it X (λ_. True) un emp"

lemma gen_Union[autoref_rules_raw]:
  assumes PRIO_TAG_GEN_ALGO
  assumes EMP: "GEN_OP emp {} (RkRs3)"
  assumes UN: "GEN_OP un (∪) (RkRs2RkRs3RkRs3)"
  assumes IT: "SIDE_GEN_ALGO (is_set_to_list (RkRs2) Rs1 tsl)"
  shows "(gen_Union (λx. foldli (tsl x)) emp un,Union)  RkRs2Rs1  RkRs3"
  apply (intro fun_relI)
  unfolding gen_Union_def 
  apply (rule det_fold_set[OF 
    foldli_Union IT[unfolded autoref_tag_defs]])
  using EMP UN
  unfolding autoref_tag_defs
  apply (parametricity)+
  done

definition "atLeastLessThan_impl a b  do {
  (_,r)  WHILET (λ(i,r). i<b) (λ(i,r). RETURN (i+1, insert i r)) (a,{});
  RETURN r
}"

lemma atLeastLessThan_impl_correct: 
  "atLeastLessThan_impl a b  SPEC (λr. r = {a..<b::nat})"
  unfolding atLeastLessThan_impl_def
  apply (refine_rcg refine_vcg WHILET_rule[where 
    I = "λ(i,r). r = {a..<i}  ai  ((a<b  ib)  (¬a<b  i=a))"
    and R = "measure (λ(i,_). b - i)"
    ])
  by auto

schematic_goal atLeastLessThan_code_aux:
  notes [autoref_rules] = IdI[of a] IdI[of b]
  assumes [autoref_rules]: "(emp,{})Rs"
  assumes [autoref_rules]: "(ins,insert)nat_rel  Rs  Rs"
  shows "(?c, atLeastLessThan_impl) 
   nat_rel  nat_rel  Rsnres_rel"
  unfolding atLeastLessThan_impl_def[abs_def]
  apply (autoref (keep_goal))
  done
concrete_definition atLeastLessThan_code uses atLeastLessThan_code_aux

schematic_goal atLeastLessThan_tr_aux:
  "RETURN ?c  atLeastLessThan_code emp ins a b"
  unfolding atLeastLessThan_code_def
  by (refine_transfer (post))
concrete_definition atLeastLessThan_tr 
  for emp ins a b uses atLeastLessThan_tr_aux

lemma atLeastLessThan_gen[autoref_rules]: 
  assumes "PRIO_TAG_GEN_ALGO"
  assumes "GEN_OP emp {} Rs"
  assumes "GEN_OP ins insert (nat_rel  Rs  Rs)"
  shows "(atLeastLessThan_tr emp ins, atLeastLessThan) 
     nat_rel  nat_rel  Rs"
proof (intro fun_relI, simp)
  fix a b
  from assms have GEN: 
    "(emp,{})Rs" "(ins,insert)nat_rel  Rs  Rs"
    by auto

  note atLeastLessThan_tr.refine[of emp ins a b]
  also note 
    atLeastLessThan_code.refine[OF GEN,param_fo, OF IdI IdI, THEN nres_relD]
  also note atLeastLessThan_impl_correct
  finally show "(atLeastLessThan_tr emp ins a b, {a..<b})  Rs"
    by (auto simp: pw_le_iff refine_pw_simps)
qed

end