author | nipkow |
Mon, 13 Jul 1998 16:04:39 +0200 | |
changeset 5134 | 51f81581e3d9 |
parent 5069 | 3ea049f7979d |
child 5146 | 1ea751ae62b2 |
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 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
14 |
val par_beta_cases = map (par_beta.mk_cases dB.simps) |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
15 |
["Var n => t", "Abs s => Abs t", |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
16 |
"(Abs s) @ t => u", "s @ t => u", "Abs s => t"]; |
1120 | 17 |
|
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1730
diff
changeset
|
18 |
AddSIs par_beta.intrs; |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1730
diff
changeset
|
19 |
AddSEs par_beta_cases; |
1120 | 20 |
|
21 |
(*** beta <= par_beta <= beta^* ***) |
|
22 |
||
5069 | 23 |
Goal "(Var n => t) = (t = Var n)"; |
2891 | 24 |
by (Blast_tac 1); |
1120 | 25 |
qed "par_beta_varL"; |
1266 | 26 |
Addsimps [par_beta_varL]; |
1120 | 27 |
|
5069 | 28 |
Goal "t => t"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
29 |
by (dB.induct_tac "t" 1); |
2031 | 30 |
by (ALLGOALS Asm_simp_tac); |
1120 | 31 |
qed"par_beta_refl"; |
1266 | 32 |
Addsimps [par_beta_refl]; |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1730
diff
changeset
|
33 |
(* AddSIs [par_beta_refl]; causes search to blow up *) |
1120 | 34 |
|
5069 | 35 |
Goal "beta <= par_beta"; |
1465 | 36 |
by (rtac subsetI 1); |
1431 | 37 |
by (split_all_tac 1); |
1730 | 38 |
by (etac beta.induct 1); |
4089 | 39 |
by (ALLGOALS(blast_tac (claset() addSIs [par_beta_refl]))); |
1120 | 40 |
qed "beta_subset_par_beta"; |
41 |
||
5069 | 42 |
Goal "par_beta <= beta^*"; |
1465 | 43 |
by (rtac subsetI 1); |
1431 | 44 |
by (split_all_tac 1); |
1730 | 45 |
by (etac par_beta.induct 1); |
2922 | 46 |
by (Blast_tac 1); |
47 |
(* rtrancl_refl complicates the proof by increasing the branching factor*) |
|
4089 | 48 |
by (ALLGOALS (blast_tac (claset() delrules [rtrancl_refl] |
2922 | 49 |
addIs [rtrancl_into_rtrancl]))); |
1120 | 50 |
qed "par_beta_subset_beta"; |
51 |
||
52 |
(*** => ***) |
|
53 |
||
5069 | 54 |
Goal "!t' n. t => t' --> lift t n => lift t' n"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
55 |
by (dB.induct_tac "t" 1); |
4089 | 56 |
by (ALLGOALS(fast_tac (claset() addss (simpset())))); |
1486 | 57 |
qed_spec_mp "par_beta_lift"; |
1266 | 58 |
Addsimps [par_beta_lift]; |
1120 | 59 |
|
5069 | 60 |
Goal |
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]"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2057
diff
changeset
|
62 |
by (dB.induct_tac "t" 1); |
4089 | 63 |
by (asm_simp_tac (addsplit(simpset())) 1); |
2057 | 64 |
by (strip_tac 1); |
65 |
by (eresolve_tac par_beta_cases 1); |
|
66 |
by (Asm_simp_tac 1); |
|
4089 | 67 |
by (asm_simp_tac (simpset() addsimps [subst_subst RS sym]) 1); |
68 |
by (fast_tac (claset() addSIs [par_beta_lift] addss (simpset())) 1); |
|
69 |
by (fast_tac (claset() addss (simpset())) 1); |
|
1486 | 70 |
qed_spec_mp "par_beta_subst"; |
1120 | 71 |
|
1156 | 72 |
(*** Confluence (directly) ***) |
73 |
||
5069 | 74 |
Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
1730 | 75 |
by (rtac (impI RS allI RS allI) 1); |
76 |
by (etac par_beta.induct 1); |
|
4089 | 77 |
by (ALLGOALS(blast_tac (claset() addSIs [par_beta_subst]))); |
1156 | 78 |
qed "diamond_par_beta"; |
79 |
||
80 |
||
81 |
(*** cd ***) |
|
82 |
||
5134 | 83 |
Addsimps cd.rules; |
84 |
||
5069 | 85 |
Goal "!t. s => t --> t => cd s"; |
5134 | 86 |
by(res_inst_tac[("u","s")] cd.induct 1); |
87 |
by(Auto_tac); |
|
88 |
by(fast_tac (claset() addSIs [par_beta_subst]) 1); |
|
1486 | 89 |
qed_spec_mp "par_beta_cd"; |
1120 | 90 |
|
1156 | 91 |
(*** Confluence (via cd) ***) |
1120 | 92 |
|
5069 | 93 |
Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
4089 | 94 |
by (blast_tac (claset() addIs [par_beta_cd]) 1); |
1266 | 95 |
qed "diamond_par_beta2"; |
1120 | 96 |
|
5069 | 97 |
Goal "confluent(beta)"; |
2891 | 98 |
by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence, |
99 |
par_beta_subset_beta, beta_subset_par_beta]) 1); |
|
1120 | 100 |
qed"beta_confluent"; |