51 trueV: "true ---> true" and |
51 trueV: "true ---> true" and |
52 falseV: "false ---> false" and |
52 falseV: "false ---> false" and |
53 pairV: "<a,b> ---> <a,b>" and |
53 pairV: "<a,b> ---> <a,b>" and |
54 lamV: "\<And>b. lam x. b(x) ---> lam x. b(x)" and |
54 lamV: "\<And>b. lam x. b(x) ---> lam x. b(x)" and |
55 |
55 |
56 caseVtrue: "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c" and |
56 caseVtrue: "\<lbrakk>t ---> true; d ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and |
57 caseVfalse: "[| t ---> false; e ---> c |] ==> case(t,d,e,f,g) ---> c" and |
57 caseVfalse: "\<lbrakk>t ---> false; e ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and |
58 caseVpair: "[| t ---> <a,b>; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" and |
58 caseVpair: "\<lbrakk>t ---> <a,b>; f(a,b) ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and |
59 caseVlam: "\<And>b. [| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c" |
59 caseVlam: "\<And>b. \<lbrakk>t ---> lam x. b(x); g(b) ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" |
60 |
60 |
61 (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) |
61 (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) |
62 |
62 |
63 axiomatization where |
63 axiomatization where |
64 canonical: "[| t ---> c; c==true ==> u--->v; |
64 canonical: "\<lbrakk>t ---> c; c==true \<Longrightarrow> u--->v; |
65 c==false ==> u--->v; |
65 c==false \<Longrightarrow> u--->v; |
66 !!a b. c==<a,b> ==> u--->v; |
66 \<And>a b. c==<a,b> \<Longrightarrow> u--->v; |
67 !!f. c==lam x. f(x) ==> u--->v |] ==> |
67 \<And>f. c==lam x. f(x) \<Longrightarrow> u--->v\<rbrakk> \<Longrightarrow> |
68 u--->v" |
68 u--->v" |
69 |
69 |
70 (* Should be derivable - but probably a bitch! *) |
70 (* Should be derivable - but probably a bitch! *) |
71 axiomatization where |
71 axiomatization where |
72 substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" |
72 substitute: "\<lbrakk>a==a'; t(a)--->c(a)\<rbrakk> \<Longrightarrow> t(a')--->c(a')" |
73 |
73 |
74 (************** LOGIC ***************) |
74 (************** LOGIC ***************) |
75 |
75 |
76 (*** Definitions used in the following rules ***) |
76 (*** Definitions used in the following rules ***) |
77 |
77 |
78 axiomatization where |
78 axiomatization where |
79 bot_def: "bot == (lam x. x`x)`(lam x. x`x)" and |
79 bot_def: "bot == (lam x. x`x)`(lam x. x`x)" and |
80 apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" |
80 apply_def: "f ` t == case(f, bot, bot, \<lambda>x y. bot, \<lambda>u. u(t))" |
81 |
81 |
82 definition "fix" :: "(i=>i)=>i" |
82 definition "fix" :: "(i\<Rightarrow>i)\<Rightarrow>i" |
83 where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" |
83 where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" |
84 |
84 |
85 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) |
85 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) |
86 (* as a bisimulation. They can both be expressed as (bi)simulations up to *) |
86 (* as a bisimulation. They can both be expressed as (bi)simulations up to *) |
87 (* behavioural equivalence (ie the relations PO and EQ defined below). *) |
87 (* behavioural equivalence (ie the relations PO and EQ defined below). *) |
88 |
88 |
89 definition SIM :: "[i,i,i set]=>o" |
89 definition SIM :: "[i,i,i set]\<Rightarrow>o" |
90 where |
90 where |
91 "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | |
91 "SIM(t,t',R) == (t=true \<and> t'=true) | (t=false \<and> t'=false) | |
92 (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | |
92 (\<exists>a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) | |
93 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))" |
93 (\<exists>f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))" |
94 |
94 |
95 definition POgen :: "i set => i set" |
95 definition POgen :: "i set \<Rightarrow> i set" |
96 where "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}" |
96 where "POgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot | SIM(t,t',R))}" |
97 |
97 |
98 definition EQgen :: "i set => i set" |
98 definition EQgen :: "i set \<Rightarrow> i set" |
99 where "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}" |
99 where "EQgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot \<and> t' = bot | SIM(t,t',R))}" |
100 |
100 |
101 definition PO :: "i set" |
101 definition PO :: "i set" |
102 where "PO == gfp(POgen)" |
102 where "PO == gfp(POgen)" |
103 |
103 |
104 definition EQ :: "i set" |
104 definition EQ :: "i set" |
302 and [dest!] = ccl_injDs |
302 and [dest!] = ccl_injDs |
303 |
303 |
304 |
304 |
305 subsection {* Facts from gfp Definition of @{text "[="} and @{text "="} *} |
305 subsection {* Facts from gfp Definition of @{text "[="} and @{text "="} *} |
306 |
306 |
307 lemma XHlemma1: "[| A=B; a:B <-> P |] ==> a:A <-> P" |
307 lemma XHlemma1: "\<lbrakk>A=B; a:B \<longleftrightarrow> P\<rbrakk> \<Longrightarrow> a:A \<longleftrightarrow> P" |
308 by simp |
308 by simp |
309 |
309 |
310 lemma XHlemma2: "(P(t,t') <-> Q) ==> (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <-> Q)" |
310 lemma XHlemma2: "(P(t,t') \<longleftrightarrow> Q) \<Longrightarrow> (<t,t'> : {p. \<exists>t t'. p=<t,t'> \<and> P(t,t')} \<longleftrightarrow> Q)" |
311 by blast |
311 by blast |
312 |
312 |
313 |
313 |
314 subsection {* Pre-Order *} |
314 subsection {* Pre-Order *} |
315 |
315 |
316 lemma POgen_mono: "mono(%X. POgen(X))" |
316 lemma POgen_mono: "mono(\<lambda>X. POgen(X))" |
317 apply (unfold POgen_def SIM_def) |
317 apply (unfold POgen_def SIM_def) |
318 apply (rule monoI) |
318 apply (rule monoI) |
319 apply blast |
319 apply blast |
320 done |
320 done |
321 |
321 |
322 lemma POgenXH: |
322 lemma POgenXH: |
323 "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | |
323 "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) | |
324 (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | |
324 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) | |
325 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))" |
325 (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))" |
326 apply (unfold POgen_def SIM_def) |
326 apply (unfold POgen_def SIM_def) |
327 apply (rule iff_refl [THEN XHlemma2]) |
327 apply (rule iff_refl [THEN XHlemma2]) |
328 done |
328 done |
329 |
329 |
330 lemma poXH: |
330 lemma poXH: |
331 "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | |
331 "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) | |
332 (EX a a' b b'. t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | |
332 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a [= a' \<and> b [= b') | |
333 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))" |
333 (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))" |
334 apply (simp add: PO_iff del: ex_simps) |
334 apply (simp add: PO_iff del: ex_simps) |
335 apply (rule POgen_mono |
335 apply (rule POgen_mono |
336 [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def]) |
336 [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def]) |
337 apply (rule iff_refl [THEN XHlemma2]) |
337 apply (rule iff_refl [THEN XHlemma2]) |
338 done |
338 done |
340 lemma po_bot: "bot [= b" |
340 lemma po_bot: "bot [= b" |
341 apply (rule poXH [THEN iffD2]) |
341 apply (rule poXH [THEN iffD2]) |
342 apply simp |
342 apply simp |
343 done |
343 done |
344 |
344 |
345 lemma bot_poleast: "a [= bot ==> a=bot" |
345 lemma bot_poleast: "a [= bot \<Longrightarrow> a=bot" |
346 apply (drule poXH [THEN iffD1]) |
346 apply (drule poXH [THEN iffD1]) |
347 apply simp |
347 apply simp |
348 done |
348 done |
349 |
349 |
350 lemma po_pair: "<a,b> [= <a',b'> <-> a [= a' & b [= b'" |
350 lemma po_pair: "<a,b> [= <a',b'> \<longleftrightarrow> a [= a' \<and> b [= b'" |
351 apply (rule poXH [THEN iff_trans]) |
351 apply (rule poXH [THEN iff_trans]) |
352 apply simp |
352 apply simp |
353 done |
353 done |
354 |
354 |
355 lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))" |
355 lemma po_lam: "lam x. f(x) [= lam x. f'(x) \<longleftrightarrow> (ALL x. f(x) [= f'(x))" |
356 apply (rule poXH [THEN iff_trans]) |
356 apply (rule poXH [THEN iff_trans]) |
357 apply fastforce |
357 apply fastforce |
358 done |
358 done |
359 |
359 |
360 lemmas ccl_porews = po_bot po_pair po_lam |
360 lemmas ccl_porews = po_bot po_pair po_lam |
361 |
361 |
362 lemma case_pocong: |
362 lemma case_pocong: |
363 assumes 1: "t [= t'" |
363 assumes 1: "t [= t'" |
364 and 2: "a [= a'" |
364 and 2: "a [= a'" |
365 and 3: "b [= b'" |
365 and 3: "b [= b'" |
366 and 4: "!!x y. c(x,y) [= c'(x,y)" |
366 and 4: "\<And>x y. c(x,y) [= c'(x,y)" |
367 and 5: "!!u. d(u) [= d'(u)" |
367 and 5: "\<And>u. d(u) [= d'(u)" |
368 shows "case(t,a,b,c,d) [= case(t',a',b',c',d')" |
368 shows "case(t,a,b,c,d) [= case(t',a',b',c',d')" |
369 apply (rule 1 [THEN po_cong, THEN po_trans]) |
369 apply (rule 1 [THEN po_cong, THEN po_trans]) |
370 apply (rule 2 [THEN po_cong, THEN po_trans]) |
370 apply (rule 2 [THEN po_cong, THEN po_trans]) |
371 apply (rule 3 [THEN po_cong, THEN po_trans]) |
371 apply (rule 3 [THEN po_cong, THEN po_trans]) |
372 apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans]) |
372 apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans]) |
373 apply (rule_tac f1 = "%d. case (t',a',b',c',d)" in |
373 apply (rule_tac f1 = "\<lambda>d. case (t',a',b',c',d)" in |
374 5 [THEN po_abstractn, THEN po_cong, THEN po_trans]) |
374 5 [THEN po_abstractn, THEN po_cong, THEN po_trans]) |
375 apply (rule po_refl) |
375 apply (rule po_refl) |
376 done |
376 done |
377 |
377 |
378 lemma apply_pocong: "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'" |
378 lemma apply_pocong: "\<lbrakk>f [= f'; a [= a'\<rbrakk> \<Longrightarrow> f ` a [= f' ` a'" |
379 unfolding ccl_data_defs |
379 unfolding ccl_data_defs |
380 apply (rule case_pocong, (rule po_refl | assumption)+) |
380 apply (rule case_pocong, (rule po_refl | assumption)+) |
381 apply (erule po_cong) |
381 apply (erule po_cong) |
382 done |
382 done |
383 |
383 |
384 lemma npo_lam_bot: "~ lam x. b(x) [= bot" |
384 lemma npo_lam_bot: "\<not> lam x. b(x) [= bot" |
385 apply (rule notI) |
385 apply (rule notI) |
386 apply (drule bot_poleast) |
386 apply (drule bot_poleast) |
387 apply (erule distinctness [THEN notE]) |
387 apply (erule distinctness [THEN notE]) |
388 done |
388 done |
389 |
389 |
390 lemma po_lemma: "[| x=a; y=b; x[=y |] ==> a[=b" |
390 lemma po_lemma: "\<lbrakk>x=a; y=b; x[=y\<rbrakk> \<Longrightarrow> a[=b" |
391 by simp |
391 by simp |
392 |
392 |
393 lemma npo_pair_lam: "~ <a,b> [= lam x. f(x)" |
393 lemma npo_pair_lam: "\<not> <a,b> [= lam x. f(x)" |
394 apply (rule notI) |
394 apply (rule notI) |
395 apply (rule npo_lam_bot [THEN notE]) |
395 apply (rule npo_lam_bot [THEN notE]) |
396 apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]]) |
396 apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]]) |
397 apply (rule po_refl npo_lam_bot)+ |
397 apply (rule po_refl npo_lam_bot)+ |
398 done |
398 done |
399 |
399 |
400 lemma npo_lam_pair: "~ lam x. f(x) [= <a,b>" |
400 lemma npo_lam_pair: "\<not> lam x. f(x) [= <a,b>" |
401 apply (rule notI) |
401 apply (rule notI) |
402 apply (rule npo_lam_bot [THEN notE]) |
402 apply (rule npo_lam_bot [THEN notE]) |
403 apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]]) |
403 apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]]) |
404 apply (rule po_refl npo_lam_bot)+ |
404 apply (rule po_refl npo_lam_bot)+ |
405 done |
405 done |
406 |
406 |
407 lemma npo_rls1: |
407 lemma npo_rls1: |
408 "~ true [= false" |
408 "\<not> true [= false" |
409 "~ false [= true" |
409 "\<not> false [= true" |
410 "~ true [= <a,b>" |
410 "\<not> true [= <a,b>" |
411 "~ <a,b> [= true" |
411 "\<not> <a,b> [= true" |
412 "~ true [= lam x. f(x)" |
412 "\<not> true [= lam x. f(x)" |
413 "~ lam x. f(x) [= true" |
413 "\<not> lam x. f(x) [= true" |
414 "~ false [= <a,b>" |
414 "\<not> false [= <a,b>" |
415 "~ <a,b> [= false" |
415 "\<not> <a,b> [= false" |
416 "~ false [= lam x. f(x)" |
416 "\<not> false [= lam x. f(x)" |
417 "~ lam x. f(x) [= false" |
417 "\<not> lam x. f(x) [= false" |
418 by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all, |
418 by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all, |
419 (rule po_refl npo_lam_bot)+)+ |
419 (rule po_refl npo_lam_bot)+)+ |
420 |
420 |
421 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1 |
421 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1 |
422 |
422 |
423 |
423 |
424 subsection {* Coinduction for @{text "[="} *} |
424 subsection {* Coinduction for @{text "[="} *} |
425 |
425 |
426 lemma po_coinduct: "[| <t,u> : R; R <= POgen(R) |] ==> t [= u" |
426 lemma po_coinduct: "\<lbrakk><t,u> : R; R <= POgen(R)\<rbrakk> \<Longrightarrow> t [= u" |
427 apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]]) |
427 apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]]) |
428 apply assumption+ |
428 apply assumption+ |
429 done |
429 done |
430 |
430 |
431 |
431 |
432 subsection {* Equality *} |
432 subsection {* Equality *} |
433 |
433 |
434 lemma EQgen_mono: "mono(%X. EQgen(X))" |
434 lemma EQgen_mono: "mono(\<lambda>X. EQgen(X))" |
435 apply (unfold EQgen_def SIM_def) |
435 apply (unfold EQgen_def SIM_def) |
436 apply (rule monoI) |
436 apply (rule monoI) |
437 apply blast |
437 apply blast |
438 done |
438 done |
439 |
439 |
440 lemma EQgenXH: |
440 lemma EQgenXH: |
441 "<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | |
441 "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | |
442 (t=false & t'=false) | |
442 (t=false \<and> t'=false) | |
443 (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | |
443 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) | |
444 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))" |
444 (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))" |
445 apply (unfold EQgen_def SIM_def) |
445 apply (unfold EQgen_def SIM_def) |
446 apply (rule iff_refl [THEN XHlemma2]) |
446 apply (rule iff_refl [THEN XHlemma2]) |
447 done |
447 done |
448 |
448 |
449 lemma eqXH: |
449 lemma eqXH: |
450 "t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | |
450 "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) | |
451 (EX a a' b b'. t=<a,b> & t'=<a',b'> & a=a' & b=b') | |
451 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a=a' \<and> b=b') | |
452 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))" |
452 (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))" |
453 apply (subgoal_tac "<t,t'> : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | (EX f f'. t=lam x. f (x) & t'=lam x. f' (x) & (ALL x. <f (x) ,f' (x) > : EQ))") |
453 apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow> |
|
454 (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) | |
|
455 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : EQ \<and> <b,b'> : EQ) | |
|
456 (EX f f'. t=lam x. f (x) \<and> t'=lam x. f' (x) \<and> (ALL x. <f (x) ,f' (x) > : EQ))") |
454 apply (erule rev_mp) |
457 apply (erule rev_mp) |
455 apply (simp add: EQ_iff [THEN iff_sym]) |
458 apply (simp add: EQ_iff [THEN iff_sym]) |
456 apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1, |
459 apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1, |
457 unfolded EQgen_def SIM_def]) |
460 unfolded EQgen_def SIM_def]) |
458 apply (rule iff_refl [THEN XHlemma2]) |
461 apply (rule iff_refl [THEN XHlemma2]) |
459 done |
462 done |
460 |
463 |
461 lemma eq_coinduct: "[| <t,u> : R; R <= EQgen(R) |] ==> t = u" |
464 lemma eq_coinduct: "\<lbrakk><t,u> : R; R <= EQgen(R)\<rbrakk> \<Longrightarrow> t = u" |
462 apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]]) |
465 apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]]) |
463 apply assumption+ |
466 apply assumption+ |
464 done |
467 done |
465 |
468 |
466 lemma eq_coinduct3: |
469 lemma eq_coinduct3: |
467 "[| <t,u> : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u" |
470 "\<lbrakk><t,u> : R; R <= EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))\<rbrakk> \<Longrightarrow> t = u" |
468 apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]]) |
471 apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]]) |
469 apply (rule EQgen_mono | assumption)+ |
472 apply (rule EQgen_mono | assumption)+ |
470 done |
473 done |
471 |
474 |
472 method_setup eq_coinduct3 = {* |
475 method_setup eq_coinduct3 = {* |