diff -r aecf1ddf3541 -r c27f04bb2262 thys3/RfltsRdistinctProps.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/RfltsRdistinctProps.thy	Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,355 @@
+theory RfltsRdistinctProps imports "Rsimp"
+begin
+
+
+
+lemma all_that_same_elem:
+  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
+       \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
+  apply(induct rs)
+   apply simp
+  apply(subgoal_tac "aa = a")
+   apply simp
+  by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
+
+
+lemma rdistinct1:
+  assumes "a \<in> acc"
+  shows "a \<notin> set (rdistinct rs acc)"
+  using assms
+  apply(induct rs arbitrary: acc a)
+   apply(auto)
+  done
+
+
+lemma rdistinct_does_the_job:
+  shows "distinct (rdistinct rs s)"
+  apply(induct rs s rule: rdistinct.induct)
+  apply(auto simp add: rdistinct1)
+  done
+
+
+
+lemma rdistinct_concat:
+  assumes "set rs \<subseteq> rset"
+  shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+  using assms
+  apply(induct rs)
+  apply simp+
+  done
+
+lemma distinct_not_exist:
+  assumes "a \<notin> set rs"
+  shows "rdistinct rs rset = rdistinct rs (insert a rset)"
+  using assms
+  apply(induct rs arbitrary: rset)
+  apply(auto)
+  done
+
+lemma rdistinct_on_distinct:
+  shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"
+  apply(induct rs)
+  apply simp
+  using distinct_not_exist by fastforce
+
+lemma distinct_rdistinct_append:
+  assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"
+  shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"
+  using assms
+  apply(induct rs1 arbitrary: rsa acc)
+   apply(auto)[1]
+  apply(auto)[1]
+  apply(drule_tac x="rsa" in meta_spec)
+  apply(drule_tac x="{a} \<union> acc" in meta_spec)
+  apply(simp)
+  apply(drule meta_mp)
+   apply(auto)[1]
+  apply(simp)
+  done
+  
+
+lemma rdistinct_set_equality1:
+  shows "set (rdistinct rs acc) = set rs - acc"
+  apply(induct rs acc rule: rdistinct.induct)
+  apply(auto)
+  done
+
+
+lemma rdistinct_set_equality:
+  shows "set (rdistinct rs {}) = set rs"
+  by (simp add: rdistinct_set_equality1)
+
+
+
+lemma distinct_removes_last:
+  shows "\<lbrakk>a \<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_middle:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
+and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
+   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
+     apply simp
+    apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp
+    apply metis
+   apply simp
+   apply (metis insertI1)
+  apply(case_tac "a = ab")
+   apply simp
+   apply(case_tac "ab \<in> rset")
+    apply simp
+    apply presburger
+   apply (meson insertI1)
+  apply(case_tac "a \<in> rset")
+  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+  apply(case_tac "ab \<in> rset")
+  apply simp
+   apply (meson insert_iff)
+  apply simp
+  by (metis insertI1)
+
+
+lemma k0b:
+  assumes "nonalt r" "r \<noteq> RZERO"
+  shows "rflts [r] = [r]"
+  using assms
+  apply(case_tac  r)
+       apply(simp_all)
+  done
+
+lemma rflts_def_idiot:
+  shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs"
+  apply(case_tac a)
+  apply simp_all
+  done
+
+lemma flts_middle0:
+  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+  apply(induct rsa)
+  apply simp
+  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+
+lemma flts_removes0:
+  shows "  rflts (rs @ [RZERO])  =
+           rflts rs"
+  apply(induct rs)
+   apply simp
+  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma rflts_spills_last:
+  shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs"
+  apply (induct rs1 rule: rflts.induct)
+  apply(auto)
+  done
+
+lemma flts_keeps1:
+  shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]"
+  apply (induct rs rule: rflts.induct)
+  apply(auto)
+  done
+
+lemma flts_keeps_others:
+  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
+  apply(induct rs rule: rflts.induct)
+  apply(auto)
+  by (meson k0b nonalt.elims(3))
+
+lemma spilled_alts_contained:
+  shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
+  apply(induct rs1)
+   apply simp 
+  apply(case_tac "a = aa")
+   apply simp
+  apply(subgoal_tac " a \<in> set rs1")
+  prefer 2
+   apply (meson set_ConsD)
+  apply(case_tac aa)
+  using rflts.simps(2) apply presburger
+      apply fastforce
+  apply fastforce
+  apply fastforce
+  apply fastforce
+  by fastforce
+
+
+lemma rflts_def_idiot2:
+  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
+  apply(induct rs rule: rflts.induct)
+  apply(auto)
+  done
+
+lemma flts_append:
+  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+  apply(induct rs1)
+   apply simp
+  apply(case_tac a)
+       apply simp+
+  done
+lemma distinct_removes_middle3:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
+  using distinct_removes_middle(1) by fastforce
+
+
+lemma distinct_removes_list:
+  shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+  apply(induct rs)
+   apply simp+
+  apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
+   prefer 2
+  apply (metis append_Cons append_Nil distinct_removes_middle(1))
+  by presburger
+
+lemma last_elem_out:
+  shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+  apply(induct xs arbitrary: rset)
+  apply simp+
+  done
+
+
+lemma rdistinct_concat_general:
+  shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+  apply(induct rs1 arbitrary: rs2 rule: rev_induct)
+   apply simp
+  apply(drule_tac x = "x # rs2" in meta_spec)
+  apply simp
+  apply(case_tac "x \<in> set xs")
+   apply simp
+  
+   apply (simp add: distinct_removes_middle3 insert_absorb)
+  apply simp
+  by (simp add: last_elem_out)
+
+
+
+  
+lemma distinct_once_enough:
+  shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+  apply(subgoal_tac "distinct (rdistinct rs {})")
+   apply(subgoal_tac 
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+  apply(simp only:)
+  using rdistinct_concat_general apply blast
+  apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)
+  by (simp add: rdistinct_does_the_job)
+  
+
+
+
+lemma distinct_removes_duplicate_flts:
+  shows " a \<in> set rsa
+       \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+           rdistinct (rflts (map rsimp rsa)) {}"
+  apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+  prefer 2
+   apply simp
+  apply(induct "rsimp a")
+       apply simp
+  using flts_removes0 apply presburger
+      apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
+                          rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
+      apply (simp only:)
+       apply(subst flts_keeps1)
+  apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
+      apply presburger
+        apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
+                            rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
+      apply (simp only:)
+      prefer 2
+      apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
+  apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
+
+    apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+   prefer 2
+   apply (metis distinct_removes_last(1) flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
+  apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
+  prefer 2
+  apply (simp add: rflts_spills_last)
+  apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
+    prefer 2
+  apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained)
+  apply (metis rflts_spills_last)
+  by (metis distinct_removes_list spilled_alts_contained)
+
+
+
+
+
+lemma distinct_early_app1:
+  shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
+  apply(induct rs arbitrary: rset rset1)
+   apply simp
+  apply simp
+  apply(case_tac "a \<in> rset1")
+   apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp+
+  
+   apply blast
+  apply(case_tac "a \<in> rset1")
+   apply simp+
+  apply(case_tac "a \<in> rset")
+   apply simp
+   apply (metis insert_subsetI)
+  apply simp
+  by (meson insert_mono)
+
+
+lemma distinct_early_app:
+  shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
+  apply(induct rsb)
+   apply simp
+  using distinct_early_app1 apply blast
+  by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
+
+
+lemma distinct_eq_interesting1:
+  shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
+  apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
+   apply(simp only:)
+  using distinct_early_app apply blast 
+  by (metis append_Cons distinct_early_app rdistinct.simps(2))
+
+
+
+
+end
\ No newline at end of file