Theory RefAssume

Up to index of Isabelle/HOL/Marvin2002

RefAssume = RefCmd +

consts
  refeq_assume :: "[Env,pred,Cmd,Cmd] => bool" ("env _ ass _ ||- _ [=] _")
  refsto_assume :: "[Env,pred,Cmd,Cmd] => bool" ("env _ ass _ ||- _ [= _")
defs
  refeq_assume_def
  "env p ass a ||- c1 [=] c2 ==
   assert(a) sand c1 [=](p) assert(a) sand c2" 
  refsto_assume_def
  "env p ass a ||- c1 [= c2 == 
   assert(a) sand c1 [=(p) assert(a) sand c2"
rules
    exists_cmono "env p ass A ||- c1 [= c2 ==> env p ass A ||- exists v c1 [= exists v c2"
  forall_cmono "env p ass A ||- c1 [= c2 ==> env p ass A ||- Cmd.all v c1 [= Cmd.all v c2"
  exists_one_point_pair
  "env p ass A ||- C U W [= (exists X (exists Y (spec((funT ''pair'' [varT U, varT W]) == (funT ''pair'' [varT X, varT Y])) sand C X Y)))"
  forall_assumpt_refine
  "[| env p ass B ||- T [= C(V); entails B (pall y (refsto_point (C(varT y)) p (S(varT y)))) |] ==> env p ass B ||- T [= S(V)"
end
  

PRELIMINARY DEFINITIONS

theorem refsto_point_property:

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

Refinement relation properties

theorem crefeq_trans:

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

theorem crefsto_trans:

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

theorem crefsto_reflex:

  env p ass A ||- c [= c

theorem crefeq_reflex:

  env p ass A ||- c [=] c

theorem crefeq_symm:

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

theorem crefeqD1:

  env p ass A ||- c1 [=] c2 ==> env p ass A ||- c1 [= c2

theorem crefeqD2:

  env p ass A ||- c1 [=] c2 ==> env p ass A ||- c2 [= c1

MONOTONICITY RULES

theorem pand_left_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c1 pand c3 [= c2 pand c3

theorem pand_right_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c3 pand c1 [= c3 pand c2

theorem por_right_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c3 por c1 [= c3 por c2

theorem por_left_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c1 por c3 [= c2 por c3

theorem pand_cmono:

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

theorem sand_right_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c3 sand c1 [= c3 sand c2

theorem sand_left_cmono:

  env p ass A ||- c1 [= c2 ==> env p ass A ||- c1 sand c3 [= c2 sand c3

ASSUMPTION RULES

theorem assume_in_context:

  env p ass A && B ||- S [= T
  ==> env p ass A ||- assert B sand S [= assert B sand T

theorem weaken_assumpt:

  entails A (B => C) ==> env p ass A ||- assert B [= assert C

theorem introduce_assumpt:

  entails A B ==> env p ass A ||- c [= assert B sand c

theorem spec_in_cont:

  env p ass B && A ||- c1 [= c2
  ==> env p ass B ||- spec A sand c1 [= spec A sand c2

theorem refsto_to_crefsto:

  env p ||- S [= T ==> env p ass ptrue ||- S [= T

theorem crefsto_to_refsto:

  env p ass ptrue ||- S [= T ==> env p ||- S [= T

theorem crefsto_antisymm:

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

theorem crefeq_simp:

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

theorem refeq_point_property:

  env p ass A ||- c1 [=] c2 = (ALL b. evalp A b --> exec p c1 {b} = exec p c2 {b})

theorem equiv_spec:

  entails A (P <=> Q) ==> env p ass A ||- spec P [=] spec Q

theorem introduce_spec:

  entails A B ==> env p ass A ||- c [=] spec B pand c

theorem assume_context_intro:

  env p ||- c1 [= c2 ==> env p ass A ||- c1 [= c2

theorem spec_in_cont2:

  env p ass A ||- c1 [= c2 ==> env p ||- spec A sand c1 [= spec A sand c2

theorem assume_in_context2:

  env p ass A ||- c1 [= c2 ==> env p ||- assert A sand c1 [= assert A sand c2