equal
deleted
inserted
replaced
31 qed "subcls1_wfD"; |
31 qed "subcls1_wfD"; |
32 |
32 |
33 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] |
33 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] |
34 "\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [ |
34 "\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [ |
35 pair_tac "r" 1, |
35 pair_tac "r" 1, |
36 Asm_full_simp_tac 1, |
36 asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]); |
37 strip_tac1 1, |
|
38 option_case_tac 1, |
|
39 Fast_tac 1]); |
|
40 |
37 |
41 Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+"; |
38 Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+"; |
42 by(etac tranclE 1); |
39 by(etac tranclE 1); |
43 by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans]))); |
40 by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans]))); |
44 qed "subcls_asym"; |
41 qed "subcls_asym"; |