author | wenzelm |
Thu, 14 Oct 1999 15:04:36 +0200 | |
changeset 7866 | 3ccaa11b6df9 |
parent 6154 | 6a00a5baef2b |
child 11318 | 6536fb8c9fc6 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Coind/ECR.ML |
915 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
915 | 4 |
Copyright 1995 University of Cambridge |
5 |
*) |
|
6 |
||
7 |
(* Specialised co-induction rule *) |
|
8 |
||
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
9 |
Goal "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
10 |
\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \ |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
11 |
\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \ |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
12 |
\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] \ |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
13 |
\ ==> <v_clos(x, e, ve),t>:HasTyRel"; |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
14 |
by (rtac (singletonI RS HasTyRel.coinduct) 1); |
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
15 |
by (ALLGOALS Blast_tac); |
915 | 16 |
qed "htr_closCI"; |
17 |
||
18 |
(* Specialised elimination rules *) |
|
19 |
||
6141 | 20 |
val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel"; |
915 | 21 |
|
6141 | 22 |
val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel"; |
915 | 23 |
|
24 |
(* Classical reasoning sets *) |
|
25 |
||
26 |
fun mk_htr_cs cs = |
|
27 |
let open HasTyRel in |
|
28 |
( cs |
|
29 |
addSIs [htr_constI] |
|
30 |
addSEs [htr_constE] |
|
31 |
addIs [htr_closI,htr_closCI] |
|
32 |
addEs [htr_closE]) |
|
33 |
end; |
|
34 |
||
4091 | 35 |
claset_ref() := mk_htr_cs (claset()); |
915 | 36 |
|
37 |
(* Properties of the pointwise extension to environments *) |
|
38 |
||
6046 | 39 |
bind_thm ("HasTyRel_non_zero", |
40 |
HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE); |
|
41 |
||
5068 | 42 |
Goalw [hastyenv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
43 |
"[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \ |
915 | 44 |
\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"; |
6046 | 45 |
by (asm_full_simp_tac |
46 |
(simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1); |
|
47 |
by Auto_tac; |
|
915 | 48 |
qed "hastyenv_owr"; |
49 |
||
5068 | 50 |
Goalw [isofenv_def,hastyenv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
51 |
"[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"; |
4152 | 52 |
by Safe_tac; |
915 | 53 |
by (dtac bspec 1); |
54 |
by (assume_tac 1); |
|
4152 | 55 |
by Safe_tac; |
915 | 56 |
by (dtac HasTyRel.htr_constI 1); |
57 |
by (assume_tac 2); |
|
58 |
by (etac te_appI 1); |
|
59 |
by (etac ve_domI 1); |
|
2469 | 60 |
by (ALLGOALS Asm_full_simp_tac); |
915 | 61 |
qed "basic_consistency_lem"; |
62 |
||
63 |
||
64 |