author | lcp |
Fri, 22 Oct 1993 11:42:02 +0100 | |
changeset 71 | 729fe026c5f3 |
parent 34 | 747f1aad03cf |
child 95 | 2246a80b1cb5 |
permissions | -rw-r--r-- |
34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
1 |
(* Title: ZF/ex/llist_eq.ML |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
5 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
6 |
Former part of llist.ML, contains definition and use of LList_Eq |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
7 |
*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
8 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
9 |
(*** Equality for llist(A) as a greatest fixed point ***) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
10 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
11 |
structure LList_Eq = Co_Inductive_Fun |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
12 |
(val thy = LList.thy addconsts [(["lleq"],"i=>i")]; |
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
34
diff
changeset
|
13 |
val rec_doms = [("lleq", "llist(A) <*> llist(A)")]; |
34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
14 |
val sintrs = |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
15 |
["<LNil; LNil> : lleq(A)", |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
16 |
"[| a:A; <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"]; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
17 |
val monos = []; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
18 |
val con_defs = []; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
19 |
val type_intrs = LList.intrs@[QSigmaI]; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
20 |
val type_elims = [QSigmaE2]); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
21 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
22 |
(** Alternatives for above: |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
23 |
val con_defs = LList.con_defs |
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
34
diff
changeset
|
24 |
val type_intrs = co_datatype_intrs |
34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
25 |
val type_elims = [quniv_QPair_E] |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
26 |
**) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
27 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
28 |
val lleq_cs = subset_cs |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
29 |
addSIs [succI1, Int_Vset_0_subset, |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
30 |
QPair_Int_Vset_succ_subset_trans, |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
31 |
QPair_Int_Vset_subset_trans]; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
32 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
33 |
(*Keep unfolding the lazy list until the induction hypothesis applies*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
34 |
goal LList_Eq.thy |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
35 |
"!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'"; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
36 |
by (etac trans_induct 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
37 |
by (safe_tac subset_cs); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
38 |
by (etac LList_Eq.elim 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
39 |
by (safe_tac (subset_cs addSEs [QPair_inject])); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
40 |
by (rewrite_goals_tac LList.con_defs); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
41 |
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
42 |
(*0 case*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
43 |
by (fast_tac lleq_cs 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
44 |
(*succ(j) case*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
45 |
by (rewtac QInr_def); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
46 |
by (fast_tac lleq_cs 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
47 |
(*Limit(i) case*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
48 |
by (etac (Limit_Vfrom_eq RS ssubst) 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
49 |
by (rtac (Int_UN_distrib RS ssubst) 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
50 |
by (fast_tac lleq_cs 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
51 |
val lleq_Int_Vset_subset_lemma = result(); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
52 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
53 |
val lleq_Int_Vset_subset = standard |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
54 |
(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
55 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
56 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
57 |
(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
58 |
val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)"; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
59 |
by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
60 |
by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
61 |
by (safe_tac qconverse_cs); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
62 |
by (etac LList_Eq.elim 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
63 |
by (ALLGOALS (fast_tac qconverse_cs)); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
64 |
val lleq_symmetric = result(); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
65 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
66 |
goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'"; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
67 |
by (rtac equalityI 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
68 |
by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
69 |
ORELSE etac lleq_symmetric 1)); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
70 |
val lleq_implies_equal = result(); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
71 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
72 |
val [eqprem,lprem] = goal LList_Eq.thy |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
73 |
"[| l=l'; l: llist(A) |] ==> <l;l'> : lleq(A)"; |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
74 |
by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
75 |
by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
76 |
by (safe_tac qpair_cs); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
77 |
by (etac LList.elim 1); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
78 |
by (ALLGOALS (fast_tac qpair_cs)); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
79 |
val equal_llist_implies_leq = result(); |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
80 |
|
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
diff
changeset
|
81 |