author | wenzelm |
Mon, 03 Nov 1997 12:24:13 +0100 | |
changeset 4091 | 771b1f6422a8 |
parent 3840 | e0baea4d485a |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: Conversion.ML |
1048 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
8 |
open Conversion; |
|
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 | 11 |
|
12 |
goal Conversion.thy |
|
3840 | 13 |
"!!u. m<--->n ==> n<--->m"; |
1732 | 14 |
by (etac Sconv.induct 1); |
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 | 18 |
|
19 |
(* ------------------------------------------------------------------------- *) |
|
20 |
(* Church_Rosser Theorem *) |
|
21 |
(* ------------------------------------------------------------------------- *) |
|
22 |
||
23 |
goal Conversion.thy |
|
3840 | 24 |
"!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)"; |
1732 | 25 |
by (etac Sconv.induct 1); |
26 |
by (etac Sconv1.induct 1); |
|
4091 | 27 |
by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
28 |
by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
|
29 |
by (blast_tac (claset() addIs [red1D1,redD2]) 1); |
|
1048 | 30 |
by (cut_facts_tac [confluence_beta_reduction] 1); |
1461 | 31 |
by (rewtac confluence_def); |
4091 | 32 |
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
|
33 |
qed "Church_Rosser"; |
1048 | 34 |