Theory Redex

(*  Title:      ZF/Resid/Redex.thy
    Author:     Ole Rasmussen, University of Cambridge
*)

theory Redex imports ZF begin
consts
  redexes     :: i

datatype
  "redexes" = Var ("n ∈ nat")            
            | Fun ("t ∈ redexes")
            | App ("b ∈ bool","f ∈ redexes", "a ∈ redexes")


consts
  Ssub  :: "i"
  Scomp :: "i"
  Sreg  :: "i"

abbreviation
  Ssub_rel  (infixl ‹⟸› 70) where
  "a ⟸ b ≡ ⟨a,b⟩ ∈ Ssub"

abbreviation
  Scomp_rel  (infixl ‹∼› 70) where
  "a ∼ b ≡ ⟨a,b⟩ ∈ Scomp"

abbreviation
  "regular(a) ≡ a ∈ Sreg"

consts union_aux        :: "i⇒i"
primrec (*explicit lambda is required because both arguments of "⊔" vary*)
  "union_aux(Var(n)) =
     (λt ∈ redexes. redexes_case(λj. Var(n), λx. 0, λb x y.0, t))"

  "union_aux(Fun(u)) =
     (λt ∈ redexes. redexes_case(λj. 0, λy. Fun(union_aux(u)`y),
                                  λb y z. 0, t))"

  "union_aux(App(b,f,a)) =
     (λt ∈ redexes.
        redexes_case(λj. 0, λy. 0,
                     λc z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"

definition
  union  (infixl ‹⊔› 70) where
  "u ⊔ v ≡ union_aux(u)`v"


inductive
  domains       "Ssub" ⊆ "redexes*redexes"
  intros
    Sub_Var:     "n ∈ nat ⟹ Var(n) ⟸ Var(n)"
    Sub_Fun:     "⟦u ⟸ v⟧⟹ Fun(u) ⟸ Fun(v)"
    Sub_App1:    "⟦u1 ⟸ v1; u2 ⟸ v2; b ∈ bool⟧⟹   
                     App(0,u1,u2) ⟸ App(b,v1,v2)"
    Sub_App2:    "⟦u1 ⟸ v1; u2 ⟸ v2⟧⟹ App(1,u1,u2) ⟸ App(1,v1,v2)"
  type_intros    redexes.intros bool_typechecks

inductive
  domains       "Scomp" ⊆ "redexes*redexes"
  intros
    Comp_Var:    "n ∈ nat ⟹ Var(n) ∼ Var(n)"
    Comp_Fun:    "⟦u ∼ v⟧⟹ Fun(u) ∼ Fun(v)"
    Comp_App:    "⟦u1 ∼ v1; u2 ∼ v2; b1 ∈ bool; b2 ∈ bool⟧
                  ⟹ App(b1,u1,u2) ∼ App(b2,v1,v2)"
  type_intros    redexes.intros bool_typechecks

inductive
  domains       "Sreg" ⊆ redexes
  intros
    Reg_Var:     "n ∈ nat ⟹ regular(Var(n))"
    Reg_Fun:     "⟦regular(u)⟧⟹ regular(Fun(u))"
    Reg_App1:    "⟦regular(Fun(u)); regular(v)⟧⟹regular(App(1,Fun(u),v))"
    Reg_App2:    "⟦regular(u); regular(v)⟧⟹regular(App(0,u,v))"
  type_intros    redexes.intros bool_typechecks


declare redexes.intros [simp]

(* ------------------------------------------------------------------------- *)
(*    Specialisation of comp-rules                                           *)
(* ------------------------------------------------------------------------- *)

lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1]
lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2]
lemmas regD [simp] = Sreg.dom_subset [THEN subsetD]

(* ------------------------------------------------------------------------- *)
(*    Equality rules for union                                               *)
(* ------------------------------------------------------------------------- *)

lemma union_Var [simp]: "n ∈ nat ⟹ Var(n) ⊔ Var(n)=Var(n)"
by (simp add: union_def)

lemma union_Fun [simp]: "v ∈ redexes ⟹ Fun(u) ⊔ Fun(v) = Fun(u ⊔ v)"
by (simp add: union_def)
 
lemma union_App [simp]:
     "⟦b2 ∈ bool; u2 ∈ redexes; v2 ∈ redexes⟧
      ⟹ App(b1,u1,v1) ⊔ App(b2,u2,v2)=App(b1 or b2,u1 ⊔ u2,v1 ⊔ v2)"
by (simp add: union_def)


lemma or_1_right [simp]: "a or 1 = 1"
by (simp add: or_def cond_def) 

lemma or_0_right [simp]: "a ∈ bool ⟹ a or 0 = a"
by (simp add: or_def cond_def bool_def, auto) 



declare Ssub.intros [simp]
declare bool_typechecks [simp]
declare Sreg.intros [simp]
declare Scomp.intros [simp]

declare Scomp.intros [intro]

inductive_cases [elim!]:
  "regular(App(b,f,a))"
  "regular(Fun(b))"
  "regular(Var(b))"
  "Fun(u) ∼ Fun(t)"
  "u ∼ Fun(t)"
  "u ∼ Var(n)"
  "u ∼ App(b,t,a)"
  "Fun(t) ∼ v"
  "App(b,f,a) ∼ v"
  "Var(n) ∼ u"



(* ------------------------------------------------------------------------- *)
(*    comp proofs                                                            *)
(* ------------------------------------------------------------------------- *)

lemma comp_refl [simp]: "u ∈ redexes ⟹ u ∼ u"
by (erule redexes.induct, blast+)

lemma comp_sym: "u ∼ v ⟹ v ∼ u"
by (erule Scomp.induct, blast+)

lemma comp_sym_iff: "u ∼ v ⟷ v ∼ u"
by (blast intro: comp_sym)

lemma comp_trans [rule_format]: "u ∼ v ⟹ ∀w. v ∼ w⟶u ∼ w"
by (erule Scomp.induct, blast+)

(* ------------------------------------------------------------------------- *)
(*   union proofs                                                            *)
(* ------------------------------------------------------------------------- *)

lemma union_l: "u ∼ v ⟹ u ⟸ (u ⊔ v)"
apply (erule Scomp.induct)
apply (erule_tac [3] boolE, simp_all)
done

lemma union_r: "u ∼ v ⟹ v ⟸ (u ⊔ v)"
apply (erule Scomp.induct)
apply (erule_tac [3] c = b2 in boolE, simp_all)
done

lemma union_sym: "u ∼ v ⟹ u ⊔ v = v ⊔ u"
by (erule Scomp.induct, simp_all add: or_commute)

(* ------------------------------------------------------------------------- *)
(*      regular proofs                                                       *)
(* ------------------------------------------------------------------------- *)

lemma union_preserve_regular [rule_format]:
     "u ∼ v ⟹ regular(u) ⟶ regular(v) ⟶ regular(u ⊔ v)"
  by (erule Scomp.induct, auto)

end