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