isabelle: src/ZF/Resid/Conversion.ML@a5839ecee7b8 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	1	(* Title: Conversion.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 Conversion;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	10	AddIs (Sconv.intrs @ Sconv1.intrs);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	11
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	goal Conversion.thy
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	13	"!!u. m<--->n ==> n<--->m";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	14	by (etac Sconv.induct 1);
38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	15	by (etac Sconv1.induct 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	16	by (ALLGOALS Blast_tac);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	17	qed "conv_sym";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	(* Church_Rosser Theorem *)
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	goal Conversion.thy
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	24	"!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	25	by (etac Sconv.induct 1);
38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	26	by (etac Sconv1.induct 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	27	by (blast_tac (!claset addIs [red1D1,redD2]) 1);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	28	by (blast_tac (!claset addIs [red1D1,redD2]) 1);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	29	by (blast_tac (!claset addIs [red1D1,redD2]) 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	30	by (cut_facts_tac [confluence_beta_reduction] 1);
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	31	by (rewtac confluence_def);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	32	by (blast_tac (!claset addIs [Sred.trans]) 1);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	33	qed "Church_Rosser";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	34

author	wenzelm
	Wed, 15 Oct 1997 15:12:59 +0200
changeset 3872	a5839ecee7b8
parent 3840	e0baea4d485a
child 4091	771b1f6422a8
permissions	-rw-r--r--