isabelle: src/HOL/Corec_Examples/Tests/Merge_A.thy@ec8bf1268f45 (annotated)

62696 7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	1	(* Title: HOL/Corec_Examples/Tests/Merge_A.thy
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	2	Author: Aymeric Bouzy, Ecole polytechnique
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	3	Author: Jasmin Blanchette, Inria, LORIA, MPII
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	4	Copyright 2015, 2016
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	5
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	6	Tests theory merges.
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	7	*)
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	8
62726 5b2a7caa855b tuned examples blanchet parents: 62696 diff changeset	9	section \<open>Tests Theory Merges\<close>
62696 7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	10
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	11	theory Merge_A
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 62726 diff changeset	12	imports "HOL-Library.BNF_Corec"
62696 7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	13	begin
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	14
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	15	codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta")
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	16
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	17	consts gb :: "'a ta \<Rightarrow> 'a ta"
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	18
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	19	corec fa where
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	20	"fa = Ca (Suc 0) fa"
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	21
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	22	corec ga :: "'a ta \<Rightarrow> 'a ta" where
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	23	"ga t = Ca (sa1 t) (sa2 t)"
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	24
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	25	friend_of_corec ga :: "'a ta \<Rightarrow> 'a ta" where
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	26	"ga t = Ca (sa1 t) (Ca (sa1 t) (sa2 t))"
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	27	sorry
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	28
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	29	thm ta.coinduct_upto
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	30	thm ta.cong_refl
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	31
7325d8573fb8 added 'corec' examples and tests blanchet parents: diff changeset	32	end

author	wenzelm
	Wed, 07 Dec 2022 15:43:47 +0100
changeset 76592	ec8bf1268f45
parent 66453	cc19f7ca2ed6
permissions	-rw-r--r--