5261
|
1 |
(* Title: HOL/Lambda/ListBeta.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
Goal
|
|
8 |
"v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
|
5326
|
9 |
by (etac beta.induct 1);
|
5525
|
10 |
by (Asm_full_simp_tac 1);
|
|
11 |
by (rtac allI 1);
|
|
12 |
by (res_inst_tac [("xs","rs")] rev_exhaust 1);
|
|
13 |
by (Asm_full_simp_tac 1);
|
|
14 |
by (force_tac (claset() addIs [append_step1I],simpset()) 1);
|
|
15 |
by (rtac allI 1);
|
|
16 |
by (res_inst_tac [("xs","rs")] rev_exhaust 1);
|
|
17 |
by (Asm_full_simp_tac 1);
|
|
18 |
by (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3);
|
5261
|
19 |
val lemma = result();
|
|
20 |
|
|
21 |
Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
|
5318
|
22 |
by (dtac lemma 1);
|
|
23 |
by (Blast_tac 1);
|
5261
|
24 |
qed "head_Var_reduction";
|
|
25 |
|
|
26 |
Goal "u -> u' ==> !r rs. u = r$$rs --> \
|
|
27 |
\ ( (? r'. r -> r' & u' = r'$$rs) | \
|
|
28 |
\ (? rs'. rs => rs' & u' = r$$rs') | \
|
|
29 |
\ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
|
5326
|
30 |
by (etac beta.induct 1);
|
5318
|
31 |
by (clarify_tac (claset() delrules [disjCI]) 1);
|
|
32 |
by (exhaust_tac "r" 1);
|
|
33 |
by (Asm_full_simp_tac 1);
|
|
34 |
by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
|
|
35 |
by (split_asm_tac [split_if_asm] 1);
|
|
36 |
by (Asm_full_simp_tac 1);
|
|
37 |
by (Blast_tac 1);
|
|
38 |
by (Asm_full_simp_tac 1);
|
|
39 |
by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
|
|
40 |
by (split_asm_tac [split_if_asm] 1);
|
|
41 |
by (Asm_full_simp_tac 1);
|
|
42 |
by (Asm_full_simp_tac 1);
|
|
43 |
by (clarify_tac (claset() delrules [disjCI]) 1);
|
|
44 |
by (dtac (App_eq_foldl_conv RS iffD1) 1);
|
|
45 |
by (split_asm_tac [split_if_asm] 1);
|
|
46 |
by (Asm_full_simp_tac 1);
|
|
47 |
by (Blast_tac 1);
|
|
48 |
by (force_tac (claset() addIs [disjI1 RS append_step1I],simpset()) 1);
|
|
49 |
by (clarify_tac (claset() delrules [disjCI]) 1);
|
|
50 |
by (dtac (App_eq_foldl_conv RS iffD1) 1);
|
|
51 |
by (split_asm_tac [split_if_asm] 1);
|
|
52 |
by (Asm_full_simp_tac 1);
|
|
53 |
by (Blast_tac 1);
|
5525
|
54 |
by (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3);
|
5261
|
55 |
val lemma = result();
|
|
56 |
|
5455
|
57 |
val major::prems =
|
|
58 |
Goal "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R; \
|
|
59 |
\ !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R; \
|
|
60 |
\ !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |] \
|
|
61 |
\ ==> R";
|
|
62 |
by (cut_facts_tac [major RS lemma RS spec RS spec] 1);
|
|
63 |
by (REPEAT_FIRST (ares_tac [refl] ORELSE'
|
|
64 |
eresolve_tac (prems @ [exE, conjE, impE, disjE])));
|
|
65 |
qed "apps_betasE";
|
5261
|
66 |
AddSEs [apps_betasE];
|
|
67 |
|
|
68 |
Goal "r -> s ==> r$$ss -> s$$ss";
|
5318
|
69 |
by (res_inst_tac [("xs","ss")] rev_induct 1);
|
|
70 |
by (Auto_tac);
|
5261
|
71 |
qed "apps_preserves_beta";
|
|
72 |
Addsimps [apps_preserves_beta];
|
|
73 |
|
|
74 |
Goal "r ->> s ==> r$$ss ->> s$$ss";
|
5318
|
75 |
by (etac rtrancl_induct 1);
|
|
76 |
by (Blast_tac 1);
|
|
77 |
by (blast_tac (claset() addIs [apps_preserves_beta,rtrancl_into_rtrancl]) 1);
|
5261
|
78 |
qed "apps_preserves_beta2";
|
|
79 |
Addsimps [apps_preserves_beta2];
|
|
80 |
|
|
81 |
Goal "!ss. rs => ss --> r$$rs -> r$$ss";
|
5318
|
82 |
by (res_inst_tac [("xs","rs")] rev_induct 1);
|
|
83 |
by (Asm_full_simp_tac 1);
|
|
84 |
by (Asm_full_simp_tac 1);
|
|
85 |
by (Clarify_tac 1);
|
|
86 |
by (res_inst_tac [("xs","ss")] rev_exhaust 1);
|
|
87 |
by (Asm_full_simp_tac 1);
|
|
88 |
by (Asm_full_simp_tac 1);
|
|
89 |
by (dtac Snoc_step1_SnocD 1);
|
|
90 |
by (Blast_tac 1);
|
5261
|
91 |
qed_spec_mp "apps_preserves_betas";
|
|
92 |
Addsimps [apps_preserves_betas];
|