equal
deleted
inserted
replaced
49 lemma flts_has_no_zero: |
49 lemma flts_has_no_zero: |
50 shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)" |
50 shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)" |
51 |
51 |
52 sorry |
52 sorry |
53 |
53 |
54 lemma not_mentioned_elem_distinct: |
|
55 shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs {a}))" |
|
56 sorry |
|
57 |
|
58 |
|
59 |
|
60 lemma flts_vs_nflts: |
54 lemma flts_vs_nflts: |
61 shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs |
55 shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs |
62 \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) |
56 \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) |
63 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) ))) |
57 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) ))) |
64 \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))" |
58 \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))" |
66 apply simp |
60 apply simp |
67 |
61 |
68 sorry |
62 sorry |
69 |
63 |
70 lemma distinct_simp_ineq_general: |
64 lemma distinct_simp_ineq_general: |
71 shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) |
65 shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) |
72 \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))" |
66 \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))" |
|
67 apply(induct rs arbitrary: no_simp has_simp) |
|
68 apply simp |
|
69 apply(case_tac "a \<in> no_simp") |
|
70 apply(subgoal_tac "rsimp a \<in> has_simp") |
|
71 apply auto[1] |
|
72 apply blast |
|
73 apply(case_tac "rsimp a \<in> no_simp") |
|
74 apply(subgoal_tac "rsimp a \<in> has_simp") |
|
75 prefer 2 |
|
76 apply (simp add: rev_image_eqI rsimp_idem) |
|
77 sledgehammer[timeout = 100] |
73 |
78 |
74 sorry |
79 sorry |
|
80 |
|
81 |
|
82 lemma not_mentioned_elem_distinct_strong: |
|
83 shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs rset)) = (r \<in> set (rdistinct rs (insert a rset)))" |
|
84 apply(induct rs arbitrary: rset) |
|
85 apply simp |
|
86 by force |
|
87 |
|
88 lemma not_mentioned_elem_distinct: |
|
89 shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs (insert a {})))" |
|
90 by (metis not_mentioned_elem_distinct_strong) |
|
91 |
|
92 |
|
93 |
|
94 |
|
95 |
75 |
96 |
76 |
97 |
77 lemma without_flts_ineq: |
98 lemma without_flts_ineq: |
78 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
99 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
79 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
100 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |