7 val widen_PrimT_conv1 = |
7 val widen_PrimT_conv1 = |
8 prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)" |
8 prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)" |
9 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"]; |
9 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"]; |
10 Addsimps [widen_PrimT_conv1]; |
10 Addsimps [widen_PrimT_conv1]; |
11 |
11 |
12 Goalw [sup_ty_opt_def] "(G \\<turnstile> any >= None) = (any = None)"; |
12 Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)"; |
13 by(simp_tac (simpset() addsplits [option.split]) 1); |
13 by(simp_tac (simpset() addsplits [option.split]) 1); |
14 qed "anyConvNone"; |
14 qed "anyConvNone"; |
15 Addsimps [anyConvNone]; |
15 Addsimps [anyConvNone]; |
16 |
16 |
17 Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty >= Some ty') = (G \\<turnstile> ty' \\<preceq> ty)"; |
17 Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)"; |
18 by(Simp_tac 1); |
18 by(Simp_tac 1); |
19 qed "SomeanyConvSome"; |
19 qed "SomeanyConvSome"; |
20 Addsimps [SomeanyConvSome]; |
20 Addsimps [SomeanyConvSome]; |
21 |
21 |
22 Goal |
22 Goal |
23 "(G \\<turnstile> X >= Some(PrimT Integer)) = (X=None \\<or> (X=Some(PrimT Integer)))"; |
23 "(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))"; |
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 Goal |
30 "CFS \\<turnstile> XT >>= [] = (XT=[])"; |
30 "CFS \\<turnstile> [] <=l XT = (XT=[])"; |
31 by (case_tac "XT=[]" 1); |
31 by (case_tac "XT=[]" 1); |
32 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 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); |
33 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1); |
34 qed "sup_loc_Nil"; |
34 qed "sup_loc_Nil"; |
35 |
35 |
36 Goal |
36 Goal |
37 "CFS \\<turnstile> XT >>= (Y#YT) = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> X>=Y \\<and> CFS \\<turnstile> XT'>>=YT)"; |
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')"; |
38 by (case_tac "XT=[]" 1); |
38 by (case_tac "XT=[]" 1); |
39 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 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); |
40 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1); |
41 qed "sup_loc_Cons"; |
41 qed "sup_loc_Cons"; |