# Theory Redex

Up to index of Isabelle/ZF/Resid

theory Redex
imports Main
begin

    (*  Title:      ZF/Resid/Redex.thy
        ID:         $Id: Redex.thy,v 1.16 2005/06/17 14:15:11 haftmann Exp $
        Author:     Ole Rasmussen
        Copyright   1995  University of Cambridge
        Logic Image: ZF
    *)

    theory Redex imports Main 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"
      union_aux        :: "i=>i"
      regular          :: "i=>o"

    (*syntax??*)
      un               :: "[i,i]=>i"  (infixl 70)
      "<=="            :: "[i,i]=>o"  (infixl 70)
      "~"              :: "[i,i]=>o"  (infixl 70)

    translations
      "a<==b"        == "<a,b> ∈ Ssub"
      "a ~ b"        == "<a,b> ∈ Scomp"
      "regular(a)"   == "a ∈ Sreg"

    primrec (*explicit lambda is required because both arguments of "un" 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))"

    defs
      union_def:  "u un v == union_aux(u)`v"

    syntax (xsymbols)
      "op un"             :: "[i,i]=>i"  (infixl "\<squnion>" 70)
      "op <=="            :: "[i,i]=>o"  (infixl "\<Longleftarrow>" 70)
      "op ~"              :: "[i,i]=>o"  (infixl "∼" 70)

    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) un Var(n)=Var(n)"
    by (simp add: union_def)

    lemma union_Fun [simp]: "v ∈ redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
    by (simp add: union_def)

    lemma union_App [simp]:
         "[|b2 ∈ bool; u2 ∈ redexes; v2 ∈ redexes|]
          ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un 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 un v)"
    apply (erule Scomp.induct)
    apply (erule_tac [3] boolE, simp_all)
    done

    lemma union_r: "u ~ v ==> v <== (u un v)"
    apply (erule Scomp.induct)
    apply (erule_tac [3] c = b2 in boolE, simp_all)
    done

    lemma union_sym: "u ~ v ==> u un v = v un 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 un v)"
      by (erule Scomp.induct, auto)

    end

lemmas compD1:

      a ~ b ==> a ∈ redexes

lemmas compD1:

      a ~ b ==> a ∈ redexes

lemmas compD2:

      a ~ b ==> b ∈ redexes

lemmas compD2:

      a ~ b ==> b ∈ redexes

lemmas regD:

      regular(c) ==> c ∈ redexes

lemmas regD:

      regular(c) ==> c ∈ redexes

lemma union_Var:

      n ∈ nat ==> Var(n) un Var(n) = Var(n)

lemma union_Fun:

      v ∈ redexes ==> Fun(u) un Fun(v) = Fun(u un v)

lemma union_App:

      [| b2.0 ∈ bool; u2.0 ∈ redexes; v2.0 ∈ redexes |]
      ==> App(b1.0, u1.0, v1.0) un App(b2.0, u2.0, v2.0) =
          App(b1.0 or b2.0, u1.0 un u2.0, v1.0 un v2.0)

lemma or_1_right:

      a or 1 = 1

lemma or_0_right:

      a ∈ bool ==> a or 0 = a

lemmas

      [| regular(App(b, f, a));
         !!u. [| regular(Fun(u)); regular(a); b = 1; f = Fun(u) |] ==> Q;
         [| regular(f); regular(a); b = 0 |] ==> Q |]
      ==> Q

      [| regular(Fun(b)); regular(b) ==> Q |] ==> Q

      [| regular(Var(b)); b ∈ nat ==> Q |] ==> Q

      [| Fun(u) ~ Fun(t); u ~ t ==> Q |] ==> Q

      [| u ~ Fun(t); !!u. [| u ~ t; u = Fun(u) |] ==> Q |] ==> Q

      [| u ~ Var(n); [| n ∈ nat; u = Var(n) |] ==> Q |] ==> Q

      [| u ~ App(b, t, a);
         !!b1 u1 u2.
            [| u1 ~ t; u2 ~ a; b1 ∈ bool; b ∈ bool; u = App(b1, u1, u2) |] ==> Q |]
      ==> Q

      [| Fun(t) ~ v; !!v. [| t ~ v; v = Fun(v) |] ==> Q |] ==> Q

      [| App(b, f, a) ~ v;
         !!b2 v1 v2.
            [| f ~ v1; a ~ v2; b ∈ bool; b2 ∈ bool; v = App(b2, v1, v2) |] ==> Q |]
      ==> Q

      [| Var(n) ~ u; [| n ∈ nat; u = Var(n) |] ==> Q |] ==> Q

lemma comp_refl:

      u ∈ redexes ==> u ~ u

lemma comp_sym:

      u ~ v ==> v ~ u

lemma comp_sym_iff:

      u ~ v <-> v ~ u

lemma comp_trans:

      [| u ~ v; v ~ w |] ==> u ~ w

lemma union_l:

      u ~ v ==> u <== (u un v)

lemma union_r:

      u ~ v ==> v <== (u un v)

lemma union_sym:

      u ~ v ==> u un v = v un u

lemma union_preserve_regular:

      [| u ~ v; regular(u); regular(v) |] ==> regular(u un v)