author | nipkow |
Thu, 29 Jun 1995 16:53:01 +0200 | |
changeset 1172 | ab725b698cb2 |
parent 1156 | b373cb33352f |
child 1266 | 3ae9fe3c0f68 |
permissions | -rw-r--r-- |
1120 | 1 |
(* Title: HOL/Lambda/ParRed.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Properties of => and cd, in particular the diamond property of => and |
|
7 |
confluence of beta. |
|
8 |
*) |
|
9 |
||
10 |
open ParRed; |
|
11 |
||
12 |
val parred_ss = lambda_ss addsimps |
|
13 |
par_beta.intrs @ [cd_Var,cd_Fun]; |
|
14 |
||
15 |
val par_beta_cases = map (par_beta.mk_cases db.simps) |
|
16 |
["Var n => t", "Fun s => Fun t", |
|
17 |
"(Fun s) @ t => u", "s @ t => u", "Fun s => t"]; |
|
18 |
||
19 |
val parred_cs = lambda_cs addSIs par_beta.intrs addSEs par_beta_cases; |
|
20 |
||
21 |
(*** beta <= par_beta <= beta^* ***) |
|
22 |
||
23 |
goal ParRed.thy "(Var n => t) = (t = Var n)"; |
|
24 |
by(fast_tac parred_cs 1); |
|
25 |
qed "par_beta_varL"; |
|
26 |
val parred_ss = parred_ss addsimps [par_beta_varL]; |
|
27 |
||
28 |
goal ParRed.thy "t => t"; |
|
29 |
by(db.induct_tac "t" 1); |
|
30 |
by(ALLGOALS(asm_simp_tac parred_ss)); |
|
31 |
qed"par_beta_refl"; |
|
32 |
val parred_ss = parred_ss addsimps [par_beta_refl]; |
|
33 |
||
34 |
goal ParRed.thy "beta <= par_beta"; |
|
35 |
br subsetI 1; |
|
36 |
by (res_inst_tac[("p","x")]PairE 1); |
|
37 |
by (hyp_subst_tac 1); |
|
38 |
be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
39 |
by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl]))); |
|
40 |
qed "beta_subset_par_beta"; |
|
41 |
||
42 |
goal ParRed.thy "par_beta <= beta^*"; |
|
43 |
br subsetI 1; |
|
44 |
by (res_inst_tac[("p","x")]PairE 1); |
|
45 |
by (hyp_subst_tac 1); |
|
46 |
be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
47 |
by (ALLGOALS(fast_tac (parred_cs addIs |
|
48 |
[rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl, |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
49 |
rtrancl_into_rtrancl] addEs [rtrancl_trans]))); |
1120 | 50 |
qed "par_beta_subset_beta"; |
51 |
||
52 |
(*** => ***) |
|
53 |
||
1172 | 54 |
goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n"; |
55 |
by(db.induct_tac "t" 1); |
|
1120 | 56 |
by(ALLGOALS(fast_tac (parred_cs addss parred_ss))); |
57 |
bind_thm("par_beta_lift", result() RS spec RS spec RS mp); |
|
58 |
val parred_ss = parred_ss addsimps [par_beta_lift]; |
|
59 |
||
60 |
goal ParRed.thy |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
61 |
"!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; |
1120 | 62 |
by(db.induct_tac "t" 1); |
63 |
by(asm_simp_tac (addsplit parred_ss) 1); |
|
64 |
by(strip_tac 1); |
|
65 |
bes par_beta_cases 1; |
|
66 |
by(asm_simp_tac parred_ss 1); |
|
67 |
by(asm_simp_tac parred_ss 1); |
|
68 |
br (zero_less_Suc RS subst_subst RS subst) 1; |
|
69 |
by(fast_tac (parred_cs addSIs [par_beta_lift] addss parred_ss) 1); |
|
70 |
by(fast_tac (parred_cs addss parred_ss) 1); |
|
71 |
bind_thm("par_beta_subst", |
|
72 |
result() RS spec RS spec RS spec RS spec RS mp RS mp); |
|
73 |
||
1156 | 74 |
(*** Confluence (directly) ***) |
75 |
||
76 |
goalw ParRed.thy [diamond_def] "diamond(par_beta)"; |
|
77 |
by(REPEAT(rtac allI 1)); |
|
78 |
br impI 1; |
|
79 |
be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
|
80 |
by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst]))); |
|
81 |
qed "diamond_par_beta"; |
|
82 |
||
83 |
||
84 |
(*** cd ***) |
|
85 |
||
86 |
goal ParRed.thy "cd(Var n @ t) = Var n @ cd t"; |
|
87 |
by(simp_tac (parred_ss addsimps [cd_App]) 1); |
|
88 |
qed"cd_App_Var"; |
|
89 |
||
90 |
goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t"; |
|
91 |
by(simp_tac (parred_ss addsimps [cd_App]) 1); |
|
92 |
qed"cd_App_App"; |
|
93 |
||
94 |
goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]"; |
|
95 |
by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1); |
|
96 |
qed"cd_App_Fun"; |
|
97 |
||
98 |
val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun]; |
|
99 |
||
1120 | 100 |
goal ParRed.thy "!t. s => t --> t => cd s"; |
101 |
by(db.induct_tac "s" 1); |
|
102 |
by(simp_tac parred_ss 1); |
|
103 |
be rev_mp 1; |
|
104 |
by(db.induct_tac "db1" 1); |
|
105 |
by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss parred_ss))); |
|
106 |
bind_thm("par_beta_cd", result() RS spec RS mp); |
|
107 |
||
1156 | 108 |
(*** Confluence (via cd) ***) |
1120 | 109 |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
110 |
goalw ParRed.thy [diamond_def] "diamond(par_beta)"; |
1120 | 111 |
by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); |
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
112 |
qed "diamond_par_beta"; |
1120 | 113 |
|
114 |
goal ParRed.thy "confluent(beta)"; |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
115 |
by(fast_tac (HOL_cs addIs [diamond_par_beta,diamond_to_confluence, |
1120 | 116 |
par_beta_subset_beta,beta_subset_par_beta]) 1); |
117 |
qed"beta_confluent"; |