equal
deleted
inserted
replaced
20 (* -------------- step case ---------------- *) |
20 (* -------------- step case ---------------- *) |
21 by (REPEAT (rtac allI 1)); |
21 by (REPEAT (rtac allI 1)); |
22 by (rtac imp_conj_lemma 1); |
22 by (rtac imp_conj_lemma 1); |
23 by (simp_tac (simpset() addsimps [trans_of_def, |
23 by (simp_tac (simpset() addsimps [trans_of_def, |
24 C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); |
24 C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); |
|
25 by (induct_tac "a" 1); |
25 by (simp_tac (simpset() addsimps [h_abs_def]) 1); |
26 by (simp_tac (simpset() addsimps [h_abs_def]) 1); |
26 by (induct_tac "a" 1); |
|
27 by Auto_tac; |
|
28 qed"h_abs_is_abstraction"; |
27 qed"h_abs_is_abstraction"; |
29 |
28 |
30 |
29 |
31 Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"; |
30 Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"; |
32 by (rtac AbsRuleT1 1); |
31 by (rtac AbsRuleT1 1); |