Theory RefCmd

Up to index of Isabelle/HOL/Marvin99-1

theory RefCmd = Execs + Recurse
files [RefCmd.ML]:

RefCmd = Execs + Recurse +

consts
  refeq_cmd :: "[Cmd, Env, Cmd] => bool"  ("_ [=]'(_') _")
  refsto_cmd :: "[Cmd, Env, Cmd] => bool"  ("_ [='(_') _")
  refeq_pcmd :: "[PCmd, Env, PCmd] => bool"  ("_ prefeq'(_') _")
  refsto_pcmd :: "[PCmd, Env, PCmd] => bool"  ("_ prefsto'(_') _")
  pcmd_apply  :: "[PCmd, rterm] => Cmd" ("_ ^@ _")
defs
  refeq_cmd_def "c1 [=](p) c2 == (exec p c1) refeq (exec p c2)"
  refsto_cmd_def "c1 [=(p) c2 == (exec p c1) refsto (exec p c2)"
  refeq_pcmd_def "c1 prefeq(p) c2 == (pexec p c1) refeq (pexec p c2)"
  refsto_pcmd_def "c1 prefsto(p) c2 == (pexec p c1) refsto (pexec p c2)"
rules
  exists_mono "[| S [=(p) T |] ==> (exists v S) [=(p) (exists v T)"
  pand_to_sand "S pand T [=(p) S sand T"
  refsto_implies_prefsto 
  "S [=(p) T ==> (v :- S) prefsto(p) (v :- T)"
  recblock_mono "S prefsto(p) T ==> re pid . S er prefsto(p) re pid . T er"
  exist_one_point "exists U (spec(X == varT U) sand S) [=](p) substC S U X"
  expand_scope_exists "(exists X S) pand T [=](p) (exists X (S pand T))"
syntax
  "@refstoenv" :: "[Env,Cmd,Cmd] \<Rightarrow> bool" ("env _ ||- _ [= _")
  "@refeqenv" :: "[Env,Cmd,Cmd] \<Rightarrow> bool" ("env _ ||- _ [=] _")
translations
  "env p ||- c1 [= c2" == "c1 [=(p) c2"
  "env p ||- c1 [=] c2" == "c1 [=](p) c2"
end

PRELIMINARY DEFINITIONS

