Cord.thy

Back to the index of PL

(*
      File: Cord.thy
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 1998.
Time-stamp: <99/08/26 12:00:25 sja4>

	Contextual ordering of expressions.

*)

Cord = Context + Howe + Diverges +

constdefs

  cord :: "(typ list * expr * expr * typ) set"
  "cord == {(env,p,q,a) . env |- p ::: a & env |- q ::: a \
		\ & (! c b. ((env, a, []) |-- c ::: b) \
			\ --> converges (c p) --> converges (c q))}"

syntax

  "@cord" :: "[typ list, expr, expr, typ] => bool"
		("((_) |- (_) /<cord> (_) /::: (_))" [50,50,50] 50)

translations

  "env |- p <cord> q ::: a" == "(env, p, q, a) : cord"


end

Theorems proved in Cord.ML:

typing_cord1

env |- s <cord> t ::: a ==> env |- s ::: a

typing_cord2

env |- s <cord> t ::: a ==> env |- t ::: a

cord_refl

env |- s ::: a ==> env |- s <cord> s ::: a

cord_trans

[| env |- s <cord> t ::: a; env |- t <cord> u ::: a |]
==> env |- s <cord> u ::: a

ctyping_opensim_lemma

[| (env1, a, env2) |-- c ::: b; env1 @ env2 |- s <opensim> t ::: a |]
==> env2 |- c s <opensim> c t ::: b

opensim_cord

env |- s <opensim> t ::: a ==> env |- s <cord> t ::: a

kleene_cord

s <kleene> t ::: a ==> env |- s <cord> t ::: a

cord_context

[| (env1, a, env2) |-- c ::: b; env1 @ env2 |- s <cord> t ::: a |]
==> env2 |- c s <cord> c t ::: b

cord_sim

[] |- s <cord> t ::: a ==> s <sim> t ::: a

cord_subst_0

[| b # env |- s <cord> t ::: a; [] |- p ::: b |]
==> env |- s [p / 0] <cord> t [p / 0] ::: a

cord_opensim

env |- s <cord> t ::: a ==> env |- s <opensim> t ::: a

cord_eq_opensim

cord = opensim