src/HOL/Lambda/ParRed.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2891 d8f254ad1ab9
child 2922 580647a879cf
permissions -rw-r--r--
Dep. on Provers/nat_transitive
nipkow@1288
     1
(*  Title:      HOL/Lambda/ParRed.ML
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
nipkow@1120
     6
Properties of => and cd, in particular the diamond property of => and
nipkow@1120
     7
confluence of beta.
nipkow@1120
     8
*)
nipkow@1120
     9
nipkow@1120
    10
open ParRed;
nipkow@1120
    11
clasohm@1266
    12
Addsimps par_beta.intrs;
nipkow@1120
    13
nipkow@2159
    14
val par_beta_cases = map (par_beta.mk_cases dB.simps)
nipkow@2159
    15
    ["Var n => t", "Abs s => Abs t",
nipkow@2159
    16
     "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
nipkow@1120
    17
nipkow@1974
    18
AddSIs par_beta.intrs;
nipkow@1974
    19
AddSEs par_beta_cases;
nipkow@1120
    20
nipkow@1120
    21
(*** beta <= par_beta <= beta^* ***)
nipkow@1120
    22
nipkow@1120
    23
goal ParRed.thy "(Var n => t) = (t = Var n)";
paulson@2891
    24
by (Blast_tac 1);
nipkow@1120
    25
qed "par_beta_varL";
clasohm@1266
    26
Addsimps [par_beta_varL];
nipkow@1120
    27
nipkow@1120
    28
goal ParRed.thy "t => t";
nipkow@2159
    29
by (dB.induct_tac "t" 1);
paulson@2031
    30
by (ALLGOALS Asm_simp_tac);
nipkow@1120
    31
qed"par_beta_refl";
clasohm@1266
    32
Addsimps [par_beta_refl];
nipkow@1974
    33
(* AddSIs [par_beta_refl]; causes search to blow up *)
nipkow@1120
    34
nipkow@1120
    35
goal ParRed.thy "beta <= par_beta";
clasohm@1465
    36
by (rtac subsetI 1);
nipkow@1431
    37
by (split_all_tac 1);
paulson@1730
    38
by (etac beta.induct 1);
paulson@2891
    39
by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl])));
nipkow@1120
    40
qed "beta_subset_par_beta";
nipkow@1120
    41
nipkow@1120
    42
goal ParRed.thy "par_beta <= beta^*";
clasohm@1465
    43
by (rtac subsetI 1);
nipkow@1431
    44
by (split_all_tac 1);
paulson@1730
    45
by (etac par_beta.induct 1);
nipkow@1974
    46
by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl] 
nipkow@1974
    47
                                     addEs [rtrancl_trans])));
nipkow@1120
    48
qed "par_beta_subset_beta";
nipkow@1120
    49
nipkow@1120
    50
(*** => ***)
nipkow@1120
    51
nipkow@1172
    52
goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
nipkow@2159
    53
by (dB.induct_tac "t" 1);
paulson@2031
    54
by (ALLGOALS(fast_tac (!claset addss (!simpset))));
nipkow@1486
    55
qed_spec_mp "par_beta_lift";
clasohm@1266
    56
Addsimps [par_beta_lift];
nipkow@1120
    57
nipkow@1120
    58
goal ParRed.thy
nipkow@1124
    59
  "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
nipkow@2159
    60
by (dB.induct_tac "t" 1);
paulson@2057
    61
  by (asm_simp_tac (addsplit(!simpset)) 1);
paulson@2057
    62
 by (strip_tac 1);
paulson@2057
    63
 by (eresolve_tac par_beta_cases 1);
paulson@2057
    64
  by (Asm_simp_tac 1);
paulson@2057
    65
 by (asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
paulson@2057
    66
 by (fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
paulson@2031
    67
by (fast_tac (!claset addss (!simpset)) 1);
nipkow@1486
    68
qed_spec_mp "par_beta_subst";
nipkow@1120
    69
nipkow@1156
    70
(*** Confluence (directly) ***)
nipkow@1156
    71
nipkow@1269
    72
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
paulson@1730
    73
by (rtac (impI RS allI RS allI) 1);
paulson@1730
    74
by (etac par_beta.induct 1);
paulson@2891
    75
by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
nipkow@1156
    76
qed "diamond_par_beta";
nipkow@1156
    77
nipkow@1156
    78
nipkow@1156
    79
(*** cd ***)
nipkow@1156
    80
nipkow@1120
    81
goal ParRed.thy "!t. s => t --> t => cd s";
nipkow@2159
    82
by (dB.induct_tac "s" 1);
paulson@2057
    83
  by (Simp_tac 1);
paulson@2057
    84
 by (etac rev_mp 1);
nipkow@2159
    85
 by (dB.induct_tac "dB1" 1);
paulson@2891
    86
 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] 
paulson@2891
    87
                                unsafe_addss (!simpset))));
nipkow@1486
    88
qed_spec_mp "par_beta_cd";
nipkow@1120
    89
nipkow@1156
    90
(*** Confluence (via cd) ***)
nipkow@1120
    91
nipkow@1269
    92
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
paulson@2891
    93
by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
clasohm@1266
    94
qed "diamond_par_beta2";
nipkow@1120
    95
nipkow@1120
    96
goal ParRed.thy "confluent(beta)";
paulson@2891
    97
by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
paulson@2891
    98
			     par_beta_subset_beta, beta_subset_par_beta]) 1);
nipkow@1120
    99
qed"beta_confluent";