theorem refines_pointwise:

  env p ||- c1 [= c2 =
  (ALL b. {b} : dom (exec p c1) -->
          {b} : dom (exec p c2) & exec p c1 {b} = exec p c2 {b})

PARAMETERISED REFINEMENT RELATIONS PROPERTIES

theorem prefeqD1:

  S prefeq(p) T ==> S prefsto(p) T

theorem prefsto_trans:

  [| S prefsto(p) T; T prefsto(p) U |] ==> S prefsto(p) U

theorem prefeq_trans:

  [| S prefeq(p) T; T prefeq(p) U |] ==> S prefeq(p) U

theorem prefsto_refl:

  S prefsto(p) S

theorem prefeq_refl:

  S prefeq(p) S

theorem prefeq_symm:

  S prefeq(p) T ==> T prefeq(p) S

REFINEMENT RELATION PROPERTIES

theorem refeq_trans:

  [| env p ||- S [=] T; env p ||- T [=] U |] ==> env p ||- S [=] U

theorem refeq_symm:

  env p ||- S [=] T ==> env p ||- T [=] S

theorem refeq_refl:

  env p ||- S [=] S

theorem refsto_trans:

  [| env p ||- S [= T; env p ||- T [= U |] ==> env p ||- S [= U

theorem refsto_refl:

  env p ||- S [= S

theorem refsto_antisymm:

  [| env p ||- c1 [= c2; env p ||- c2 [= c1 |] ==> env p ||- c1 [=] c2

theorem refeqD1:

  env p ||- S [=] T ==> env p ||- S [= T

theorem refeqD2:

  env p ||- S [=] T ==> env p ||- T [= S

theorem refeq_simp:

  (env p ||- c1 [= c2 & env p ||- c2 [= c1) = env p ||- c1 [=] c2

ALGEBRA RULES

theorem fail_sand:

  env p ||- fail sand S [=] fail

theorem abort_sand:

  env p ||- abort sand S [=] abort

theorem skip_sand:

  env p ||- spec ptrue sand S [=] S

theorem pand_commute:

  env p ||- S pand T [=] T pand S

theorem por_commute:

  env p ||- S por T [=] T por S

theorem pand_assoc:

  env p ||- S pand T pand U [=] (S pand T) pand U

theorem por_assoc:

  env p ||- S por T por U [=] (S por T) por U

theorem distribute_pand_over_por:

  env p ||- S pand T por U [=] (S pand T) por S pand U

theorem distribute_por_over_pand:

  env p ||- S por T pand U [=] (S por T) pand S por U

theorem left_distrib_sand_over_por:

  env p ||- S sand T por U [=] (S sand T) por S sand U

theorem left_distrib_sand_over_pand:

  env p ||- S sand T pand U [=] (S sand T) pand S sand U

theorem right_distribute_pand_over_por:

  env p ||- (S por T) pand U [=] (S pand U) por T pand U

theorem sand_assoc:

  env p ||- (S sand T) sand U [=] S sand T sand U

MONOTONICITY RULES

theorem pand_mono:

  [| env p ||- c1 [= c2; env p ||- c3 [= c4 |]
  ==> env p ||- c1 pand c3 [= c2 pand c4

theorem por_mono:

  [| env p ||- c1 [= c2; env p ||- c3 [= c4 |]
  ==> env p ||- c1 por c3 [= c2 por c4

theorem sand_mono:

  [| env p ||- c1 [= c2; env p ||- c3 [= c4 |]
  ==> env p ||- c1 sand c3 [= c2 sand c4

theorem pand_left_mono:

  env p ||- S [= T ==> env p ||- S pand U [= T pand U

theorem pand_right_mono:

  env p ||- S [= T ==> env p ||- U pand S [= U pand T

theorem por_left_mono:

  env p ||- S [= T ==> env p ||- S por U [= T por U

theorem por_right_mono:

  env p ||- S [= T ==> env p ||- U por S [= U por T

theorem sand_left_mono:

  env p ||- S [= T ==> env p ||- S sand U [= T sand U

theorem sand_right_mono:

  env p ||- S [= T ==> env p ||- U sand S [= U sand T

theorem sand_refeq_mono:

  [| env p ||- S [=] T; env p ||- U [=] V |] ==> env p ||- S sand U [=] T sand V

theorem pand_refeq_mono:

  [| env p ||- S [=] T; env p ||- U [=] V |] ==> env p ||- S pand U [=] T pand V

theorem por_refeq_mono:

  [| env p ||- S [=] T; env p ||- U [=] V |] ==> env p ||- S por U [=] T por V

theorem exists_refeq_mono:

  env p ||- S [=] T ==> env p ||- exists V S [=] exists V T

PREDICATE LIFTING RULES

theorem lift_pand:

  env p ||- spec P pand spec Q [=] spec (P && Q)

theorem lift_por:

  env p ||- spec P por spec Q [=] spec (P || Q)

theorem lift_exists:

  env p ||- exists v (spec P) [=] spec (PEX v. P)

theorem lift_forall:

  env p ||- Cmd.all v (spec P) [=] spec (pall v P)

ASSUMPTION RULES

theorem combine_assert:

  env p ||- assert A sand assert B [=] assert (A && B)

theorem remove_assert:

  env p ||- assert A sand S [= S

theorem weaken_assert:

  |[P => Q]| ==> env p ||- assert P [= assert Q

theorem establish_assert:

  env p ||- spec P [=] spec P sand assert P

theorem introduce_assert:

  |[A]| ==> env p ||- S [=] assert A sand S

theorem equivalent_under_assert:

  |[A => P <=> Q]| ==> env p ||- assert A sand spec P [=] assert A sand spec Q

theorem assert_after_spec:

  |[P => A]| ==> env p ||- spec P [=] spec P sand assert A

SPECIFICATION RULES

theorem equivalent_spec:

  |[P <=> Q]| ==> env p ||- spec P [=] spec Q