1 (* Title: ZF/ex/llist_eq.ML |
1 (* Title: ZF/ex/llist_eq.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Former part of llist.ML, contains definition and use of LList_Eq |
6 Equality for llist(A) as a greatest fixed point |
7 *) |
7 ***) |
8 |
8 |
9 (*** Equality for llist(A) as a greatest fixed point ***) |
9 (*Previously used <*> in the domain and variant pairs as elements. But |
|
10 standard pairs work just as well. To use variant pairs, must change prefix |
|
11 a q/Q to the Sigma, Pair and converse rules.*) |
10 |
12 |
11 structure LList_Eq = Co_Inductive_Fun |
13 structure LList_Eq = CoInductive_Fun |
12 (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; |
14 (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; |
13 val rec_doms = [("lleq", "llist(A) <*> llist(A)")]; |
15 val rec_doms = [("lleq", "llist(A) * llist(A)")]; |
14 val sintrs = |
16 val sintrs = |
15 ["<LNil; LNil> : lleq(A)", |
17 ["<LNil, LNil> : lleq(A)", |
16 "[| a:A; <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"]; |
18 "[| a:A; <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"]; |
17 val monos = []; |
19 val monos = []; |
18 val con_defs = []; |
20 val con_defs = []; |
19 val type_intrs = LList.intrs@[QSigmaI]; |
21 val type_intrs = LList.intrs@[SigmaI]; |
20 val type_elims = [QSigmaE2]); |
22 val type_elims = [SigmaE2]); |
21 |
23 |
22 (** Alternatives for above: |
24 (** Alternatives for above: |
23 val con_defs = LList.con_defs |
25 val con_defs = LList.con_defs |
24 val type_intrs = co_datatype_intrs |
26 val type_intrs = codatatype_intrs |
25 val type_elims = [quniv_QPair_E] |
27 val type_elims = [quniv_QPair_E] |
26 **) |
28 **) |
27 |
29 |
28 val lleq_cs = subset_cs |
30 val lleq_cs = subset_cs |
29 addSIs [succI1, Int_Vset_0_subset, |
31 addSIs [succI1, Int_Vset_0_subset, |
32 |
34 |
33 (** Some key feature of this proof needs to be made a general theorem! **) |
35 (** Some key feature of this proof needs to be made a general theorem! **) |
34 |
36 |
35 (*Keep unfolding the lazy list until the induction hypothesis applies*) |
37 (*Keep unfolding the lazy list until the induction hypothesis applies*) |
36 goal LList_Eq.thy |
38 goal LList_Eq.thy |
37 "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'"; |
39 "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'"; |
38 by (etac trans_induct 1); |
40 by (etac trans_induct 1); |
39 by (safe_tac subset_cs); |
41 by (safe_tac subset_cs); |
40 by (etac LList_Eq.elim 1); |
42 by (etac LList_Eq.elim 1); |
41 by (safe_tac (subset_cs addSEs [QPair_inject])); |
43 by (safe_tac (subset_cs addSEs [Pair_inject])); |
42 by (rewrite_goals_tac LList.con_defs); |
44 by (rewrite_goals_tac LList.con_defs); |
43 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
45 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
44 (*0 case*) |
46 (*0 case*) |
45 by (fast_tac lleq_cs 1); |
47 by (fast_tac lleq_cs 1); |
46 (*succ(j) case*) |
48 (*succ(j) case*) |
55 val lleq_Int_Vset_subset = standard |
57 val lleq_Int_Vset_subset = standard |
56 (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); |
58 (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); |
57 |
59 |
58 |
60 |
59 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
61 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
60 val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)"; |
62 val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)"; |
61 by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); |
63 by (rtac (prem RS converseI RS LList_Eq.coinduct) 1); |
62 by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); |
64 by (rtac (LList_Eq.dom_subset RS converse_type) 1); |
63 by (safe_tac qconverse_cs); |
65 by (safe_tac converse_cs); |
64 by (etac LList_Eq.elim 1); |
66 by (etac LList_Eq.elim 1); |
65 by (ALLGOALS (fast_tac qconverse_cs)); |
67 by (ALLGOALS (fast_tac qconverse_cs)); |
66 val lleq_symmetric = result(); |
68 val lleq_symmetric = result(); |
67 |
69 |
68 goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'"; |
70 goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'"; |
69 by (rtac equalityI 1); |
71 by (rtac equalityI 1); |
70 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 |
72 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 |
71 ORELSE etac lleq_symmetric 1)); |
73 ORELSE etac lleq_symmetric 1)); |
72 val lleq_implies_equal = result(); |
74 val lleq_implies_equal = result(); |
73 |
75 |
74 val [eqprem,lprem] = goal LList_Eq.thy |
76 val [eqprem,lprem] = goal LList_Eq.thy |
75 "[| l=l'; l: llist(A) |] ==> <l;l'> : lleq(A)"; |
77 "[| l=l'; l: llist(A) |] ==> <l,l'> : lleq(A)"; |
76 by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1); |
78 by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1); |
77 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); |
79 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); |
78 by (safe_tac qpair_cs); |
80 by (safe_tac qpair_cs); |
79 by (etac LList.elim 1); |
81 by (etac LList.elim 1); |
80 by (ALLGOALS (fast_tac qpair_cs)); |
82 by (ALLGOALS (fast_tac pair_cs)); |
81 val equal_llist_implies_leq = result(); |
83 val equal_llist_implies_leq = result(); |
82 |
84 |
83 |
|