diff --git a/etc/symbols b/etc/symbols --- a/etc/symbols +++ b/etc/symbols @@ -1,508 +1,508 @@ # Default interpretation of some Isabelle symbols \ code: 0x01d7ec group: digit \ code: 0x01d7ed group: digit \ code: 0x01d7ee group: digit \ code: 0x01d7ef group: digit \ code: 0x01d7f0 group: digit \ code: 0x01d7f1 group: digit \ code: 0x01d7f2 group: digit \ code: 0x01d7f3 group: digit \ code: 0x01d7f4 group: digit \ code: 0x01d7f5 group: digit \ code: 0x01d49c group: letter \ code: 0x00212c group: letter \ code: 0x01d49e group: letter \ code: 0x01d49f group: letter \ code: 0x002130 group: letter \ code: 0x002131 group: letter \ code: 0x01d4a2 group: letter \ code: 0x00210b group: letter \ code: 0x002110 group: letter \ code: 0x01d4a5 group: letter \ code: 0x01d4a6 group: letter \ code: 0x002112 group: letter \ code: 0x002133 group: letter \ code: 0x01d4a9 group: letter \ code: 0x01d4aa group: letter \

code: 0x01d5c9 group: letter \ code: 0x01d5ca group: letter \ code: 0x01d5cb group: letter \ code: 0x01d5cc group: letter \ code: 0x01d5cd group: letter \ code: 0x01d5ce group: letter \ code: 0x01d5cf group: letter \ code: 0x01d5d0 group: letter \ code: 0x01d5d1 group: letter \ code: 0x01d5d2 group: letter \ code: 0x01d5d3 group: letter \ code: 0x01d504 group: letter \ code: 0x01d505 group: letter \ code: 0x00212d group: letter \

