equal
deleted
inserted
replaced
1910 |
1910 |
1911 text {* |
1911 text {* |
1912 Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} |
1912 Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} |
1913 (therefore we printing it out using the function @{ML pretty_term in Pretty}). |
1913 (therefore we printing it out using the function @{ML pretty_term in Pretty}). |
1914 We can turn this function into a proper simproc using the function |
1914 We can turn this function into a proper simproc using the function |
1915 @{ML Simplifier.simproc_i}: |
1915 @{ML Simplifier.simproc_global_i}: |
1916 *} |
1916 *} |
1917 |
1917 |
1918 |
1918 |
1919 ML{*val fail' = |
1919 ML{*val fail' = |
1920 let |
1920 let |
1921 val thy = @{theory} |
1921 val thy = @{theory} |
1922 val pat = [@{term "Suc n"}] |
1922 val pat = [@{term "Suc n"}] |
1923 in |
1923 in |
1924 Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc') |
1924 Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc') |
1925 end*} |
1925 end*} |
1926 |
1926 |
1927 text {* |
1927 text {* |
1928 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1928 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1929 The function also takes a list of patterns that can trigger the simproc. |
1929 The function also takes a list of patterns that can trigger the simproc. |
1976 ML{*val plus_one = |
1976 ML{*val plus_one = |
1977 let |
1977 let |
1978 val thy = @{theory} |
1978 val thy = @{theory} |
1979 val pat = [@{term "Suc n"}] |
1979 val pat = [@{term "Suc n"}] |
1980 in |
1980 in |
1981 Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc) |
1981 Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc) |
1982 end*} |
1982 end*} |
1983 |
1983 |
1984 text {* |
1984 text {* |
1985 Now the simproc is set up so that it is triggered by terms |
1985 Now the simproc is set up so that it is triggered by terms |
1986 of the form @{term "Suc n"}, but inside the simproc we only produce |
1986 of the form @{term "Suc n"}, but inside the simproc we only produce |
2084 ML{*val nat_number = |
2084 ML{*val nat_number = |
2085 let |
2085 let |
2086 val thy = @{theory} |
2086 val thy = @{theory} |
2087 val pat = [@{term "Suc n"}] |
2087 val pat = [@{term "Suc n"}] |
2088 in |
2088 in |
2089 Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc) |
2089 Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) |
2090 end*} |
2090 end*} |
2091 |
2091 |
2092 text {* |
2092 text {* |
2093 Now in the lemma |
2093 Now in the lemma |
2094 *} |
2094 *} |