src/ZF/Coind/Types.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: 916
diff changeset
     1
(*  Title:      ZF/Coind/Types.ML
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 916
diff changeset
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     7
open Types;
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     9
val te_owrE = 
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    10
  TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    11
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
goalw Types.thy TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    13
by (simp_tac rank_ss 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    14
qed "rank_te_owr1";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    15
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    16
goal Types.thy "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    17
by (rtac (te_rec_def RS def_Vrec RS trans) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    18
by (simp_tac (ZF_ss addsimps TyEnv.case_eqns) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    19
qed "te_rec_emp";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    21
goal Types.thy 
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    22
  " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    23
\   f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    24
by (rtac (te_rec_def RS def_Vrec RS trans) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    25
by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    26
qed "te_rec_owr";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    27
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    28
goalw Types.thy [te_dom_def] "te_dom(te_emp) = 0";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    29
by (simp_tac (ZF_ss addsimps [te_rec_emp]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    30
qed "te_dom_emp";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    31
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    32
goalw Types.thy [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    33
by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    34
qed "te_dom_owr";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    35
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    36
goalw Types.thy [te_app_def] "te_app(te_owr(te,x,t),x) = t";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    37
by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    38
qed "te_app_owr1";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    39
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    40
val prems = goalw Types.thy [te_app_def]
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    41
  "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    42
by (cut_facts_tac prems 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    43
by (asm_simp_tac (ZF_ss addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    44
qed "te_app_owr2";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    45
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    46
val prems = goal Types.thy
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    47
  "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    48
by (cut_facts_tac prems 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    49
by (res_inst_tac [("P","x:te_dom(te)")] impE 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    50
by (assume_tac 2);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    51
by (assume_tac 2);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    52
by (etac TyEnv.induct 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    53
by (simp_tac (ZF_ss addsimps [te_dom_emp]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    54
by (rtac impI 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    55
by (rtac (excluded_middle RS disjE) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    56
by (rtac (te_app_owr2 RS ssubst) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    57
by (assume_tac 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    58
by (asm_full_simp_tac (ZF_ss addsimps [te_dom_owr]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    59
by (fast_tac ZF_cs 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    60
by (asm_simp_tac (ZF_ss addsimps [te_app_owr1]) 1);
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    61
qed "te_appI";
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    62
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    63
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
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
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    73
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    74
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    75
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    76
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    77
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    78
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    79