isabelle: src/ZF/Resid/Conversion.ML@5f4182667032 (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
5268 59ef39008514 even more tidying of Goal commands paulson parents: 5068 diff changeset	12	Goal "m<--->n ==> n<--->m";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	13	by (etac Sconv.induct 1);
38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	14	by (etac Sconv1.induct 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	15	by (ALLGOALS Blast_tac);
33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	16	qed "conv_sym";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	17
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19	(* Church_Rosser Theorem *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 5268 diff changeset	22	Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	23	by (etac Sconv.induct 1);
38776e927da8 Updated for new form of induction rules paulson parents: 1461 diff changeset	24	by (etac Sconv1.induct 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	25	by (blast_tac (claset() addIs [red1D1,redD2]) 1);
771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	26	by (blast_tac (claset() addIs [red1D1,redD2]) 1);
771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	27	by (blast_tac (claset() addIs [red1D1,redD2]) 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	28	by (cut_facts_tac [confluence_beta_reduction] 1);
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	29	by (rewtac confluence_def);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	30	by (blast_tac (claset() addIs [Sred.trans]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	31	qed "Church_Rosser";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	32

author	wenzelm
	Tue, 11 Dec 2001 16:00:26 +0100
changeset 12466	5f4182667032
parent 11319	8b84ee2cc79c
permissions	-rw-r--r--