542   by (simp add: frewrites_cons)

   542   apply (simp add: frewrites_cons)

   543 

   543   apply (auto simp add: frewrites_cons)

   544   using frewrite.intros(1) many_steps_later by blast

   545   

   645   by blast

   647   apply blast

   648   by simp

  1050   by simp

  1053   by simp_all

  1124   by simp

  1127   by simp_all

  1251   

  1254       apply(auto)

  1252   apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21))

  1255   apply (meson created_by_seq.cases rrexp.distinct(23) rrexp.distinct(25))

  1253   apply (metis created_by_seq.simps rder.simps(5))

  1256   using created_by_seq.simps apply blast

  1254    apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3))

  1257   apply (meson created_by_seq.simps)

  1255   using created_by_seq.intros(1) by force

  1258   using created_by_seq.intros(1) apply blast

  1259   apply (metis (no_types, lifting) created_by_seq.simps k0a list.set_intros(1) list.simps(8) list.simps(9) rrexp.distinct(31))

  1260   apply (simp add: created_by_seq.intros(1))

  1261   using created_by_seq.simps apply blast

  1262   by (simp add: created_by_seq.intros(1))

  1569   by simp

  1571   by simp_all

  1603   using cbs_hfau_rsimpeq1 by fastforce

  1605   using cbs_hfau_rsimpeq1 apply(fastforce)

  1606   by simp

  1607   

  1648   shows "\<forall>s \<in> set  Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"

  1655   shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"

  1674   apply(induct s)

  1681   apply(case_tac s)

  1680 unused_thms

  1687 

  1681 

  1688 

  1689 fun nupdate :: "char \<Rightarrow> rrexp \<Rightarrow>  (string * nat) option  list \<Rightarrow> (string * nat) option  list" where

  1690   "nupdate c r [] = []"

  1691 | "nupdate c r (Some (s, Suc n) # Ss) = (if (rnullable (rders r s)) 

  1692                                           then Some (s@[c], Suc n) # Some ([c], n) # (nupdate c r Ss) 

  1693                                           else Some ((s@[c]), Suc n)  # (nupdate c r Ss) 

  1694                                         )"

  1695 | "nupdate c r (Some (s, 0) # Ss) =  (if (rnullable (rders r s)) 

  1696                                         then Some (s@[c], 0) # None # (nupdate c r Ss) 

  1697                                         else Some ((s@[c]), 0)  # (nupdate c r Ss) 

  1698                                       ) "

  1699 | "nupdate c r (None # Ss) = (None # nupdate c r Ss)"

  1700 

  1701 

  1702 fun nupdates :: "char list \<Rightarrow> rrexp \<Rightarrow> (string * nat) option list \<Rightarrow> (string * nat) option list"

  1703   where

  1704   "nupdates [] r Ss = Ss"

  1705 | "nupdates (c # cs) r Ss = nupdates cs r (nupdate c r Ss)"

  1706 

  1707 fun ntset :: "rrexp \<Rightarrow> nat \<Rightarrow> string \<Rightarrow> (string * nat) option list" where

  1708   "ntset r (Suc n)  (c # cs) = nupdates cs r [Some ([c], n)]"

  1709 | "ntset r 0 _ = [None]"

  1710 | "ntset r _ [] = []"

  1711 

  1712 inductive created_by_ntimes :: "rrexp \<Rightarrow> bool" where

  1713   "created_by_ntimes RZERO"

  1714 | "created_by_ntimes (RSEQ ra (RNTIMES rb n))"

  1715 | "\<lbrakk>created_by_ntimes r1; created_by_ntimes r2\<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r1 r2)"

  1716 | "\<lbrakk>created_by_ntimes r \<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r RZERO)"

  1717 

  1718 fun highest_power_aux :: "(string * nat) option list \<Rightarrow> nat \<Rightarrow> nat" where

  1719   "highest_power_aux [] n = n"

  1720 | "highest_power_aux (None # rs) n = highest_power_aux rs n"

  1721 | "highest_power_aux (Some (s, n) # rs) m = highest_power_aux rs (max n m)"

  1722 

  1723 fun hpower :: "(string * nat) option list \<Rightarrow> nat" where

  1724   "hpower rs =  highest_power_aux rs 0"

  1725                         

  1726 

  1727 lemma nupdate_mono:

  1728   shows " (highest_power_aux (nupdate c r optlist) m) \<le> (highest_power_aux optlist m)"

  1729   apply(induct optlist arbitrary: m)

  1730    apply simp

  1731   apply(case_tac a)

  1732    apply simp

  1733   apply(case_tac aa)

  1734   apply(case_tac b)

  1735    apply simp+

  1736   done

  1737 

  1738 lemma nupdate_mono1:

  1739   shows "hpower (nupdate c r optlist) \<le> hpower optlist"

  1740   by (simp add: nupdate_mono)

  1741 

  1742 

  1743 

  1744 lemma cbn_ders_cbn:

  1745   shows "created_by_ntimes r \<Longrightarrow> created_by_ntimes (rder c r)"

  1746   apply(induct r rule: created_by_ntimes.induct)

  1747     apply simp

  1748 

  1749   using created_by_ntimes.intros(1) created_by_ntimes.intros(2) created_by_ntimes.intros(3) apply presburger

  1750   

  1751   apply (metis created_by_ntimes.simps rder.simps(5) rder.simps(7))

  1752   using created_by_star.intros(1) created_by_star.intros(2) apply auto[1]

  1753   using created_by_ntimes.intros(1) created_by_ntimes.intros(3) apply auto[1]

  1754   by (metis (mono_tags, lifting) created_by_ntimes.simps list.simps(8) list.simps(9) rder.simps(1) rder.simps(4))

  1755 

  1756 lemma ntimes_ders_cbn:

  1757   shows "created_by_ntimes (rders (RSEQ r' (RNTIMES r n)) s)"

  1758   apply(induct s rule: rev_induct)

  1759    apply simp

  1760   apply (simp add: created_by_ntimes.intros(2))

  1761   apply(subst rders_append)

  1762   using cbn_ders_cbn by auto

  1763 

  1764 lemma always0:

  1765   shows "rders RZERO s = RZERO"

  1766   apply(induct s)

  1767   by simp+

  1768 

  1769 lemma ntimes_ders_cbn1:

  1770   shows "created_by_ntimes (rders (RNTIMES r n) (c#s))"

  1771   apply(case_tac n)

  1772    apply simp

  1773   using always0 created_by_ntimes.intros(1) apply auto[1]

  1774   by (simp add: ntimes_ders_cbn)

  1775 

  1776 

  1777 lemma ntimes_hfau_pushin: 

  1778   shows "created_by_ntimes r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))"

  1779   apply(induct r rule: created_by_ntimes.induct)

  1780   apply simp+

  1781   done

  1782 

  1783 

  1784 abbreviation

  1785   "opterm r SN \<equiv>     case SN of

  1786                                 Some (s, n) \<Rightarrow> RSEQ (rders r s) (RNTIMES r n)

  1787                             |   None \<Rightarrow> RZERO

  1788                      

  1789               

  1790 "

  1791 

  1792 fun nonempty_string :: "(string * nat) option \<Rightarrow> bool" where

  1793   "nonempty_string None = True"

  1794 | "nonempty_string (Some ([], n)) = False"

  1795 | "nonempty_string (Some (c#s, n)) = True"

  1796 

  1797 

  1798 lemma nupdate_nonempty:

  1799   shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdate c r Ss). nonempty_string opt"

  1800   apply(induct c r Ss rule: nupdate.induct)

  1801      apply(auto)

  1802   apply (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3))

  1803   by (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3))

  1804 

  1805 

  1806 

  1807 lemma nupdates_nonempty:

  1808   shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdates s r Ss). nonempty_string opt"

  1809   apply(induct s arbitrary: Ss)

  1810    apply simp

  1811   apply simp

  1812   using nupdate_nonempty by presburger

  1813 

  1814 lemma nullability1: shows "rnullable (rders r s) = rnullable (rders_simp r s)"

  1815   by (metis der_simp_nullability rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders)

  1816 

  1817 lemma nupdate_induct1:

  1818   shows 

  1819   "concat (map (hflat_aux \<circ> (rder c \<circ> (opterm r)))  sl ) = 

  1820    map (opterm r) (nupdate c r sl)"

  1821   apply(induct sl)

  1822    apply simp

  1823   apply(simp add: rders_append)

  1824   apply(case_tac "a")

  1825    apply simp+

  1826   apply(case_tac "aa")

  1827   apply(case_tac "b")

  1828   apply(case_tac "rnullable (rders r ab)")

  1829   apply(subgoal_tac "rnullable (rders_simp r ab)")

  1830     apply simp

  1831   using rders.simps(1) rders.simps(2) rders_append apply presburger

  1832   using nullability1 apply blast

  1833    apply simp

  1834   using rders.simps(1) rders.simps(2) rders_append apply presburger

  1835   apply simp

  1836   using rders.simps(1) rders.simps(2) rders_append by presburger

  1837 

  1838 

  1839 lemma nupdates_join_general:

  1840   shows  "concat (map hflat_aux (map (rder x) (map (opterm r) (nupdates xs r Ss))  )) =

  1841            map (opterm r) (nupdates (xs @ [x]) r Ss)"

  1842   apply(induct xs arbitrary: Ss)

  1843    apply (simp)

  1844   prefer 2

  1845    apply auto[1]

  1846   using nupdate_induct1 by blast

  1847 

  1848 

  1849 lemma nupdates_join_general1:

  1850   shows  "concat (map (hflat_aux \<circ> (rder x) \<circ> (opterm r)) (nupdates xs r Ss)) =

  1851            map (opterm r) (nupdates (xs @ [x]) r Ss)"

  1852   by (metis list.map_comp nupdates_join_general)

  1853 

  1854 lemma nupdates_append: shows 

  1855 "nupdates (s @ [c]) r Ss = nupdate c r (nupdates s r Ss)"

  1856   apply(induct s arbitrary: Ss)

  1857    apply simp

  1858   apply simp

  1859   done

  1860 

  1861 lemma nupdates_mono:

  1862   shows "highest_power_aux (nupdates s r optlist) m \<le> highest_power_aux optlist m"

  1863   apply(induct s rule: rev_induct)

  1864    apply simp

  1865   apply(subst nupdates_append)

  1866   by (meson le_trans nupdate_mono)

  1867 

  1868 lemma nupdates_mono1:

  1869   shows "hpower (nupdates s r optlist) \<le> hpower optlist"

  1870   by (simp add: nupdates_mono)

  1871 

  1872 

  1873 (*"\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"*)

  1874 lemma nupdates_mono2:

  1875   shows "hpower (nupdates s r [Some ([c], n)]) \<le> n"

  1876   by (metis highest_power_aux.simps(1) highest_power_aux.simps(3) hpower.simps max_nat.right_neutral nupdates_mono1)

  1877 

  1878 lemma hpow_arg_mono:

  1879   shows "m \<ge> n \<Longrightarrow> highest_power_aux rs m \<ge> highest_power_aux rs n"

  1880   apply(induct rs arbitrary: m n)

  1881    apply simp

  1882   apply(case_tac a)

  1883    apply simp

  1884   apply(case_tac aa)

  1885   apply simp

  1886   done

  1887 

  1888 

  1889 lemma hpow_increase:

  1890   shows "highest_power_aux (a # rs') m \<ge> highest_power_aux rs' m"

  1891   apply(case_tac a)

  1892    apply simp

  1893   apply simp

  1894   apply(case_tac aa)

  1895   apply(case_tac b)

  1896    apply simp+

  1897   apply(case_tac "Suc nat > m")

  1898   using hpow_arg_mono max.cobounded2 apply blast

  1899   using hpow_arg_mono max.cobounded2 by blast

  1900 

  1901 lemma hpow_append:

  1902   shows "highest_power_aux (rsa @ rsb) m  = highest_power_aux rsb (highest_power_aux rsa m)"

  1903   apply (induct rsa arbitrary: rsb m)

  1904    apply simp

  1905   apply simp

  1906   apply(case_tac a)

  1907    apply simp

  1908   apply(case_tac aa)

  1909   apply simp

  1910   done

  1911 

  1912 lemma hpow_aux_mono:

  1913   shows "highest_power_aux (rsa @ rsb) m \<ge> highest_power_aux rsb m"

  1914   apply(induct rsa arbitrary: rsb rule: rev_induct)

  1915   apply simp

  1916   apply simp

  1917   using hpow_increase order.trans by blast

  1918  

  1919 

  1920 

  1921 

  1922 lemma hpow_mono:

  1923   shows "hpower (rsa @ rsb) \<le> n \<Longrightarrow> hpower rsb \<le> n"

  1924   apply(induct rsb arbitrary: rsa)

  1925    apply simp

  1926   apply(subgoal_tac "hpower rsb \<le> n")

  1927   apply simp

  1928   apply (metis dual_order.trans hpow_aux_mono)

  1929   by (metis hpow_append hpow_increase hpower.simps nat_le_iff_add trans_le_add1)

  1930 

  1931 

  1932 lemma hpower_rs_elems_aux:

  1933   shows "highest_power_aux rs k \<le> n \<Longrightarrow> \<forall>r\<in>set rs. r = None \<or> (\<exists>s' m. r = Some (s', m) \<and> m \<le> n)"

  1934 apply(induct rs k arbitrary: n rule: highest_power_aux.induct)

  1935     apply(auto)

  1936   by (metis dual_order.trans highest_power_aux.simps(1) hpow_append hpow_aux_mono linorder_le_cases max.absorb1 max.absorb2)

  1937 

  1938 

  1939 lemma hpower_rs_elems:

  1940   shows "hpower rs \<le> n \<Longrightarrow> \<forall>r \<in> set rs. r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"

  1941   by (simp add: hpower_rs_elems_aux)

  1942 

  1943 lemma nupdates_elems_leqn:

  1944   shows "\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"

  1945   by (meson hpower_rs_elems nupdates_mono2)

  1946 

  1947 lemma ntimes_hfau_induct:

  1948   shows "hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) s) =   

  1949       map (opterm r) (nupdates s r [Some ([c], n)])"

  1950   apply(induct s rule: rev_induct)

  1951    apply simp

  1952   apply(subst rders_append)+

  1953   apply simp

  1954   apply(subst nupdates_append)

  1955   apply(subgoal_tac "created_by_ntimes (rders (RSEQ (rder c r) (RNTIMES r n)) xs)")

  1956   prefer 2

  1957   apply (simp add: ntimes_ders_cbn)

  1958   apply(subst ntimes_hfau_pushin)

  1959    apply simp

  1960   apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) xs)))) =

  1961                      concat (map hflat_aux (map (rder x) ( map (opterm r) (nupdates xs r [Some ([c], n)])))) ")

  1962    apply(simp only:)

  1963   prefer 2

  1964    apply presburger

  1965   apply(subst nupdates_append[symmetric])  

  1966   using nupdates_join_general by blast

  1967 

  1968 

  1969 (*nupdates s r [Some ([c], n)]*)

  1970 lemma ntimes_ders_hfau_also1:

  1971   shows "hflat_aux (rders (RNTIMES r (Suc n)) (c # xs)) = map (opterm r) (nupdates xs r [Some ([c], n)])"

  1972   using ntimes_hfau_induct by force

  1973 

  1974 

  1975 

  1976 lemma hfau_rsimpeq2_ntimes:

  1977   shows "created_by_ntimes r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"

  1978   apply(induct r)

  1979        apply simp+

  1980   

  1981     apply (metis rsimp_seq_equal1)

  1982   prefer 2

  1983    apply simp

  1984   apply(case_tac x)

  1985    apply simp

  1986   apply(case_tac "list")

  1987    apply simp

  1988   

  1989   apply (metis idem_after_simp1)

  1990   apply(case_tac "lista")

  1991   prefer 2

  1992    apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))

  1993   apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")

  1994   apply simp

  1995   apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")

  1996   using hflat_aux.simps(1) apply presburger

  1997   apply simp

  1998   using cbs_hfau_rsimpeq1 apply(fastforce)

  1999   by simp

  2000   

  2001 

  2002 lemma ntimes_closed_form1:

  2003   shows "rsimp (rders (RNTIMES r (Suc n)) (c#s)) = 

  2004 rsimp ( ( RALTS (  map (opterm r) (nupdates s r [Some ([c], n)]) )))"

  2005   apply(subgoal_tac "created_by_ntimes (rders (RNTIMES r (Suc n)) (c#s))")

  2006    apply(subst hfau_rsimpeq2_ntimes)

  2007   apply linarith

  2008   using ntimes_ders_hfau_also1 apply auto[1]

  2009   using ntimes_ders_cbn1 by blast

  2010 

  2011 

  2012 lemma ntimes_closed_form2:

  2013   shows  "rsimp (rders_simp (RNTIMES r (Suc n)) (c#s) ) = 

  2014 rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))"

  2015   by (metis list.distinct(1) ntimes_closed_form1 rders_simp_same_simpders rsimp_idem)

  2016 

  2017 

  2018 lemma ntimes_closed_form3:

  2019   shows  "rsimp (rders_simp (RNTIMES r n) (c#s)) =   (rders_simp (RNTIMES r n) (c#s))"

  2020   by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem)

  2021 

  2022 

  2023 lemma ntimes_closed_form4:

  2024   shows " (rders_simp (RNTIMES r (Suc n)) (c#s)) = 

  2025 rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) )  )))"

  2026   using ntimes_closed_form2 ntimes_closed_form3 

  2027   by metis

  2028 

  2029 

  2030 

  2031 

  2032 lemma ntimes_closed_form5:

  2033   shows " rsimp (  RALTS (map (\<lambda>s1. RSEQ (rders r0 s1) (RNTIMES r n) )         Ss)) = 

  2034           rsimp (  RALTS (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r n)) ) Ss))"

  2035   by (smt (verit, ccfv_SIG) list.map_comp map_eq_conv o_apply simp_flatten_aux0)

  2036 

  2037 

  2038 

  2039 lemma ntimes_closed_form6_hrewrites:

  2040   shows "  

  2041 (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss )

  2042  scf\<leadsto>*

  2043 (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )"

  2044   apply(induct Ss)

  2045   apply simp

  2046   apply (simp add: ss1)

  2047   by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2)

  2048 

  2049 

  2050 

  2051 lemma ntimes_closed_form6:

  2052   shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )))) = 

  2053           rsimp ( ( RALTS ( (map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ))))"

  2054   apply(subgoal_tac " map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss  scf\<leadsto>*

  2055                       map (\<lambda>s1.  rsimp (RSEQ  (rders r0 s1) (RNTIMES r0 n)) ) Ss ")

  2056   using hrewrites_simpeq srewritescf_alt1 apply fastforce

  2057   using ntimes_closed_form6_hrewrites by blast

  2058 

  2059 abbreviation

  2060   "optermsimp r SN \<equiv>     case SN of

  2061                                 Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n)

  2062                             |   None \<Rightarrow> RZERO

  2063                      

  2064               

  2065 "

  2066 

  2067 abbreviation

  2068   "optermOsimp r SN \<equiv>     case SN of

  2069                                 Some (s, n) \<Rightarrow> rsimp (RSEQ (rders r s) (RNTIMES r n))

  2070                             |   None \<Rightarrow> RZERO

  2071                      

  2072               

  2073 "

  2074 

  2075 abbreviation

  2076   "optermosimp r SN \<equiv> case SN of

  2077                               Some (s, n) \<Rightarrow> RSEQ (rsimp (rders r s)) (RNTIMES r n)

  2078                             | None \<Rightarrow> RZERO

  2079 "

  2080 

  2081 lemma ntimes_closed_form51:

  2082   shows "rsimp (RALTS (map (opterm r) (nupdates s r [Some ([c], n)]))) =

  2083          rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)])))"

  2084   by (metis map_map simp_flatten_aux0)

  2085 

  2086 

  2087 

  2088 lemma osimp_Osimp:

  2089   shows " nonempty_string sn \<Longrightarrow> optermosimp r sn = optermsimp r sn"

  2090   apply(induct rule: nonempty_string.induct)

  2091   apply force

  2092    apply auto[1]

  2093   apply simp

  2094   by (metis list.distinct(1) rders.simps(2) rders_simp.simps(2) rders_simp_same_simpders)

  2095 

  2096 

  2097 

  2098 lemma osimp_Osimp_list:

  2099   shows "\<forall>sn \<in> set snlist. nonempty_string sn \<Longrightarrow> map (optermosimp r) snlist = map (optermsimp r) snlist"

  2100   by (simp add: osimp_Osimp)

  2101 

  2102 

  2103 lemma ntimes_closed_form8:

  2104   shows  

  2105 "rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) =

  2106  rsimp (RALTS (map (optermsimp r) (nupdates s r [Some ([c], n)])))"

  2107   apply(subgoal_tac "\<forall>opt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string opt")

  2108   using osimp_Osimp_list apply presburger

  2109   by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD)

  2110 

  2111 

  2112 

  2113 lemma ntimes_closed_form9aux:

  2114   shows "\<forall>snopt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string snopt"

  2115   by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD)

  2116 

  2117 lemma ntimes_closed_form9aux1:

  2118   shows  "\<forall>snopt \<in> set snlist. nonempty_string snopt \<Longrightarrow> 

  2119 rsimp (RALTS (map (optermosimp r) snlist)) =

  2120 rsimp (RALTS (map (optermOsimp r) snlist))"

  2121   apply(induct snlist)

  2122    apply simp+

  2123   apply(case_tac "a")

  2124    apply simp+

  2125   by (smt (z3) case_prod_conv idem_after_simp1 map_eq_conv nonempty_string.elims(2) o_apply option.simps(4) option.simps(5) rsimp.simps(1) rsimp.simps(7) rsimp_idem)

  2126   

  2127 

  2128 

  2129 

  2130 lemma ntimes_closed_form9:

  2131   shows  

  2132 "rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) =

  2133  rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))"

  2134   using ntimes_closed_form9aux ntimes_closed_form9aux1 by presburger

  2135 

  2136 

  2137 lemma ntimes_closed_form10rewrites_aux:

  2138   shows "  map (rsimp \<circ> (opterm r)) optlist scf\<leadsto>* 

  2139            map (optermOsimp r)      optlist"

  2140   apply(induct optlist)

  2141    apply simp

  2142    apply (simp add: ss1)

  2143   apply simp

  2144   apply(case_tac a)

  2145   using ss2 apply fastforce

  2146   using ss2 by force

  2147   

  2148 

  2149 lemma ntimes_closed_form10rewrites:

  2150   shows "  map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]) scf\<leadsto>* 

  2151            map (optermOsimp r) (nupdates s r [Some ([c], n)])"

  2152   using ntimes_closed_form10rewrites_aux by blast

  2153 

  2154 lemma ntimes_closed_form10:

  2155   shows "rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]))) = 

  2156          rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))"

  2157   by (smt (verit, best) case_prod_conv hpower_rs_elems map_eq_conv nupdates_mono2 o_apply option.case(2) option.simps(4) rsimp.simps(3))

  2158 

  2159 

  2160 lemma rders_simp_cons:

  2161   shows "rders_simp r (c # s) = rders_simp (rsimp (rder c r)) s"

  2162   by simp

  2163 

  2164 lemma rder_ntimes:

  2165   shows "rder c (RNTIMES r (Suc n)) = RSEQ (rder c r) (RNTIMES r n)"

  2166   by simp

  2167 

  2168 

  2169 lemma ntimes_closed_form:

  2170   shows "rders_simp (RNTIMES r0 (Suc n)) (c#s) = 

  2171 rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))"

  2172   apply (subst rders_simp_cons)

  2173   apply(subst rder_ntimes)  

  2174   using ntimes_closed_form10 ntimes_closed_form4 ntimes_closed_form51 ntimes_closed_form8 ntimes_closed_form9 by force

  2175 

  2176 

  2177 

  2178 

  2179 

  2180 

  2181 (*

  2182 lemma ntimes_closed_form:

  2183   assumes "s \<noteq> []"

  2184   shows "rders_simp (RNTIMES r (Suc n)) s = 

  2185 rsimp ( RALTS  (     map 

  2186                      (\<lambda> optSN. case optSN of

  2187                                 Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n)

  2188                             |   None \<Rightarrow> RZERO

  2189                      ) 

  2190                      (ntset r n s) 

  2191                )

  2192       )"

  2193   

  2194 *)