equal
deleted
inserted
replaced
24 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1); |
24 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1); |
25 qed "sup_PTS_eq"; |
25 qed "sup_PTS_eq"; |
26 |
26 |
27 |
27 |
28 |
28 |
29 Goal |
29 Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])"; |
30 "CFS \\<turnstile> [] <=l XT = (XT=[])"; |
30 by(Simp_tac 1); |
31 by (case_tac "XT=[]" 1); |
|
32 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1); |
|
33 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1); |
|
34 qed "sup_loc_Nil"; |
31 qed "sup_loc_Nil"; |
|
32 AddIffs [sup_loc_Nil]; |
35 |
33 |
36 Goal |
34 |
|
35 Goalw [sup_loc_def] |
37 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
36 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
38 by (case_tac "XT=[]" 1); |
37 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1); |
39 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1); |
|
40 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1); |
|
41 qed "sup_loc_Cons"; |
38 qed "sup_loc_Cons"; |
|
39 AddIffs [sup_loc_Cons]; |