1 open I; |
1 open I; |
2 |
|
3 Unify.trace_bound := 45; |
|
4 Unify.search_bound := 50; |
|
5 |
2 |
6 goal thy |
3 goal thy |
7 "! a m s s' t n. \ |
4 "! a m s s' t n. \ |
8 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
5 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
9 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |
6 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |
10 by (expr.induct_tac "e" 1); |
7 by (expr.induct_tac "e" 1); |
11 |
8 |
12 (* case Var n *) |
9 (* case Var n *) |
13 by (simp_tac (!simpset addsimps [app_subst_list] |
10 by (simp_tac (!simpset addsimps [app_subst_list] |
14 setloop (split_tac [expand_if])) 1); |
11 setloop (split_tac [expand_if])) 1); |
15 by (fast_tac (HOL_cs addss !simpset) 1); |
12 by (fast_tac (HOL_cs addss !simpset) 1); |
16 |
13 |
17 (* case Abs e *) |
14 (* case Abs e *) |
18 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
15 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
19 by (strip_tac 1); |
16 by (strip_tac 1); |
20 by (rtac conjI 1); |
17 by (rtac conjI 1); |
|
18 by (strip_tac 1); |
|
19 by (REPEAT (etac allE 1)); |
|
20 by (etac impE 1); |
|
21 by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); |
|
22 by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, |
|
23 less_imp_le,lessI]) 1); |
21 |
24 |
22 by (strip_tac 1); |
25 by (strip_tac 1); |
23 by (REPEAT (etac allE 1)); |
26 by (REPEAT (etac allE 1)); |
24 by (etac impE 1); |
27 by (etac impE 1); |
25 by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); |
28 by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); |
26 by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, |
29 by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, |
27 less_imp_le,lessI]) 1); |
30 less_imp_le,lessI]) 1); |
28 |
|
29 by (strip_tac 1); |
|
30 by (REPEAT (etac allE 1)); |
|
31 by (etac impE 1); |
|
32 by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); |
|
33 by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, |
|
34 less_imp_le,lessI]) 1); |
|
35 |
31 |
36 (* case App e1 e2 *) |
32 (* case App e1 e2 *) |
37 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
33 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
38 by (strip_tac 1); |
34 by (strip_tac 1); |
39 by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1); |
35 by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1); |
40 by (rtac conjI 1); |
36 by (rtac conjI 1); |
41 by (fast_tac (HOL_cs addss !simpset) 1); |
37 by (fast_tac (HOL_cs addss !simpset) 1); |
42 |
|
43 by (strip_tac 1); |
38 by (strip_tac 1); |
44 by (rename_tac "s1 t1' n1'" 1); |
39 by (rename_tac "s1 t1' n1'" 1); |
45 by (eres_inst_tac [("x","a")] allE 1); |
40 by (eres_inst_tac [("x","a")] allE 1); |
46 by (eres_inst_tac [("x","m")] allE 1); |
41 by (eres_inst_tac [("x","m")] allE 1); |
47 by (eres_inst_tac [("x","s")] allE 1); |
42 by (eres_inst_tac [("x","s")] allE 1); |
52 by (eres_inst_tac [("x","n1")] allE 1); |
47 by (eres_inst_tac [("x","n1")] allE 1); |
53 by (eres_inst_tac [("x","s1'")] allE 1); |
48 by (eres_inst_tac [("x","s1'")] allE 1); |
54 by (eres_inst_tac [("x","s2'")] allE 1); |
49 by (eres_inst_tac [("x","s2'")] allE 1); |
55 by (eres_inst_tac [("x","t2")] allE 1); |
50 by (eres_inst_tac [("x","t2")] allE 1); |
56 by (eres_inst_tac [("x","n2")] allE 1); |
51 by (eres_inst_tac [("x","n2")] allE 1); |
57 |
|
58 by (rtac conjI 1); |
52 by (rtac conjI 1); |
|
53 by (strip_tac 1); |
|
54 by (mp_tac 1); |
|
55 by (mp_tac 1); |
|
56 by (etac exE 1); |
|
57 by (etac conjE 1); |
|
58 by (etac impE 1); |
|
59 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
|
60 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
|
61 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
|
62 addss !simpset) 1); |
|
63 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1); |
|
64 by (strip_tac 1); |
|
65 by (rename_tac "s2 t2' n2'" 1); |
|
66 by (rtac conjI 1); |
|
67 by (strip_tac 1); |
|
68 by (mp_tac 1); |
|
69 by (mp_tac 1); |
|
70 by (etac exE 1); |
|
71 by (etac conjE 1); |
|
72 by (etac impE 1); |
|
73 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
|
74 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
|
75 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
|
76 addss !simpset) 1); |
|
77 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1); |
59 by (strip_tac 1); |
78 by (strip_tac 1); |
60 by (mp_tac 1); |
79 by (mp_tac 1); |
61 by (mp_tac 1); |
80 by (mp_tac 1); |
62 by (etac exE 1); |
81 by (etac exE 1); |
63 by (etac conjE 1); |
82 by (etac conjE 1); |
64 by (etac impE 1); |
83 by (etac impE 1); |
65 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
84 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
66 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
85 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
67 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
86 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
68 addss !simpset) 1); |
87 addss !simpset) 1); |
69 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1); |
|
70 |
|
71 by (strip_tac 1); |
|
72 by (rename_tac "s2 t2' n2'" 1); |
|
73 by (rtac conjI 1); |
|
74 by (strip_tac 1); |
|
75 by (mp_tac 1); |
|
76 by (mp_tac 1); |
|
77 by (etac exE 1); |
|
78 by (etac conjE 1); |
|
79 by (etac impE 1); |
|
80 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
|
81 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
|
82 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
|
83 addss !simpset) 1); |
|
84 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1); |
|
85 |
|
86 by (strip_tac 1); |
|
87 by (mp_tac 1); |
|
88 by (mp_tac 1); |
|
89 by (etac exE 1); |
|
90 by (etac conjE 1); |
|
91 by (etac impE 1); |
|
92 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
|
93 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
|
94 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
|
95 addss !simpset) 1); |
|
96 |
|
97 by (mp_tac 1); |
88 by (mp_tac 1); |
98 by (REPEAT (eresolve_tac [exE,conjE] 1)); |
89 by (REPEAT (eresolve_tac [exE,conjE] 1)); |
99 by (REPEAT |
90 by (REPEAT(EVERY1 |
100 ((asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]) 1) THEN |
91 [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]), |
101 (REPEAT (etac conjE 1)) THEN (hyp_subst_tac 1) )); |
92 REPEAT o etac conjE, hyp_subst_tac])); |
102 by (rtac exI 1); |
93 by (rtac exI 1); |
103 by (safe_tac HOL_cs); |
94 by (safe_tac HOL_cs); |
104 by (fast_tac HOL_cs 1); |
95 by (fast_tac HOL_cs 1); |
105 by (Simp_tac 2); |
96 by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2); |
106 |
|
107 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1); |
97 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1); |
108 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
98 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
109 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
99 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
110 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
100 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
111 by (safe_tac HOL_cs); |
101 by (safe_tac HOL_cs); |
112 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
102 by (fast_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
113 addss !simpset) 1); |
103 addss !simpset) 1); |
114 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
104 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
115 addss !simpset) 1); |
105 addss !simpset) 1); |
116 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1); |
106 by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1); |
117 by ((dtac new_tv_subst_tel 1) THEN (atac 1)); |
107 by ((dtac new_tv_subst_tel 1) THEN (atac 1)); |
118 by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1)); |
108 by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1)); |
119 by ((dtac new_tv_subst_tel 1) THEN (atac 1)); |
109 by ((dtac new_tv_subst_tel 1) THEN (atac 1)); |
120 by (fast_tac (HOL_cs addDs [new_tv_W] addss |
110 by (fast_tac (HOL_cs addDs [new_tv_W] addss |
121 (!simpset addsimps [subst_comp_tel])) 1); |
111 (!simpset addsimps [subst_comp_tel])) 1); |
122 |
|
123 qed_spec_mp "I_correct_wrt_W"; |
112 qed_spec_mp "I_correct_wrt_W"; |