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
     1 (*  Title:      HOL/Lambda/ParRed.ML
     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 Addsimps par_beta.intrs;
    13 
    14 val par_beta_cases = map (par_beta.mk_cases dB.simps)
    15     ["Var n => t", "Abs s => Abs t",
    16      "(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
    17 
    18 AddSIs par_beta.intrs;
    19 AddSEs par_beta_cases;
    20 
    21 (*** beta <= par_beta <= beta^* ***)
    22 
    23 goal ParRed.thy "(Var n => t) = (t = Var n)";
    24 by (Blast_tac 1);
    25 qed "par_beta_varL";
    26 Addsimps [par_beta_varL];
    27 
    28 goal ParRed.thy "t => t";
    29 by (dB.induct_tac "t" 1);
    30 by (ALLGOALS Asm_simp_tac);
    31 qed"par_beta_refl";
    32 Addsimps [par_beta_refl];
    33 (* AddSIs [par_beta_refl]; causes search to blow up *)
    34 
    35 goal ParRed.thy "beta <= par_beta";
    36 by (rtac subsetI 1);
    37 by (split_all_tac 1);
    38 by (etac beta.induct 1);
    39 by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl])));
    40 qed "beta_subset_par_beta";
    41 
    42 goal ParRed.thy "par_beta <= beta^*";
    43 by (rtac subsetI 1);
    44 by (split_all_tac 1);
    45 by (etac par_beta.induct 1);
    46 by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl] 
    47                                      addEs [rtrancl_trans])));
    48 qed "par_beta_subset_beta";
    49 
    50 (*** => ***)
    51 
    52 goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
    53 by (dB.induct_tac "t" 1);
    54 by (ALLGOALS(fast_tac (!claset addss (!simpset))));
    55 qed_spec_mp "par_beta_lift";
    56 Addsimps [par_beta_lift];
    57 
    58 goal ParRed.thy
    59   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
    60 by (dB.induct_tac "t" 1);
    61   by (asm_simp_tac (addsplit(!simpset)) 1);
    62  by (strip_tac 1);
    63  by (eresolve_tac par_beta_cases 1);
    64   by (Asm_simp_tac 1);
    65  by (asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
    66  by (fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
    67 by (fast_tac (!claset addss (!simpset)) 1);
    68 qed_spec_mp "par_beta_subst";
    69 
    70 (*** Confluence (directly) ***)
    71 
    72 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    73 by (rtac (impI RS allI RS allI) 1);
    74 by (etac par_beta.induct 1);
    75 by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
    76 qed "diamond_par_beta";
    77 
    78 
    79 (*** cd ***)
    80 
    81 goal ParRed.thy "!t. s => t --> t => cd s";
    82 by (dB.induct_tac "s" 1);
    83   by (Simp_tac 1);
    84  by (etac rev_mp 1);
    85  by (dB.induct_tac "dB1" 1);
    86  by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] 
    87                                 unsafe_addss (!simpset))));
    88 qed_spec_mp "par_beta_cd";
    89 
    90 (*** Confluence (via cd) ***)
    91 
    92 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    93 by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
    94 qed "diamond_par_beta2";
    95 
    96 goal ParRed.thy "confluent(beta)";
    97 by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
    98 			     par_beta_subset_beta, beta_subset_par_beta]) 1);
    99 qed"beta_confluent";