isabelle: src/ZF/Resid/Confluence.thy@922f944f03b2 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: Confluence.thy
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Ole Rasmussen
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	5	Logic Image: ZF
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	6	*)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	7
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 13339 diff changeset	8	theory Confluence imports Reduction begin
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	9
24893 b8ef7afe3a6b modernized specifications; wenzelm parents: 22808 diff changeset	10	definition
b8ef7afe3a6b modernized specifications; wenzelm parents: 22808 diff changeset	11	confluence :: "i=>o" where
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	12	"confluence(R) ==
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	13	\<forall>x y. <x,y> \<in> R --> (\<forall>z.<x,z> \<in> R --> (\<exists>u.<y,u> \<in> R & <z,u> \<in> R))"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	14
24893 b8ef7afe3a6b modernized specifications; wenzelm parents: 22808 diff changeset	15	definition
b8ef7afe3a6b modernized specifications; wenzelm parents: 22808 diff changeset	16	strip :: "o" where
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	17	"strip == \<forall>x y. (x ===> y) -->
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	18	(\<forall>z.(x =1=> z) --> (\<exists>u.(y =1=> u) & (z===>u)))"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	19
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	20
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	21	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	22	(* strip lemmas *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	23	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	24
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	25	lemma strip_lemma_r:
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	26	"[\|confluence(Spar_red1)\|]==> strip"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	27	apply (unfold confluence_def strip_def)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	28	apply (rule impI [THEN allI, THEN allI])
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	29	apply (erule Spar_red.induct, fast)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	30	apply (fast intro: Spar_red.trans)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	31	done
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	32
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	33
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	34	lemma strip_lemma_l:
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	35	"strip==> confluence(Spar_red)"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	36	apply (unfold confluence_def strip_def)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	37	apply (rule impI [THEN allI, THEN allI])
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	38	apply (erule Spar_red.induct, blast)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	39	apply clarify
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	40	apply (blast intro: Spar_red.trans)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	41	done
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	42
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	43	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	44	(* Confluence *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	45	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	46
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	47
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	48	lemma parallel_moves: "confluence(Spar_red1)"
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	49	apply (unfold confluence_def, clarify)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	50	apply (frule simulation)
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	51	apply (frule_tac n = z in simulation, clarify)
0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	52	apply (frule_tac v = va in paving)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	53	apply (force intro: completeness)+
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	54	done
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	55
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	56	lemmas confluence_parallel_reduction =
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	57	parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	58
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	59	lemma lemma1: "[\|confluence(Spar_red)\|]==> confluence(Sred)"
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	60	by (unfold confluence_def, blast intro: par_red_red red_par_red)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	61
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	62	lemmas confluence_beta_reduction =
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	63	confluence_parallel_reduction [THEN lemma1, standard]
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	64
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	65
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	66	(** Conversion **)
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	67
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	68	consts
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	69	Sconv1 :: "i"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	70	Sconv :: "i"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	71
22808 a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	72	abbreviation
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	73	Sconv1_rel (infixl "<-1->" 50) where
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	74	"a<-1->b == <a,b> \<in> Sconv1"
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	75
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	76	abbreviation
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	77	Sconv_rel (infixl "<--->" 50) where
a7daa74e2980 eliminated unnamed infixes, tuned syntax; wenzelm parents: 16417 diff changeset	78	"a<--->b == <a,b> \<in> Sconv"
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	79
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	80	inductive
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	81	domains "Sconv1" <= "lambda*lambda"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	82	intros
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	83	red1: "m -1-> n ==> m<-1->n"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	84	expl: "n -1-> m ==> m<-1->n"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	85	type_intros red1D1 red1D2 lambda.intros bool_typechecks
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	86
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	87	declare Sconv1.intros [intro]
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	88
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	89	inductive
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	90	domains "Sconv" <= "lambda*lambda"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	91	intros
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	92	one_step: "m<-1->n ==> m<--->n"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	93	refl: "m \<in> lambda ==> m<--->m"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	94	trans: "[\|m<--->n; n<--->p\|] ==> m<--->p"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	95	type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	96
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	97	declare Sconv.intros [intro]
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	98
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	99	lemma conv_sym: "m<--->n ==> n<--->m"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	100	apply (erule Sconv.induct)
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 12593 diff changeset	101	apply (erule Sconv1.induct, blast+)
12593 cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	102	done
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	103
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	104	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	105	(* Church_Rosser Theorem *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	106	(* ------------------------------------------------------------------------- *)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	107
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	108	lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)"
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	109	apply (erule Sconv.induct)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	110	apply (erule Sconv1.induct)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	111	apply (blast intro: red1D1 redD2)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	112	apply (blast intro: red1D1 redD2)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	113	apply (blast intro: red1D1 redD2)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	114	apply (cut_tac confluence_beta_reduction)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	115	apply (unfold confluence_def)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	116	apply (blast intro: Sred.trans)
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	117	done
cd35fe5947d4 Resid converted to Isar/ZF paulson parents: 11319 diff changeset	118
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	119	end
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	120

author	nipkow
	Mon, 02 Mar 2009 16:53:55 +0100
changeset 30198	922f944f03b2
parent 24893	b8ef7afe3a6b
child 35762	af3ff2ba4c54
permissions	-rw-r--r--