src/ZF/Coind/Static.thy
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 32960 69916a850301
child 41779 a68f503805ed
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Coind/Static.thy
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Jacob Frost, Cambridge University Computer Laboratory
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     3
    Copyright   1995  University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12610
diff changeset
     6
theory Static imports Values Types begin
12595
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
     7
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
     8
(*** Basic correspondence relation -- not completely specified, as it is a
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
     9
     parameter of the proof.  A concrete version could be defined inductively.
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    10
***)
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    11
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    12
consts
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    13
  isof :: "[i,i] => o"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    14
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    15
axioms
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    16
  isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    17
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    18
(*Its extension to environments*)
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    19
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    20
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    21
  isofenv :: "[i,i] => o"  where
12595
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    22
   "isofenv(ve,te) ==                
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    23
      ve_dom(ve) = te_dom(te) &            
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    24
      (\<forall>x \<in> ve_dom(ve).                          
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    25
        \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
12595
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    26
  
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    27
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    28
(*** Elaboration ***)
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    29
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 1478
diff changeset
    30
consts  ElabRel :: i
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 1478
diff changeset
    31
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    32
inductive
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    33
  domains "ElabRel" <= "TyEnv * Exp * Ty"
12595
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    34
  intros
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    35
    constI [intro!]:
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    36
      "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    37
       <te,e_const(c),t> \<in> ElabRel"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    38
    varI [intro!]:
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    39
      "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==>   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    40
       <te,e_var(x),te_app(te,x)> \<in> ElabRel"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    41
    fnI [intro!]:
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    42
      "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    43
          <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==>   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    44
       <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    45
    fixI [intro!]:
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    46
      "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty;   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    47
          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==>   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    48
       <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    49
    appI [intro]:
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    50
      "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    51
          <te,e1,t_fun(t1,t2)> \<in> ElabRel;   
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    52
          <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel"
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    53
  type_intros te_appI Exp.intros Ty.intros
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    54
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    55
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    56
inductive_cases
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    57
    elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    58
  and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    59
  and elab_fnE [elim]:   "<te,e_fn(x,e),t> \<in> ElabRel"
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    60
  and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
8b9845807f77 tuned document sources;
wenzelm
parents: 12595
diff changeset
    61
  and elab_appE [elim]:  "<te,e_app(e1,e2),t> \<in> ElabRel"
12595
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    62
0480d02221b8 conversion to Isar
paulson
parents: 11318
diff changeset
    63
declare ElabRel.dom_subset [THEN subsetD, dest]
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    64
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    65
end
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    66
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    67
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    68
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    69
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    70
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    71
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    72