lexing: thys/Sulzmann.thy@2de3cf684ba0 (annotated)

148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	theory Sulzmann
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	imports "ReStar"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	begin
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	section {* Sulzmann's "Ordering" of Values *}
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ >_ _" [100, 100, 100] 100)
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	where
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	C2: "v1 >r1 v1' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1' v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\| C1: "v2 >r2 v2' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1 v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) >(ALT r1 r2) (Left v1)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) >(ALT r1 r2) (Right v2)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\| A3: "v2 >r2 v2' \<Longrightarrow> (Right v2) >(ALT r1 r2) (Right v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\| A4: "v1 >r1 v1' \<Longrightarrow> (Left v1) >(ALT r1 r2) (Left v1')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) >(STAR r) (Stars (v # vs))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) >(STAR r) (Stars [])"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	\| K3: "v1 >r v2 \<Longrightarrow> (Stars (v1 # vs1)) >(STAR r) (Stars (v2 # vs2))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	\| K4: "(Stars vs1) >(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) >(STAR r) (Stars (v # vs2))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	where
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	"v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	(*
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	where
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	"v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	\| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	\| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	\| "Void \<succ>EMPTY Void"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\| "(Char c) \<succ>(CHAR c) (Char c)"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	\| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	\| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	\| "(Stars []) \<succ>(STAR r) (Stars [])"
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	*)
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	48	section {* Bit-Encodings *}
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	49
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	50
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	51	fun
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	52	code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	53	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	54	"code Void ONE = []"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	55	\| "code (Char c) (CHAR d) = []"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	56	\| "code (Left v) (ALT r1 r2) = False # (code v r1)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	57	\| "code (Right v) (ALT r1 r2) = True # (code v r2)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	58	\| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	59	\| "code (Stars []) (STAR r) = [True]"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	60	\| "code (Stars (v # vs)) (STAR r) = False # (code v r) @ code (Stars vs) (STAR r)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	61
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	62	fun
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	63	Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	64	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	65	"Stars_add v (Stars vs) = Stars (v # vs)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	66
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	67	function
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	68	decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	69	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	70	"decode' ds ZERO = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	71	\| "decode' ds ONE = (Void, ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	72	\| "decode' ds (CHAR d) = (Char d, ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	73	\| "decode' [] (ALT r1 r2) = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	74	\| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	75	\| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	76	\| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	77	let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	78	\| "decode' [] (STAR r) = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	79	\| "decode' (True # ds) (STAR r) = (Stars [], ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	80	\| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	81	let (vs, ds'') = decode' ds' (STAR r)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	82	in (Stars_add v vs, ds''))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	83	by pat_completeness auto
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	84
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	85	term "inv_image (measure(%cs. size cs) <lex> measure(%s. size s)) (%(ds,r). (r,ds))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	86
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	87	lemma decode'_smaller:
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	88	assumes "decode'_dom (ds, r)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	89	shows "length (snd (decode' ds r)) \<le> length ds"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	90	using assms
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	91	apply(induct ds r)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	92	apply(auto simp add: decode'.psimps split: prod.split)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	93	using dual_order.trans apply blast
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	94	by (meson dual_order.trans le_SucI)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	95
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	96	termination "decode'"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	97	apply(relation "inv_image (measure(%cs. size cs) <lex> measure(%s. size s)) (%(ds,r). (r,ds))")
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	98	apply(auto dest!: decode'_smaller)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	99	by (metis less_Suc_eq_le snd_conv)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	100
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	101	fun
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	102	decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	103	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	104	"decode ds r = (let (v, ds') = decode' ds r
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	105	in (if ds' = [] then Some v else None))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	106
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	107	lemma decode'_code:
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	108	assumes "\<turnstile> v : r"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	109	shows "decode' ((code v r) @ ds) r = (v, ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	110	using assms
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	111	by (induct v r arbitrary: ds) (auto)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	112
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	113
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	114	lemma decode_code:
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	115	assumes "\<turnstile> v : r"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	116	shows "decode (code v r) r = Some v"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	117	using assms decode'_code[of _ _ "[]"]
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	118	by auto
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	119
148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 18 Mar 2016 01:26:14 +0000
changeset 154	2de3cf684ba0
parent 148	702ed601349b
child 159	940530087f30
permissions	-rw-r--r--