Theory CollectionsV1

section ‹Backwards Compatibility for Version 1›
theory CollectionsV1
imports Collections
begin
  text ‹
    This theory defines some stuff to establish (partial) backwards
    compatibility with ICF Version 1.
›

  (*
    TODO: Dirty hack to workaround a problem that occurs with sublocale here:
      When declaring
        
  sublocale poly_map_iteratei < v1_iteratei: map_iteratei α invar iteratei
    by (rule v1_iteratei_impl)

      Any further 

  interpretation StdMap hm_ops

    will fail with
*** exception TYPE raised (line 414 of "type.ML"):
*** Type variable "?'a" has two distinct sorts
*** ?'a::type
*** ?'a::hashable

  The problem seems difficult to track down, as it, e.g., does not iccur for 
  sets.
*)

  attribute_setup locale_witness_add = ‹
    Scan.succeed (Locale.witness_add)
› "Add witness for locale instantiation. HACK, use 
      sublocale or interpretation whereever possible!"


  subsection ‹Iterators›
  text ‹We define all the monomorphic iterator locales›
  subsubsection "Set"
locale set_iteratei = finite_set α invar for α :: "'s ⇒ 'x set" and invar +
  fixes iteratei :: "'s ⇒ ('x, 'σ) set_iterator"

  assumes iteratei_rule: "invar S ⟹ set_iterator (iteratei S) (α S)"
begin
  lemma iteratei_rule_P:
    "⟦
      invar S;
      I (α S) σ0;
      !!x it σ. ⟦ c σ; x ∈ it; it ⊆ α S; I it σ ⟧ ⟹ I (it - {x}) (f x σ);
      !!σ. I {} σ ⟹ P σ;
      !!σ it. ⟦ it ⊆ α S; it ≠ {}; ¬ c σ; I it σ ⟧ ⟹ P σ
    ⟧ ⟹ P (iteratei S c f σ0)"
   apply (rule set_iterator_rule_P [OF iteratei_rule, of S I σ0 c f P])
   apply simp_all
  done

  lemma iteratei_rule_insert_P:
    "⟦
      invar S;
      I {} σ0;
      !!x it σ. ⟦ c σ; x ∈ α S - it; it ⊆ α S; I it σ ⟧ ⟹ I (insert x it) (f x σ);
      !!σ. I (α S) σ ⟹ P σ;
      !!σ it. ⟦ it ⊆ α S; it ≠ α S; ¬ c σ; I it σ ⟧ ⟹ P σ
    ⟧ ⟹ P (iteratei S c f σ0)"
    apply (rule set_iterator_rule_insert_P [OF iteratei_rule, of S I σ0 c f P])
    apply simp_all
  done

  text ‹Versions without break condition.›
  lemma iterate_rule_P:
    "⟦
      invar S;
      I (α S) σ0;
      !!x it σ. ⟦ x ∈ it; it ⊆ α S; I it σ ⟧ ⟹ I (it - {x}) (f x σ);
      !!σ. I {} σ ⟹ P σ
    ⟧ ⟹ P (iteratei S (λ_. True) f σ0)"
   apply (rule set_iterator_no_cond_rule_P [OF iteratei_rule, of S I σ0 f P])
   apply simp_all
  done

  lemma iterate_rule_insert_P:
    "⟦
      invar S;
      I {} σ0;
      !!x it σ. ⟦ x ∈ α S - it; it ⊆ α S; I it σ ⟧ ⟹ I (insert x it) (f x σ);
      !!σ. I (α S) σ ⟹ P σ
    ⟧ ⟹ P (iteratei S (λ_. True) f σ0)"
    apply (rule set_iterator_no_cond_rule_insert_P [OF iteratei_rule, of S I σ0 f P])
    apply simp_all
  done
end

lemma set_iteratei_I :
assumes "⋀s. invar s ⟹ set_iterator (iti s) (α s)"
shows "set_iteratei α invar iti"
proof
  fix s 
  assume invar_s: "invar s"
  from assms(1)[OF invar_s] show it_OK: "set_iterator (iti s) (α s)" .
  
  from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
  show "finite (α s)" .
