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 |
|
2469
|
10 |
val (!simpset) = (!simpset) addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]);
|
1048
|
11 |
|
|
12 |
goal Conversion.thy
|
|
13 |
"!!u.m<--->n ==> n<--->m";
|
1732
|
14 |
by (etac Sconv.induct 1);
|
|
15 |
by (etac Sconv1.induct 1);
|
1048
|
16 |
by (resolve_tac [Sconv.trans] 4);
|
2469
|
17 |
by (ALLGOALS(asm_simp_tac (!simpset) ));
|
1048
|
18 |
val conv_sym = result();
|
|
19 |
|
|
20 |
(* ------------------------------------------------------------------------- *)
|
|
21 |
(* Church_Rosser Theorem *)
|
|
22 |
(* ------------------------------------------------------------------------- *)
|
|
23 |
|
|
24 |
goal Conversion.thy
|
|
25 |
"!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)";
|
1732
|
26 |
by (etac Sconv.induct 1);
|
|
27 |
by (etac Sconv1.induct 1);
|
2469
|
28 |
by (fast_tac (!claset addIs [red1D1,redD2]) 1);
|
|
29 |
by (fast_tac (!claset addIs [red1D1,redD2]) 1);
|
|
30 |
by (fast_tac (!claset addIs [red1D1,redD2]) 1);
|
1048
|
31 |
by (cut_facts_tac [confluence_beta_reduction] 1);
|
1461
|
32 |
by (rewtac confluence_def);
|
2469
|
33 |
by (step_tac (!claset) 1);
|
1048
|
34 |
by (dres_inst_tac [("x4","n"),("x3","pa"),("x1","pb")]
|
|
35 |
(spec RS spec RS mp RS spec RS mp) 1);
|
|
36 |
by (TRYALL assume_tac);
|
2469
|
37 |
by (step_tac (!claset) 1);
|
|
38 |
by (step_tac (!claset) 1);
|
|
39 |
by (step_tac (!claset) 1);
|
1048
|
40 |
by (res_inst_tac [("n","pa")]Sred.trans 1);
|
|
41 |
by (res_inst_tac [("n","pb"),("p","ua")] Sred.trans 3);
|
|
42 |
by (TRYALL assume_tac);
|
|
43 |
val Church_Rosser = result();
|
|
44 |
|