author | nipkow |
Fri, 09 Feb 1996 13:41:59 +0100 | |
changeset 1486 | 7b95d7b49f7a |
parent 1465 | 5d7a7e439cec |
child 1730 | 1c7f793fc374 |
permissions | -rw-r--r-- |
1288 | 1 |
(* Title: HOL/Lambda/ParRed.ML |
1120 | 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 |
||
1266 | 12 |
Addsimps par_beta.intrs; |
1120 | 13 |
|
14 |
val par_beta_cases = map (par_beta.mk_cases db.simps) |
|
15 |
["Var n => t", "Fun s => Fun t", |
|
16 |
"(Fun s) @ t => u", "s @ t => u", "Fun s => t"]; |
|
17 |
||
18 |
val parred_cs = lambda_cs addSIs par_beta.intrs addSEs par_beta_cases; |
|
19 |
||
20 |
(*** beta <= par_beta <= beta^* ***) |
|
21 |
||
22 |
goal ParRed.thy "(Var n => t) = (t = Var n)"; |
|
23 |
by(fast_tac parred_cs 1); |
|
24 |
qed "par_beta_varL"; |
|
1266 | 25 |
Addsimps [par_beta_varL]; |
1120 | 26 |
|
27 |
goal ParRed.thy "t => t"; |
|
28 |
by(db.induct_tac "t" 1); |
|
1266 | 29 |
by(ALLGOALS Asm_simp_tac); |
1120 | 30 |
qed"par_beta_refl"; |
1266 | 31 |
Addsimps [par_beta_refl]; |
1120 | 32 |
|
33 |
goal ParRed.thy "beta <= par_beta"; |
|
1465 | 34 |
by (rtac subsetI 1); |
1431 | 35 |
by (split_all_tac 1); |
1465 | 36 |
by (etac (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); |
1120 | 37 |
by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl]))); |
38 |
qed "beta_subset_par_beta"; |
|
39 |
||
40 |
goal ParRed.thy "par_beta <= beta^*"; |
|
1465 | 41 |
by (rtac subsetI 1); |
1431 | 42 |
by (split_all_tac 1); |
1465 | 43 |
by (etac (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); |
1120 | 44 |
by (ALLGOALS(fast_tac (parred_cs addIs |
45 |
[rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl, |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
46 |
rtrancl_into_rtrancl] addEs [rtrancl_trans]))); |
1120 | 47 |
qed "par_beta_subset_beta"; |
48 |
||
49 |
(*** => ***) |
|
50 |
||
1172 | 51 |
goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n"; |
52 |
by(db.induct_tac "t" 1); |
|
1266 | 53 |
by(ALLGOALS(fast_tac (parred_cs addss (!simpset)))); |
1486 | 54 |
qed_spec_mp "par_beta_lift"; |
1266 | 55 |
Addsimps [par_beta_lift]; |
1120 | 56 |
|
57 |
goal ParRed.thy |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
58 |
"!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; |
1120 | 59 |
by(db.induct_tac "t" 1); |
1269 | 60 |
by(asm_simp_tac (addsplit(!simpset)) 1); |
1120 | 61 |
by(strip_tac 1); |
62 |
bes par_beta_cases 1; |
|
1266 | 63 |
by(Asm_simp_tac 1); |
1288 | 64 |
by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1); |
1266 | 65 |
by(fast_tac (parred_cs addSIs [par_beta_lift] addss (!simpset)) 1); |
66 |
by(fast_tac (parred_cs addss (!simpset)) 1); |
|
1486 | 67 |
qed_spec_mp "par_beta_subst"; |
1120 | 68 |
|
1156 | 69 |
(*** Confluence (directly) ***) |
70 |
||
1269 | 71 |
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
1465 | 72 |
by (rtac par_beta.mutual_induct 1); |
1156 | 73 |
by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst]))); |
74 |
qed "diamond_par_beta"; |
|
75 |
||
76 |
||
77 |
(*** cd ***) |
|
78 |
||
1120 | 79 |
goal ParRed.thy "!t. s => t --> t => cd s"; |
80 |
by(db.induct_tac "s" 1); |
|
1266 | 81 |
by(Simp_tac 1); |
1120 | 82 |
be rev_mp 1; |
83 |
by(db.induct_tac "db1" 1); |
|
1266 | 84 |
by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset)))); |
1486 | 85 |
qed_spec_mp "par_beta_cd"; |
1120 | 86 |
|
1156 | 87 |
(*** Confluence (via cd) ***) |
1120 | 88 |
|
1269 | 89 |
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
1120 | 90 |
by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); |
1266 | 91 |
qed "diamond_par_beta2"; |
1120 | 92 |
|
93 |
goal ParRed.thy "confluent(beta)"; |
|
1266 | 94 |
by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, |
1120 | 95 |
par_beta_subset_beta,beta_subset_par_beta]) 1); |
96 |
qed"beta_confluent"; |