qed

  locale set_iterateoi = ordered_finite_set α invar
    for α :: "'s ⇒ ('u::linorder) set" and invar
    +
    fixes iterateoi :: "'s ⇒ ('u,'σ) set_iterator"
    assumes iterateoi_rule: 
      "invar s ⟹ set_iterator_linord (iterateoi s) (α s)"
  begin
    lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (α m) σ0"
      assumes IP: "!!k it σ. ⟦ 
        c σ; 
        k ∈ it; 
        ∀j∈it. k≤j; 
        ∀j∈α m - it. j≤k; 
        it ⊆ α m; 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f k σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      assumes II: "!!σ it. ⟦ 
        it ⊆ α m; 
        it ≠ {}; 
        ¬ c σ; 
        I it σ; 
        ∀k∈it. ∀j∈α m - it. j≤k 
      ⟧ ⟹ P σ"
      shows "P (iterateoi m c f σ0)"  
    using set_iterator_linord_rule_P [OF iterateoi_rule, OF MINV, of I σ0 c f P,
       OF I0 _ IF] IP II
    by simp

    lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]: 
      assumes MINV: "invar m"
      assumes I0: "I ((α m)) σ0"
      assumes IP: "!!k it σ. ⟦ k ∈ it; ∀j∈it. k≤j; ∀j∈(α m) - it. j≤k; it ⊆ (α m); I it σ ⟧ 
                  ⟹ I (it - {k}) (f k σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
    shows "P (iterateoi m (λ_. True) f σ0)"
      apply (rule iterateoi_rule_P [where I = I])
      apply (simp_all add: assms)
    done
  end

  lemma set_iterateoi_I :
  assumes "⋀s. invar s ⟹ set_iterator_linord (itoi s) (α s)"
  shows "set_iterateoi α invar itoi"
  proof
    fix s
    assume invar_s: "invar s"
    from assms(1)[OF invar_s] show it_OK: "set_iterator_linord (itoi s) (α s)" .
  
    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_linord_def]]
    show "finite (α s)" by simp 
  qed

  (* Deprecated *)
  locale set_reverse_iterateoi = ordered_finite_set α invar 
    for α :: "'s ⇒ ('u::linorder) set" and invar
    +
    fixes reverse_iterateoi :: "'s ⇒ ('u,'σ) set_iterator"
    assumes reverse_iterateoi_rule: "
      invar m ⟹ set_iterator_rev_linord (reverse_iterateoi m) (α m)" 
  begin
    lemma reverse_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I ((α m)) σ0"
      assumes IP: "!!k it σ. ⟦ 
        c σ; 
        k ∈ it; 
        ∀j∈it. k≥j; 
        ∀j∈(α m) - it. j≥k; 
        it ⊆ (α m); 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f k σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      assumes II: "!!σ it. ⟦ 
        it ⊆ (α m); 
        it ≠ {}; 
        ¬ c σ; 
        I it σ; 
        ∀k∈it. ∀j∈(α m) - it. j≥k 
      ⟧ ⟹ P σ"
    shows "P (reverse_iterateoi m c f σ0)"
    using set_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, OF MINV, of I σ0 c f P,
       OF I0 _ IF] IP II
    by simp

    lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
      assumes MINV: "invar m"
      assumes I0: "I ((α m)) σ0"
      assumes IP: "!!k it σ. ⟦ 
        k ∈ it; 
        ∀j∈it. k≥j; 
        ∀j∈ (α m) - it. j≥k; 
        it ⊆ (α m); 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f k σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
    shows "P (reverse_iterateoi m (λ_. True) f σ0)"
      apply (rule reverse_iterateoi_rule_P [where I = I])
      apply (simp_all add: assms)
    done
  end

  lemma set_reverse_iterateoi_I :
  assumes "⋀s. invar s ⟹ set_iterator_rev_linord (itoi s) (α s)"
  shows "set_reverse_iterateoi α invar itoi"
  proof
    fix s
    assume invar_s: "invar s"
    from assms(1)[OF invar_s] show it_OK: "set_iterator_rev_linord (itoi s) (α s)" .
  
    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_rev_linord_def]]
    show "finite (α s)" by simp 
  qed


  lemma (in poly_set_iteratei) v1_iteratei_impl: 
    "set_iteratei α invar iteratei"
    by unfold_locales (rule iteratei_correct)
  lemma (in poly_set_iterateoi) v1_iterateoi_impl: 
    "set_iterateoi α invar iterateoi"
    by unfold_locales (rule iterateoi_correct)
  lemma (in poly_set_rev_iterateoi) v1_reverse_iterateoi_impl: 
    "set_reverse_iterateoi α invar rev_iterateoi"
    by unfold_locales (rule rev_iterateoi_correct)

  declare (in poly_set_iteratei) v1_iteratei_impl[locale_witness_add]
  declare (in poly_set_iterateoi) v1_iterateoi_impl[locale_witness_add]
  declare (in poly_set_rev_iterateoi) 
    v1_reverse_iterateoi_impl[locale_witness_add]

  (* Commented out, as it causes strange errors of the kind:
    Type variable "?'a" has two distinct sorts

  sublocale poly_set_iteratei < v1_iteratei: set_iteratei α invar iteratei
    by (rule v1_iteratei_impl)
  sublocale poly_set_iterateoi < v1_iteratei: set_iterateoi α invar iterateoi
    by (rule v1_iterateoi_impl)
  sublocale poly_set_rev_iterateoi 
    < v1_iteratei!: set_reverse_iterateoi α invar rev_iterateoi
    by (rule v1_reverse_iterateoi_impl)
    *)

