pip: Precedence_ord.thy@c0f14399c12f (annotated)

0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	header {* Order on product types *}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	theory Precedence_ord
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	imports Main
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	begin
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	datatype precedence = Prc nat nat
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	instantiation precedence :: order
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	begin
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	definition
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	precedence_le_def: "x \<le> y \<longleftrightarrow> (case (x, y) of
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	(Prc fx sx, Prc fy sy) \<Rightarrow>
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	definition
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	(Prc fx sx, Prc fy sy) \<Rightarrow>
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	fx < fy \<or> (fx \<le> fy \<and> sy < sx))"
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	instance
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	proof
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	qed (auto simp: precedence_le_def precedence_less_def
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	intro: order_trans split:precedence.splits)
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	end
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	instance precedence :: preorder ..
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	30	instance precedence :: linorder
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	31	proof
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	qed (auto simp: precedence_le_def precedence_less_def
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	intro: order_trans split:precedence.splits)
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	35	instantiation precedence :: zero
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	36	begin
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	37
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	38	definition Zero_precedence_def:
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	39	"0 = Prc 0 0"
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	40
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	41	instance ..
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	42
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	end
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	44
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	45	end

author	xingyuan zhang <xingyuanzhang@126.com>
	Tue, 06 Oct 2015 13:08:00 +0800
changeset 48	c0f14399c12f
parent 33	9b9f2117561f
child 63	b620a2a0806a
permissions	-rw-r--r--