src/ZF/Resid/Redex.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
paulson@9284
     1
(*  Title:      ZF/Resid/Redex.thy
lcp@1048
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Ole Rasmussen
lcp@1048
     4
    Copyright   1995  University of Cambridge
lcp@1048
     5
    Logic Image: ZF
lcp@1048
     6
*)
lcp@1048
     7
haftmann@16417
     8
theory Redex imports Main begin
lcp@1048
     9
consts
clasohm@1401
    10
  redexes     :: i
lcp@1048
    11
lcp@1048
    12
datatype
paulson@12593
    13
  "redexes" = Var ("n \<in> nat")            
paulson@12593
    14
            | Fun ("t \<in> redexes")
paulson@13339
    15
            | App ("b \<in> bool","f \<in> redexes", "a \<in> redexes")
lcp@1048
    16
paulson@6046
    17
lcp@1048
    18
consts
paulson@12593
    19
  Ssub  :: "i"
paulson@12593
    20
  Scomp :: "i"
paulson@12593
    21
  Sreg  :: "i"
wenzelm@22808
    22
wenzelm@22808
    23
abbreviation
wenzelm@22808
    24
  Ssub_rel  (infixl "<==" 70) where
wenzelm@22808
    25
  "a<==b == <a,b> \<in> Ssub"
paulson@12593
    26
wenzelm@22808
    27
abbreviation
wenzelm@22808
    28
  Scomp_rel  (infixl "~" 70) where
wenzelm@22808
    29
  "a ~ b == <a,b> \<in> Scomp"
paulson@12593
    30
wenzelm@22808
    31
abbreviation
wenzelm@22808
    32
  "regular(a) == a \<in> Sreg"
paulson@9284
    33
wenzelm@22808
    34
consts union_aux        :: "i=>i"
paulson@6046
    35
primrec (*explicit lambda is required because both arguments of "un" vary*)
paulson@6046
    36
  "union_aux(Var(n)) =
paulson@12593
    37
     (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
paulson@6046
    38
paulson@6046
    39
  "union_aux(Fun(u)) =
paulson@12593
    40
     (\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
paulson@6046
    41
	 			  %b y z. 0, t))"
paulson@6046
    42
paulson@6046
    43
  "union_aux(App(b,f,a)) =
paulson@12593
    44
     (\<lambda>t \<in> redexes.
paulson@6046
    45
        redexes_case(%j. 0, %y. 0,
paulson@9284
    46
		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
paulson@6046
    47
wenzelm@22808
    48
definition
wenzelm@22808
    49
  union  (infixl "un" 70) where
wenzelm@22808
    50
  "u un v == union_aux(u)`v"
paulson@6046
    51
wenzelm@22808
    52
notation (xsymbols)
wenzelm@22808
    53
  union  (infixl "\<squnion>" 70) and
wenzelm@22808
    54
  Ssub_rel  (infixl "\<Longleftarrow>" 70) and
wenzelm@22808
    55
  Scomp_rel  (infixl "\<sim>" 70)
wenzelm@22808
    56
paulson@6046
    57
paulson@6046
    58
inductive
paulson@6046
    59
  domains       "Ssub" <= "redexes*redexes"
paulson@12593
    60
  intros
paulson@12593
    61
    Sub_Var:     "n \<in> nat ==> Var(n)<== Var(n)"
paulson@12593
    62
    Sub_Fun:     "[|u<== v|]==> Fun(u)<== Fun(v)"
paulson@12593
    63
    Sub_App1:    "[|u1<== v1; u2<== v2; b \<in> bool|]==>   
paulson@6046
    64
                     App(0,u1,u2)<== App(b,v1,v2)"
paulson@12593
    65
    Sub_App2:    "[|u1<== v1; u2<== v2|]==> App(1,u1,u2)<== App(1,v1,v2)"
paulson@12593
    66
  type_intros    redexes.intros bool_typechecks
paulson@6046
    67
paulson@6046
    68
inductive
paulson@6046
    69
  domains       "Scomp" <= "redexes*redexes"
paulson@12593
    70
  intros
paulson@12593
    71
    Comp_Var:    "n \<in> nat ==> Var(n) ~ Var(n)"
paulson@12593
    72
    Comp_Fun:    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
paulson@12593
    73
    Comp_App:    "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|]
paulson@12593
    74
                  ==> App(b1,u1,u2) ~ App(b2,v1,v2)"
paulson@12593
    75
  type_intros    redexes.intros bool_typechecks
paulson@6046
    76
paulson@6046
    77
inductive
paulson@13339
    78
  domains       "Sreg" <= redexes
paulson@12593
    79
  intros
paulson@12593
    80
    Reg_Var:     "n \<in> nat ==> regular(Var(n))"
paulson@12593
    81
    Reg_Fun:     "[|regular(u)|]==> regular(Fun(u))"
paulson@12593
    82
    Reg_App1:    "[|regular(Fun(u)); regular(v) |]==>regular(App(1,Fun(u),v))"
paulson@12593
    83
    Reg_App2:    "[|regular(u); regular(v) |]==>regular(App(0,u,v))"
paulson@12593
    84
  type_intros    redexes.intros bool_typechecks
paulson@12593
    85
paulson@12593
    86
paulson@12593
    87
declare redexes.intros [simp]
paulson@12593
    88
paulson@12593
    89
(* ------------------------------------------------------------------------- *)
paulson@12593
    90
(*    Specialisation of comp-rules                                           *)
paulson@12593
    91
(* ------------------------------------------------------------------------- *)
paulson@12593
    92
paulson@12593
    93
lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1]
paulson@12593
    94
lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2]
paulson@12593
    95