subsubsection "Map"
locale map_iteratei = finite_map α invar for α :: "'s ⇒ 'u ⇀ 'v" and invar +
  fixes iteratei :: "'s ⇒ ('u × 'v,'σ) set_iterator"

  assumes iteratei_rule: "invar m ⟹ map_iterator (iteratei m) (α m)"
begin

  lemma iteratei_rule_P:
    assumes "invar m"
        and I0: "I (dom (α m)) σ0"
        and IP: "!!k v it σ. ⟦ c σ; k ∈ it; α m k = Some v; it ⊆ dom (α m); I it σ ⟧ 
                    ⟹ I (it - {k}) (f (k, v) σ)"
        and IF: "!!σ. I {} σ ⟹ P σ"
        and II: "!!σ it. ⟦ it ⊆ dom (α m); it ≠ {}; ¬ c σ; I it σ ⟧ ⟹ P σ"
    shows "P (iteratei m c f σ0)"
    using map_iterator_rule_P [OF iteratei_rule, of m I σ0 c f P]
    by (simp_all add: assms)

  lemma iteratei_rule_insert_P:
    assumes  
      "invar m" 
      "I {} σ0"
      "!!k v it σ. ⟦ c σ; k ∈ (dom (α m) - it); α m k = Some v; it ⊆ dom (α m); I it σ ⟧ 
          ⟹ I (insert k it) (f (k, v) σ)"
      "!!σ. I (dom (α m)) σ ⟹ P σ"
      "!!σ it. ⟦ it ⊆ dom (α m); it ≠ dom (α m); 
               ¬ (c σ); 
               I it σ ⟧ ⟹ P σ"
    shows "P (iteratei m c f σ0)"
    using map_iterator_rule_insert_P [OF iteratei_rule, of m I σ0 c f P]
    by (simp_all add: assms)

  lemma iterate_rule_P:
    "⟦
      invar m;
      I (dom (α m)) σ0;
      !!k v it σ. ⟦ k ∈ it; α m k = Some v; it ⊆ dom (α m); I it σ ⟧ 
                  ⟹ I (it - {k}) (f (k, v) σ);
      !!σ. I {} σ ⟹ P σ
    ⟧ ⟹ P (iteratei m (λ_. True) f σ0)"
    using iteratei_rule_P [of m I σ0 "λ_. True" f P]
    by fast

  lemma iterate_rule_insert_P:
    "⟦
      invar m;
      I {} σ0;
      !!k v it σ. ⟦ k ∈ (dom (α m) - it); α m k = Some v; it ⊆ dom (α m); I it σ ⟧ 
                  ⟹ I (insert k it) (f (k, v) σ);
      !!σ. I (dom (α m)) σ ⟹ P σ
    ⟧ ⟹ P (iteratei m (λ_. True) f σ0)"
    using iteratei_rule_insert_P [of m I σ0 "λ_. True" f P]
    by fast
end

lemma map_iteratei_I :
  assumes "⋀m. invar m ⟹ map_iterator (iti m) (α m)"
  shows "map_iteratei α invar iti"
proof
  fix m 
  assume invar_m: "invar m"
  from assms(1)[OF invar_m] show it_OK: "map_iterator (iti m) (α m)" .
  
  from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
  show "finite (dom (α m))" by (simp add: finite_map_to_set) 
