val state_obeys_st_laws (uses:inames)
  : Lemma (S.st_laws (state0 uses))
let state_obeys_st_laws uses =
  Classical.forall_intro_3 star_associative;
  Classical.forall_intro_2 star_commutative;
  is_unit ();
  FStar.Classical.forall_intro_3 disjoint_join;
  let aux (m0 m1:mem)
    : Lemma (requires disjoint m0 m1)
            (ensures join m0 m1 == join m1 m0)
            [SMTPat (disjoint m0 m1)]
    = join_commutative m0 m1
  in
  let aux (m0 m1 m2:mem)
    : Lemma
      (requires
        disjoint m1 m2 /\
        disjoint m0 (join m1 m2))
      (ensures
        (disjoint_join m0 m1 m2;
        join m0 (join m1 m2) == join (join m0 m1) m2))
      [SMTPat (disjoint m0 (join m1 m2))]
    = join_associative m0 m1 m2
  in
  let aux (p1 p2 p3:slprop)
    : Lemma (p1 `equiv` p2 ==> (p1 `star` p3) `equiv` (p2 `star` p3))
      [SMTPat ()]
    = equiv_extensional_on_star  p1 p2 p3
  in
  ()
val state_obeys_st_laws (uses:inames)
  : Lemma (S.st_laws (state0 uses))
let state_obeys_st_laws uses =
Classical.forall_intro_3 star_associative;
Classical.forall_intro_2 star_commutative;
is_unit ();
FStar.Classical.forall_intro_3 disjoint_join;
let aux (m0 m1: mem)
    : Lemma (requires disjoint m0 m1) (ensures join m0 m1 == join m1 m0) [SMTPat (disjoint m0 m1)] =
  join_commutative m0 m1
in
let aux (m0 m1 m2: mem)
    : Lemma (requires disjoint m1 m2 /\ disjoint m0 (join m1 m2))
      (ensures
        (disjoint_join m0 m1 m2;
          join m0 (join m1 m2) == join (join m0 m1) m2))
      [SMTPat (disjoint m0 (join m1 m2))] =
  join_associative m0 m1 m2
in
let aux (p1 p2 p3: slprop)
    : Lemma (p1 `equiv` p2 ==> (p1 `star` p3) `equiv` (p2 `star` p3)) [SMTPat ()] =
  equiv_extensional_on_star p1 p2 p3
in
()
Steel.Semantics.Instantiate.fst.checked
Steel.Semantics.Hoare.MST.fst.checked Steel.Memory.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Steel.Semantics.Instantiate.fst
Steel.Memory.inames Steel.Memory.slprop Prims.unit Prims.l_True Prims.squash Prims.l_imp Steel.Memory.equiv Steel.Memory.star Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil Steel.Memory.equiv_extensional_on_star Steel.Memory.mem Prims.l_and Steel.Memory.disjoint Steel.Memory.join Prims.eq2 Prims.prop Steel.Memory.join_associative Steel.Memory.disjoint_join Steel.Memory.join_commutative FStar.Classical.forall_intro_3 Steel.Semantics.Instantiate.is_unit FStar.Classical.forall_intro_2 Steel.Memory.star_commutative Steel.Memory.star_associative
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Steel.Semantics.Instantiate
open Steel.Memory
module S = Steel.Semantics.Hoare.MST

let is_unit ()
  : Lemma (S.is_unit emp equiv star)
  = let aux (y:slprop)
      : Lemma (star emp y `equiv` y /\ star y emp `equiv` y)
      = emp_unit y; star_commutative emp y
    in
    Classical.forall_intro aux

#push-options "--warn_error -271"
val state_obeys_st_laws (uses:inames)
  : Lemma (S.st_laws (state0 uses))
uses: Steel.Memory.inames
  -> FStar.Pervasives.Lemma
    (ensures Steel.Semantics.Hoare.MST.st_laws (Steel.Semantics.Instantiate.state0 uses))