Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Redex.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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 \<open>\<Longleftarrow>\<close> 70) where
  "a \ b == \ Ssub"

abbreviation
  Scomp_rel  (infixl \<open>\<sim>\<close> 70) where
  "a \ b == \ Scomp"

abbreviation
  "regular(a) == a \ Sreg"

consts union_aux        :: "i=>i"
primrec (*explicit lambda is required because both arguments of "\<squnion>" vary*)
  "union_aux(Var(n)) =
     (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"

  "union_aux(Fun(u)) =
     (\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
                                  %b y z. 0, t))"

  "union_aux(App(b,f,a)) =
     (\<lambda>t \<in> 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 \<open>\<squnion>\<close> 70) where
  "u \ v == union_aux(u)`v"

inductive
  domains       "Ssub" \<subseteq> "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) \<Longleftarrow> 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" \<subseteq> "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) \<sim> App(b2,v1,v2)"
  type_intros    redexes.intros bool_typechecks

inductive
  domains       "Sreg" \<subseteq> 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) \<squnion> App(b2,u2,v2)=App(b1 or b2,u1 \<squnion> u2,v1 \<squnion> 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

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.