qed


  locale map_iterateoi = ordered_finite_map α invar
    for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar
    +
    fixes iterateoi :: "'s ⇒ ('u × 'v,'σ) set_iterator"
    assumes iterateoi_rule: "
      invar m ⟹ map_iterator_linord (iterateoi m) (α m)"
  begin
    lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (dom (α m)) σ0"
      assumes IP: "!!k v it σ. ⟦ 
        c σ; 
        k ∈ it; 
        ∀j∈it. k≤j; 
        ∀j∈dom (α m) - it. j≤k; 
        α m k = Some v; 
        it ⊆ dom (α m); 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      assumes II: "!!σ it. ⟦ 
        it ⊆ dom (α m); 
        it ≠ {}; 
        ¬ c σ; 
        I it σ; 
        ∀k∈it. ∀j∈dom (α m) - it. j≤k 
      ⟧ ⟹ P σ"
      shows "P (iterateoi m c f σ0)"
    using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 c f P] assms
    by simp

    lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]: 
      assumes MINV: "invar m"
      assumes I0: "I (dom (α m)) σ0"
      assumes IP: "!!k v it σ. ⟦ k ∈ it; ∀j∈it. k≤j; ∀j∈dom (α m) - it. j≤k; α m k = Some v; it ⊆ dom (α m); I it σ ⟧ 
                  ⟹ I (it - {k}) (f (k, v) σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      shows "P (iterateoi m (λ_. True) f σ0)"
    using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 "λ_. True" f P] assms
    by simp
  end

  lemma map_iterateoi_I :
  assumes "⋀m. invar m ⟹ map_iterator_linord (itoi m) (α m)"
  shows "map_iterateoi α invar itoi"
  proof
    fix m 
    assume invar_m: "invar m"
    from assms(1)[OF invar_m] show it_OK: "map_iterator_linord (itoi m) (α m)" .
  
    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_linord_def]]
    show "finite (dom (α m))" by (simp add: finite_map_to_set) 
  qed

  locale map_reverse_iterateoi = ordered_finite_map α invar 
    for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar
    +
    fixes reverse_iterateoi :: "'s ⇒ ('u × 'v,'σ) set_iterator"
    assumes reverse_iterateoi_rule: "
      invar m ⟹ map_iterator_rev_linord (reverse_iterateoi m) (α m)"
  begin
    lemma reverse_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (dom (α m)) σ0"
      assumes IP: "!!k v it σ. ⟦ 
        c σ; 
        k ∈ it; 
        ∀j∈it. k≥j; 
        ∀j∈dom (α m) - it. j≥k; 
        α m k = Some v; 
        it ⊆ dom (α m); 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      assumes II: "!!σ it. ⟦ 
        it ⊆ dom (α m); 
        it ≠ {}; 
        ¬ c σ; 
        I it σ; 
        ∀k∈it. ∀j∈dom (α m) - it. j≥k 
      ⟧ ⟹ P σ"
      shows "P (reverse_iterateoi m c f σ0)"
    using map_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, of m I σ0 c f P] assms
    by simp

    lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
      assumes MINV: "invar m"
      assumes I0: "I (dom (α m)) σ0"
      assumes IP: "!!k v it σ. ⟦ 
        k ∈ it; 
        ∀j∈it. k≥j; 
        ∀j∈dom (α m) - it. j≥k; 
        α m k = Some v; 
        it ⊆ dom (α m); 
        I it σ 
      ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
      assumes IF: "!!σ. I {} σ ⟹ P σ"
      shows "P (reverse_iterateoi m (λ_. True) f σ0)"
    using map_iterator_rev_linord_rule_P[OF reverse_iterateoi_rule, of m I σ0 "λ_. True" f P] assms
    by simp
  end

  lemma map_reverse_iterateoi_I :
  assumes "⋀m. invar m ⟹ map_iterator_rev_linord (ritoi m) (α m)"
  shows "map_reverse_iterateoi α invar ritoi"
  proof
    fix m 
    assume invar_m: "invar m"
    from assms(1)[OF invar_m] show it_OK: "map_iterator_rev_linord (ritoi m) (α m)" .
  
    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_rev_linord_def]]
    show "finite (dom (α m))" by (simp add: finite_map_to_set) 
  qed


  lemma (in poly_map_iteratei) v1_iteratei_impl: 
    "map_iteratei α invar iteratei"
    by unfold_locales (rule iteratei_correct)
  lemma (in poly_map_iterateoi) v1_iterateoi_impl: 
    "map_iterateoi α invar iterateoi"
    by unfold_locales (rule iterateoi_correct)
  lemma (in poly_map_rev_iterateoi) v1_reverse_iterateoi_impl: 
    "map_reverse_iterateoi α invar rev_iterateoi"
    by unfold_locales (rule rev_iterateoi_correct)


  declare (in poly_map_iteratei) v1_iteratei_impl[locale_witness_add]
  declare (in poly_map_iterateoi) v1_iterateoi_impl[locale_witness_add]
  declare (in poly_map_rev_iterateoi) 
    v1_reverse_iterateoi_impl[locale_witness_add]

  (*
  sublocale poly_map_iteratei < v1_iteratei: map_iteratei α invar iteratei
    by (rule v1_iteratei_impl)
  sublocale poly_map_iterateoi < v1_iteratei: map_iterateoi α invar iterateoi
    by (rule v1_iterateoi_impl)
  sublocale poly_map_rev_iterateoi 
    < v1_iteratei!: map_reverse_iterateoi α invar rev_iterateoi
    by (rule v1_reverse_iterateoi_impl)
    *)

  subsection ‹Concrete Operation Names›
  text ‹We define abbreviations to recover the ‹xx_op›-names›

  (* TODO: This may take long, as Local_Theory.abbrev seems to be really slow *)
  local_setup ‹let
    val thy = @{theory}
    val ctxt = Proof_Context.init_global thy;
    val pats = [
    "hs","hm",
    "rs","rm",
    "ls","lm","lsi","lmi","lsnd","lss",
    "ts","tm",
    "ias","iam",
    "ahs","ahm",
    "bino",
    "fifo",
    "ft",
    "alprioi",
    "aluprioi",
    "skew"
    ];

    val {const_space, constants, ...} = Sign.consts_of thy |> Consts.dest
    val clist = Name_Space.extern_entries true ctxt const_space constants |> map (apfst #1)

    fun abbrevs_for pat = clist
    |> map_filter (fn (n,_) => case Long_Name.explode n of
        [_,prefix,opname] =>
          if prefix = pat then let 
              val aname = prefix ^ "_" ^ opname
              val rhs = Proof_Context.read_term_abbrev ctxt n
            in SOME (aname,rhs) end
          else NONE
      | _ => NONE);

    fun do_abbrevs pat lthy = let
      val abbrevs = abbrevs_for pat;
    in 
      case abbrevs of [] => (warning ("No stuff found for "^pat); lthy)
      | _ => let 
        (*val _ = tracing ("Defining " ^ pat ^ "_xxx ...");*)
        val lthy = fold (fn (name,rhs) =>
          Local_Theory.abbrev 
            Syntax.mode_input 
            ((Binding.name name,NoSyn),rhs) #> #2
        ) abbrevs lthy
        (*val _ = tracing "Done";*)
      in lthy end
    end
  in
    fold do_abbrevs pats
  end

›


lemmas hs_correct = hs.correct
lemmas hm_correct = hm.correct
lemmas rs_correct = rs.correct
lemmas rm_correct = rm.correct
lemmas ls_correct = ls.correct
lemmas lm_correct = lm.correct
lemmas lsi_correct = lsi.correct
lemmas lmi_correct = lmi.correct
lemmas lsnd_correct = lsnd.correct
lemmas lss_correct = lss.correct
lemmas ts_correct = ts.correct
lemmas tm_correct = tm.correct
lemmas ias_correct = ias.correct
lemmas iam_correct = iam.correct
lemmas ahs_correct = ahs.correct
lemmas ahm_correct = ahm.correct
lemmas bino_correct = bino.correct
lemmas fifo_correct = fifo.correct
lemmas ft_correct = ft.correct
lemmas alprioi_correct = alprioi.correct
lemmas aluprioi_correct = aluprioi.correct
lemmas skew_correct = skew.correct


locale list_enqueue = list_appendr
locale list_dequeue = list_removel

locale list_push = list_appendl
locale list_pop = list_remover
locale list_top = list_leftmost
locale list_bot = list_rightmost

instantiation rbt :: ("{equal,linorder}",equal) equal 
begin
  (*definition equal_rbt :: "('a,'b) RBT.rbt ⇒ _" where "equal_rbt ≡ (=)"*)

  definition "equal_class.equal (r :: ('a, 'b) rbt) r' 
    == RBT.impl_of r = RBT.impl_of r'"


  instance
    apply intro_classes
    apply (simp add: equal_rbt_def RBT.impl_of_inject)
    done
end

end