src/ZF/Coind/ECR.ML
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1461 6bcb44e4d6e5
child 2034 5079fdf938dd
permissions -rw-r--r--
expanded tabs
clasohm@1461
     1
(*  Title:      ZF/Coind/ECR.ML
lcp@915
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
lcp@915
     4
    Copyright   1995  University of Cambridge
lcp@915
     5
*)
lcp@915
     6
lcp@915
     7
open Dynamic ECR;
lcp@915
     8
lcp@915
     9
(* Specialised co-induction rule *)
lcp@915
    10
lcp@915
    11
goal ECR.thy
lcp@915
    12
 "!!x.[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
lcp@915
    13
\    <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
lcp@915
    14
\    {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
lcp@915
    15
\    Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==>  \
lcp@915
    16
\ <v_clos(x, e, ve),t>:HasTyRel";
lcp@915
    17
by (rtac HasTyRel.coinduct 1);
lcp@915
    18
by (rtac singletonI 1);
lcp@915
    19
by (fast_tac (ZF_cs addIs Val_ValEnv.intrs) 1);
lcp@915
    20
by (rtac disjI2 1);
lcp@915
    21
by (etac singletonE 1); 
lcp@915
    22
by (REPEAT_FIRST (resolve_tac [conjI,exI]));
lcp@915
    23
by (REPEAT (atac 1));
lcp@915
    24
qed "htr_closCI";
lcp@915
    25
lcp@915
    26
(* Specialised elimination rules *)
lcp@915
    27
lcp@915
    28
val htr_constE = 
lcp@915
    29
  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
lcp@915
    30
lcp@915
    31
val htr_closE =
lcp@915
    32
  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
lcp@915
    33
lcp@915
    34
(* Classical reasoning sets *)
lcp@915
    35
lcp@915
    36
fun mk_htr_cs cs =
lcp@915
    37
  let open HasTyRel in 
lcp@915
    38
    ( cs 
lcp@915
    39
      addSIs [htr_constI] 
lcp@915
    40
      addSEs [htr_constE]
lcp@915
    41
      addIs [htr_closI,htr_closCI]
lcp@915
    42
      addEs [htr_closE])
lcp@915
    43
  end;
lcp@915
    44
lcp@915
    45
val htr_cs = mk_htr_cs(static_cs);
lcp@915
    46
lcp@915
    47
(* Properties of the pointwise extension to environments *)
lcp@915
    48
lcp@915
    49
goalw ECR.thy [hastyenv_def]
lcp@915
    50
  "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
lcp@915
    51
\   hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
lcp@915
    52
by (safe_tac ZF_cs);
lcp@915
    53
by (rtac (ve_dom_owr RS ssubst) 1);
lcp@915
    54
by (assume_tac 1);
lcp@915
    55
by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
lcp@915
    56
by (rtac (te_dom_owr RS ssubst) 1);
lcp@915
    57
by (asm_simp_tac ZF_ss 1);
lcp@915
    58
by (rtac (excluded_middle RS disjE) 1);
lcp@915
    59
by (rtac (ve_app_owr2 RS ssubst) 1);
lcp@915
    60
by (assume_tac 1);
lcp@915
    61
by (assume_tac 1);
lcp@915
    62
by (rtac (te_app_owr2 RS ssubst) 1);
lcp@915
    63
by (assume_tac 1);
lcp@915
    64
by (dtac (ve_dom_owr RS subst) 1);
lcp@915
    65
by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
lcp@915
    66
by ((fast_tac ZF_cs 1) THEN (fast_tac ZF_cs 1));
lcp@915
    67
by (asm_simp_tac (ZF_ss addsimps [ve_app_owr1,te_app_owr1]) 1);
lcp@915
    68
qed "hastyenv_owr";
lcp@915
    69
lcp@915
    70
goalw ECR.thy  [isofenv_def,hastyenv_def]
lcp@915
    71
  "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
lcp@915
    72
by (safe_tac ZF_cs);
lcp@915
    73
by (dtac bspec 1);
lcp@915
    74
by (assume_tac 1);
lcp@915
    75
by (safe_tac ZF_cs);
lcp@915
    76
by (dtac HasTyRel.htr_constI 1);
lcp@915
    77
by (assume_tac 2);
lcp@915
    78
by (etac te_appI 1);
lcp@915
    79
by (etac ve_domI 1);
lcp@915
    80
by (ALLGOALS (asm_full_simp_tac ZF_ss));
lcp@915
    81
qed "basic_consistency_lem";
lcp@915
    82
lcp@915
    83
lcp@915
    84