1914 fun expand_proof thy thms prf = |
1914 fun expand_proof thy thms prf = |
1915 let |
1915 let |
1916 fun do_expand a prop = |
1916 fun do_expand a prop = |
1917 exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms; |
1917 exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms; |
1918 |
1918 |
1919 fun expand maxidx prfs (AbsP (s, t, prf)) = |
1919 fun expand seen maxidx (AbsP (s, t, prf)) = |
1920 let val (maxidx', prfs', prf') = expand maxidx prfs prf |
1920 let val (seen', maxidx', prf') = expand seen maxidx prf |
1921 in (maxidx', prfs', AbsP (s, t, prf')) end |
1921 in (seen', maxidx', AbsP (s, t, prf')) end |
1922 | expand maxidx prfs (Abst (s, T, prf)) = |
1922 | expand seen maxidx (Abst (s, T, prf)) = |
1923 let val (maxidx', prfs', prf') = expand maxidx prfs prf |
1923 let val (seen', maxidx', prf') = expand seen maxidx prf |
1924 in (maxidx', prfs', Abst (s, T, prf')) end |
1924 in (seen', maxidx', Abst (s, T, prf')) end |
1925 | expand maxidx prfs (prf1 %% prf2) = |
1925 | expand seen maxidx (prf1 %% prf2) = |
1926 let |
1926 let |
1927 val (maxidx', prfs', prf1') = expand maxidx prfs prf1; |
1927 val (seen', maxidx', prf1') = expand seen maxidx prf1; |
1928 val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2; |
1928 val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2; |
1929 in (maxidx'', prfs'', prf1' %% prf2') end |
1929 in (seen'', maxidx'', prf1' %% prf2') end |
1930 | expand maxidx prfs (prf % t) = |
1930 | expand seen maxidx (prf % t) = |
1931 let val (maxidx', prfs', prf') = expand maxidx prfs prf |
1931 let val (seen', maxidx', prf') = expand seen maxidx prf |
1932 in (maxidx', prfs', prf' % t) end |
1932 in (seen', maxidx', prf' % t) end |
1933 | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) = |
1933 | expand seen maxidx (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) = |
1934 if do_expand a prop then |
1934 if do_expand a prop then |
1935 let |
1935 let |
1936 val (maxidx', prfs', prf') = |
1936 val (seen', maxidx', prf') = |
1937 (case AList.lookup (op =) prfs (a, prop) of |
1937 (case AList.lookup (op =) seen (a, prop) of |
1938 NONE => |
1938 NONE => |
1939 let |
1939 let |
1940 val prf1 = |
1940 val prf1 = |
1941 thm_body_proof_open thm_body |
1941 thm_body_proof_open thm_body |
1942 |> reconstruct_proof thy prop |
1942 |> reconstruct_proof thy prop |
1943 |> forall_intr_vfs_prf prop; |
1943 |> forall_intr_vfs_prf prop; |
1944 val (maxidx1, prfs1, prf2) = expand (maxidx_proof prf1 ~1) prfs prf1 |
1944 val (seen1, maxidx1, prf2) = expand_init seen prf1 |
1945 val prfs2 = ((a, prop), (maxidx1, prf2)) :: prfs1; |
1945 val seen2 = ((a, prop), (maxidx1, prf2)) :: seen1; |
1946 in (maxidx1, prfs2, prf2) end |
1946 in (seen2, maxidx1, prf2) end |
1947 | SOME (maxidx1, prf1) => (maxidx1, prfs, prf1)); |
1947 | SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); |
1948 val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts; |
1948 val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts; |
1949 in (maxidx' + maxidx + 1, prfs', prf'') end |
1949 in (seen', maxidx' + maxidx + 1, prf'') end |
1950 else (maxidx, prfs, prf) |
1950 else (seen, maxidx, prf) |
1951 | expand maxidx prfs prf = (maxidx, prfs, prf); |
1951 | expand seen maxidx prf = (seen, maxidx, prf) |
1952 |
1952 and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf; |
1953 in #3 (expand (maxidx_proof prf ~1) [] prf) end; |
1953 |
|
1954 in #3 (expand_init [] prf) end; |
1954 |
1955 |
1955 end; |
1956 end; |
1956 |
1957 |
1957 |
1958 |
1958 |
1959 |