code: 0x01d507 group: letter \ code: 0x01d508 group: letter \ code: 0x01d509 group: letter \ code: 0x01d50a group: letter \ code: 0x00210c group: letter \ code: 0x002111 group: letter \ code: 0x01d50d group: letter \ code: 0x01d50e group: letter \ code: 0x01d50f group: letter \ code: 0x01d510 group: letter \ code: 0x01d511 group: letter \ code: 0x01d512 group: letter \ code: 0x01d513 group: letter \ code: 0x01d514 group: letter \ code: 0x00211c group: letter \ code: 0x01d516 group: letter \ code: 0x01d517 group: letter \ code: 0x01d518 group: letter \ code: 0x01d519 group: letter \ code: 0x01d51a group: letter \ code: 0x01d51b group: letter \ code: 0x01d51c group: letter \ code: 0x002128 group: letter \ code: 0x01d51e group: letter \ code: 0x01d51f group: letter \ code: 0x01d520 group: letter \
code: 0x01d521 group: letter \ code: 0x01d522 group: letter \ code: 0x01d523 group: letter \ code: 0x01d524 group: letter \ code: 0x01d525 group: letter \ code: 0x01d526 group: letter \ code: 0x01d527 group: letter \ code: 0x01d528 group: letter \ code: 0x01d529 group: letter \ code: 0x01d52a group: letter \ code: 0x01d52b group: letter \ code: 0x01d52c group: letter \ code: 0x01d52d group: letter \ code: 0x01d52e group: letter \ code: 0x01d52f group: letter \ code: 0x01d530 group: letter \ code: 0x01d531 group: letter \ code: 0x01d532 group: letter \ code: 0x01d533 group: letter \ code: 0x01d534 group: letter \ code: 0x01d535 group: letter \ code: 0x01d536 group: letter \ code: 0x01d537 group: letter \ code: 0x0003b1 group: greek \ code: 0x0003b2 group: greek \ code: 0x0003b3 group: greek \ code: 0x0003b4 group: greek \ code: 0x0003b5 group: greek \ code: 0x0003b6 group: greek \ code: 0x0003b7 group: greek \ code: 0x0003b8 group: greek \ code: 0x0003b9 group: greek \ code: 0x0003ba group: greek \ code: 0x0003bb group: greek abbrev: % \ code: 0x0003bc group: greek \ code: 0x0003bd group: greek \ code: 0x0003be group: greek \ code: 0x0003c0 group: greek \ code: 0x0003c1 group: greek \ code: 0x0003c3 group: greek \ code: 0x0003c4 group: greek \ code: 0x0003c5 group: greek \ code: 0x0003c6 group: greek \ code: 0x0003c7 group: greek \ code: 0x0003c8 group: greek \ code: 0x0003c9 group: greek \ code: 0x000393 group: greek \ code: 0x000394 group: greek \ code: 0x000398 group: greek \ code: 0x00039b group: greek \ code: 0x00039e group: greek \ code: 0x0003a0 group: greek \ code: 0x0003a3 group: greek \ code: 0x0003a5 group: greek \ code: 0x0003a6 group: greek \ code: 0x0003a8 group: greek \ code: 0x0003a9 group: greek \ code: 0x01D538 group: letter group: Z_Notation \ code: 0x01d539 group: letter group: Z_Notation \ code: 0x002102 group: letter \ code: 0x01D53B group: letter \ code: 0x01D53C group: letter \ code: 0x01D53D group: letter group: Z_Notation \ code: 0x01D53E group: letter \ code: 0x00210D group: letter \ code: 0x01D540 group: letter \ code: 0x01D541 group: letter \ code: 0x01D542 group: letter \ code: 0x01D543 group: letter \ code: 0x01D544 group: letter \ code: 0x002115 group: letter group: Z_Notation \ code: 0x01D546 group: letter \ code: 0x002119 group: letter group: Z_Notation \ code: 0x00211a group: letter \ code: 0x00211d group: letter group: Z_Notation \ code: 0x01D54A group: letter \ code: 0x01D54B group: letter \ code: 0x01D54C group: letter group: Z_Notation \ code: 0x01D54D group: letter \ code: 0x01D54E group: letter group: Z_Notation \ code: 0x01D54F group: letter \ code: 0x01D550 group: letter \ code: 0x002124 group: letter \ code: 0x002190 group: arrow abbrev: <. \ code: 0x0027f5 group: arrow abbrev: <. \ code: 0x00290e group: arrow abbrev: <. \ code: 0x0021e0 group: arrow abbrev: <. \ code: 0x002192 group: arrow group: Z_Notation abbrev: .> abbrev: -> \ code: 0x0027f6 group: arrow abbrev: .> abbrev: --> \ code: 0x00290f group: arrow abbrev: .> abbrev: ---> \ code: 0x0021e2 group: arrow abbrev: .> abbrev: ---> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. \ code: 0x0021da group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => \ code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> \ code: 0x0021db group: arrow abbrev: .> \ code: 0x002194 group: arrow group: Z_Notation abbrev: <> abbrev: <-> \ code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> \ code: 0x0021d4 group: arrow abbrev: <> \ code: 0x0027fa group: arrow abbrev: <> \ code: 0x0021a6 group: arrow group: Z_Notation abbrev: .> abbrev: |-> \ code: 0x0027fc group: arrow abbrev: .> abbrev: |--> \ code: 0x002500 group: arrow abbrev: <> \ code: 0x002550 group: arrow abbrev: <> \ code: 0x0021a9 group: arrow abbrev: <. \ code: 0x0021aa group: arrow abbrev: .> \ code: 0x0021bd group: arrow abbrev: <. \ code: 0x0021c1 group: arrow abbrev: .> \ code: 0x0021bc group: arrow abbrev: <. \ code: 0x0021c0 group: arrow abbrev: .> \ code: 0x0021cc group: arrow abbrev: <> abbrev: == \ code: 0x00219d group: arrow group: Z_Notation abbrev: .> abbrev: ~> \ code: 0x0021c3 group: arrow \ code: 0x0021c2 group: arrow \ code: 0x0021bf group: arrow group: Z_Notation #\ code: 0x0021be group: arrow \ code: 0x0021be group: operator group: Z_Notation \ code: 0x002237 group: punctuation \ code: 0x002191 group: arrow \ code: 0x0021d1 group: arrow \ code: 0x002193 group: arrow \ code: 0x0021d3 group: arrow \ code: 0x002195 group: arrow \ code: 0x0021d5 group: arrow \ code: 0x0027e8 group: punctuation group: Z_Notation abbrev: << \ code: 0x0027e9 group: punctuation group: Z_Notation abbrev: >> \ code: 0x0027ea group: punctuation group: Z_Notation abbrev: << \ code: 0x0027eb group: punctuation group: Z_Notation abbrev: >> \ code: 0x002308 group: punctuation abbrev: [. \ code: 0x002309 group: punctuation abbrev: .] \ code: 0x00230a group: punctuation abbrev: [. \ code: 0x00230b group: punctuation abbrev: .] \ code: 0x002987 group: punctuation group: Z_Notation abbrev: (| \ code: 0x002988 group: punctuation group: Z_Notation abbrev: |) \ code: 0x0027e6 group: punctuation group: Z_Notation abbrev: [| \ code: 0x0027e7 group: punctuation group: Z_Notation abbrev: |] \ code: 0x002983 group: punctuation abbrev: {| \ code: 0x002984 group: punctuation abbrev: |} \ code: 0x002989 group: punctuation group: Z_Notation abbrev: << \ code: 0x00298A group: punctuation group: Z_Notation abbrev: >> \ code: 0x0000ab group: punctuation abbrev: << \ code: 0x0000bb group: punctuation abbrev: >> \ code: 0x0022a5 group: logic \ code: 0x0022a4 group: logic \ code: 0x002227 group: logic abbrev: /\ abbrev: & \ code: 0x0022c0 group: logic abbrev: !! \ code: 0x002228 group: logic abbrev: \/ abbrev: | \ code: 0x0022c1 group: logic abbrev: ?? \ code: 0x002200 group: logic abbrev: ! abbrev: ALL \ code: 0x002203 group: logic abbrev: ? abbrev: EX \ code: 0x002204 group: logic abbrev: ~? \ code: 0x0000ac group: logic abbrev: ~ \ code: 0x0025cb group: logic \ code: 0x0025a1 group: logic \ code: 0x0025c7 group: logic \ code: 0x0022c4 group: operator \ code: 0x0022a2 group: relation abbrev: |- \ code: 0x0022a8 group: relation abbrev: |= \ code: 0x0022a9 group: relation abbrev: |- \ code: 0x0022ab group: relation abbrev: |= \ code: 0x0022a3 group: relation abbrev: -| \ code: 0x00221a group: relation \ code: 0x002264 group: relation abbrev: <= \ code: 0x002265 group: relation abbrev: >= \ code: 0x00226a group: relation abbrev: << \ code: 0x00226b group: relation abbrev: >> \ code: 0x002272 group: relation \ code: 0x002273 group: relation \ code: 0x002a85 group: relation \ code: 0x002a86 group: relation \ code: 0x002208 group: relation abbrev: : \ code: 0x002209 group: relation abbrev: ~: \ code: 0x002282 group: relation \ code: 0x002283 group: relation \ code: 0x002286 group: relation abbrev: (= \ code: 0x002287 group: relation abbrev: )= \ code: 0x00228f group: relation \ code: 0x002290 group: relation \ code: 0x002291 group: relation abbrev: [= \ code: 0x002292 group: relation abbrev: ]= \ code: 0x002229 group: operator abbrev: Int \ code: 0x0022c2 group: operator abbrev: Inter abbrev: INT \ code: 0x00222a group: operator abbrev: Un \ code: 0x0022c3 group: operator abbrev: Union abbrev: UN \ code: 0x002294 group: operator \ code: 0x002a06 group: operator abbrev: SUP \ code: 0x002293 group: operator \ code: 0x002a05 group: operator abbrev: INF \ code: 0x002216 group: operator \ code: 0x00221d group: operator \ code: 0x00228e group: operator group: Z_Notation \ code: 0x002a04 group: operator \ code: 0x002260 group: relation abbrev: ~= \ code: 0x00223c group: relation \ code: 0x002250 group: relation abbrev: .= \ code: 0x002243 group: relation \ code: 0x002248 group: relation \ code: 0x00224d group: relation \ code: 0x002245 group: relation \ code: 0x002323 group: relation \ code: 0x002261 group: relation abbrev: == \ code: 0x002322 group: relation \ code: 0x0022c8 \ code: 0x002a1d \ code: 0x00227a group: relation \ code: 0x00227b group: relation \ code: 0x00227c group: relation \ code: 0x00227d group: relation \ code: 0x002225 group: relation abbrev: || \ code: 0x002016 group: relation abbrev: || \ code: 0x002af4 group: relation abbrev: || \ code: 0x002afd group: relation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || \ code: 0x002aff group: punctuation abbrev: || \ code: 0x0000b1 group: operator \ code: 0x002213 group: operator \ code: 0x0000d7 group: operator abbrev: <*> \
code: 0x0000f7 group: operator \ code: 0x0022c5 group: operator \ code: 0x0022c6 group: operator \ code: 0x002219 group: operator \ code: 0x002218 group: operator \ code: 0x002020 \ code: 0x002021 \ code: 0x0022b2 group: relation \ code: 0x0022b3 group: relation \ code: 0x0022b4 group: relation \ code: 0x0022b5 group: relation \ code: 0x0025c3 group: relation \ code: 0x0025b9 group: relation \ code: 0x0025b3 group: relation \ code: 0x00225c group: relation \ code: 0x002295 group: operator group: Z_Notation \ code: 0x002a01 group: operator \ code: 0x002297 group: operator \ code: 0x002a02 group: operator \ code: 0x002299 group: operator \ code: 0x002a00 group: operator \ code: 0x002296 group: operator \ code: 0x002298 group: operator \ code: 0x002026 group: punctuation abbrev: ... \ code: 0x0022ef group: punctuation \ code: 0x002211 group: operator abbrev: SUM \ code: 0x00220f group: operator abbrev: PROD \ code: 0x002210 group: operator \ code: 0x00221e \ code: 0x00222b group: operator \ code: 0x00222e group: operator \ code: 0x002663 \ code: 0x002662 \ code: 0x002661 \ code: 0x002660 \ code: 0x002135 \ code: 0x002205 \ code: 0x002207 \ code: 0x002202 \ code: 0x00266d \ code: 0x00266e \ code: 0x00266f group: Z_Notation \ code: 0x002220 \ code: 0x0000a9 \ code: 0x0000ae \ code: 0x002010 group: punctuation \ code: 0x0000af group: operator \ code: 0x0000b7 group: punctuation \ code: 0x0000bc group: digit \ code: 0x0000bd group: digit \ code: 0x0000be group: digit \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 \ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac \ code: 0x0000a3 \ code: 0x0000a5 \ code: 0x0000a2 \ code: 0x0000a4 \ code: 0x0000b0 \ code: 0x002a3f group: operator \ code: 0x002127 group: operator \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 group: relation \ code: 0x0000b4 \ code: 0x000131 \ code: 0x0000a8 \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x00291c group: operator abbrev: >>= \ code: 0x002aa2 group: operator group: Z_Notation abbrev: >> \ code: 0x0003f5 \ code: 0x002A3E group: Z_Notation group: punctuation \ code: 0x0021A3 group: Z_Notation group: arrow abbrev: .> \ code: 0x002914 group: Z_Notation group: arrow abbrev: .> \ code: 0x002915 group: Z_Notation group: arrow abbrev: .> \ code: 0x0021A0 group: Z_Notation group: arrow abbrev: .> \ code: 0x002900 group: Z_Notation group: arrow abbrev: .> \ code: 0x002916 group: Z_Notation group: arrow abbrev: .> \ code: 0x0021F8 group: Z_Notation group: arrow abbrev: .> \ code: 0x0021FB group: Z_Notation group: arrow abbrev: .> \ code: 0x0025C1 group: Z_Notation group: relation \ code: 0x002A64 group: Z_Notation group: relation \ code: 0x0025B7 group: Z_Notation group: relation \ code: 0x002A65 group: Z_Notation group: relation \ code: 0x002981 group: Z_Notation group: punctuation \ code: 0x002A1F group: Z_Notation \ code: 0x002A21 group: Z_Notation group: operator \ code: 0x002982 group: Z_Notation group: relation \ code: 0x0029F9 group: Z_Notation group: operator \ code: 0x002040 group: Z_Notation group: operator \ code: 0x0022FF group: Z_Notation group: relation \ code: 0x002032 group: Z_Notation group: punctuation \ code: 0x002311 \ code: 0x0023ce \ code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^latex> group: document argument: cartouche \<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \ code: 0x002713 \ code: 0x002717 \ code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: << \ code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >> \<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono \<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono \<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_( \<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_) \<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^( \<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^) \<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^assert> \<^binding> argument: cartouche \<^can> argument: cartouche \<^class> argument: cartouche \<^class_syntax> argument: cartouche \<^command_keyword> argument: cartouche \<^const> argument: cartouche \<^const_abbrev> argument: cartouche \<^const_name> argument: cartouche \<^const_syntax> argument: cartouche \<^context> \<^cprop> argument: cartouche \<^cterm> argument: cartouche \<^ctyp> argument: cartouche +\<^instantiate> argument: cartouche \<^keyword> argument: cartouche -\<^let> argument: cartouche \<^locale> argument: cartouche \<^make_judgment> \<^dest_judgment> \<^make_string> \<^method> argument: cartouche \<^named_theorems> argument: cartouche \<^nonterminal> argument: cartouche \<^path> argument: cartouche \<^path_binding> argument: cartouche \<^plugin> argument: cartouche \<^print> \<^prop> argument: cartouche \<^bash_function> argument: cartouche \<^scala> argument: cartouche \<^scala_function> argument: cartouche \<^scala_method> argument: cartouche \<^scala_object> argument: cartouche \<^scala_thread> argument: cartouche \<^scala_type> argument: cartouche \<^session> argument: cartouche \<^simproc> argument: cartouche \<^sort> argument: cartouche \<^syntax_const> argument: cartouche \<^system_option> argument: cartouche \<^term> argument: cartouche \<^theory> argument: cartouche \<^theory_context> argument: cartouche \<^tool> argument: cartouche \<^try> argument: cartouche \<^tvar> argument: cartouche \<^typ> argument: cartouche \<^type_abbrev> argument: cartouche \<^type_name> argument: cartouche \<^type_syntax> argument: cartouche \<^var> argument: cartouche \<^oracle_name> argument: cartouche \<^Const> argument: cartouche \<^Const_> argument: cartouche \<^Const_fn> argument: cartouche \<^Type> argument: cartouche \<^Type_fn> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche \<^computation_check> argument: cartouche \<^if_linux> argument: cartouche \<^if_macos> argument: cartouche \<^if_windows> argument: cartouche \<^if_unix> argument: cartouche diff --git a/lib/texinputs/isabellesym.sty b/lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty +++ b/lib/texinputs/isabellesym.sty @@ -1,496 +1,496 @@ %% %% definitions of standard Isabelle symbols %% \newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb \newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb \newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb \newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb \newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb \newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb \newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb \newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb \newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb \newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb \newcommand{\isasymA}{\isamath{\mathcal{A}}} \newcommand{\isasymB}{\isamath{\mathcal{B}}} \newcommand{\isasymC}{\isamath{\mathcal{C}}} \newcommand{\isasymD}{\isamath{\mathcal{D}}} \newcommand{\isasymE}{\isamath{\mathcal{E}}} \newcommand{\isasymF}{\isamath{\mathcal{F}}} \newcommand{\isasymG}{\isamath{\mathcal{G}}} \newcommand{\isasymH}{\isamath{\mathcal{H}}} \newcommand{\isasymI}{\isamath{\mathcal{I}}} \newcommand{\isasymJ}{\isamath{\mathcal{J}}} \newcommand{\isasymK}{\isamath{\mathcal{K}}} \newcommand{\isasymL}{\isamath{\mathcal{L}}} \newcommand{\isasymM}{\isamath{\mathcal{M}}} \newcommand{\isasymN}{\isamath{\mathcal{N}}} \newcommand{\isasymO}{\isamath{\mathcal{O}}} \newcommand{\isasymP}{\isamath{\mathcal{P}}} \newcommand{\isasymQ}{\isamath{\mathcal{Q}}} \newcommand{\isasymR}{\isamath{\mathcal{R}}} \newcommand{\isasymS}{\isamath{\mathcal{S}}} \newcommand{\isasymT}{\isamath{\mathcal{T}}} \newcommand{\isasymU}{\isamath{\mathcal{U}}} \newcommand{\isasymV}{\isamath{\mathcal{V}}} \newcommand{\isasymW}{\isamath{\mathcal{W}}} \newcommand{\isasymX}{\isamath{\mathcal{X}}} \newcommand{\isasymY}{\isamath{\mathcal{Y}}} \newcommand{\isasymZ}{\isamath{\mathcal{Z}}} \newcommand{\isasyma}{\isamath{\mathrm{a}}} \newcommand{\isasymb}{\isamath{\mathrm{b}}} \newcommand{\isasymc}{\isamath{\mathrm{c}}} \newcommand{\isasymd}{\isamath{\mathrm{d}}} \newcommand{\isasyme}{\isamath{\mathrm{e}}} \newcommand{\isasymf}{\isamath{\mathrm{f}}} \newcommand{\isasymg}{\isamath{\mathrm{g}}} \newcommand{\isasymh}{\isamath{\mathrm{h}}} \newcommand{\isasymi}{\isamath{\mathrm{i}}} \newcommand{\isasymj}{\isamath{\mathrm{j}}} \newcommand{\isasymk}{\isamath{\mathrm{k}}} \newcommand{\isasyml}{\isamath{\mathrm{l}}} \newcommand{\isasymm}{\isamath{\mathrm{m}}} \newcommand{\isasymn}{\isamath{\mathrm{n}}} \newcommand{\isasymo}{\isamath{\mathrm{o}}} \newcommand{\isasymp}{\isamath{\mathrm{p}}} \newcommand{\isasymq}{\isamath{\mathrm{q}}} \newcommand{\isasymr}{\isamath{\mathrm{r}}} \newcommand{\isasyms}{\isamath{\mathrm{s}}} \newcommand{\isasymt}{\isamath{\mathrm{t}}} \newcommand{\isasymu}{\isamath{\mathrm{u}}} \newcommand{\isasymv}{\isamath{\mathrm{v}}} \newcommand{\isasymw}{\isamath{\mathrm{w}}} \newcommand{\isasymx}{\isamath{\mathrm{x}}} \newcommand{\isasymy}{\isamath{\mathrm{y}}} \newcommand{\isasymz}{\isamath{\mathrm{z}}} \newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak \newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak \newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak \newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak \newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak \newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak \newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak \newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak \newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak \newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak \newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak \newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak \newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak \newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak \newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak \newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak \newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak \newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak \newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak \newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak \newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak \newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak \newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak \newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak \newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak \newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak \newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak \newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak \newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak \newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak \newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak \newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak \newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak \newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak \newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak \newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak \newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak \newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak \newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak \newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak \newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak \newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak \newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak \newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak \newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak \newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak \newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak \newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak \newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak \newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak \newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak \newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak \newcommand{\isasymalpha}{\isamath{\alpha}} \newcommand{\isasymbeta}{\isamath{\beta}} \newcommand{\isasymgamma}{\isamath{\gamma}} \newcommand{\isasymdelta}{\isamath{\delta}} \newcommand{\isasymepsilon}{\isamath{\varepsilon}} \newcommand{\isasymzeta}{\isamath{\zeta}} \newcommand{\isasymeta}{\isamath{\eta}} \newcommand{\isasymtheta}{\isamath{\vartheta}} \newcommand{\isasymiota}{\isamath{\iota}} \newcommand{\isasymkappa}{\isamath{\kappa}} \newcommand{\isasymlambda}{\isamath{\lambda}} \newcommand{\isasymmu}{\isamath{\mu}} \newcommand{\isasymnu}{\isamath{\nu}} \newcommand{\isasymxi}{\isamath{\xi}} \newcommand{\isasympi}{\isamath{\pi}} \newcommand{\isasymrho}{\isamath{\varrho}} \newcommand{\isasymsigma}{\isamath{\sigma}} \newcommand{\isasymtau}{\isamath{\tau}} \newcommand{\isasymupsilon}{\isamath{\upsilon}} \newcommand{\isasymphi}{\isamath{\varphi}} \newcommand{\isasymchi}{\isamath{\chi}} \newcommand{\isasympsi}{\isamath{\psi}} \newcommand{\isasymomega}{\isamath{\omega}} \newcommand{\isasymGamma}{\isamath{\Gamma}} \newcommand{\isasymDelta}{\isamath{\Delta}} \newcommand{\isasymTheta}{\isamath{\Theta}} \newcommand{\isasymLambda}{\isamath{\Lambda}} \newcommand{\isasymXi}{\isamath{\Xi}} \newcommand{\isasymPi}{\isamath{\Pi}} \newcommand{\isasymSigma}{\isamath{\Sigma}} \newcommand{\isasymUpsilon}{\isamath{\Upsilon}} \newcommand{\isasymPhi}{\isamath{\Phi}} \newcommand{\isasymPsi}{\isamath{\Psi}} \newcommand{\isasymOmega}{\isamath{\Omega}} \newcommand{\isasymbbbA}{\isamath{\bbbA}} %requires font txmia from txfonts \newcommand{\isasymbool}{\isamath{\bbbB}} %requires font txmia from txfonts \newcommand{\isasymcomplex}{\isamath{\bbbC}} %requires font txmia from txfonts \newcommand{\isasymbbbD}{\isamath{\bbbD}} %requires font txmia from txfonts \newcommand{\isasymbbbE}{\isamath{\bbbE}} %requires font txmia from txfonts \newcommand{\isasymbbbF}{\isamath{\bbbF}} %requires font txmia from txfonts \newcommand{\isasymbbbG}{\isamath{\bbbG}} %requires font txmia from txfonts \newcommand{\isasymbbbH}{\isamath{\bbbH}} %requires font txmia from txfonts \newcommand{\isasymbbbI}{\isamath{\bbbI}} %requires font txmia from txfonts \newcommand{\isasymbbbJ}{\isamath{\bbbJ}} %requires font txmia from txfonts \newcommand{\isasymbbbK}{\isamath{\bbbK}} %requires font txmia from txfonts \newcommand{\isasymbbbL}{\isamath{\bbbL}} %requires font txmia from txfonts \newcommand{\isasymbbbM}{\isamath{\bbbM}} %requires font txmia from txfonts \newcommand{\isasymnat}{\isamath{\bbbN}} %requires font txmia from txfonts \newcommand{\isasymbbbO}{\isamath{\bbbO}} %requires font txmia from txfonts \newcommand{\isasymbbbP}{\isamath{\bbbP}} %requires font txmia from txfonts \newcommand{\isasymrat}{\isamath{\bbbQ}} %requires font txmia from txfonts \newcommand{\isasymreal}{\isamath{\bbbR}} %requires font txmia from txfonts \newcommand{\isasymbbbS}{\isamath{\bbbS}} %requires font txmia from txfonts \newcommand{\isasymbbbT}{\isamath{\bbbT}} %requires font txmia from txfonts \newcommand{\isasymbbbU}{\isamath{\bbbU}} %requires font txmia from txfonts \newcommand{\isasymbbbV}{\isamath{\bbbV}} %requires font txmia from txfonts \newcommand{\isasymbbbW}{\isamath{\bbbW}} %requires font txmia from txfonts \newcommand{\isasymbbbX}{\isamath{\bbbX}} %requires font txmia from txfonts \newcommand{\isasymbbbY}{\isamath{\bbbY}} %requires font txmia from txfonts \newcommand{\isasymint}{\isamath{\bbbZ}} %requires font txmia from txfonts \newcommand{\isasymleftarrow}{\isamath{\leftarrow}} \newcommand{\isasymrightarrow}{\isamath{\rightarrow}} \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} \newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} \newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} \newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} \newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb \newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb \newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} \newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} \newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} \newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}} \newcommand{\isasymmapsto}{\isamath{\mapsto}} \newcommand{\isasymlongmapsto}{\isamath{\longmapsto}} \newcommand{\isasymmidarrow}{\isamath{\relbar}} \newcommand{\isasymMidarrow}{\isamath{\Relbar}} \newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}} \newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}} \newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}} \newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}} \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}} \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}} \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} \newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb \newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb \newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb \newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb \newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb \newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb \newcommand{\isasymColon}{\isamath{\mathrel{::}}} \newcommand{\isasymup}{\isamath{\uparrow}} \newcommand{\isasymUp}{\isamath{\Uparrow}} \newcommand{\isasymdown}{\isamath{\downarrow}} \newcommand{\isasymDown}{\isamath{\Downarrow}} \newcommand{\isasymupdown}{\isamath{\updownarrow}} \newcommand{\isasymUpdown}{\isamath{\Updownarrow}} \newcommand{\isasymlangle}{\isamath{\langle}} \newcommand{\isasymrangle}{\isamath{\rangle}} \newcommand{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}} \newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}} \newcommand{\isasymlceil}{\isamath{\lceil}} \newcommand{\isasymrceil}{\isamath{\rceil}} \newcommand{\isasymlfloor}{\isamath{\lfloor}} \newcommand{\isasymrfloor}{\isamath{\rfloor}} \newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3.3mu\mid}}} \newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3.3mu)}}} \newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} \newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} \newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.3mu\mid}}} \newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}} \newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}} \newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}} \newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}} \newcommand{\isasymguillemotright}{\isatext{\guillemotright}} \newcommand{\isasymbottom}{\isamath{\bot}} \newcommand{\isasymtop}{\isamath{\top}} \newcommand{\isasymand}{\isamath{\wedge}} \newcommand{\isasymAnd}{\isamath{\bigwedge}} \newcommand{\isasymor}{\isamath{\vee}} \newcommand{\isasymOr}{\isamath{\bigvee}} \newcommand{\isasymforall}{\isamath{\forall\,}} \newcommand{\isasymexists}{\isamath{\exists\,}} \newcommand{\isasymnot}{\isamath{\neg}} \newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb \newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym \newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb \newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb \newcommand{\isasymdiamondop}{\isamath{\diamond}} \newcommand{\isasymsurd}{\isamath{\surd}} \newcommand{\isasymturnstile}{\isamath{\vdash}} \newcommand{\isasymTurnstile}{\isamath{\models}} \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} \newcommand{\isasymstileturn}{\isamath{\dashv}} \newcommand{\isasymle}{\isamath{\le}} \newcommand{\isasymge}{\isamath{\ge}} \newcommand{\isasymlless}{\isamath{\ll}} \newcommand{\isasymggreater}{\isamath{\gg}} \newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb \newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb \newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb \newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb \newcommand{\isasymin}{\isamath{\in}} \newcommand{\isasymnotin}{\isamath{\notin}} \newcommand{\isasymsubset}{\isamath{\subset}} \newcommand{\isasymsupset}{\isamath{\supset}} \newcommand{\isasymsubseteq}{\isamath{\subseteq}} \newcommand{\isasymsupseteq}{\isamath{\supseteq}} \newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb \newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} \newcommand{\isasyminter}{\isamath{\cap}} \newcommand{\isasymInter}{\isamath{\bigcap\,}} \newcommand{\isasymunion}{\isamath{\cup}} \newcommand{\isasymUnion}{\isamath{\bigcup\,}} \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} \newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymsetminus}{\isamath{\setminus}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymuplus}{\isamath{\uplus}} \newcommand{\isasymUplus}{\isamath{\biguplus\,}} \newcommand{\isasymnoteq}{\isamath{\not=}} \newcommand{\isasymsim}{\isamath{\sim}} \newcommand{\isasymdoteq}{\isamath{\doteq}} \newcommand{\isasymsimeq}{\isamath{\simeq}} \newcommand{\isasymapprox}{\isamath{\approx}} \newcommand{\isasymasymp}{\isamath{\asymp}} \newcommand{\isasymcong}{\isamath{\cong}} \newcommand{\isasymsmile}{\isamath{\smile}} \newcommand{\isasymequiv}{\isamath{\equiv}} \newcommand{\isasymfrown}{\isamath{\frown}} \newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb \newcommand{\isasymbowtie}{\isamath{\bowtie}} \newcommand{\isasymprec}{\isamath{\prec}} \newcommand{\isasymsucc}{\isamath{\succ}} \newcommand{\isasympreceq}{\isamath{\preceq}} \newcommand{\isasymsucceq}{\isamath{\succeq}} \newcommand{\isasymparallel}{\isamath{\parallel}} \newcommand{\isasymParallel}{\isamath{\bigparallel}} %requires stmaryrd \newcommand{\isasyminterleace}{\isamath{\interleave}} %requires stmaryrd \newcommand{\isasymsslash}{\isamath{\sslash}} %requires stmaryrd \newcommand{\isasymbar}{\isamath{\mid}} \newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}} \newcommand{\isasymplusminus}{\isamath{\pm}} \newcommand{\isasymminusplus}{\isamath{\mp}} \newcommand{\isasymtimes}{\isamath{\times}} \newcommand{\isasymdiv}{\isamath{\div}} \newcommand{\isasymcdot}{\isamath{\cdot}} \newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb \newcommand{\isasymstar}{\isamath{\star}} \newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}} \newcommand{\isasymcirc}{\isamath{\circ}} \newcommand{\isasymdagger}{\isamath{\dagger}} \newcommand{\isasymddagger}{\isamath{\ddagger}} \newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb \newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb \newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb \newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}} \newcommand{\isasymtriangleright}{\isamath{\triangleright}} \newcommand{\isasymtriangle}{\isamath{\triangle}} \newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb \newcommand{\isasymoplus}{\isamath{\oplus}} \newcommand{\isasymOplus}{\isamath{\bigoplus\,}} \newcommand{\isasymotimes}{\isamath{\otimes}} \newcommand{\isasymOtimes}{\isamath{\bigotimes\,}} \newcommand{\isasymodot}{\isamath{\odot}} \newcommand{\isasymOdot}{\isamath{\bigodot\,}} \newcommand{\isasymominus}{\isamath{\ominus}} \newcommand{\isasymoslash}{\isamath{\oslash}} \newcommand{\isasymdots}{\isamath{\dots}} \newcommand{\isasymcdots}{\isamath{\cdots}} \newcommand{\isasymSum}{\isamath{\sum\,}} \newcommand{\isasymProd}{\isamath{\prod\,}} \newcommand{\isasymCoprod}{\isamath{\coprod\,}} \newcommand{\isasyminfinity}{\isamath{\infty}} \newcommand{\isasymintegral}{\isamath{\int\,}} \newcommand{\isasymointegral}{\isamath{\oint\,}} \newcommand{\isasymclubsuit}{\isamath{\clubsuit}} \newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}} \newcommand{\isasymheartsuit}{\isamath{\heartsuit}} \newcommand{\isasymspadesuit}{\isamath{\spadesuit}} \newcommand{\isasymaleph}{\isamath{\aleph}} \newcommand{\isasymemptyset}{\isamath{\emptyset}} \newcommand{\isasymnabla}{\isamath{\nabla}} \newcommand{\isasympartial}{\isamath{\partial}} \newcommand{\isasymRe}{\isamath{\Re}} \newcommand{\isasymIm}{\isamath{\Im}} \newcommand{\isasymflat}{\isamath{\flat}} \newcommand{\isasymnatural}{\isamath{\natural}} \newcommand{\isasymsharp}{\isamath{\sharp}} \newcommand{\isasymangle}{\isamath{\angle}} \newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}} \newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}} \newcommand{\isasyminverse}{\isamath{{}^{-1}}} \newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp \newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp \newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp \newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}} \newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}} \newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}} \newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}} \newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}} \newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}} \newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym \newcommand{\isasympounds}{\isamath{\pounds}} \newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb \newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp \newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}} %requires textcomp \newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}} \newcommand{\isasymamalg}{\isamath{\amalg}} \newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb \newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb \newcommand{\isasymwp}{\isamath{\wp}} \newcommand{\isasymwrong}{\isamath{\wr}} \newcommand{\isasymacute}{\isatext{\'\relax}} \newcommand{\isasymindex}{\isatext{\i}} \newcommand{\isasymdieresis}{\isatext{\"\relax}} \newcommand{\isasymcedilla}{\isatext{\c\relax}} \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} %Z notation \newcommand{\isaZhbar}[1]{\rlap{\raise.0001ex\hbox{\isamath{-}}}#1} \newcommand{\isaZpvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 5mu}\hfil\cr#1}} \newcommand{\isaZfvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 3mu\mapstochar\mkern 5mu}\hfil\cr#1}} \newcommand{\isaZdarrow}[3]{\ooalign{\isamath{#1}\hfil\cr\isamath{\mkern#3mu\isamath{#2}}}} \newcommand{\isasymZcomp}{\isamath{\fatsemi}} %requires stmaryrd \newcommand{\isasymZinj}{\isamath{\rightarrowtail}} %requires amssymb \newcommand{\isasymZpinj}{\isaZpvbar{\isamath{\rightarrowtail}}} %requires amssymb \newcommand{\isasymZfinj}{\isaZfvbar{\isasymZinj}} %requires amssymb \newcommand{\isasymZsurj}{\isaZdarrow{\rightarrow}{\rightarrow}{4}} %requires amssymb \newcommand{\isasymZpsurj}{\isaZpvbar{\isasymZsurj}} %requires amssymb \newcommand{\isasymZbij}{\isaZdarrow{\rightarrowtail}{\rightarrow}{5}} %requires amssymb \newcommand{\isasymZpfun}{\isaZpvbar{\isamath{\rightarrow}}} \newcommand{\isasymZffun}{\isaZfvbar{\isamath{\rightarrow}}} \newcommand{\isasymZdres}{\isamath{\lhd}} %requires amssymb \newcommand{\isasymZndres}{\isaZhbar{\isamath{\lhd}}} %requires amssymb \newcommand{\isasymZrres}{\isamath{\rhd}} %requires amssymb \newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}} %requires amssymb \newcommand{\isasymZspot}{\isamath{\bullet}} \newcommand{\isasymZproject}{\isamath{\upharpoonright}} %requires amssymb \newcommand{\isasymZsemi}{\isatext{\raise 0.66ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{9}}\hfil}}}} \newcommand{\isasymZtypecolon}{\isatext{\raise 0.6ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil}}}} \newcommand{\isasymZhide}{\isamath{\backslash}} \newcommand{\isasymZcat}{\isatext{\raise 0.8ex\hbox{\isamath{\mathchar\frown}}}} \newcommand{\isasymZinbag}{\isatext{\ooalign{\isamath{\sqsubset\mkern-1mu}\cr\isamath{-\mkern-1mu}\cr}}} \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymcomment}{\isatext{\isastylecmt---}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} \newcommand{\isasymopen}{\isatext{\guilsinglleft}} \newcommand{\isasymclose}{\isatext{\guilsinglright}} \newcommand{\isasymcheckmark}{\isatext{\ding{51}}} %requires pifont \newcommand{\isasymcrossmark}{\isatext{\ding{55}}} %requires pifont \newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont \newcommand{\isactrltry}{\isakeywordcontrol{try}} \newcommand{\isactrlcan}{\isakeywordcontrol{can}} \newcommand{\isactrlassert}{\isakeywordcontrol{assert}} \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}} \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} \newcommand{\isactrlclass}{\isakeywordcontrol{class}} \newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} \newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} \newcommand{\isactrlconst}{\isakeywordcontrol{const}} \newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} \newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} \newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} \newcommand{\isactrlcontext}{\isakeywordcontrol{context}} \newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} \newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} \newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} \newcommand{\isactrldir}{\isakeywordcontrol{dir}} \newcommand{\isactrlfile}{\isakeywordcontrol{file}} \newcommand{\isactrlhere}{\isakeywordcontrol{here}} +\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}} \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} \newcommand{\isactrllatex}{\isakeywordcontrol{latex}} -\newcommand{\isactrllet}{\isakeywordcontrol{let}} \newcommand{\isactrllocale}{\isakeywordcontrol{locale}} \newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}} \newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}} \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}} \newcommand{\isactrlmethod}{\isakeywordcontrol{method}} \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} \newcommand{\isactrloracleUNDERSCOREname}{\isakeywordcontrol{oracle{\isacharunderscore}name}} \newcommand{\isactrlpath}{\isakeywordcontrol{path}} \newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} \newcommand{\isactrlprint}{\isakeywordcontrol{print}} \newcommand{\isactrlprop}{\isakeywordcontrol{prop}} \newcommand{\isactrlscala}{\isakeywordcontrol{scala}} \newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}} \newcommand{\isactrlscalaUNDERSCOREmethod}{\isakeywordcontrol{scala{\isacharunderscore}method}} \newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}} \newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}} \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} \newcommand{\isactrlsort}{\isakeywordcontrol{sort}} \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} \newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} \newcommand{\isactrlterm}{\isakeywordcontrol{term}} \newcommand{\isactrltheory}{\isakeywordcontrol{theory}} \newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} \newcommand{\isactrltyp}{\isakeywordcontrol{typ}} \newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} \newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} \newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} \newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} \newcommand{\isactrltvar}{\isakeywordcontrol{tvar}} \newcommand{\isactrlvar}{\isakeywordcontrol{var}} \newcommand{\isactrlConst}{\isakeywordcontrol{Const}} \newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}} \newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}} \newcommand{\isactrlType}{\isakeywordcontrol{Type}} \newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}} \newcommand{\isactrlcode}{\isakeywordcontrol{code}} \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} \newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} \newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} \newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}} \newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}} \newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}} \newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}} diff --git a/src/HOL/Decision_Procs/Commutative_Ring.thy b/src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy @@ -1,963 +1,963 @@ (* Title: HOL/Decision_Procs/Commutative_Ring.thy Author: Bernhard Haeupler, Stefan Berghofer, and Amine Chaieb Proving equalities in commutative rings done "right" in Isabelle/HOL. *) section \Proving equalities in commutative rings\ theory Commutative_Ring imports Conversions Algebra_Aux "HOL-Library.Code_Target_Numeral" begin text \Syntax of multivariate polynomials (pol) and polynomial expressions.\ datatype pol = Pc int | Pinj nat pol | PX pol nat pol datatype polex = Var nat | Const int | Add polex polex | Sub polex polex | Mul polex polex | Pow polex nat | Neg polex text \Interpretation functions for the shadow syntax.\ context cring begin definition in_carrier :: "'a list \ bool" where "in_carrier xs \ (\x\set xs. x \ carrier R)" lemma in_carrier_Nil: "in_carrier []" by (simp add: in_carrier_def) lemma in_carrier_Cons: "x \ carrier R \ in_carrier xs \ in_carrier (x # xs)" by (simp add: in_carrier_def) lemma drop_in_carrier [simp]: "in_carrier xs \ in_carrier (drop n xs)" using set_drop_subset [of n xs] by (auto simp add: in_carrier_def) primrec head :: "'a list \ 'a" where "head [] = \" | "head (x # xs) = x" lemma head_closed [simp]: "in_carrier xs \ head xs \ carrier R" by (cases xs) (simp_all add: in_carrier_def) primrec Ipol :: "'a list \ pol \ 'a" where "Ipol l (Pc c) = \c\" | "Ipol l (Pinj i P) = Ipol (drop i l) P" | "Ipol l (PX P x Q) = Ipol l P \ head l [^] x \ Ipol (drop 1 l) Q" lemma Ipol_Pc: "Ipol l (Pc 0) = \" "Ipol l (Pc 1) = \" "Ipol l (Pc (numeral n)) = \numeral n\" "Ipol l (Pc (- numeral n)) = \ \numeral n\" by simp_all lemma Ipol_closed [simp]: "in_carrier l \ Ipol l p \ carrier R" by (induct p arbitrary: l) simp_all primrec Ipolex :: "'a list \ polex \ 'a" where "Ipolex l (Var n) = head (drop n l)" | "Ipolex l (Const i) = \i\" | "Ipolex l (Add P Q) = Ipolex l P \ Ipolex l Q" | "Ipolex l (Sub P Q) = Ipolex l P \ Ipolex l Q" | "Ipolex l (Mul P Q) = Ipolex l P \ Ipolex l Q" | "Ipolex l (Pow p n) = Ipolex l p [^] n" | "Ipolex l (Neg P) = \ Ipolex l P" lemma Ipolex_Const: "Ipolex l (Const 0) = \" "Ipolex l (Const 1) = \" "Ipolex l (Const (numeral n)) = \numeral n\" by simp_all end text \Create polynomial normalized polynomials given normalized inputs.\ definition mkPinj :: "nat \ pol \ pol" where "mkPinj x P = (case P of Pc c \ Pc c | Pinj y P \ Pinj (x + y) P | PX p1 y p2 \ Pinj x P)" definition mkPX :: "pol \ nat \ pol \ pol" where "mkPX P i Q = (case P of Pc c \ if c = 0 then mkPinj 1 Q else PX P i Q | Pinj j R \ PX P i Q | PX P2 i2 Q2 \ if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)" text \Defining the basic ring operations on normalized polynomials\ function add :: "pol \ pol \ pol" (infixl "\+\" 65) where "Pc a \+\ Pc b = Pc (a + b)" | "Pc c \+\ Pinj i P = Pinj i (P \+\ Pc c)" | "Pinj i P \+\ Pc c = Pinj i (P \+\ Pc c)" | "Pc c \+\ PX P i Q = PX P i (Q \+\ Pc c)" | "PX P i Q \+\ Pc c = PX P i (Q \+\ Pc c)" | "Pinj x P \+\ Pinj y Q = (if x = y then mkPinj x (P \+\ Q) else (if x > y then mkPinj y (Pinj (x - y) P \+\ Q) else mkPinj x (Pinj (y - x) Q \+\ P)))" | "Pinj x P \+\ PX Q y R = (if x = 0 then P \+\ PX Q y R else (if x = 1 then PX Q y (R \+\ P) else PX Q y (R \+\ Pinj (x - 1) P)))" | "PX P x R \+\ Pinj y Q = (if y = 0 then PX P x R \+\ Q else (if y = 1 then PX P x (R \+\ Q) else PX P x (R \+\ Pinj (y - 1) Q)))" | "PX P1 x P2 \+\ PX Q1 y Q2 = (if x = y then mkPX (P1 \+\ Q1) x (P2 \+\ Q2) else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \+\ Q1) y (P2 \+\ Q2) else mkPX (PX Q1 (y - x) (Pc 0) \+\ P1) x (P2 \+\ Q2)))" by pat_completeness auto termination by (relation "measure (\(x, y). size x + size y)") auto function mul :: "pol \ pol \ pol" (infixl "\*\" 70) where "Pc a \*\ Pc b = Pc (a * b)" | "Pc c \*\ Pinj i P = (if c = 0 then Pc 0 else mkPinj i (P \*\ Pc c))" | "Pinj i P \*\ Pc c = (if c = 0 then Pc 0 else mkPinj i (P \*\ Pc c))" | "Pc c \*\ PX P i Q = (if c = 0 then Pc 0 else mkPX (P \*\ Pc c) i (Q \*\ Pc c))" | "PX P i Q \*\ Pc c = (if c = 0 then Pc 0 else mkPX (P \*\ Pc c) i (Q \*\ Pc c))" | "Pinj x P \*\ Pinj y Q = (if x = y then mkPinj x (P \*\ Q) else (if x > y then mkPinj y (Pinj (x - y) P \*\ Q) else mkPinj x (Pinj (y - x) Q \*\ P)))" | "Pinj x P \*\ PX Q y R = (if x = 0 then P \*\ PX Q y R else (if x = 1 then mkPX (Pinj x P \*\ Q) y (R \*\ P) else mkPX (Pinj x P \*\ Q) y (R \*\ Pinj (x - 1) P)))" | "PX P x R \*\ Pinj y Q = (if y = 0 then PX P x R \*\ Q else (if y = 1 then mkPX (Pinj y Q \*\ P) x (R \*\ Q) else mkPX (Pinj y Q \*\ P) x (R \*\ Pinj (y - 1) Q)))" | "PX P1 x P2 \*\ PX Q1 y Q2 = mkPX (P1 \*\ Q1) (x + y) (P2 \*\ Q2) \+\ (mkPX (P1 \*\ mkPinj 1 Q2) x (Pc 0) \+\ (mkPX (Q1 \*\ mkPinj 1 P2) y (Pc 0)))" by pat_completeness auto termination by (relation "measure (\(x, y). size x + size y)") (auto simp add: mkPinj_def split: pol.split) text \Negation\ primrec neg :: "pol \ pol" where "neg (Pc c) = Pc (- c)" | "neg (Pinj i P) = Pinj i (neg P)" | "neg (PX P x Q) = PX (neg P) x (neg Q)" text \Subtraction\ definition sub :: "pol \ pol \ pol" (infixl "\-\" 65) where "sub P Q = P \+\ neg Q" text \Square for Fast Exponentiation\ primrec sqr :: "pol \ pol" where "sqr (Pc c) = Pc (c * c)" | "sqr (Pinj i P) = mkPinj i (sqr P)" | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \+\ mkPX (Pc 2 \*\ A \*\ mkPinj 1 B) x (Pc 0)" text \Fast Exponentiation\ fun pow :: "nat \ pol \ pol" where pow_if [simp del]: "pow n P = (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P) else P \*\ pow (n div 2) (sqr P))" lemma pow_simps [simp]: "pow 0 P = Pc 1" "pow (2 * n) P = pow n (sqr P)" "pow (Suc (2 * n)) P = P \*\ pow n (sqr P)" by (simp_all add: pow_if) lemma even_pow: "even n \ pow n P = pow (n div 2) (sqr P)" by (erule evenE) simp lemma odd_pow: "odd n \ pow n P = P \*\ pow (n div 2) (sqr P)" by (erule oddE) simp text \Normalization of polynomial expressions\ primrec norm :: "polex \ pol" where "norm (Var n) = (if n = 0 then PX (Pc 1) 1 (Pc 0) else Pinj n (PX (Pc 1) 1 (Pc 0)))" | "norm (Const i) = Pc i" | "norm (Add P Q) = norm P \+\ norm Q" | "norm (Sub P Q) = norm P \-\ norm Q" | "norm (Mul P Q) = norm P \*\ norm Q" | "norm (Pow P n) = pow n (norm P)" | "norm (Neg P) = neg (norm P)" context cring begin text \mkPinj preserve semantics\ lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)" by (induct B) (auto simp add: mkPinj_def algebra_simps) text \mkPX preserves semantics\ lemma mkPX_ci: "in_carrier l \ Ipol l (mkPX A b C) = Ipol l (PX A b C)" by (cases A) (auto simp add: mkPX_def mkPinj_ci nat_pow_mult [symmetric] m_ac) text \Correctness theorems for the implemented operations\ text \Negation\ lemma neg_ci: "in_carrier l \ Ipol l (neg P) = \ (Ipol l P)" by (induct P arbitrary: l) (auto simp add: minus_add l_minus) text \Addition\ lemma add_ci: "in_carrier l \ Ipol l (P \+\ Q) = Ipol l P \ Ipol l Q" proof (induct P Q arbitrary: l rule: add.induct) case (6 x P y Q) consider "x < y" | "x = y" | "x > y" by arith then show ?case proof cases case 1 with 6 show ?thesis by (simp add: mkPinj_ci a_ac) next case 2 with 6 show ?thesis by (simp add: mkPinj_ci) next case 3 with 6 show ?thesis by (simp add: mkPinj_ci) qed next case (7 x P Q y R) consider "x = 0" | "x = 1" | "x > 1" by arith then show ?case proof cases case 1 with 7 show ?thesis by simp next case 2 with 7 show ?thesis by (simp add: a_ac) next case 3 with 7 show ?thesis by (cases x) (simp_all add: a_ac) qed next case (8 P x R y Q) then show ?case by (simp add: a_ac) next case (9 P1 x P2 Q1 y Q2) consider "x = y" | d where "d + x = y" | d where "d + y = x" by atomize_elim arith then show ?case proof cases case 1 with 9 show ?thesis by (simp add: mkPX_ci r_distr a_ac m_ac) next case 2 with 9 show ?thesis by (auto simp add: mkPX_ci nat_pow_mult [symmetric] r_distr a_ac m_ac) next case 3 with 9 show ?thesis by (auto simp add: nat_pow_mult [symmetric] mkPX_ci r_distr a_ac m_ac) qed qed (auto simp add: a_ac m_ac) text \Multiplication\ lemma mul_ci: "in_carrier l \ Ipol l (P \*\ Q) = Ipol l P \ Ipol l Q" by (induct P Q arbitrary: l rule: mul.induct) (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric]) text \Subtraction\ lemma sub_ci: "in_carrier l \ Ipol l (P \-\ Q) = Ipol l P \ Ipol l Q" by (simp add: add_ci neg_ci sub_def minus_eq) text \Square\ lemma sqr_ci: "in_carrier ls \ Ipol ls (sqr P) = Ipol ls P \ Ipol ls P" by (induct P arbitrary: ls) (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci l_distr r_distr a_ac m_ac nat_pow_mult [symmetric] of_int_2) text \Power\ lemma pow_ci: "in_carrier ls \ Ipol ls (pow n P) = Ipol ls P [^] n" proof (induct n arbitrary: P rule: less_induct) case (less k) consider "k = 0" | "k > 0" by arith then show ?case proof cases case 1 then show ?thesis by simp next case 2 then have "k div 2 < k" by arith with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) [^] (k div 2)" by simp show ?thesis proof (cases "even k") case True with * \in_carrier ls\ show ?thesis by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult mult_2 [symmetric] even_two_times_div_two) next case False with * \in_carrier ls\ show ?thesis by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric]) qed qed qed text \Normalization preserves semantics\ lemma norm_ci: "in_carrier l \ Ipolex l Pe = Ipol l (norm Pe)" by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci) text \Reflection lemma: Key to the (incomplete) decision procedure\ lemma norm_eq: assumes "in_carrier l" and "norm P1 = norm P2" shows "Ipolex l P1 = Ipolex l P2" proof - from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp with assms show ?thesis by (simp only: norm_ci) qed end text \Monomials\ datatype mon = Mc int | Minj nat mon | MX nat mon primrec (in cring) Imon :: "'a list \ mon \ 'a" where "Imon l (Mc c) = \c\" | "Imon l (Minj i M) = Imon (drop i l) M" | "Imon l (MX x M) = Imon (drop 1 l) M \ head l [^] x" lemma (in cring) Imon_closed [simp]: "in_carrier l \ Imon l m \ carrier R" by (induct m arbitrary: l) simp_all definition mkMinj :: "nat \ mon \ mon" where "mkMinj i M = (case M of Mc c \ Mc c | Minj j M \ Minj (i + j) M | _ \ Minj i M)" definition Minj_pred :: "nat \ mon \ mon" where "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)" primrec mkMX :: "nat \ mon \ mon" where "mkMX i (Mc c) = MX i (Mc c)" | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))" | "mkMX i (MX j M) = MX (i + j) M" lemma (in cring) mkMinj_correct: "Imon l (mkMinj i M) = Imon l (Minj i M)" by (simp add: mkMinj_def add.commute split: mon.split) lemma (in cring) Minj_pred_correct: "0 < i \ Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)" by (simp add: Minj_pred_def mkMinj_correct) lemma (in cring) mkMX_correct: "in_carrier l \ Imon l (mkMX i M) = Imon l M \ head l [^] i" by (induct M) (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split) fun cfactor :: "pol \ int \ pol \ pol" where "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))" | "cfactor (Pinj i P) c = (let (R, S) = cfactor P c in (mkPinj i R, mkPinj i S))" | "cfactor (PX P i Q) c = (let (R1, S1) = cfactor P c; (R2, S2) = cfactor Q c in (mkPX R1 i R2, mkPX S1 i S2))" lemma (in cring) cfactor_correct: "in_carrier l \ Ipol l P = Ipol l (fst (cfactor P c)) \ \c\ \ Ipol l (snd (cfactor P c))" proof (induct P c arbitrary: l rule: cfactor.induct) case (1 c' c) show ?case by (simp add: of_int_mult [symmetric] of_int_add [symmetric] del: of_int_mult) next case (2 i P c) then show ?case by (simp add: mkPinj_ci split_beta) next case (3 P i Q c) from 3(1) 3(2) [OF refl prod.collapse] 3(3) show ?case by (simp add: mkPX_ci r_distr a_ac m_ac split_beta) qed fun mfactor :: "pol \ mon \ pol \ pol" where "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)" | "mfactor (Pc d) M = (Pc d, Pc 0)" | "mfactor (Pinj i P) (Minj j M) = (if i = j then let (R, S) = mfactor P M in (mkPinj i R, mkPinj i S) else if i < j then let (R, S) = mfactor P (Minj (j - i) M) in (mkPinj i R, mkPinj i S) else (Pinj i P, Pc 0))" | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)" | "mfactor (PX P i Q) (Minj j M) = (if j = 0 then mfactor (PX P i Q) M else let (R1, S1) = mfactor P (Minj j M); (R2, S2) = mfactor Q (Minj_pred j M) in (mkPX R1 i R2, mkPX S1 i S2))" | "mfactor (PX P i Q) (MX j M) = (if i = j then let (R, S) = mfactor P (mkMinj 1 M) in (mkPX R i Q, S) else if i < j then let (R, S) = mfactor P (MX (j - i) M) in (mkPX R i Q, S) else let (R, S) = mfactor P (mkMinj 1 M) in (mkPX R i Q, mkPX S (i - j) (Pc 0)))" lemmas mfactor_induct = mfactor.induct [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX] lemma (in cring) mfactor_correct: "in_carrier l \ Ipol l P = Ipol l (fst (mfactor P M)) \ Imon l M \ Ipol l (snd (mfactor P M))" proof (induct P M arbitrary: l rule: mfactor_induct) case (Mc P c) then show ?case by (simp add: cfactor_correct) next case (Pc_Minj d i M) then show ?case by simp next case (Pc_MX d i M) then show ?case by simp next case (Pinj_Minj i P j M) then show ?case by (simp add: mkPinj_ci split_beta) next case (Pinj_MX i P j M) then show ?case by simp next case (PX_Minj P i Q j M) from PX_Minj(1,2) PX_Minj(3) [OF _ refl prod.collapse] PX_Minj(4) show ?case by (simp add: mkPX_ci Minj_pred_correct [simplified] r_distr a_ac m_ac split_beta) next case (PX_MX P i Q j M) from \in_carrier l\ have eq1: "(Imon (drop (Suc 0) l) M \ head l [^] (j - i)) \ Ipol l (snd (mfactor P (MX (j - i) M))) \ head l [^] i = Imon (drop (Suc 0) l) M \ Ipol l (snd (mfactor P (MX (j - i) M))) \ (head l [^] (j - i) \ head l [^] i)" by (simp add: m_ac) from \in_carrier l\ have eq2: "(Imon (drop (Suc 0) l) M \ head l [^] j) \ (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \ head l [^] (i - j)) = Imon (drop (Suc 0) l) M \ Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \ (head l [^] (i - j) \ head l [^] j)" by (simp add: m_ac) from PX_MX \in_carrier l\ show ?case by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult) (simp add: a_ac m_ac) qed primrec mon_of_pol :: "pol \ mon option" where "mon_of_pol (Pc c) = Some (Mc c)" | "mon_of_pol (Pinj i P) = (case mon_of_pol P of None \ None | Some M \ Some (mkMinj i M))" | "mon_of_pol (PX P i Q) = (if Q = Pc 0 then (case mon_of_pol P of None \ None | Some M \ Some (mkMX i M)) else None)" lemma (in cring) mon_of_pol_correct: assumes "in_carrier l" and "mon_of_pol P = Some M" shows "Ipol l P = Imon l M" using assms proof (induct P arbitrary: M l) case (PX P1 i P2) from PX(1,3,4) show ?case by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm) qed (auto simp add: mkMinj_correct split: option.split_asm) fun (in cring) Ipolex_polex_list :: "'a list \ (polex \ polex) list \ bool" where "Ipolex_polex_list l [] = True" | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \ Ipolex_polex_list l pps)" fun (in cring) Imon_pol_list :: "'a list \ (mon \ pol) list \ bool" where "Imon_pol_list l [] = True" | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \ Imon_pol_list l mps)" fun mk_monpol_list :: "(polex \ polex) list \ (mon \ pol) list" where "mk_monpol_list [] = []" | "mk_monpol_list ((P, Q) # pps) = (case mon_of_pol (norm P) of None \ mk_monpol_list pps | Some M \ (M, norm Q) # mk_monpol_list pps)" lemma (in cring) mk_monpol_list_correct: "in_carrier l \ Ipolex_polex_list l pps \ Imon_pol_list l (mk_monpol_list pps)" by (induct pps rule: mk_monpol_list.induct) (auto split: option.split simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric]) definition ponesubst :: "pol \ mon \ pol \ pol option" where "ponesubst P1 M P2 = (let (Q, R) = mfactor P1 M in (case R of Pc c \ if c = 0 then None else Some (add Q (mul P2 R)) | _ \ Some (add Q (mul P2 R))))" fun pnsubst1 :: "pol \ mon \ pol \ nat \ pol" where "pnsubst1 P1 M P2 n = (case ponesubst P1 M P2 of None \ P1 | Some P3 \ if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))" lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of None \ P1 | Some P3 \ P3)" by (simp split: option.split) lemma pnsubst1_Suc [simp]: "pnsubst1 P1 M P2 (Suc n) = (case ponesubst P1 M P2 of None \ P1 | Some P3 \ pnsubst1 P3 M P2 n)" by (simp split: option.split) declare pnsubst1.simps [simp del] definition pnsubst :: "pol \ mon \ pol \ nat \ pol option" where "pnsubst P1 M P2 n = (case ponesubst P1 M P2 of None \ None | Some P3 \ Some (pnsubst1 P3 M P2 n))" fun psubstl1 :: "pol \ (mon \ pol) list \ nat \ pol" where "psubstl1 P1 [] n = P1" | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n" fun psubstl :: "pol \ (mon \ pol) list \ nat \ pol option" where "psubstl P1 [] n = None" | "psubstl P1 ((M, P2) # mps) n = (case pnsubst P1 M P2 n of None \ psubstl P1 mps n | Some P3 \ Some (psubstl1 P3 mps n))" fun pnsubstl :: "pol \ (mon \ pol) list \ nat \ nat \ pol" where "pnsubstl P1 mps m n = (case psubstl P1 mps n of None \ P1 | Some P3 \ if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)" lemma pnsubstl_0 [simp]: "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of None \ P1 | Some P3 \ P3)" by (simp split: option.split) lemma pnsubstl_Suc [simp]: "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of None \ P1 | Some P3 \ pnsubstl P3 mps m n)" by (simp split: option.split) declare pnsubstl.simps [simp del] lemma (in cring) ponesubst_correct: "in_carrier l \ ponesubst P1 M P2 = Some P3 \ Imon l M = Ipol l P2 \ Ipol l P1 = Ipol l P3" by (auto simp add: ponesubst_def split_beta mfactor_correct [of l P1 M] add_ci mul_ci split: pol.split_asm if_split_asm) lemma (in cring) pnsubst1_correct: "in_carrier l \ Imon l M = Ipol l P2 \ Ipol l (pnsubst1 P1 M P2 n) = Ipol l P1" by (induct n arbitrary: P1) (simp_all add: ponesubst_correct split: option.split) lemma (in cring) pnsubst_correct: "in_carrier l \ pnsubst P1 M P2 n = Some P3 \ Imon l M = Ipol l P2 \ Ipol l P1 = Ipol l P3" by (auto simp add: pnsubst_def pnsubst1_correct ponesubst_correct split: option.split_asm) lemma (in cring) psubstl1_correct: "in_carrier l \ Imon_pol_list l mps \ Ipol l (psubstl1 P1 mps n) = Ipol l P1" by (induct P1 mps n rule: psubstl1.induct) (simp_all add: pnsubst1_correct) lemma (in cring) psubstl_correct: "in_carrier l \ psubstl P1 mps n = Some P2 \ Imon_pol_list l mps \ Ipol l P1 = Ipol l P2" by (induct P1 mps n rule: psubstl.induct) (auto simp add: psubstl1_correct pnsubst_correct split: option.split_asm) lemma (in cring) pnsubstl_correct: "in_carrier l \ Imon_pol_list l mps \ Ipol l (pnsubstl P1 mps m n) = Ipol l P1" by (induct m arbitrary: P1) (simp_all add: psubstl_correct split: option.split) lemma (in cring) norm_subst_correct: "in_carrier l \ Ipolex_polex_list l pps \ Ipolex l P = Ipol l (pnsubstl (norm P) (mk_monpol_list pps) m n)" by (simp add: pnsubstl_correct mk_monpol_list_correct norm_ci) lemma in_carrier_trivial: "cring_class.in_carrier l" by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class) ML \ val term_of_nat = HOLogic.mk_number \<^Type>\nat\ o @{code integer_of_nat}; val term_of_int = HOLogic.mk_number \<^Type>\int\ o @{code integer_of_int}; fun term_of_pol (@{code Pc} k) = \<^Const>\Pc\ $ term_of_int k | term_of_pol (@{code Pinj} (n, p)) = \<^Const>\Pinj\ $ term_of_nat n $ term_of_pol p | term_of_pol (@{code PX} (p, n, q)) = \<^Const>\PX\ $ term_of_pol p $ term_of_nat n $ term_of_pol q; local fun pol (ctxt, ct, t) = - \<^let>\x = ct and y = \Thm.cterm_of ctxt t\ + \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: pol\; val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\pnsubstl\, pol))); fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t); in val cv = @{computation_conv pol terms: pnsubstl mk_monpol_list norm nat_of_integer Code_Target_Nat.natural "0::nat" "1::nat" "2::nat" "3::nat" "0::int" "1::int" "2::int" "3::int" "-1::int" datatypes: polex "(polex * polex) list" int integer num} (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p)) end \ ML \ signature RING_TAC = sig structure Ring_Simps: sig type T val get: Context.generic -> T val put: T -> Context.generic -> Context.generic val map: (T -> T) -> Context.generic -> Context.generic end val insert_rules: ((term * 'a) * (term * 'a) -> bool) -> (term * 'a) -> (term * 'a) Net.net -> (term * 'a) Net.net val eq_ring_simps: (term * (thm list * thm list * thm list * thm list * thm * thm)) * (term * (thm list * thm list * thm list * thm list * thm * thm)) -> bool val ring_tac: bool -> thm list -> Proof.context -> int -> tactic val get_matching_rules: Proof.context -> (term * 'a) Net.net -> term -> 'a option val norm: thm -> thm val mk_in_carrier: Proof.context -> term -> thm list -> (string * typ) list -> thm val mk_ring: typ -> term end structure Ring_Tac : RING_TAC = struct fun eq_ring_simps ((t, (ths1, ths2, ths3, ths4, th5, th)), (t', (ths1', ths2', ths3', ths4', th5', th'))) = t aconv t' andalso eq_list Thm.eq_thm (ths1, ths1') andalso eq_list Thm.eq_thm (ths2, ths2') andalso eq_list Thm.eq_thm (ths3, ths3') andalso eq_list Thm.eq_thm (ths4, ths4') andalso Thm.eq_thm (th5, th5') andalso Thm.eq_thm (th, th'); structure Ring_Simps = Generic_Data (struct type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net val empty = Net.empty val merge = Net.merge eq_ring_simps end); fun get_matching_rules ctxt net t = get_first (fn (p, x) => if Pattern.matches (Proof_Context.theory_of ctxt) (p, t) then SOME x else NONE) (Net.match_term net t); fun insert_rules eq (t, x) = Net.insert_term eq (t, (t, x)); fun norm thm = thm COMP_INCR asm_rl; fun get_ring_simps ctxt optcT t = (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of SOME (ths1, ths2, ths3, ths4, th5, th) => let val tr = Thm.transfer' ctxt #> (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end | NONE => error "get_ring_simps: lookup failed"); fun ring_struct \<^Const_>\Ring.ring.add _ _ for R _ _\ = SOME R | ring_struct \<^Const_>\Ring.a_minus _ _ for R _ _\ = SOME R | ring_struct \<^Const_>\Group.monoid.mult _ _ for R _ _\ = SOME R | ring_struct \<^Const_>\Ring.a_inv _ _ for R _\ = SOME R | ring_struct \<^Const_>\Group.pow _ _ _ for R _ _\ = SOME R | ring_struct \<^Const_>\Ring.ring.zero _ _ for R\ = SOME R | ring_struct \<^Const_>\Group.monoid.one _ _ for R\ = SOME R | ring_struct \<^Const_>\Algebra_Aux.of_integer _ _ for R _\ = SOME R | ring_struct _ = NONE; fun reif_polex vs \<^Const_>\Ring.ring.add _ _ for _ a b\ = \<^Const>\Add for \reif_polex vs a\ \reif_polex vs b\\ | reif_polex vs \<^Const_>\Ring.a_minus _ _ for _ a b\ = \<^Const>\Sub for \reif_polex vs a\ \reif_polex vs b\\ | reif_polex vs \<^Const_>\Group.monoid.mult _ _ for _ a b\ = \<^Const>\Mul for \reif_polex vs a\ \reif_polex vs b\\ | reif_polex vs \<^Const_>\Ring.a_inv _ _ for _ a\ = \<^Const>\Neg for \reif_polex vs a\\ | reif_polex vs \<^Const_>\Group.pow _ _ _ for _ a n\ = \<^Const>\Pow for \reif_polex vs a\ n\ | reif_polex vs (Free x) = \<^Const>\Var for \HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\\ | reif_polex _ \<^Const_>\Ring.ring.zero _ _ for _\ = \<^term>\Const 0\ | reif_polex _ \<^Const_>\Group.monoid.one _ _ for _\ = \<^term>\Const 1\ | reif_polex _ \<^Const_>\Algebra_Aux.of_integer _ _ for _ n\ = \<^Const>\Const for n\ | reif_polex _ _ = error "reif_polex: bad expression"; fun reif_polex' vs \<^Const_>\plus _ for a b\ = \<^Const>\Add for \reif_polex' vs a\ \reif_polex' vs b\\ | reif_polex' vs \<^Const_>\minus _ for a b\ = \<^Const>\Sub for \reif_polex' vs a\ \reif_polex' vs b\\ | reif_polex' vs \<^Const_>\times _ for a b\ = \<^Const>\Mul for \reif_polex' vs a\ \reif_polex' vs b\\ | reif_polex' vs \<^Const_>\uminus _ for a\ = \<^Const>\Neg for \reif_polex' vs a\\ | reif_polex' vs \<^Const_>\power _ for a n\ = \<^Const>\Pow for \reif_polex' vs a\ n\ | reif_polex' vs (Free x) = \<^Const>\Var for \HOLogic.mk_number \<^Type>\nat\ (find_index (equal x) vs)\\ | reif_polex' _ \<^Const_>\numeral _ for b\ = \<^Const>\Const for \<^Const>\numeral \<^Type>\int\ for b\\ | reif_polex' _ \<^Const_>\zero_class.zero _\ = \<^term>\Const 0\ | reif_polex' _ \<^Const_>\one_class.one _\ = \<^term>\Const 1\ | reif_polex' _ t = error "reif_polex: bad expression"; fun head_conv (_, _, _, _, head_simp, _) ys = (case strip_app ys of (\<^const_name>\Cons\, [y, xs]) => inst [] [y, xs] head_simp); fun Ipol_conv (rls as ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3, Ipol_simps_4, Ipol_simps_5, Ipol_simps_6, Ipol_simps_7], _, _, _, _, _)) = let val a = type_of_eqn Ipol_simps_1; val drop_conv_a = drop_conv a; fun conv l p = (case strip_app p of (\<^const_name>\Pc\, [c]) => (case strip_numeral c of (\<^const_name>\zero_class.zero\, _) => inst [] [l] Ipol_simps_4 | (\<^const_name>\one_class.one\, _) => inst [] [l] Ipol_simps_5 | (\<^const_name>\numeral\, [m]) => inst [] [l, m] Ipol_simps_6 | (\<^const_name>\uminus\, [m]) => inst [] [l, m] Ipol_simps_7 | _ => inst [] [l, c] Ipol_simps_1) | (\<^const_name>\Pinj\, [i, P]) => transitive' (inst [] [l, i, P] Ipol_simps_2) (cong2' conv (args2 drop_conv_a) Thm.reflexive) | (\<^const_name>\PX\, [P, x, Q]) => transitive' (inst [] [l, P, x, Q] Ipol_simps_3) (cong2 (cong2 (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive)) (cong2' conv (args2 drop_conv_a) Thm.reflexive))) in conv end; fun Ipolex_conv (rls as (_, [Ipolex_Var, Ipolex_Const, Ipolex_Add, Ipolex_Sub, Ipolex_Mul, Ipolex_Pow, Ipolex_Neg, Ipolex_Const_0, Ipolex_Const_1, Ipolex_Const_numeral], _, _, _, _)) = let val a = type_of_eqn Ipolex_Var; val drop_conv_a = drop_conv a; fun conv l r = (case strip_app r of (\<^const_name>\Var\, [n]) => transitive' (inst [] [l, n] Ipolex_Var) (cong1' (head_conv rls) (args2 drop_conv_a)) | (\<^const_name>\Const\, [i]) => (case strip_app i of (\<^const_name>\zero_class.zero\, _) => inst [] [l] Ipolex_Const_0 | (\<^const_name>\one_class.one\, _) => inst [] [l] Ipolex_Const_1 | (\<^const_name>\numeral\, [m]) => inst [] [l, m] Ipolex_Const_numeral | _ => inst [] [l, i] Ipolex_Const) | (\<^const_name>\Add\, [P, Q]) => transitive' (inst [] [l, P, Q] Ipolex_Add) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\Sub\, [P, Q]) => transitive' (inst [] [l, P, Q] Ipolex_Sub) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\Mul\, [P, Q]) => transitive' (inst [] [l, P, Q] Ipolex_Mul) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\Pow\, [P, n]) => transitive' (inst [] [l, P, n] Ipolex_Pow) (cong2 (args2 conv) Thm.reflexive) | (\<^const_name>\Neg\, [P]) => transitive' (inst [] [l, P] Ipolex_Neg) (cong1 (args2 conv))) in conv end; fun Ipolex_polex_list_conv (rls as (_, _, [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps = (case strip_app pps of (\<^const_name>\Nil\, []) => inst [] [l] Ipolex_polex_list_Nil | (\<^const_name>\Cons\, [p, pps']) => (case strip_app p of (\<^const_name>\Pair\, [P, Q]) => transitive' (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons) (cong2 (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls))) (args2 (Ipolex_polex_list_conv rls))))); fun dest_conj th = let val th1 = th RS @{thm conjunct1}; val th2 = th RS @{thm conjunct2} in dest_conj th1 @ dest_conj th2 end handle THM _ => [th]; fun mk_in_carrier ctxt R prems xs = let val (_, _, _, [in_carrier_Nil, in_carrier_Cons], _, _) = get_ring_simps ctxt NONE R; val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems; val ths = map (fn p as (x, _) => (case find_first ((fn \<^Const_>\Trueprop for \<^Const_>\Set.member _ for \Free (y, _)\ \<^Const_>\carrier _ _ for S\\\ => x = y andalso R aconv S | _ => false) o Thm.prop_of) props of SOME th => th | NONE => error ("Variable " ^ Syntax.string_of_term ctxt (Free p) ^ " not in carrier"))) xs in fold_rev (fn th1 => fn th2 => [th1, th2] MRS in_carrier_Cons) ths in_carrier_Nil end; fun mk_ring T = \<^Const>\cring_class_ops T\; val iterations = \<^cterm>\1000::nat\; val Trueprop_cong = Thm.combination (Thm.reflexive \<^cterm>\Trueprop\); fun commutative_ring_conv ctxt prems eqs ct = let val cT = Thm.ctyp_of_cterm ct; val T = Thm.typ_of cT; val eqs' = map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) eqs; val xs = filter (equal T o snd) (rev (fold Term.add_frees (map fst eqs' @ map snd eqs' @ [Thm.term_of ct]) [])); val (R, optcT, prem', reif) = (case ring_struct (Thm.term_of ct) of SOME R => (R, NONE, mk_in_carrier ctxt R prems xs, reif_polex xs) | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs)); val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R; val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs)); val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\polex \ polex\ (map (HOLogic.mk_prod o apply2 reif) eqs')); val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct)); val prem = Thm.equal_elim (Trueprop_cong (Thm.symmetric (Ipolex_polex_list_conv rls cxs ceqs))) (fold_rev (fn th1 => fn th2 => [th1, th2] MRS @{thm conjI}) eqs @{thm TrueI}); in Thm.transitive (Thm.symmetric (Ipolex_conv rls cxs cp)) (transitive' ([prem', prem] MRS inst [] [cxs, ceqs, cp, iterations, iterations] norm_subst_correct) (cong2' (Ipol_conv rls) Thm.reflexive (cv ctxt))) end; fun ring_tac in_prems thms ctxt = tactic_of_conv (fn ct => (if in_prems then Conv.prems_conv else Conv.concl_conv) (Logic.count_prems (Thm.term_of ct)) (Conv.arg_conv (Conv.binop_conv (commutative_ring_conv ctxt [] thms))) ct) THEN' TRY o (assume_tac ctxt ORELSE' resolve_tac ctxt [@{thm refl}]); end \ context cring begin local_setup \ Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps (Morphism.term phi \<^term>\R\, (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]}, Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]}, Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]}, Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons}, singleton (Morphism.fact phi) @{thm head.simps(2) [meta]}, singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]})))) \ end method_setup ring = \ Scan.lift (Args.mode "prems") -- Attrib.thms >> (SIMPLE_METHOD' oo uncurry Ring_Tac.ring_tac) \ "simplify equations involving rings" end diff --git a/src/HOL/Decision_Procs/Reflective_Field.thy b/src/HOL/Decision_Procs/Reflective_Field.thy --- a/src/HOL/Decision_Procs/Reflective_Field.thy +++ b/src/HOL/Decision_Procs/Reflective_Field.thy @@ -1,930 +1,930 @@ (* Title: HOL/Decision_Procs/Reflective_Field.thy Author: Stefan Berghofer Reducing equalities in fields to equalities in rings. *) theory Reflective_Field imports Commutative_Ring begin datatype fexpr = FCnst int | FVar nat | FAdd fexpr fexpr | FSub fexpr fexpr | FMul fexpr fexpr | FNeg fexpr | FDiv fexpr fexpr | FPow fexpr nat fun (in field) nth_el :: "'a list \ nat \ 'a" where "nth_el [] n = \" | "nth_el (x # xs) 0 = x" | "nth_el (x # xs) (Suc n) = nth_el xs n" lemma (in field) nth_el_Cons: "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))" by (cases n) simp_all lemma (in field) nth_el_closed [simp]: "in_carrier xs \ nth_el xs n \ carrier R" by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def) primrec (in field) feval :: "'a list \ fexpr \ 'a" where "feval xs (FCnst c) = \c\" | "feval xs (FVar n) = nth_el xs n" | "feval xs (FAdd a b) = feval xs a \ feval xs b" | "feval xs (FSub a b) = feval xs a \ feval xs b" | "feval xs (FMul a b) = feval xs a \ feval xs b" | "feval xs (FNeg a) = \ feval xs a" | "feval xs (FDiv a b) = feval xs a \ feval xs b" | "feval xs (FPow a n) = feval xs a [^] n" lemma (in field) feval_Cnst: "feval xs (FCnst 0) = \" "feval xs (FCnst 1) = \" "feval xs (FCnst (numeral n)) = \numeral n\" by simp_all datatype pexpr = PExpr1 pexpr1 | PExpr2 pexpr2 and pexpr1 = PCnst int | PVar nat | PAdd pexpr pexpr | PSub pexpr pexpr | PNeg pexpr and pexpr2 = PMul pexpr pexpr | PPow pexpr nat lemma pexpr_cases [case_names PCnst PVar PAdd PSub PNeg PMul PPow]: assumes "\c. e = PExpr1 (PCnst c) \ P" "\n. e = PExpr1 (PVar n) \ P" "\e1 e2. e = PExpr1 (PAdd e1 e2) \ P" "\e1 e2. e = PExpr1 (PSub e1 e2) \ P" "\e'. e = PExpr1 (PNeg e') \ P" "\e1 e2. e = PExpr2 (PMul e1 e2) \ P" "\e' n. e = PExpr2 (PPow e' n) \ P" shows P proof (cases e) case (PExpr1 e') then show ?thesis apply (cases e') apply simp_all apply (erule assms)+ done next case (PExpr2 e') then show ?thesis apply (cases e') apply simp_all apply (erule assms)+ done qed lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases] fun (in field) peval :: "'a list \ pexpr \ 'a" where "peval xs (PExpr1 (PCnst c)) = \c\" | "peval xs (PExpr1 (PVar n)) = nth_el xs n" | "peval xs (PExpr1 (PAdd a b)) = peval xs a \ peval xs b" | "peval xs (PExpr1 (PSub a b)) = peval xs a \ peval xs b" | "peval xs (PExpr1 (PNeg a)) = \ peval xs a" | "peval xs (PExpr2 (PMul a b)) = peval xs a \ peval xs b" | "peval xs (PExpr2 (PPow a n)) = peval xs a [^] n" lemma (in field) peval_Cnst: "peval xs (PExpr1 (PCnst 0)) = \" "peval xs (PExpr1 (PCnst 1)) = \" "peval xs (PExpr1 (PCnst (numeral n))) = \numeral n\" "peval xs (PExpr1 (PCnst (- numeral n))) = \ \numeral n\" by simp_all lemma (in field) peval_closed [simp]: "in_carrier xs \ peval xs e \ carrier R" "in_carrier xs \ peval xs (PExpr1 e1) \ carrier R" "in_carrier xs \ peval xs (PExpr2 e2) \ carrier R" by (induct e and e1 and e2) simp_all definition npepow :: "pexpr \ nat \ pexpr" where "npepow e n = (if n = 0 then PExpr1 (PCnst 1) else if n = 1 then e else (case e of PExpr1 (PCnst c) \ PExpr1 (PCnst (c ^ n)) | _ \ PExpr2 (PPow e n)))" lemma (in field) npepow_correct: "in_carrier xs \ peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))" by (cases e rule: pexpr_cases) (simp_all add: npepow_def) fun npemul :: "pexpr \ pexpr \ pexpr" where "npemul x y = (case x of PExpr1 (PCnst c) \ if c = 0 then x else if c = 1 then y else (case y of PExpr1 (PCnst d) \ PExpr1 (PCnst (c * d)) | _ \ PExpr2 (PMul x y)) | PExpr2 (PPow e1 n) \ (case y of PExpr2 (PPow e2 m) \ if n = m then npepow (npemul e1 e2) n else PExpr2 (PMul x y) | PExpr1 (PCnst d) \ if d = 0 then y else if d = 1 then x else PExpr2 (PMul x y) | _ \ PExpr2 (PMul x y)) | _ \ (case y of PExpr1 (PCnst d) \ if d = 0 then y else if d = 1 then x else PExpr2 (PMul x y) | _ \ PExpr2 (PMul x y)))" lemma (in field) npemul_correct: "in_carrier xs \ peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))" proof (induct e1 e2 rule: npemul.induct) case (1 x y) then show ?case proof (cases x y rule: pexpr_cases2) case (PPow_PPow e n e' m) then show ?thesis by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distrib npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"]) qed simp_all qed declare npemul.simps [simp del] definition npeadd :: "pexpr \ pexpr \ pexpr" where "npeadd x y = (case x of PExpr1 (PCnst c) \ if c = 0 then y else (case y of PExpr1 (PCnst d) \ PExpr1 (PCnst (c + d)) | _ \ PExpr1 (PAdd x y)) | _ \ (case y of PExpr1 (PCnst d) \ if d = 0 then x else PExpr1 (PAdd x y) | _ \ PExpr1 (PAdd x y)))" lemma (in field) npeadd_correct: "in_carrier xs \ peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))" by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def) definition npesub :: "pexpr \ pexpr \ pexpr" where "npesub x y = (case y of PExpr1 (PCnst d) \ if d = 0 then x else (case x of PExpr1 (PCnst c) \ PExpr1 (PCnst (c - d)) | _ \ PExpr1 (PSub x y)) | _ \ (case x of PExpr1 (PCnst c) \ if c = 0 then PExpr1 (PNeg y) else PExpr1 (PSub x y) | _ \ PExpr1 (PSub x y)))" lemma (in field) npesub_correct: "in_carrier xs \ peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))" by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def) definition npeneg :: "pexpr \ pexpr" where "npeneg e = (case e of PExpr1 (PCnst c) \ PExpr1 (PCnst (- c)) | _ \ PExpr1 (PNeg e))" lemma (in field) npeneg_correct: "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))" by (cases e rule: pexpr_cases) (simp_all add: npeneg_def) lemma option_pair_cases [case_names None Some]: obtains (None) "x = None" | (Some) p q where "x = Some (p, q)" proof (cases x) case None then show ?thesis by (rule that) next case (Some r) then show ?thesis by (cases r, simp) (rule that) qed fun isin :: "pexpr \ nat \ pexpr \ nat \ (nat \ pexpr) option" where "isin e n (PExpr2 (PMul e1 e2)) m = (case isin e n e1 m of Some (k, e3) \ if k = 0 then Some (0, npemul e3 (npepow e2 m)) else (case isin e k e2 m of Some (l, e4) \ Some (l, npemul e3 e4) | None \ Some (k, npemul e3 (npepow e2 m))) | None \ (case isin e n e2 m of Some (k, e3) \ Some (k, npemul (npepow e1 m) e3) | None \ None))" | "isin e n (PExpr2 (PPow e' k)) m = (if k = 0 then None else isin e n e' (k * m))" | "isin (PExpr1 e) n (PExpr1 e') m = (if e = e' then if n \ m then Some (n - m, PExpr1 (PCnst 1)) else Some (0, npepow (PExpr1 e) (m - n)) else None)" | "isin (PExpr2 e) n (PExpr1 e') m = None" lemma (in field) isin_correct: assumes "in_carrier xs" and "isin e n e' m = Some (p, e'')" shows "peval xs (PExpr2 (PPow e' m)) = peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))" and "p \ n" using assms by (induct e n e' m arbitrary: p e'' rule: isin.induct) (force simp add: nat_pow_distrib nat_pow_pow nat_pow_mult m_ac npemul_correct npepow_correct split: option.split_asm prod.split_asm if_split_asm)+ lemma (in field) isin_correct': "in_carrier xs \ isin e n e' 1 = Some (p, e'') \ peval xs e' = peval xs e [^] (n - p) \ peval xs e''" "in_carrier xs \ isin e n e' 1 = Some (p, e'') \ p \ n" using isin_correct [where m = 1] by simp_all fun split_aux :: "pexpr \ nat \ pexpr \ pexpr \ pexpr \ pexpr" where "split_aux (PExpr2 (PMul e1 e2)) n e = (let (left1, common1, right1) = split_aux e1 n e; (left2, common2, right2) = split_aux e2 n right1 in (npemul left1 left2, npemul common1 common2, right2))" | "split_aux (PExpr2 (PPow e' m)) n e = (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e) else split_aux e' (m * n) e)" | "split_aux (PExpr1 e') n e = (case isin (PExpr1 e') n e 1 of Some (m, e'') \ (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'') else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e'')) | None \ (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))" hide_const Left Right (* FIXME !? *) abbreviation Left :: "pexpr \ pexpr \ pexpr" where "Left e1 e2 \ fst (split_aux e1 (Suc 0) e2)" abbreviation Common :: "pexpr \ pexpr \ pexpr" where "Common e1 e2 \ fst (snd (split_aux e1 (Suc 0) e2))" abbreviation Right :: "pexpr \ pexpr \ pexpr" where "Right e1 e2 \ snd (snd (split_aux e1 (Suc 0) e2))" lemma split_aux_induct [case_names 1 2 3]: assumes I1: "\e1 e2 n e. P e1 n e \ P e2 n (snd (snd (split_aux e1 n e))) \ P (PExpr2 (PMul e1 e2)) n e" and I2: "\e' m n e. (m \ 0 \ P e' (m * n) e) \ P (PExpr2 (PPow e' m)) n e" and I3: "\e' n e. P (PExpr1 e') n e" shows "P x y z" proof (induct x y z rule: split_aux.induct) case 1 from 1(1) 1(2) [OF refl prod.collapse prod.collapse] show ?case by (rule I1) next case 2 then show ?case by (rule I2) next case 3 then show ?case by (rule I3) qed lemma (in field) split_aux_correct: "in_carrier xs \ peval xs (PExpr2 (PPow e\<^sub>1 n)) = peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))" "in_carrier xs \ peval xs e\<^sub>2 = peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))" by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct) (auto simp add: split_beta nat_pow_distrib nat_pow_pow nat_pow_mult m_ac npemul_correct npepow_correct isin_correct' split: option.split) lemma (in field) split_aux_correct': "in_carrier xs \ peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \ peval xs (Common e\<^sub>1 e\<^sub>2)" "in_carrier xs \ peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \ peval xs (Common e\<^sub>1 e\<^sub>2)" using split_aux_correct [where n = 1] by simp_all fun fnorm :: "fexpr \ pexpr \ pexpr \ pexpr list" where "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])" | "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])" | "fnorm (FAdd e1 e2) = (let (xn, xd, xc) = fnorm e1; (yn, yd, yc) = fnorm e2; (left, common, right) = split_aux xd 1 yd in (npeadd (npemul xn right) (npemul yn left), npemul left (npemul right common), List.union xc yc))" | "fnorm (FSub e1 e2) = (let (xn, xd, xc) = fnorm e1; (yn, yd, yc) = fnorm e2; (left, common, right) = split_aux xd 1 yd in (npesub (npemul xn right) (npemul yn left), npemul left (npemul right common), List.union xc yc))" | "fnorm (FMul e1 e2) = (let (xn, xd, xc) = fnorm e1; (yn, yd, yc) = fnorm e2; (left1, common1, right1) = split_aux xn 1 yd; (left2, common2, right2) = split_aux yn 1 xd in (npemul left1 left2, npemul right2 right1, List.union xc yc))" | "fnorm (FNeg e) = (let (n, d, c) = fnorm e in (npeneg n, d, c))" | "fnorm (FDiv e1 e2) = (let (xn, xd, xc) = fnorm e1; (yn, yd, yc) = fnorm e2; (left1, common1, right1) = split_aux xn 1 yn; (left2, common2, right2) = split_aux xd 1 yd in (npemul left1 right2, npemul left2 right1, List.insert yn (List.union xc yc)))" | "fnorm (FPow e m) = (let (n, d, c) = fnorm e in (npepow n m, npepow d m, c))" abbreviation Num :: "fexpr \ pexpr" where "Num e \ fst (fnorm e)" abbreviation Denom :: "fexpr \ pexpr" where "Denom e \ fst (snd (fnorm e))" abbreviation Cond :: "fexpr \ pexpr list" where "Cond e \ snd (snd (fnorm e))" primrec (in field) nonzero :: "'a list \ pexpr list \ bool" where "nonzero xs [] \ True" | "nonzero xs (p # ps) \ peval xs p \ \ \ nonzero xs ps" lemma (in field) nonzero_singleton: "nonzero xs [p] = (peval xs p \ \)" by simp lemma (in field) nonzero_append: "nonzero xs (ps @ qs) = (nonzero xs ps \ nonzero xs qs)" by (induct ps) simp_all lemma (in field) nonzero_idempotent: "p \ set ps \ (peval xs p \ \ \ nonzero xs ps) = nonzero xs ps" by (induct ps) auto lemma (in field) nonzero_insert: "nonzero xs (List.insert p ps) = (peval xs p \ \ \ nonzero xs ps)" by (simp add: List.insert_def nonzero_idempotent) lemma (in field) nonzero_union: "nonzero xs (List.union ps qs) = (nonzero xs ps \ nonzero xs qs)" by (induct ps rule: rev_induct) (auto simp add: List.union_def nonzero_insert nonzero_append) lemma (in field) fnorm_correct: assumes "in_carrier xs" and "nonzero xs (Cond e)" shows "feval xs e = peval xs (Num e) \ peval xs (Denom e)" and "peval xs (Denom e) \ \" using assms proof (induct e) case (FCnst c) { case 1 show ?case by simp next case 2 show ?case by simp } next case (FVar n) { case 1 then show ?case by simp next case 2 show ?case by simp } next case (FAdd e1 e2) note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"] { case 1 let ?left = "peval xs (Left (Denom e1) (Denom e2))" let ?common = "peval xs (Common (Denom e1) (Denom e2))" let ?right = "peval xs (Right (Denom e1) (Denom e2))" from 1 FAdd have "feval xs (FAdd e1 e2) = (?common \ (peval xs (Num e1) \ ?right \ peval xs (Num e2) \ ?left)) \ (?common \ (?left \ (?right \ ?common)))" by (simp add: split_beta split nonzero_union add_frac_eq r_distr m_ac) also from 1 FAdd have "\ = peval xs (Num (FAdd e1 e2)) \ peval xs (Denom (FAdd e1 e2))" by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff) finally show ?case . next case 2 with FAdd show ?case by (simp add: split_beta split nonzero_union npemul_correct integral_iff) } next case (FSub e1 e2) note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"] { case 1 let ?left = "peval xs (Left (Denom e1) (Denom e2))" let ?common = "peval xs (Common (Denom e1) (Denom e2))" let ?right = "peval xs (Right (Denom e1) (Denom e2))" from 1 FSub have "feval xs (FSub e1 e2) = (?common \ (peval xs (Num e1) \ ?right \ peval xs (Num e2) \ ?left)) \ (?common \ (?left \ (?right \ ?common)))" by (simp add: split_beta split nonzero_union diff_frac_eq r_diff_distr m_ac) also from 1 FSub have "\ = peval xs (Num (FSub e1 e2)) \ peval xs (Denom (FSub e1 e2))" by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff) finally show ?case . next case 2 with FSub show ?case by (simp add: split_beta split nonzero_union npemul_correct integral_iff) } next case (FMul e1 e2) note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Denom e2"] split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e2" and e\<^sub>2 = "Denom e1"] { case 1 let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))" let ?common\<^sub>1 = "peval xs (Common (Num e1) (Denom e2))" let ?right\<^sub>1 = "peval xs (Right (Num e1) (Denom e2))" let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))" let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))" let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))" from 1 FMul have "feval xs (FMul e1 e2) = ((?common\<^sub>1 \ ?common\<^sub>2) \ (?left\<^sub>1 \ ?left\<^sub>2)) \ ((?common\<^sub>1 \ ?common\<^sub>2) \ (?right\<^sub>2 \ ?right\<^sub>1))" by (simp add: split_beta split nonzero_union nonzero_divide_divide_eq_left m_ac) also from 1 FMul have "\ = peval xs (Num (FMul e1 e2)) \ peval xs (Denom (FMul e1 e2))" by (simp add: split_beta split nonzero_union npemul_correct integral_iff) finally show ?case . next case 2 with FMul show ?case by (simp add: split_beta split nonzero_union npemul_correct integral_iff) } next case (FNeg e) { case 1 with FNeg show ?case by (simp add: split_beta npeneg_correct) next case 2 with FNeg show ?case by (simp add: split_beta) } next case (FDiv e1 e2) note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Num e2"] split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"] { case 1 let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))" let ?common\<^sub>1 = "peval xs (Common (Num e1) (Num e2))" let ?right\<^sub>1 = "peval xs (Right (Num e1) (Num e2))" let ?left\<^sub>2 = "peval xs (Left (Denom e1) (Denom e2))" let ?common\<^sub>2 = "peval xs (Common (Denom e1) (Denom e2))" let ?right\<^sub>2 = "peval xs (Right (Denom e1) (Denom e2))" from 1 FDiv have "feval xs (FDiv e1 e2) = ((?common\<^sub>1 \ ?common\<^sub>2) \ (?left\<^sub>1 \ ?right\<^sub>2)) \ ((?common\<^sub>1 \ ?common\<^sub>2) \ (?left\<^sub>2 \ ?right\<^sub>1))" by (simp add: split_beta split nonzero_union nonzero_insert nonzero_divide_divide_eq m_ac) also from 1 FDiv have "\ = peval xs (Num (FDiv e1 e2)) \ peval xs (Denom (FDiv e1 e2))" by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff) finally show ?case . next case 2 with FDiv show ?case by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff) } next case (FPow e n) { case 1 with FPow show ?case by (simp add: split_beta nonzero_power_divide npepow_correct) next case 2 with FPow show ?case by (simp add: split_beta npepow_correct) } qed lemma (in field) feval_eq0: assumes "in_carrier xs" and "fnorm e = (n, d, c)" and "nonzero xs c" and "peval xs n = \" shows "feval xs e = \" using assms fnorm_correct [of xs e] by simp lemma (in field) fexpr_in_carrier: assumes "in_carrier xs" and "nonzero xs (Cond e)" shows "feval xs e \ carrier R" using assms proof (induct e) case (FDiv e1 e2) then have "feval xs e1 \ carrier R" "feval xs e2 \ carrier R" "peval xs (Num e2) \ \" "nonzero xs (Cond e2)" by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm) from \in_carrier xs\ \nonzero xs (Cond e2)\ have "feval xs e2 = peval xs (Num e2) \ peval xs (Denom e2)" by (rule fnorm_correct) moreover from \in_carrier xs\ \nonzero xs (Cond e2)\ have "peval xs (Denom e2) \ \" by (rule fnorm_correct) ultimately have "feval xs e2 \ \" using \peval xs (Num e2) \ \\ \in_carrier xs\ by (simp add: divide_eq_0_iff) with \feval xs e1 \ carrier R\ \feval xs e2 \ carrier R\ show ?case by simp qed (simp_all add: nonzero_union split: prod.split_asm) lemma (in field) feval_eq: assumes "in_carrier xs" and "fnorm (FSub e e') = (n, d, c)" and "nonzero xs c" shows "(feval xs e = feval xs e') = (peval xs n = \)" proof - from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')" by (auto simp add: nonzero_union split: prod.split_asm) with assms fnorm_correct [of xs "FSub e e'"] have "feval xs e \ feval xs e' = peval xs n \ peval xs d" "peval xs d \ \" by simp_all show ?thesis proof assume "feval xs e = feval xs e'" with \feval xs e \ feval xs e' = peval xs n \ peval xs d\ \in_carrier xs\ \nonzero xs (Cond e')\ have "peval xs n \ peval xs d = \" by (simp add: fexpr_in_carrier minus_eq r_neg) with \peval xs d \ \\ \in_carrier xs\ show "peval xs n = \" by (simp add: divide_eq_0_iff) next assume "peval xs n = \" with \feval xs e \ feval xs e' = peval xs n \ peval xs d\ \peval xs d \ \\ \nonzero xs (Cond e)\ \nonzero xs (Cond e')\ \in_carrier xs\ show "feval xs e = feval xs e'" by (simp add: eq_diff0 fexpr_in_carrier) qed qed ML \ val term_of_nat = HOLogic.mk_number \<^Type>\nat\ o @{code integer_of_nat}; val term_of_int = HOLogic.mk_number \<^Type>\int\ o @{code integer_of_int}; fun term_of_pexpr (@{code PExpr1} x) = \<^Const>\PExpr1\ $ term_of_pexpr1 x | term_of_pexpr (@{code PExpr2} x) = \<^Const>\PExpr2\ $ term_of_pexpr2 x and term_of_pexpr1 (@{code PCnst} k) = \<^Const>\PCnst\ $ term_of_int k | term_of_pexpr1 (@{code PVar} n) = \<^Const>\PVar\ $ term_of_nat n | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^Const>\PAdd\ $ term_of_pexpr x $ term_of_pexpr y | term_of_pexpr1 (@{code PSub} (x, y)) = \<^Const>\PSub\ $ term_of_pexpr x $ term_of_pexpr y | term_of_pexpr1 (@{code PNeg} x) = \<^Const>\PNeg\ $ term_of_pexpr x and term_of_pexpr2 (@{code PMul} (x, y)) = \<^Const>\PMul\ $ term_of_pexpr x $ term_of_pexpr y | term_of_pexpr2 (@{code PPow} (x, n)) = \<^Const>\PPow\ $ term_of_pexpr x $ term_of_nat n fun term_of_result (x, (y, zs)) = HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod (term_of_pexpr y, HOLogic.mk_list \<^Type>\pexpr\ (map term_of_pexpr zs))); local fun fnorm (ctxt, ct, t) = - \<^let>\x = ct and y = \Thm.cterm_of ctxt t\ + \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: \pexpr \ pexpr \ pexpr list\\; val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\fnorm\, fnorm))); fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t); in val cv = @{computation_conv "pexpr \ pexpr \ pexpr list" terms: fnorm nat_of_integer Code_Target_Nat.natural "0::nat" "1::nat" "2::nat" "3::nat" "0::int" "1::int" "2::int" "3::int" "-1::int" datatypes: fexpr int integer num} (fn ctxt => fn result => fn ct => fnorm_oracle ctxt ct (term_of_result result)) end \ ML \ signature FIELD_TAC = sig structure Field_Simps: sig type T val get: Context.generic -> T val put: T -> Context.generic -> Context.generic val map: (T -> T) -> Context.generic -> Context.generic end val eq_field_simps: (term * (thm list * thm list * thm list * thm * thm)) * (term * (thm list * thm list * thm list * thm * thm)) -> bool val field_tac: bool -> Proof.context -> int -> tactic end structure Field_Tac : FIELD_TAC = struct open Ring_Tac; fun field_struct \<^Const_>\Ring.ring.add _ _ for R _ _\ = SOME R | field_struct \<^Const_>\Ring.a_minus _ _ for R _ _\ = SOME R | field_struct \<^Const_>\Group.monoid.mult _ _ for R _ _\ = SOME R | field_struct \<^Const_>\Ring.a_inv _ _ for R _\ = SOME R | field_struct \<^Const_>\Group.pow _ _ _ for R _ _\ = SOME R | field_struct \<^Const_>\Algebra_Aux.m_div _ _for R _ _\ = SOME R | field_struct \<^Const_>\Ring.ring.zero _ _ for R\ = SOME R | field_struct \<^Const_>\Group.monoid.one _ _ for R\ = SOME R | field_struct \<^Const_>\Algebra_Aux.of_integer _ _ for R _\ = SOME R | field_struct _ = NONE; fun reif_fexpr vs \<^Const_>\Ring.ring.add _ _ for _ a b\ = \<^Const>\FAdd for \reif_fexpr vs a\ \reif_fexpr vs b\\ | reif_fexpr vs \<^Const_>\Ring.a_minus _ _ for _ a b\ = \<^Const>\FSub for \reif_fexpr vs a\ \reif_fexpr vs b\\ | reif_fexpr vs \<^Const_>\Group.monoid.mult _ _ for _ a b\ = \<^Const>\FMul for \reif_fexpr vs a\ \reif_fexpr vs b\\ | reif_fexpr vs \<^Const_>\Ring.a_inv _ _ for _ a\ = \<^Const>\FNeg for \reif_fexpr vs a\\ | reif_fexpr vs \<^Const>\Group.pow _ _ _ for _ a n\ = \<^Const>\FPow for \reif_fexpr vs a\ n\ | reif_fexpr vs \<^Const_>\Algebra_Aux.m_div _ _ for _ a b\ = \<^Const>\FDiv for \reif_fexpr vs a\ \reif_fexpr vs b\\ | reif_fexpr vs (Free x) = \<^Const>\FVar for \HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\\ | reif_fexpr vs \<^Const_>\Ring.ring.zero _ _ for _\ = \<^term>\FCnst 0\ | reif_fexpr vs \<^Const_>\Group.monoid.one _ _ for _\ = \<^term>\FCnst 1\ | reif_fexpr vs \<^Const_>\Algebra_Aux.of_integer _ _ for _ n\ = \<^Const>\FCnst for n\ | reif_fexpr _ _ = error "reif_fexpr: bad expression"; fun reif_fexpr' vs \<^Const_>\plus _ for a b\ = \<^Const>\FAdd for \reif_fexpr' vs a\ \reif_fexpr' vs b\\ | reif_fexpr' vs \<^Const_>\minus _ for a b\ = \<^Const>\FSub for \reif_fexpr' vs a\ \reif_fexpr' vs b\\ | reif_fexpr' vs \<^Const_>\times _ for a b\ = \<^Const>\FMul for \reif_fexpr' vs a\ \reif_fexpr' vs b\\ | reif_fexpr' vs \<^Const_>\uminus _ for a\ = \<^Const>\FNeg for \reif_fexpr' vs a\\ | reif_fexpr' vs \<^Const_>\power _ for a n\ = \<^Const>\FPow for \reif_fexpr' vs a\ n\ | reif_fexpr' vs \<^Const_>\divide _ for a b\ = \<^Const>\FDiv for \reif_fexpr' vs a\ \reif_fexpr' vs b\\ | reif_fexpr' vs (Free x) = \<^Const>\FVar for \HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\\ | reif_fexpr' vs \<^Const_>\zero_class.zero _\ = \<^term>\FCnst 0\ | reif_fexpr' vs \<^Const_>\one_class.one _\ = \<^term>\FCnst 1\ | reif_fexpr' vs \<^Const_>\numeral _ for b\ = \<^Const>\FCnst for \<^Const>\numeral \<^Type>\int\ for b\\ | reif_fexpr' _ _ = error "reif_fexpr: bad expression"; fun eq_field_simps ((t, (ths1, ths2, ths3, th4, th)), (t', (ths1', ths2', ths3', th4', th'))) = t aconv t' andalso eq_list Thm.eq_thm (ths1, ths1') andalso eq_list Thm.eq_thm (ths2, ths2') andalso eq_list Thm.eq_thm (ths3, ths3') andalso Thm.eq_thm (th4, th4') andalso Thm.eq_thm (th, th'); structure Field_Simps = Generic_Data (struct type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net val empty = Net.empty val merge = Net.merge eq_field_simps end); fun get_field_simps ctxt optcT t = (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of SOME (ths1, ths2, ths3, th4, th) => let val tr = Thm.transfer' ctxt #> (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end | NONE => error "get_field_simps: lookup failed"); fun nth_el_conv (_, _, _, nth_el_Cons, _) = let val a = type_of_eqn nth_el_Cons; val If_conv_a = If_conv a; fun conv ys n = (case strip_app ys of (\<^const_name>\Cons\, [x, xs]) => transitive' (inst [] [x, xs, n] nth_el_Cons) (If_conv_a (args2 nat_eq_conv) Thm.reflexive (cong2' conv Thm.reflexive (args2 nat_minus_conv)))) in conv end; fun feval_conv (rls as ([feval_simps_1, feval_simps_2, feval_simps_3, feval_simps_4, feval_simps_5, feval_simps_6, feval_simps_7, feval_simps_8, feval_simps_9, feval_simps_10, feval_simps_11], _, _, _, _)) = let val nth_el_conv' = nth_el_conv rls; fun conv xs x = (case strip_app x of (\<^const_name>\FCnst\, [c]) => (case strip_app c of (\<^const_name>\zero_class.zero\, _) => inst [] [xs] feval_simps_9 | (\<^const_name>\one_class.one\, _) => inst [] [xs] feval_simps_10 | (\<^const_name>\numeral\, [n]) => inst [] [xs, n] feval_simps_11 | _ => inst [] [xs, c] feval_simps_1) | (\<^const_name>\FVar\, [n]) => transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv') | (\<^const_name>\FAdd\, [a, b]) => transitive' (inst [] [xs, a, b] feval_simps_3) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\FSub\, [a, b]) => transitive' (inst [] [xs, a, b] feval_simps_4) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\FMul\, [a, b]) => transitive' (inst [] [xs, a, b] feval_simps_5) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\FNeg\, [a]) => transitive' (inst [] [xs, a] feval_simps_6) (cong1 (args2 conv)) | (\<^const_name>\FDiv\, [a, b]) => transitive' (inst [] [xs, a, b] feval_simps_7) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\FPow\, [a, n]) => transitive' (inst [] [xs, a, n] feval_simps_8) (cong2 (args2 conv) Thm.reflexive)) in conv end; fun peval_conv (rls as (_, [peval_simps_1, peval_simps_2, peval_simps_3, peval_simps_4, peval_simps_5, peval_simps_6, peval_simps_7, peval_simps_8, peval_simps_9, peval_simps_10, peval_simps_11], _, _, _)) = let val nth_el_conv' = nth_el_conv rls; fun conv xs x = (case strip_app x of (\<^const_name>\PExpr1\, [e]) => (case strip_app e of (\<^const_name>\PCnst\, [c]) => (case strip_numeral c of (\<^const_name>\zero_class.zero\, _) => inst [] [xs] peval_simps_8 | (\<^const_name>\one_class.one\, _) => inst [] [xs] peval_simps_9 | (\<^const_name>\numeral\, [n]) => inst [] [xs, n] peval_simps_10 | (\<^const_name>\uminus\, [n]) => inst [] [xs, n] peval_simps_11 | _ => inst [] [xs, c] peval_simps_1) | (\<^const_name>\PVar\, [n]) => transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv') | (\<^const_name>\PAdd\, [a, b]) => transitive' (inst [] [xs, a, b] peval_simps_3) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\PSub\, [a, b]) => transitive' (inst [] [xs, a, b] peval_simps_4) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\PNeg\, [a]) => transitive' (inst [] [xs, a] peval_simps_5) (cong1 (args2 conv))) | (\<^const_name>\PExpr2\, [e]) => (case strip_app e of (\<^const_name>\PMul\, [a, b]) => transitive' (inst [] [xs, a, b] peval_simps_6) (cong2 (args2 conv) (args2 conv)) | (\<^const_name>\PPow\, [a, n]) => transitive' (inst [] [xs, a, n] peval_simps_7) (cong2 (args2 conv) Thm.reflexive))) in conv end; fun nonzero_conv (rls as (_, _, [nonzero_Nil, nonzero_Cons, nonzero_singleton], _, _)) = let val peval_conv' = peval_conv rls; fun conv xs qs = (case strip_app qs of (\<^const_name>\Nil\, []) => inst [] [xs] nonzero_Nil | (\<^const_name>\Cons\, [p, ps]) => (case Thm.term_of ps of \<^Const_>\Nil _\ => transitive' (inst [] [xs, p] nonzero_singleton) (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons) (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv)))) in conv end; fun field_tac in_prem ctxt = SUBGOAL (fn (g, i) => let val (prems, concl) = Logic.strip_horn g; fun find_eq s = (case s of (_ $ \<^Const_>\HOL.eq T for t u\) => (case (field_struct t, field_struct u) of (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr) | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr) | _ => if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\field\) then SOME ((t, u), mk_ring T, T, SOME T, K @{thm in_carrier_trivial}, reif_fexpr') else NONE) | _ => NONE); val ((t, u), R, T, optT, mkic, reif) = (case get_first find_eq (if in_prem then prems else [concl]) of SOME q => q | NONE => error "cannot determine field"); val rls as (_, _, _, _, feval_eq) = get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R; val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd); val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs)); val ce = Thm.cterm_of ctxt (reif xs t); val ce' = Thm.cterm_of ctxt (reif xs u); - val fnorm = cv ctxt \<^let>\e = ce and e' = ce' in cterm \fnorm (FSub e e')\\; + val fnorm = cv ctxt \<^instantiate>\e = ce and e' = ce' in cterm \fnorm (FSub e e')\\; val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm); val (_, [_, c]) = strip_app dc; val th = Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv (binop_conv (binop_conv (K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce'))) (Conv.arg1_conv (K (peval_conv rls cxs n)))))) ([mkic xs, HOLogic.mk_obj_eq fnorm, HOLogic.mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS feval_eq); val th' = Drule.rotate_prems 1 (th RS (if in_prem then @{thm iffD1} else @{thm iffD2})); in if in_prem then dresolve_tac ctxt [th'] 1 THEN defer_tac 1 else resolve_tac ctxt [th'] 1 end); end \ context field begin local_setup \ Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps (Morphism.term phi \<^term>\R\, (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]}, Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]}, Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]}, singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]}, singleton (Morphism.fact phi) @{thm feval_eq})))) \ end method_setup field = \ Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt => SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt)) \ "reduce equations over fields to equations over rings" end diff --git a/src/HOL/Decision_Procs/langford.ML b/src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML +++ b/src/HOL/Decision_Procs/langford.ML @@ -1,260 +1,260 @@ (* Title: HOL/Decision_Procs/langford.ML Author: Amine Chaieb, TU Muenchen *) signature LANGFORD = sig val dlo_tac : Proof.context -> int -> tactic val dlo_conv : Proof.context -> cterm -> thm end structure Langford: LANGFORD = struct val dest_set = let fun h acc ct = (case Thm.term_of ct of \<^Const_>\bot _\ => acc | \<^Const_>\insert _ for _ _\ => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)); in h [] end; fun prove_finite cT u = let val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros} fun ins x th = Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th in fold ins u th0 end; fun simp_rule ctxt = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms}))); fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = (case Thm.term_of ep of \<^Const_>\Ex _ for _\ => let val p = Thm.dest_arg ep val ths = simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (Thm.instantiate' [] [SOME p] stupid) val (L, U) = let val (_, q) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of ths)) in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end fun proveneF S = let val (a, A) = Thm.dest_comb S |>> Thm.dest_arg val cT = Thm.ctyp_of_cterm a val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty} val f = prove_finite cT (dest_set S) in (ne, f) end val qe = (case (Thm.term_of L, Thm.term_of U) of (\<^Const_>\bot _\, _) => let val (neU, fU) = proveneF U in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end | (_, \<^Const_>\bot _\) => let val (neL,fL) = proveneF L in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end | _ => let val (neL, fL) = proveneF L val (neU, fU) = proveneF U in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end) in qe end | _ => error "dlo_qe : Not an existential formula"); val all_conjuncts = let fun h acc ct = (case Thm.term_of ct of \<^Const>\HOL.conj for _ _\ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct) | _ => ct :: acc) in h [] end; fun conjuncts ct = (case Thm.term_of ct of \<^Const>\HOL.conj for _ _\ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct) | _ => [ct]); val list_conj = - foldr1 (fn (A, B) => \<^let>\A = A and B = B in cterm \A \ B\\); + foldr1 (fn (A, B) => \<^instantiate>\A and B in cterm \A \ B\\); fun mk_conj_tab th = let fun h acc th = (case Thm.prop_of th of \<^Const_>\Trueprop for \<^Const_>\HOL.conj for p q\\ => h (h acc (th RS conjunct2)) (th RS conjunct1) | \<^Const_>\Trueprop for p\ => (p, th) :: acc) in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; fun is_conj \<^Const_>\HOL.conj for _ _\ = true | is_conj _ = false; fun prove_conj tab cjs = (case cjs of [c] => if is_conj (Thm.term_of c) then prove_conj tab (conjuncts c) else tab c | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]); fun conj_aci_rule eq = let val (l, r) = Thm.dest_equals eq fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (Thm.term_of c)) fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (Thm.term_of c)) val ll = Thm.dest_arg l val rr = Thm.dest_arg r val thl = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps val thr = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI} in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (Thm.term_of ct)) (Thm.term_of x); fun is_eqx x eq = (case Thm.term_of eq of \<^Const_>\HOL.eq _ for l r\ => l aconv Thm.term_of x orelse r aconv Thm.term_of x | _ => false); local fun proc ctxt ct = (case Thm.term_of ct of \<^Const_>\Ex _ for \Abs _\\ => let val e = Thm.dest_fun ct val (x,p) = Thm.dest_abs_global (Thm.dest_arg ct) val Free (xn, _) = Thm.term_of x val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p) in (case eqs of [] => let val (dx, ndx) = List.partition (contains x) neqs in case ndx of [] => NONE | _ => conj_aci_rule - \<^let>\A = p and B = \list_conj (ndx @ dx)\ in cterm \Trueprop A \ Trueprop B\\ + \<^instantiate>\A = p and B = \list_conj (ndx @ dx)\ in cterm \Trueprop A \ Trueprop B\\ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |> SOME end | _ => conj_aci_rule - \<^let>\A = p and B = \list_conj (eqs @ neqs)\ in cterm \Trueprop A \ Trueprop B\\ + \<^instantiate>\A = p and B = \list_conj (eqs @ neqs)\ in cterm \Trueprop A \ Trueprop B\\ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |> SOME) end | _ => NONE); in val reduce_ex_simproc = Simplifier.make_simproc \<^context> "reduce_ex_simproc" {lhss = [\<^term>\\x. P x\], proc = K proc}; end; fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) = let val ctxt' = Context_Position.set_visible false (put_simpset dlo_ss ctxt) addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc] val dnfex_conv = Simplifier.rewrite ctxt' val pcv = Simplifier.rewrite (put_simpset dlo_ss ctxt addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}) val mk_env = Cterms.list_set_rev o Cterms.build o Drule.add_frees_cterm in fn p => Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons (mk_env p) (K Thm.reflexive) (K Thm.reflexive) (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p end; val grab_atom_bop = let fun h ctxt tm = (case Thm.term_of tm of \<^Const_>\HOL.eq \<^Type>\bool\ for _ _\ => find_args ctxt tm | \<^Const_>\Not for _\ => h ctxt (Thm.dest_arg tm) | \<^Const_>\All _ for _\ => find_body ctxt (Thm.dest_arg tm) | \<^Const_>\Pure.all _ for _\ => find_body ctxt (Thm.dest_arg tm) | \<^Const_>\Ex _ for _\ => find_body ctxt (Thm.dest_arg tm) | \<^Const_>\HOL.conj for _ _\ => find_args ctxt tm | \<^Const_>\HOL.disj for _ _\ => find_args ctxt tm | \<^Const_>\HOL.implies for _ _\ => find_args ctxt tm | \<^Const_>\Pure.imp for _ _\ => find_args ctxt tm | \<^Const_>\Pure.eq _ for _ _\ => find_args ctxt tm | \<^Const_>\Trueprop for _\ => h ctxt (Thm.dest_arg tm) | _ => Thm.dest_fun2 tm) and find_args ctxt tm = (h ctxt (Thm.dest_arg tm) handle CTERM _ => h ctxt (Thm.dest_arg1 tm)) and find_body ctxt b = let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt in h ctxt' b' end; in h end; fun dlo_instance ctxt tm = (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop ctxt tm)); fun dlo_conv ctxt tm = (case dlo_instance ctxt tm of (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm]) | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm); fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let fun all x t = Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) val ts = sort Thm.fast_term_ord (f p) val p' = fold_rev all ts p in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); fun cfrees ats ct = let val ins = insert (op aconvc) fun h acc t = (case Thm.term_of t of _ $ _ $ _ => if member (op aconvc) ats (Thm.dest_fun2 t) then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc)) | Free _ => if member (op aconvc) ats t then acc else ins t acc | Var _ => if member (op aconvc) ats t then acc else ins t acc | _ => acc) in h [] ct end fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => (case dlo_instance ctxt p of (ss, NONE) => simp_tac (put_simpset ss ctxt) i | (ss, SOME instance) => Object_Logic.full_atomize_tac ctxt i THEN simp_tac (put_simpset ss ctxt) i THEN (CONVERSION Thm.eta_long_conversion) i THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i THEN Object_Logic.full_atomize_tac ctxt i THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i THEN (simp_tac (put_simpset ss ctxt) i))); end; diff --git a/src/Pure/ML/ml_antiquotations.ML b/src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML +++ b/src/Pure/ML/ml_antiquotations.ML @@ -1,608 +1,611 @@ (* Title: Pure/ML/ml_antiquotations.ML Author: Makarius Miscellaneous ML antiquotations. *) signature ML_ANTIQUOTATIONS = sig val make_judgment: Proof.context -> term -> term val dest_judgment: Proof.context -> term -> term type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val instantiate_typ: insts -> typ -> typ val instantiate_ctyp: cinsts -> ctyp -> ctyp val instantiate_term: insts -> term -> term val instantiate_cterm: cinsts -> cterm -> cterm end; structure ML_Antiquotations: ML_ANTIQUOTATIONS = struct (* ML support *) val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\undefined\ (Scan.succeed "(raise General.Match)") #> ML_Antiquotation.inline \<^binding>\assert\ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> ML_Antiquotation.declaration_embedded \<^binding>\print\ (Scan.lift (Scan.optional Parse.embedded "Output.writeln")) (fn src => fn output => fn ctxt => let val struct_name = ML_Context.struct_name ctxt; val (_, pos) = Token.name_of_src src; val (a, ctxt') = ML_Context.variant "output" ctxt; val env = "val " ^ a ^ ": string -> unit =\n\ \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ ML_Syntax.print_position pos ^ "));\n"; val body = "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; in (K (env, body), ctxt') end) #> ML_Antiquotation.value \<^binding>\rat\ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); (* formal entities *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\system_option\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> ML_Antiquotation.value_embedded \<^binding>\theory\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value_embedded \<^binding>\theory_context\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> ML_Antiquotation.inline \<^binding>\context\ (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> ML_Antiquotation.inline_embedded \<^binding>\typ\ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> ML_Antiquotation.inline_embedded \<^binding>\term\ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.inline_embedded \<^binding>\prop\ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); (* schematic variables *) val schematic_input = Args.context -- Scan.lift Parse.embedded_input >> (fn (ctxt, src) => (Proof_Context.set_mode Proof_Context.mode_schematic ctxt, (Syntax.implode_input src, Input.pos_of src))); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\tvar\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_typ ctxt s of TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> ML_Antiquotation.inline_embedded \<^binding>\var\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_term ctxt s of Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v | _ => error ("Schematic variable expected" ^ Position.here pos))))); (* type classes *) fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => Proof_Context.read_class ctxt s |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> ML_Antiquotation.inline_embedded \<^binding>\sort\ (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); (* type constructors *) fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); val res = (case try check (c, decl) of SOME res => res | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\type_name\ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ (type_name "type" (fn (c, _) => Lexicon.mark_type c))); (* constants *) fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; val res = check (Proof_Context.consts_of ctxt, c) handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\const_name\ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ (const_name (fn (_, c) => Lexicon.mark_const c)) #> ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> ML_Antiquotation.inline_embedded \<^binding>\const\ (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, (raw_c, pos)), Ts) => let val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; val consts = Proof_Context.consts_of ctxt; val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); val _ = length Ts <> n andalso error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); val const = Const (c, Consts.instance consts (c, Ts)); in ML_Syntax.atomic (ML_Syntax.print_term const) end))); (* object-logic judgment *) fun make_judgment ctxt = let val const = Object_Logic.judgment_const ctxt in fn t => Const const $ t end; fun dest_judgment ctxt = let val is_judgment = Object_Logic.is_judgment ctxt; val drop_judgment = Object_Logic.drop_judgment ctxt; in fn t => if is_judgment t then drop_judgment t else raise TERM ("dest_judgment", [t]) end; val _ = Theory.setup (ML_Antiquotation.value \<^binding>\make_judgment\ (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #> ML_Antiquotation.value \<^binding>\dest_judgment\ (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); (* type/term instantiations and constructors *) type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts)); fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts)); fun instantiate_term (insts: insts) = let val instT = TVars.make (#1 insts); val instantiateT = Term_Subst.instantiateT instT; val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); in Term_Subst.instantiate (instT, inst) end; fun instantiate_cterm (cinsts: cinsts) = let val cinstT = TVars.make (#1 cinsts); val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); in Thm.instantiate_cterm (cinstT, cinst) end; local fun make_keywords ctxt = Thy_Header.get_keywords' ctxt |> Keyword.no_major_keywords |> Keyword.add_major_keywords ["typ", "term", "prop", "ctyp", "cterm", "cprop"]; +val parse_inst_name = Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false); + val parse_inst = - Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false) -- - (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml))); + (parse_inst_name -- (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) || + Scan.ahead parse_inst_name -- Parse.embedded_ml) + >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml))); val parse_insts = Parse.and_list1 parse_inst >> (List.partition #1 #> apply2 (map #2)); val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); val ml_list_pair = ml_list o ListPair.map ml_pair; fun get_tfree envT (a, pos) = (case AList.lookup (op =) envT a of SOME S => (a, S) - | NONE => error ("Unused type variable " ^ quote a ^ Position.here pos)); + | NONE => error ("No occurrence of type variable " ^ quote a ^ Position.here pos)); fun get_free env (x, pos) = (case AList.lookup (op =) env x of SOME T => (x, T) - | NONE => error ("Unused variable " ^ quote x ^ Position.here pos)); + | NONE => error ("No occurrence of variable " ^ quote x ^ Position.here pos)); fun make_instT (a, pos) T = (case try (Term.dest_TVar o Logic.dest_type) T of NONE => error ("Not a free type variable " ^ quote a ^ Position.here pos) | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v)); fun make_inst (a, pos) t = (case try Term.dest_Var t of NONE => error ("Not a free variable " ^ quote a ^ Position.here pos) | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v)); fun prepare_insts ctxt1 ctxt0 (instT, inst) t = let val envT = Term.add_tfrees t []; val env = Term.add_frees t []; val freesT = map (Logic.mk_type o TFree o get_tfree envT) instT; val frees = map (Free o get_free env) inst; val (t' :: varsT, vars) = Variable.export_terms ctxt1 ctxt0 (t :: freesT @ frees) |> chop (1 + length freesT); val ml_insts = (map2 make_instT instT varsT, map2 make_inst inst vars); in (ml_insts, t') end; fun prepare_ml range (kind, ml1, ml2) ml_val (ml_instT, ml_inst) ctxt = let val (ml_name, ctxt') = ML_Context.variant kind ctxt; val ml_env = ml ("val " ^ ml_name ^ " = ") @ ml ml1 @ ml_parens (ml ml_val) @ ml ";\n"; fun ml_body (ml_argsT, ml_args) = ml_parens (ml ml2 @ ml_pair (ml_list_pair (ml_instT, ml_argsT), ml_list_pair (ml_inst, ml_args)) @ ml_range range (ML_Context.struct_name ctxt ^ "." ^ ml_name)); in ((ml_env, ml_body), ctxt') end; fun prepare_type range (arg, s) insts ctxt = let val T = Syntax.read_typ ctxt s; val t = Logic.mk_type T; val ctxt1 = Proof_Context.augment t ctxt; val (ml_insts, T') = prepare_insts ctxt1 ctxt insts t ||> Logic.dest_type; in prepare_ml range arg (ML_Syntax.print_typ T') ml_insts ctxt end; fun prepare_term read range (arg, (s, fixes)) insts ctxt = let val ctxt' = #2 (Proof_Context.add_fixes_cmd fixes ctxt); val t = read ctxt' s; val ctxt1 = Proof_Context.augment t ctxt'; val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t; in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end; fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ"); fun ctyp_ml kind = (kind, "Thm.ctyp_of ML_context", "ML_Antiquotations.instantiate_ctyp"); fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term"); fun cterm_ml kind = (kind, "Thm.cterm_of ML_context", "ML_Antiquotations.instantiate_cterm"); fun parse_body range = (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) -- Parse.!!! Parse.typ >> prepare_type range || (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml) -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml) -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range; val _ = Theory.setup - (ML_Context.add_antiquotation \<^binding>\let\ true + (ML_Context.add_antiquotation \<^binding>\instantiate\ true (fn range => fn src => fn ctxt => let val (insts, prepare_val) = src |> Parse.read_embedded_src ctxt (make_keywords ctxt) ((parse_insts --| Parse.$$$ "in") -- parse_body range); val (((ml_env, ml_body), decls), ctxt1) = ctxt |> prepare_val (apply2 (map #1) insts) ||>> ML_Context.expand_antiquotes_list (op @ (apply2 (map #2) insts)); fun decl' ctxt' = let val (ml_args_env, ml_args) = split_list (decls ctxt') in (ml_env @ flat ml_args_env, ml_body (chop (length (#1 insts)) ml_args)) end; in (decl', ctxt1) end)); in end; local val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; val parse_name = Parse.input Parse.name; val parse_args = Scan.repeat Parse.embedded_ml_underscore; val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) []; fun parse_body b = if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single) else Scan.succeed []; fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" | is_dummy _ = false; val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; val ml_dummy = ml "_"; fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; val ml_string = ml o ML_Syntax.print_string; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); fun type_antiquotation binding {function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val ((s, type_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function); val pos = Input.pos_of s; val Type (c, Ts) = Proof_Context.read_type_name {proper = true, strict = true} ctxt (Syntax.implode_input s); val n = length Ts; val _ = length type_args = n orelse error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list fn_body ctxt1; fun decl' ctxt' = let val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); val ml1 = ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| T => " @ ml_range range "raise" @ ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") else ml1; in (flat (ml_args_env @ ml_fn_env), ml2) end; in (decl', ctxt2) end); fun const_antiquotation binding {pattern, function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val (((s, type_args), term_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_for_args -- parse_body function); val Const (c, T) = Proof_Context.read_const {proper = true, strict = true} ctxt (Syntax.implode_input s); val consts = Proof_Context.consts_of ctxt; val type_paths = Consts.type_arguments consts c; val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); val n = length type_params; val m = length (Term.binder_types T); fun err msg = error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ Position.here (Input.pos_of s)); val _ = length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); val _ = length term_args > m andalso Term.is_Type (Term.body_type T) andalso err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list term_args ctxt1; val (decls3, ctxt3) = ML_Context.expand_antiquotes_list fn_body ctxt2; fun decl' ctxt' = let val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); val relevant = map is_dummy type_args ~~ type_paths; fun relevant_path is = not pattern orelse let val p = rev is in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); fun ml_typ is (Type (d, Us)) = if relevant_path is then ml "Term.Type " @ ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) else ml_dummy | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy | ml_typ _ (TFree _) = raise Match; fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| t => " @ ml_range range "raise" @ ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") else ml1; in (ml_env, ml2) end; in (decl', ctxt3) end); val _ = Theory.setup (type_antiquotation \<^binding>\Type\ {function = false} #> type_antiquotation \<^binding>\Type_fn\ {function = true} #> const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); in end; (* special forms *) val _ = Theory.setup (ML_Antiquotation.special_form \<^binding>\try\ "() |> Basics.try" #> ML_Antiquotation.special_form \<^binding>\can\ "() |> Basics.can"); (* basic combinators *) local val parameter = Parse.position Parse.nat >> (fn (n, pos) => if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); fun indices n = map string_of_int (1 upto n); fun empty n = replicate_string n " []"; fun dummy n = replicate_string n " _"; fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); val tuple = enclose "(" ")" o commas; fun tuple_empty n = tuple (replicate n "[]"); fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); in val _ = Theory.setup (ML_Antiquotation.value \<^binding>\map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun map _" ^ empty n ^ " = []\n\ \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ " in map f end")) #> ML_Antiquotation.value \<^binding>\fold\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold _" ^ empty n ^ " a = a\n\ \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold f end")) #> ML_Antiquotation.value \<^binding>\fold_map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ \ | fold_map f" ^ cons n ^ " a =\n\ \ let\n\ \ val (x, a') = f" ^ vars "x" n ^ " a\n\ \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ \ in (x :: xs, a'') end\n\ \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold_map f end")) #> ML_Antiquotation.value \<^binding>\split_list\ (Scan.lift parameter >> (fn n => "fn list =>\n\ \ let\n\ \ fun split_list [] =" ^ tuple_empty n ^ "\n\ \ | split_list" ^ tuple_cons n ^ " =\n\ \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ \ in " ^ cons_tuple n ^ "end\n\ \ in split_list list end")) #> ML_Antiquotation.value \<^binding>\apply\ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> (fn (n, opt_index) => let val cond = (case opt_index of NONE => K true | SOME (index, index_pos) => if 1 <= index andalso index <= n then equal (string_of_int index) else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); in "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) end))); end; (* outer syntax *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\keyword\ (Args.context -- Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> ML_Antiquotation.value_embedded \<^binding>\command_keyword\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); end;

code: 0x01d4ab group: letter \ code: 0x01d4ac group: letter \ code: 0x00211b group: letter \ code: 0x01d4ae group: letter \ code: 0x01d4af group: letter \ code: 0x01d4b0 group: letter \ code: 0x01d4b1 group: letter \ code: 0x01d4b2 group: letter \ code: 0x01d4b3 group: letter \ code: 0x01d4b4 group: letter \ code: 0x01d4b5 group: letter \ code: 0x01d5ba group: letter \ code: 0x01d5bb group: letter \ code: 0x01d5bc group: letter \ code: 0x01d5bd group: letter \ code: 0x01d5be group: letter \ code: 0x01d5bf group: letter \ code: 0x01d5c0 group: letter \ code: 0x01d5c1 group: letter \ code: 0x01d5c2 group: letter \ code: 0x01d5c3 group: letter \ code: 0x01d5c4 group: letter \ code: 0x01d5c5 group: letter \ code: 0x01d5c6 group: letter \ code: 0x01d5c7 group: letter \ code: 0x01d5c8 group: letter \