isabelle: src/ZF/Resid/Confluence.thy@330eb65c9469 (annotated)

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

author	wenzelm
	Sun, 28 Nov 2010 21:07:28 +0100
changeset 40800	330eb65c9469
parent 35762	af3ff2ba4c54
child 45602	2a858377c3d2
permissions	-rw-r--r--