isabelle: src/ZF/Resid/Confluence.ML@34bb65b037dd (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	1	(* Title: Confluence.ML
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 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
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	8	open Confluence;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	10	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	11	(* strip lemmas *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	13
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	14	goalw Confluence.thy [confluence_def,strip_def]
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15	"!!u.[\|confluence(Spar_red1)\|]==> strip";
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	16	by (resolve_tac [impI RS allI RS allI] 1);
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	17	by (etac Spar_red.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1732 diff changeset	18	by (Fast_tac 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	19	by (fast_tac (claset() addIs [Spar_red.trans]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	20	qed "strip_lemma_r";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	22
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	23	goalw Confluence.thy [confluence_def,strip_def]
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	24	"!!u. strip==> confluence(Spar_red)";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	25	by (resolve_tac [impI RS allI RS allI] 1);
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	26	by (etac Spar_red.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1732 diff changeset	27	by (Fast_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	28	by (Clarify_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	29	by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	30	by (REPEAT(eresolve_tac [exE,conjE] 2));
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	31	by (dres_inst_tac [("x1","ua")] (spec RS mp) 2);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	32	by (fast_tac (claset() addIs [Spar_red.trans]) 3);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	33	by (TRYALL assume_tac );
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	34	qed "strip_lemma_l";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	35
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	36	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	37	(* Confluence *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	38	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	39
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	40
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	41	goalw Confluence.thy [confluence_def] "confluence(Spar_red1)";
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	42	by (Clarify_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	43	by (forward_tac [simulation] 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	44	by (forw_inst_tac [("n","z")] simulation 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	45	by (Clarify_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	46	by (forw_inst_tac [("v","va")] paving 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	47	by (TRYALL assume_tac);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	48	by (fast_tac (claset() addIs [completeness] addss (simpset())) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	49	qed "parallel_moves";
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	50
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	51	bind_thm ("confluence_parallel_reduction",
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	52	parallel_moves RS strip_lemma_r RS strip_lemma_l);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	53
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	54	goalw Confluence.thy [confluence_def]
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	55	"!!u.[\|confluence(Spar_red)\|]==> confluence(Sred)";
4152 451104c223e2 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	56	by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	57	val lemma1 = result();
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	58
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	59	bind_thm ("confluence_beta_reduction",
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	60	confluence_parallel_reduction RS lemma1);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	61

author	paulson
	Mon, 01 Dec 1997 12:52:18 +0100
changeset 4331	34bb65b037dd
parent 4152	451104c223e2
child 5068	fb28eaa07e01
permissions	-rw-r--r--