equal
deleted
inserted
replaced
4 Copyright 1998 TU Muenchen |
4 Copyright 1998 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 Goal |
7 Goal |
8 "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)"; |
8 "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)"; |
9 be beta.induct 1; |
9 by (etac beta.induct 1); |
10 by (Asm_full_simp_tac 1); |
10 by (Asm_full_simp_tac 1); |
11 by (rtac allI 1); |
11 by (rtac allI 1); |
12 by (res_inst_tac [("xs","rs")] rev_exhaust 1); |
12 by (res_inst_tac [("xs","rs")] rev_exhaust 1); |
13 by (Asm_full_simp_tac 1); |
13 by (Asm_full_simp_tac 1); |
14 by (force_tac (claset() addIs [append_step1I],simpset()) 1); |
14 by (force_tac (claset() addIs [append_step1I],simpset()) 1); |
26 |
26 |
27 Goal "u -> u' ==> !r rs. u = r$$rs --> \ |
27 Goal "u -> u' ==> !r rs. u = r$$rs --> \ |
28 \ ( (? r'. r -> r' & u' = r'$$rs) | \ |
28 \ ( (? r'. r -> r' & u' = r'$$rs) | \ |
29 \ (? rs'. rs => rs' & u' = r$$rs') | \ |
29 \ (? rs'. rs => rs' & u' = r$$rs') | \ |
30 \ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))"; |
30 \ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))"; |
31 be beta.induct 1; |
31 by (etac beta.induct 1); |
32 by (clarify_tac (claset() delrules [disjCI]) 1); |
32 by (clarify_tac (claset() delrules [disjCI]) 1); |
33 by (exhaust_tac "r" 1); |
33 by (exhaust_tac "r" 1); |
34 by (Asm_full_simp_tac 1); |
34 by (Asm_full_simp_tac 1); |
35 by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1); |
35 by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1); |
36 by (split_asm_tac [split_if_asm] 1); |
36 by (split_asm_tac [split_if_asm] 1); |