9 (*Previously used <*> in the domain and variant pairs as elements. But |
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 |
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.*) |
11 a q/Q to the Sigma, Pair and converse rules.*) |
12 |
12 |
13 structure LList_Eq = CoInductive_Fun |
13 structure LList_Eq = CoInductive_Fun |
14 (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; |
14 (val thy = LList.thy addconsts [(["lleq"],"i=>i")] |
15 val rec_doms = [("lleq", "llist(A) * llist(A)")]; |
15 val rec_doms = [("lleq", "llist(A) * llist(A)")] |
16 val sintrs = |
16 val sintrs = |
17 ["<LNil, LNil> : lleq(A)", |
17 ["<LNil, LNil> : lleq(A)", |
18 "[| 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)"] |
19 val monos = []; |
19 val monos = [] |
20 val con_defs = []; |
20 val con_defs = [] |
21 val type_intrs = LList.intrs@[SigmaI]; |
21 val type_intrs = LList.intrs @ [SigmaI] |
22 val type_elims = [SigmaE2]); |
22 val type_elims = [SigmaE2]); |
23 |
23 |
24 (** Alternatives for above: |
24 (** Alternatives for above: |
25 val con_defs = LList.con_defs |
25 val con_defs = LList.con_defs |
26 val type_intrs = codatatype_intrs |
26 val type_intrs = codatatype_intrs |