pip: Precedence_ord.thy@b620a2a0806a (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
63 b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	17	lemma preced_leI1[intro]:
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	18	assumes "fx < fy"
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	19	shows "Prc fx sx \<le> Prc fy sy"
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	20	using assms
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	21	by (simp add: precedence_le_def)
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	22
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	23	lemma preced_leI2[intro]:
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	24	assumes "fx \<le> fy"
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	25	and "sy \<le> sx"
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	26	shows "Prc fx sx \<le> Prc fy sy"
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	27	using assms
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	28	by (simp add: precedence_le_def)
b620a2a0806a ExtGG.thy finished, but more comments are needed. zhangx parents: 33 diff changeset	29
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	definition
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	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	32	(Prc fx sx, Prc fy sy) \<Rightarrow>
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	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	34
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	instance
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	proof
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	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	38	intro: order_trans split:precedence.splits)
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	end
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	instance precedence :: preorder ..
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	43	instance precedence :: linorder
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	44	proof
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	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	46	intro: order_trans split:precedence.splits)
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	48	instantiation precedence :: zero
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	49	begin
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	50
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	51	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	52	"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	53
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	54	instance ..
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	55
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	end
33 9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	57
9b9f2117561f simplified the cp_rec proof Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	58	end

author	zhangx
	Wed, 06 Jan 2016 20:46:14 +0800
changeset 63	b620a2a0806a
parent 33	9b9f2117561f
child 197	ca4ddf26a7c7
permissions	-rw-r--r--