lemmas regD [simp] = Sreg.dom_subset [THEN subsetD]
paulson@12593
    96
paulson@12593
    97
(* ------------------------------------------------------------------------- *)
paulson@12593
    98
(*    Equality rules for union                                               *)
paulson@12593
    99
(* ------------------------------------------------------------------------- *)
paulson@12593
   100
paulson@12593
   101
lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)"
paulson@12593
   102
by (simp add: union_def)
paulson@12593
   103
paulson@12593
   104
lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
paulson@12593
   105
by (simp add: union_def)
paulson@12593
   106
 
paulson@12593
   107
lemma union_App [simp]:
paulson@12593
   108
     "[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|]
paulson@12593
   109
      ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"
paulson@12593
   110
by (simp add: union_def)
paulson@12593
   111
paulson@12593
   112
paulson@12593
   113
lemma or_1_right [simp]: "a or 1 = 1"
paulson@12593
   114
by (simp add: or_def cond_def) 
paulson@12593
   115
paulson@12593
   116
lemma or_0_right [simp]: "a \<in> bool \<Longrightarrow> a or 0 = a"
paulson@12593
   117
by (simp add: or_def cond_def bool_def, auto) 
paulson@12593
   118
paulson@12593
   119
paulson@12593
   120
paulson@12593
   121
declare Ssub.intros [simp]
paulson@12593
   122
declare bool_typechecks [simp]
paulson@12593
   123
declare Sreg.intros [simp]
paulson@12593
   124
declare Scomp.intros [simp]
paulson@12593
   125
paulson@12593
   126
declare Scomp.intros [intro]
paulson@6046
   127
wenzelm@12610
   128
inductive_cases [elim!]:
wenzelm@12610
   129
  "regular(App(b,f,a))"
wenzelm@12610
   130
  "regular(Fun(b))"
wenzelm@12610
   131
  "regular(Var(b))"
wenzelm@12610
   132
  "Fun(u) ~ Fun(t)"
wenzelm@12610
   133
  "u ~ Fun(t)"
wenzelm@12610
   134
  "u ~ Var(n)"
wenzelm@12610
   135
  "u ~ App(b,t,a)"
wenzelm@12610
   136
  "Fun(t) ~ v"
wenzelm@12610
   137
  "App(b,f,a) ~ v"
wenzelm@12610
   138
  "Var(n) ~ u"
paulson@12593
   139
paulson@12593
   140
paulson@12593
   141
paulson@12593
   142
(* ------------------------------------------------------------------------- *)
paulson@12593
   143
(*    comp proofs                                                            *)
paulson@12593
   144
(* ------------------------------------------------------------------------- *)
paulson@12593
   145
paulson@12593
   146
lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
paulson@12593
   147
by (erule redexes.induct, blast+)
paulson@12593
   148
paulson@12593
   149
lemma comp_sym: "u ~ v ==> v ~ u"
paulson@12593
   150
by (erule Scomp.induct, blast+)
paulson@12593
   151
paulson@12593
   152
lemma comp_sym_iff: "u ~ v <-> v ~ u"
paulson@12593
   153
by (blast intro: comp_sym)
paulson@12593
   154
paulson@12593
   155
lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w"
paulson@12593
   156
by (erule Scomp.induct, blast+)
paulson@12593
   157
paulson@12593
   158
(* ------------------------------------------------------------------------- *)
paulson@12593
   159
(*   union proofs                                                            *)
paulson@12593
   160
(* ------------------------------------------------------------------------- *)
paulson@12593
   161
paulson@12593
   162
lemma union_l: "u ~ v ==> u <== (u un v)"
paulson@12593
   163
apply (erule Scomp.induct)
paulson@13339
   164
apply (erule_tac [3] boolE, simp_all)
paulson@12593
   165
done
paulson@12593
   166
paulson@12593
   167
lemma union_r: "u ~ v ==> v <== (u un v)"
paulson@12593
   168
apply (erule Scomp.induct)
paulson@13339
   169
apply (erule_tac [3] c = b2 in boolE, simp_all)
paulson@12593
   170
done
paulson@12593
   171
paulson@12593
   172
lemma union_sym: "u ~ v ==> u un v = v un u"
paulson@12593
   173
by (erule Scomp.induct, simp_all add: or_commute)
paulson@12593
   174
paulson@12593
   175
(* ------------------------------------------------------------------------- *)
paulson@12593
   176
(*      regular proofs                                                       *)
paulson@12593
   177
(* ------------------------------------------------------------------------- *)
paulson@12593
   178
paulson@12593
   179
lemma union_preserve_regular [rule_format]:
paulson@12593
   180
     "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
berghofe@13612
   181
  by (erule Scomp.induct, auto)
paulson@6046
   182
lcp@1048
   183
end
lcp@1048
   184