equal
deleted
inserted
replaced
41 "(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))"; |
41 "(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))"; |
42 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1); |
42 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1); |
43 qed "sup_PTS_eq"; |
43 qed "sup_PTS_eq"; |
44 |
44 |
45 |
45 |
46 |
|
47 Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])"; |
46 Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])"; |
48 by(Simp_tac 1); |
47 by(Simp_tac 1); |
49 qed "sup_loc_Nil"; |
48 qed "sup_loc_Nil"; |
50 AddIffs [sup_loc_Nil]; |
49 AddIffs [sup_loc_Nil]; |
51 |
50 |
54 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
53 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
55 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1); |
54 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1); |
56 qed "sup_loc_Cons"; |
55 qed "sup_loc_Cons"; |
57 AddIffs [sup_loc_Cons]; |
56 AddIffs [sup_loc_Cons]; |
58 |
57 |
|
58 |
|
59 |
|
60 Goal "\\<forall> b. G \\<turnstile> a <=l b \\<longrightarrow> length a = length b"; |
|
61 by (induct_tac "a" 1); |
|
62 by (Simp_tac 1); |
|
63 by (Clarsimp_tac 1); |
|
64 qed_spec_mp "sup_loc_length"; |
|
65 |
|
66 Goal "\\<forall> n b. (G \\<turnstile> a <=l b) \\<longrightarrow> n < length a \\<longrightarrow> (G \\<turnstile> (a!n) <=o (b!n))"; |
|
67 by (induct_tac "a" 1); |
|
68 by (Simp_tac 1); |
|
69 by (Clarsimp_tac 1); |
|
70 by (exhaust_tac "n" 1); |
|
71 by (Asm_full_simp_tac 1); |
|
72 by (eres_inst_tac [("x","nat")] allE 1); |
|
73 by (smp_tac 1 1); |
|
74 by (Asm_full_simp_tac 1); |
|
75 qed_spec_mp "sup_loc_nth"; |
|
76 |
|
77 Goalw[sup_state_def] |
|
78 "(G \\<turnstile> (x, y) <=s (a, b)) \\<Longrightarrow> length x = length a"; |
|
79 by (Clarsimp_tac 1); |
|
80 bd sup_loc_length 1; |
|
81 by Auto_tac; |
|
82 qed "sup_state_length_fst"; |
|
83 |
|
84 Goalw[sup_state_def] |
|
85 "(G \\<turnstile> (x, y) <=s (a, b)) \\<longrightarrow> length y = length b"; |
|
86 by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_length]) 1); |
|
87 qed "sup_state_length_snd"; |
|
88 |