57 Addsimps [par_beta_lift]; |
57 Addsimps [par_beta_lift]; |
58 |
58 |
59 goal ParRed.thy |
59 goal ParRed.thy |
60 "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; |
60 "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; |
61 by(db.induct_tac "t" 1); |
61 by(db.induct_tac "t" 1); |
62 by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
62 by(asm_simp_tac (addsplit(!simpset)) 1); |
63 by(strip_tac 1); |
63 by(strip_tac 1); |
64 bes par_beta_cases 1; |
64 bes par_beta_cases 1; |
65 by(Asm_simp_tac 1); |
65 by(Asm_simp_tac 1); |
66 by(Asm_simp_tac 1); |
66 by(Asm_simp_tac 1); |
67 br (zero_less_Suc RS subst_subst RS subst) 1; |
67 br (zero_less_Suc RS subst_subst RS subst) 1; |
70 bind_thm("par_beta_subst", |
70 bind_thm("par_beta_subst", |
71 result() RS spec RS spec RS spec RS spec RS mp RS mp); |
71 result() RS spec RS spec RS spec RS spec RS mp RS mp); |
72 |
72 |
73 (*** Confluence (directly) ***) |
73 (*** Confluence (directly) ***) |
74 |
74 |
75 goalw ParRed.thy [diamond_def] "diamond(par_beta)"; |
75 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
76 by(REPEAT(rtac allI 1)); |
76 by(REPEAT(rtac allI 1)); |
77 br impI 1; |
77 br impI 1; |
78 be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
78 be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; |
79 by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst]))); |
79 by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst]))); |
80 qed "diamond_par_beta"; |
80 qed "diamond_par_beta"; |
81 |
81 |
82 |
82 |
83 (*** cd ***) |
83 (*** cd ***) |
84 |
|
85 goal ParRed.thy "cd(Var n @ t) = Var n @ cd t"; |
|
86 by(Simp_tac 1); |
|
87 qed"cd_App_Var"; |
|
88 |
|
89 goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t"; |
|
90 by(Simp_tac 1); |
|
91 qed"cd_App_App"; |
|
92 |
|
93 goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]"; |
|
94 by(Simp_tac 1); |
|
95 qed"cd_App_Fun"; |
|
96 |
|
97 Addsimps [cd_App_Var,cd_App_App,cd_App_Fun]; |
|
98 |
84 |
99 goal ParRed.thy "!t. s => t --> t => cd s"; |
85 goal ParRed.thy "!t. s => t --> t => cd s"; |
100 by(db.induct_tac "s" 1); |
86 by(db.induct_tac "s" 1); |
101 by(Simp_tac 1); |
87 by(Simp_tac 1); |
102 be rev_mp 1; |
88 be rev_mp 1; |
104 by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset)))); |
90 by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset)))); |
105 bind_thm("par_beta_cd", result() RS spec RS mp); |
91 bind_thm("par_beta_cd", result() RS spec RS mp); |
106 |
92 |
107 (*** Confluence (via cd) ***) |
93 (*** Confluence (via cd) ***) |
108 |
94 |
109 goalw ParRed.thy [diamond_def] "diamond(par_beta)"; |
95 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
110 by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); |
96 by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); |
111 qed "diamond_par_beta2"; |
97 qed "diamond_par_beta2"; |
112 |
98 |
113 goal ParRed.thy "confluent(beta)"; |
99 goal ParRed.thy "confluent(beta)"; |
114 by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, |
100 by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, |