--- a/thys2/ClosedForms.thy Sat Mar 19 10:36:52 2022 +0000
+++ b/thys2/ClosedForms.thy Sun Mar 20 23:32:08 2022 +0000
@@ -7,6 +7,52 @@
sorry
+
+
+lemma distinct_removes_last:
+ shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
+ apply(induct as arbitrary: rset ab rset1 a)
+ apply simp
+ apply simp
+ apply(case_tac "aa \<in> rset")
+ apply(case_tac "a = aa")
+ apply (metis append_Cons)
+ apply simp
+ apply(case_tac "a \<in> set as")
+ apply (metis append_Cons rdistinct.simps(2) set_ConsD)
+ apply(case_tac "a = aa")
+ prefer 2
+ apply simp
+ apply (metis append_Cons)
+ apply(case_tac "ab \<in> rset1")
+ prefer 2
+ apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 =
+ ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
+ prefer 2
+ apply force
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
+ apply blast
+ apply(case_tac "a \<in> insert ab rset1")
+ apply simp
+ apply (metis insertI1)
+ apply simp
+ apply (meson insertI1)
+ apply simp
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
+ apply simp
+ by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
+
+
+lemma distinct_removes_last2:
+ shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+ using distinct_removes_last(1) by presburger
+
lemma distinct_append_simp:
shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
rsimp (rsimp_ALTs (f a # rs1)) =
@@ -84,10 +130,8 @@
shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
apply(case_tac r2)
apply simp+
-
using rrexp.distinct(1) apply presburger
apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
-
apply simp+
done
@@ -134,93 +178,8 @@
apply simp
done
-
-lemma alts_preimage_cases:
- shows "rder x r = RALT (RSEQ r1 r2) r3 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd re. r = RALT (RSEQ rc rd) re)"
- apply(case_tac r)
- apply simp+
-
- apply (metis rrexp.simps(12) rrexp.simps(20))
- prefer 3
- apply simp
- apply blast
- apply(frule alts_preimage_case2_2)
- apply(case_tac "(\<exists>ra rb. r = RSEQ ra rb)")
- apply blast
- apply(subgoal_tac " (\<exists> rc rd. r = RALT rc rd )")
- prefer 2
- apply blast
- apply(erule exE)+
- apply(subgoal_tac "rder x r = RALT (rder x rc) (rder x rd)")
- prefer 2
- apply force
- apply(subgoal_tac "rder x rc = RSEQ r1 r2")
- oops
-
-
-lemma der_seq_eq_case:
- shows "\<lbrakk>r1 \<noteq> r2 ; r1 = RSEQ ra rb; rder x r1 = rder x r2\<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO \<and> rsimp (rder x r2) = RZERO"
- apply(case_tac "rnullable ra")
- apply simp
- oops
-
-
-
-
-lemma der_map_unequal_to_equal_zero_only:
- shows "\<lbrakk>r1 \<noteq> r2 ; rder x r1 = rder x r2 \<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO"
- apply(induct r1)
- apply simp
- apply simp
- apply simp
- apply(case_tac "x = xa")
- apply simp
- apply(subgoal_tac "r2 = RCHAR xa")
- prefer 2
- using inv_one_derx apply blast
- apply simp
- using rsimp.simps(3) apply presburger
- apply(case_tac "rder x (RSEQ r11 r12)")
- apply simp
- apply (metis inv_one_derx)
- apply (metis rrexp.distinct(21) rrexp.simps(24) shape_of_derseq)
- apply(subgoal_tac "rder x r2 = RSEQ x41 x42")
- prefer 2
- apply presburger
- apply(subgoal_tac "x41 = rder x r11")
- prefer 2
- apply (meson shape_of_derseq2)
- apply(case_tac r2)
- apply simp+
- apply (metis rrexp.distinct(13) rrexp.simps(10))
- apply(subgoal_tac "x42a = x42")
- prefer 2
- apply (metis rrexp.inject(2) rrexp.simps(30) shape_of_derseq)
- apply(subgoal_tac "rder x x41a = x41")
- prefer 2
- apply (metis shape_of_derseq2)
- apply(simp)
- apply(subgoal_tac "\<not> rnullable r11")
- prefer 2
- apply force
- apply simp
- apply(subgoal_tac "\<not> rnullable x41a")
- prefer 2
- apply force
- apply simp
-
- oops
-
-
-
-lemma der_maps_1to1_except0:
- shows "\<lbrakk>rder x ` rset = dset; a \<notin> rset; rder x a \<in> dset\<rbrakk> \<Longrightarrow> rsimp (rder x a) = RZERO"
-
-
- sorry
-
lemma distinct_der_set:
shows "(rder x) ` rset = dset \<Longrightarrow>
rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
@@ -263,19 +222,46 @@
lemma non_empty_list:
shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
-
by (metis empty_iff empty_set)
+lemma distinct_comp:
+ shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+ apply(induct rs2 arbitrary: rs1)
+ apply simp
+ apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2")
+ apply(simp only:)
+ apply(case_tac "a \<in> set rs1")
+ apply simp
+ oops
-lemma distinct_removes_last:
- shows "\<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as)\<rbrakk>
- \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =
- rsimp_ALTs (rdistinct (rflts (map rsimp as)) {})"
- apply(induct "rsimp a" arbitrary: as)
- apply(simp)
- apply (metis append.right_neutral append_self_conv2 empty_set list.simps(9) map_append rflts.simps(2) rsimp.simps(2) rsimp_idem simp_more_distinct spawn_simp_rsimpalts)
+lemma instantiate1:
+ shows "\<lbrakk>\<And>ab rset1. rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow>
+rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset"
+ apply(drule_tac x = "aa" in meta_spec)
+ apply(drule_tac x = "rset" in meta_spec)
apply simp
- sorry
+ done
+
+
+lemma not_head_elem:
+ shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa"
+
+ by fastforce
+
+(*
+ apply simp
+ apply (metis append_Cons)
+ apply(case_tac "ab \<in> rset1")
+ apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+ apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 =
+ ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)")
+ apply blast
+*)
+
lemma flts_identity1:
shows "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
@@ -319,7 +305,68 @@
using flts_identity11 apply auto[1]
apply blast
using flts_identity12 by presburger
+
+lemma flts_identity3:
+ shows "a = RZERO \<Longrightarrow> rflts (rs @ [a]) = rflts rs"
+ apply simp
+ apply(induct rs)
+ apply simp+
+ apply(case_tac aa)
+ apply simp+
+ done
+
+lemma distinct_removes_last3:
+ shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
+ using distinct_removes_last2 by blast
+
+lemma set_inclusion_with_flts1:
+ shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE \<in> set (rflts rs)"
+ apply(induct rs)
+ apply simp
+ apply(case_tac " RONE \<in> set rs")
+ apply simp
+ apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append)
+ apply(case_tac "RONE = a")
+ apply simp
+ apply simp
+ done
+
+lemma set_inclusion_with_flts10:
+ shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x \<in> set (rflts rs)"
+ apply(induct rs)
+ apply simp
+ apply(case_tac " RCHAR x \<in> set rs")
+ apply simp
+ apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+ apply(case_tac "RCHAR x = a")
+ apply simp
+ apply fastforce
+ apply simp
+ done
+
+lemma set_inclusion_with_flts11:
+ shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2 \<in> set (rflts rs)"
+ apply(induct rs)
+ apply simp
+ apply(case_tac " RSEQ r1 r2 \<in> set rs")
+ apply simp
+ apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+ apply(case_tac "RSEQ r1 r2 = a")
+ apply simp
+ apply fastforce
+ apply simp
+ done
+
+
+lemma set_inclusion_with_flts:
+ shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
+ by (simp add: set_inclusion_with_flts1)
+lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
+ \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =
+rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
+
lemma last_elem_dup1:
shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
@@ -327,7 +374,17 @@
apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
prefer 2
apply simp
-
+ apply(case_tac "rsimp a")
+ apply simp
+
+ using flts_identity3 apply presburger
+ apply(subst flts_identity2)
+ using rrexp.distinct(1) rrexp.distinct(15) apply presburger
+ apply(subst distinct_removes_last3[symmetric])
+ using set_inclusion_with_flts apply blast
+ apply simp
+ apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10)
+ apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11)
sorry
lemma last_elem_dup: