src/HOL/Decision_Procs/Reflective_Field.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65043 fd753468786f
child 67123 3fe40ff1b921
permissions -rw-r--r--
executable domain membership checks
berghofe@64962
     1
(*  Title:      HOL/Decision_Procs/Reflective_Field.thy
berghofe@64962
     2
    Author:     Stefan Berghofer
berghofe@64962
     3
berghofe@64962
     4
Reducing equalities in fields to equalities in rings.
berghofe@64962
     5
*)
berghofe@64962
     6
berghofe@64962
     7
theory Reflective_Field
haftmann@64999
     8
imports "~~/src/HOL/Decision_Procs/Commutative_Ring"
berghofe@64962
     9
begin
berghofe@64962
    10
berghofe@64962
    11
datatype fexpr =
berghofe@64962
    12
    FCnst int
berghofe@64962
    13
  | FVar nat
berghofe@64962
    14
  | FAdd fexpr fexpr
berghofe@64962
    15
  | FSub fexpr fexpr
berghofe@64962
    16
  | FMul fexpr fexpr
berghofe@64962
    17
  | FNeg fexpr
berghofe@64962
    18
  | FDiv fexpr fexpr
berghofe@64962
    19
  | FPow fexpr nat
berghofe@64962
    20
berghofe@64962
    21
fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
berghofe@64962
    22
  "nth_el [] n = \<zero>"
berghofe@64962
    23
| "nth_el (x # xs) 0 = x"
berghofe@64962
    24
| "nth_el (x # xs) (Suc n) = nth_el xs n"
berghofe@64962
    25
berghofe@64962
    26
lemma (in field) nth_el_Cons:
berghofe@64962
    27
  "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))"
berghofe@64962
    28
  by (cases n) simp_all
berghofe@64962
    29
berghofe@64962
    30
lemma (in field) nth_el_closed [simp]:
berghofe@64962
    31
  "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R"
berghofe@64962
    32
  by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def)
berghofe@64962
    33
berghofe@64962
    34
primrec (in field) feval :: "'a list \<Rightarrow> fexpr \<Rightarrow> 'a"
berghofe@64962
    35
where
berghofe@64962
    36
  "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>"
berghofe@64962
    37
| "feval xs (FVar n) = nth_el xs n"
berghofe@64962
    38
| "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b"
berghofe@64962
    39
| "feval xs (FSub a b) = feval xs a \<ominus> feval xs b"
berghofe@64962
    40
| "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
berghofe@64962
    41
| "feval xs (FNeg a) = \<ominus> feval xs a"
berghofe@64962
    42
| "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
berghofe@64962
    43
| "feval xs (FPow a n) = feval xs a (^) n"
berghofe@64962
    44
berghofe@64962
    45
lemma (in field) feval_Cnst:
berghofe@64962
    46
  "feval xs (FCnst 0) = \<zero>"
berghofe@64962
    47
  "feval xs (FCnst 1) = \<one>"
berghofe@64962
    48
  "feval xs (FCnst (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
berghofe@64962
    49
  by simp_all
berghofe@64962
    50
berghofe@64962
    51
datatype pexpr =
berghofe@64962
    52
    PExpr1 pexpr1
berghofe@64962
    53
  | PExpr2 pexpr2
berghofe@64962
    54
and pexpr1 =
berghofe@64962
    55
    PCnst int
berghofe@64962
    56
  | PVar nat
berghofe@64962
    57
  | PAdd pexpr pexpr
berghofe@64962
    58
  | PSub pexpr pexpr
berghofe@64962
    59
  | PNeg pexpr
berghofe@64962
    60
and pexpr2 =
berghofe@64962
    61
    PMul pexpr pexpr
berghofe@64962
    62
  | PPow pexpr nat
berghofe@64962
    63
berghofe@64962
    64
lemma pexpr_cases [case_names PCnst PVar PAdd PSub PNeg PMul PPow]:
berghofe@64962
    65
  assumes
berghofe@64962
    66
    "\<And>c. e = PExpr1 (PCnst c) \<Longrightarrow> P"
berghofe@64962
    67
    "\<And>n. e = PExpr1 (PVar n) \<Longrightarrow> P"
berghofe@64962
    68
    "\<And>e1 e2. e = PExpr1 (PAdd e1 e2) \<Longrightarrow> P"
berghofe@64962
    69
    "\<And>e1 e2. e = PExpr1 (PSub e1 e2) \<Longrightarrow> P"
berghofe@64962
    70
    "\<And>e'. e = PExpr1 (PNeg e') \<Longrightarrow> P"
berghofe@64962
    71
    "\<And>e1 e2. e = PExpr2 (PMul e1 e2) \<Longrightarrow> P"
berghofe@64962
    72
    "\<And>e' n. e = PExpr2 (PPow e' n) \<Longrightarrow> P"
berghofe@64962
    73
  shows P
berghofe@64962
    74
proof (cases e)
berghofe@64962
    75
  case (PExpr1 e')
berghofe@64962
    76
  then show ?thesis
berghofe@64962
    77
    apply (cases e')
berghofe@64962
    78
    apply simp_all
berghofe@64962
    79
    apply (erule assms)+
berghofe@64962
    80
    done
berghofe@64962
    81
next
berghofe@64962
    82
  case (PExpr2 e')
berghofe@64962
    83
  then show ?thesis
berghofe@64962
    84
    apply (cases e')
berghofe@64962
    85
    apply simp_all
berghofe@64962
    86
    apply (erule assms)+
berghofe@64962
    87
    done
berghofe@64962
    88
qed
berghofe@64962
    89
berghofe@64962
    90
lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases]
berghofe@64962
    91
berghofe@64962
    92
fun (in field) peval :: "'a list \<Rightarrow> pexpr \<Rightarrow> 'a"
berghofe@64962
    93
where
berghofe@64962
    94
  "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>"
berghofe@64962
    95
| "peval xs (PExpr1 (PVar n)) = nth_el xs n"
berghofe@64962
    96
| "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b"
berghofe@64962
    97
| "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
berghofe@64962
    98
| "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
berghofe@64962
    99
| "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
berghofe@64962
   100
| "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n"
berghofe@64962
   101
berghofe@64962
   102
lemma (in field) peval_Cnst:
berghofe@64962
   103
  "peval xs (PExpr1 (PCnst 0)) = \<zero>"
berghofe@64962
   104
  "peval xs (PExpr1 (PCnst 1)) = \<one>"
berghofe@64962
   105
  "peval xs (PExpr1 (PCnst (numeral n))) = \<guillemotleft>numeral n\<guillemotright>"
berghofe@64962
   106
  "peval xs (PExpr1 (PCnst (- numeral n))) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
berghofe@64962
   107
  by simp_all
berghofe@64962
   108
berghofe@64962
   109
lemma (in field) peval_closed [simp]:
berghofe@64962
   110
  "in_carrier xs \<Longrightarrow> peval xs e \<in> carrier R"
berghofe@64962
   111
  "in_carrier xs \<Longrightarrow> peval xs (PExpr1 e1) \<in> carrier R"
berghofe@64962
   112
  "in_carrier xs \<Longrightarrow> peval xs (PExpr2 e2) \<in> carrier R"
berghofe@64962
   113
  by (induct e and e1 and e2) simp_all
berghofe@64962
   114
berghofe@64962
   115
definition npepow :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr"
berghofe@64962
   116
where
berghofe@64962
   117
  "npepow e n =
berghofe@64962
   118
     (if n = 0 then PExpr1 (PCnst 1)
berghofe@64962
   119
      else if n = 1 then e
berghofe@64962
   120
      else (case e of
berghofe@64962
   121
          PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n))
berghofe@64962
   122
        | _ \<Rightarrow> PExpr2 (PPow e n)))"
berghofe@64962
   123
berghofe@64962
   124
lemma (in field) npepow_correct:
berghofe@64962
   125
  "in_carrier xs \<Longrightarrow> peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))"
berghofe@64962
   126
  by (cases e rule: pexpr_cases)
berghofe@64962
   127
    (simp_all add: npepow_def)
berghofe@64962
   128
berghofe@64962
   129
fun npemul :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
berghofe@64962
   130
where
berghofe@64962
   131
  "npemul x y = (case x of
berghofe@64962
   132
       PExpr1 (PCnst c) \<Rightarrow>
berghofe@64962
   133
         if c = 0 then x
berghofe@64962
   134
         else if c = 1 then y else
berghofe@64962
   135
           (case y of
berghofe@64962
   136
              PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d))
berghofe@64962
   137
            | _ \<Rightarrow> PExpr2 (PMul x y))
berghofe@64962
   138
     | PExpr2 (PPow e1 n) \<Rightarrow>
berghofe@64962
   139
         (case y of
berghofe@64962
   140
            PExpr2 (PPow e2 m) \<Rightarrow>
berghofe@64962
   141
              if n = m then npepow (npemul e1 e2) n
berghofe@64962
   142
              else PExpr2 (PMul x y)
berghofe@64962
   143
          | PExpr1 (PCnst d) \<Rightarrow>
berghofe@64962
   144
              if d = 0 then y
berghofe@64962
   145
              else if d = 1 then x
berghofe@64962
   146
              else PExpr2 (PMul x y)
berghofe@64962
   147
          | _ \<Rightarrow> PExpr2 (PMul x y))
berghofe@64962
   148
     | _ \<Rightarrow> (case y of
berghofe@64962
   149
         PExpr1 (PCnst d) \<Rightarrow>
berghofe@64962
   150
           if d = 0 then y
berghofe@64962
   151
           else if d = 1 then x
berghofe@64962
   152
           else PExpr2 (PMul x y)
berghofe@64962
   153
       | _ \<Rightarrow> PExpr2 (PMul x y)))"
berghofe@64962
   154
berghofe@64962
   155
lemma (in field) npemul_correct:
berghofe@64962
   156
  "in_carrier xs \<Longrightarrow> peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))"
berghofe@64962
   157
proof (induct e1 e2 rule: npemul.induct)
berghofe@64962
   158
  case (1 x y)
berghofe@64962
   159
  then show ?case
berghofe@64962
   160
  proof (cases x y rule: pexpr_cases2)
berghofe@64962
   161
    case (PPow_PPow e n e' m)
berghofe@64962
   162
    then show ?thesis
berghofe@64962
   163
    by (simp add: 1 npepow_correct nat_pow_distr
berghofe@64962
   164
      npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"]
berghofe@64962
   165
      del: npemul.simps)
berghofe@64962
   166
  qed simp_all
berghofe@64962
   167
qed
berghofe@64962
   168
berghofe@64962
   169
declare npemul.simps [simp del]
berghofe@64962
   170
berghofe@64962
   171
definition npeadd :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
berghofe@64962
   172
where
berghofe@64962
   173
  "npeadd x y = (case x of
berghofe@64962
   174
       PExpr1 (PCnst c) \<Rightarrow>
berghofe@64962
   175
         if c = 0 then y else
berghofe@64962
   176
           (case y of
berghofe@64962
   177
              PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d))
berghofe@64962
   178
            | _ \<Rightarrow> PExpr1 (PAdd x y))
berghofe@64962
   179
     | _ \<Rightarrow> (case y of
berghofe@64962
   180
         PExpr1 (PCnst d) \<Rightarrow>
berghofe@64962
   181
           if d = 0 then x
berghofe@64962
   182
           else PExpr1 (PAdd x y)
berghofe@64962
   183
       | _ \<Rightarrow> PExpr1 (PAdd x y)))"
berghofe@64962
   184
berghofe@64962
   185
lemma (in field) npeadd_correct:
berghofe@64962
   186
  "in_carrier xs \<Longrightarrow> peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))"
berghofe@64962
   187
  by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def)
berghofe@64962
   188
berghofe@64962
   189
definition npesub :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
berghofe@64962
   190
where
berghofe@64962
   191
  "npesub x y = (case y of
berghofe@64962
   192
       PExpr1 (PCnst d) \<Rightarrow>
berghofe@64962
   193
         if d = 0 then x else
berghofe@64962
   194
           (case x of
berghofe@64962
   195
              PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d))
berghofe@64962
   196
            | _ \<Rightarrow> PExpr1 (PSub x y))
berghofe@64962
   197
     | _ \<Rightarrow> (case x of
berghofe@64962
   198
         PExpr1 (PCnst c) \<Rightarrow>
berghofe@64962
   199
           if c = 0 then PExpr1 (PNeg y)
berghofe@64962
   200
           else PExpr1 (PSub x y)
berghofe@64962
   201
       | _ \<Rightarrow> PExpr1 (PSub x y)))"
berghofe@64962
   202
berghofe@64962
   203
lemma (in field) npesub_correct:
berghofe@64962
   204
  "in_carrier xs \<Longrightarrow> peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))"
berghofe@64962
   205
  by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def)
berghofe@64962
   206
berghofe@64962
   207
definition npeneg :: "pexpr \<Rightarrow> pexpr"
berghofe@64962
   208
where
berghofe@64962
   209
  "npeneg e = (case e of
berghofe@64962
   210
       PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c))
berghofe@64962
   211
     | _ \<Rightarrow> PExpr1 (PNeg e))"
berghofe@64962
   212
berghofe@64962
   213
lemma (in field) npeneg_correct:
berghofe@64962
   214
  "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))"
berghofe@64962
   215
  by (cases e rule: pexpr_cases) (simp_all add: npeneg_def)
berghofe@64962
   216
berghofe@64962
   217
lemma option_pair_cases [case_names None Some]:
berghofe@64962
   218
  assumes
berghofe@64962
   219
    "x = None \<Longrightarrow> P"
berghofe@64962
   220
    "\<And>p q. x = Some (p, q) \<Longrightarrow> P"
berghofe@64962
   221
  shows P
berghofe@64962
   222
proof (cases x)
berghofe@64962
   223
  case None
berghofe@64962
   224
  then show ?thesis by (rule assms)
berghofe@64962
   225
next
berghofe@64962
   226
  case (Some r)
berghofe@64962
   227
  then show ?thesis
berghofe@64962
   228
    apply (cases r)
berghofe@64962
   229
    apply simp
berghofe@64962
   230
    by (rule assms)
berghofe@64962
   231
qed
berghofe@64962
   232
berghofe@64962
   233
fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat * pexpr) option"
berghofe@64962
   234
where
berghofe@64962
   235
  "isin e n (PExpr2 (PMul e1 e2)) m =
berghofe@64962
   236
     (case isin e n e1 m of
berghofe@64962
   237
        Some (k, e3) \<Rightarrow>
berghofe@64962
   238
          if k = 0 then Some (0, npemul e3 (npepow e2 m))
berghofe@64962
   239
          else (case isin e k e2 m of
berghofe@64962
   240
              Some (l, e4) \<Rightarrow> Some (l, npemul e3 e4)
berghofe@64962
   241
            | None \<Rightarrow> Some (k, npemul e3 (npepow e2 m)))
berghofe@64962
   242
      | None \<Rightarrow> (case isin e n e2 m of
berghofe@64962
   243
          Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3)
berghofe@64962
   244
        | None \<Rightarrow> None))"
berghofe@64962
   245
| "isin e n (PExpr2 (PPow e' k)) m =
berghofe@64962
   246
     (if k = 0 then None else isin e n e' (k * m))"
berghofe@64962
   247
| "isin (PExpr1 e) n (PExpr1 e') m =
berghofe@64962
   248
     (if e = e' then
berghofe@64962
   249
        if n >= m then Some (n - m, PExpr1 (PCnst 1))
berghofe@64962
   250
        else Some (0, npepow (PExpr1 e) (m - n))
berghofe@64962
   251
      else None)"
berghofe@64962
   252
| "isin (PExpr2 e) n (PExpr1 e') m = None"
berghofe@64962
   253
berghofe@64962
   254
lemma (in field) isin_correct:
berghofe@64962
   255
  assumes "in_carrier xs"
berghofe@64962
   256
  and "isin e n e' m = Some (p, e'')"
berghofe@64962
   257
  shows
berghofe@64962
   258
    "peval xs (PExpr2 (PPow e' m)) =
berghofe@64962
   259
     peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))"
berghofe@64962
   260
    "p \<le> n"
berghofe@64962
   261
  using assms
berghofe@64962
   262
  by (induct e n e' m arbitrary: p e'' rule: isin.induct)
berghofe@64962
   263
    (force
berghofe@64962
   264
       simp add:
berghofe@64962
   265
         nat_pow_distr nat_pow_pow nat_pow_mult m_ac
berghofe@64962
   266
         npemul_correct npepow_correct
berghofe@64962
   267
       split: option.split_asm prod.split_asm if_split_asm)+
berghofe@64962
   268
berghofe@64962
   269
lemma (in field) isin_correct':
berghofe@64962
   270
  "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow>
berghofe@64962
   271
   peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''"
berghofe@64962
   272
  "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n"
berghofe@64962
   273
  using isin_correct [where m=1]
berghofe@64962
   274
  by simp_all
berghofe@64962
   275
berghofe@64962
   276
fun split_aux :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr"
berghofe@64962
   277
where
berghofe@64962
   278
  "split_aux (PExpr2 (PMul e1 e2)) n e =
berghofe@64962
   279
     (let
berghofe@64962
   280
        (left1, common1, right1) = split_aux e1 n e;
berghofe@64962
   281
        (left2, common2, right2) = split_aux e2 n right1
berghofe@64962
   282
      in (npemul left1 left2, npemul common1 common2, right2))"
berghofe@64962
   283
| "split_aux (PExpr2 (PPow e' m)) n e =
berghofe@64962
   284
     (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e)
berghofe@64962
   285
      else split_aux e' (m * n) e)"
berghofe@64962
   286
| "split_aux (PExpr1 e') n e =
berghofe@64962
   287
     (case isin (PExpr1 e') n e 1 of
berghofe@64962
   288
        Some (m, e'') \<Rightarrow>
berghofe@64962
   289
          (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'')
berghofe@64962
   290
           else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e''))
berghofe@64962
   291
      | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))"
berghofe@64962
   292
berghofe@64962
   293
hide_const Left Right
berghofe@64962
   294
berghofe@64962
   295
abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
berghofe@64962
   296
  "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)"
berghofe@64962
   297
berghofe@64962
   298
abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
berghofe@64962
   299
  "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))"
berghofe@64962
   300
berghofe@64962
   301
abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
berghofe@64962
   302
  "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))"
berghofe@64962
   303
berghofe@64962
   304
lemma split_aux_induct [case_names 1 2 3]:
berghofe@64962
   305
  assumes I1: "\<And>e1 e2 n e. P e1 n e \<Longrightarrow> P e2 n (snd (snd (split_aux e1 n e))) \<Longrightarrow>
berghofe@64962
   306
    P (PExpr2 (PMul e1 e2)) n e"
berghofe@64962
   307
  and I2: "\<And>e' m n e. (m \<noteq> 0 \<Longrightarrow> P e' (m * n) e) \<Longrightarrow> P (PExpr2 (PPow e' m)) n e"
berghofe@64962
   308
  and I3: "\<And>e' n e. P (PExpr1 e') n e"
berghofe@64962
   309
  shows "P x y z"
berghofe@64962
   310
proof (induct x y z rule: split_aux.induct)
berghofe@64962
   311
  case 1
berghofe@64962
   312
  from 1(1) 1(2) [OF refl prod.collapse prod.collapse]
berghofe@64962
   313
  show ?case by (rule I1)
berghofe@64962
   314
next
berghofe@64962
   315
  case 2
berghofe@64962
   316
  then show ?case by (rule I2)
berghofe@64962
   317
next
berghofe@64962
   318
  case 3
berghofe@64962
   319
  then show ?case by (rule I3)
berghofe@64962
   320
qed
berghofe@64962
   321
berghofe@64962
   322
lemma (in field) split_aux_correct:
berghofe@64962
   323
  "in_carrier xs \<Longrightarrow>
berghofe@64962
   324
   peval xs (PExpr2 (PPow e\<^sub>1 n)) =
berghofe@64962
   325
   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)))))"
berghofe@64962
   326
  "in_carrier xs \<Longrightarrow>
berghofe@64962
   327
   peval xs e\<^sub>2 =
berghofe@64962
   328
   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)))))"
berghofe@64962
   329
  by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
berghofe@64962
   330
    (auto simp add: split_beta
berghofe@64962
   331
       nat_pow_distr nat_pow_pow nat_pow_mult m_ac
berghofe@64962
   332
       npemul_correct npepow_correct isin_correct'
berghofe@64962
   333
       split: option.split)
berghofe@64962
   334
berghofe@64962
   335
lemma (in field) split_aux_correct':
berghofe@64962
   336
  "in_carrier xs \<Longrightarrow>
berghofe@64962
   337
   peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
berghofe@64962
   338
  "in_carrier xs \<Longrightarrow>
berghofe@64962
   339
   peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
berghofe@64962
   340
  using split_aux_correct [where n=1]
berghofe@64962
   341
  by simp_all
berghofe@64962
   342
berghofe@64962
   343
fun fnorm :: "fexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list"
berghofe@64962
   344
where
berghofe@64962
   345
  "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])"
berghofe@64962
   346
| "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])"
berghofe@64962
   347
| "fnorm (FAdd e1 e2) =
berghofe@64962
   348
     (let
berghofe@64962
   349
        (xn, xd, xc) = fnorm e1;
berghofe@64962
   350
        (yn, yd, yc) = fnorm e2;
berghofe@64962
   351
        (left, common, right) = split_aux xd 1 yd
berghofe@64962
   352
      in
berghofe@64962
   353
        (npeadd (npemul xn right) (npemul yn left),
berghofe@64962
   354
         npemul left (npemul right common),
berghofe@64962
   355
         List.union xc yc))"
berghofe@64962
   356
| "fnorm (FSub e1 e2) =
berghofe@64962
   357
     (let
berghofe@64962
   358
        (xn, xd, xc) = fnorm e1;
berghofe@64962
   359
        (yn, yd, yc) = fnorm e2;
berghofe@64962
   360
        (left, common, right) = split_aux xd 1 yd
berghofe@64962
   361
      in
berghofe@64962
   362
        (npesub (npemul xn right) (npemul yn left),
berghofe@64962
   363
         npemul left (npemul right common),
berghofe@64962
   364
         List.union xc yc))"
berghofe@64962
   365
| "fnorm (FMul e1 e2) =
berghofe@64962
   366
     (let
berghofe@64962
   367
        (xn, xd, xc) = fnorm e1;
berghofe@64962
   368
        (yn, yd, yc) = fnorm e2;
berghofe@64962
   369
        (left1, common1, right1) = split_aux xn 1 yd;
berghofe@64962
   370
        (left2, common2, right2) = split_aux yn 1 xd
berghofe@64962
   371
      in
berghofe@64962
   372
        (npemul left1 left2,
berghofe@64962
   373
         npemul right2 right1,
berghofe@64962
   374
         List.union xc yc))"
berghofe@64962
   375
| "fnorm (FNeg e) =
berghofe@64962
   376
     (let (n, d, c) = fnorm e
berghofe@64962
   377
      in (npeneg n, d, c))"
berghofe@64962
   378
| "fnorm (FDiv e1 e2) =
berghofe@64962
   379
     (let
berghofe@64962
   380
        (xn, xd, xc) = fnorm e1;
berghofe@64962
   381
        (yn, yd, yc) = fnorm e2;
berghofe@64962
   382
        (left1, common1, right1) = split_aux xn 1 yn;
berghofe@64962
   383
        (left2, common2, right2) = split_aux xd 1 yd
berghofe@64962
   384
      in
berghofe@64962
   385
        (npemul left1 right2,
berghofe@64962
   386
         npemul left2 right1,
berghofe@64962
   387
         List.insert yn (List.union xc yc)))"
berghofe@64962
   388
| "fnorm (FPow e m) =
berghofe@64962
   389
     (let (n, d, c) = fnorm e
berghofe@64962
   390
      in (npepow n m, npepow d m, c))"
berghofe@64962
   391
berghofe@64962
   392
abbreviation Num :: "fexpr \<Rightarrow> pexpr" where
berghofe@64962
   393
  "Num e \<equiv> fst (fnorm e)"
berghofe@64962
   394
berghofe@64962
   395
abbreviation Denom :: "fexpr \<Rightarrow> pexpr" where
berghofe@64962
   396
  "Denom e \<equiv> fst (snd (fnorm e))"
berghofe@64962
   397
berghofe@64962
   398
abbreviation Cond :: "fexpr \<Rightarrow> pexpr list" where
berghofe@64962
   399
  "Cond e \<equiv> snd (snd (fnorm e))"
berghofe@64962
   400
berghofe@64962
   401
primrec (in field) nonzero :: "'a list \<Rightarrow> pexpr list \<Rightarrow> bool"
berghofe@64962
   402
where
berghofe@64962
   403
  "nonzero xs [] = True"
berghofe@64962
   404
| "nonzero xs (p # ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
berghofe@64962
   405
berghofe@64962
   406
lemma (in field) nonzero_singleton:
berghofe@64962
   407
  "nonzero xs [p] = (peval xs p \<noteq> \<zero>)"
berghofe@64962
   408
  by simp
berghofe@64962
   409
berghofe@64962
   410
lemma (in field) nonzero_append:
berghofe@64962
   411
  "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)"
berghofe@64962
   412
  by (induct ps) simp_all
berghofe@64962
   413
berghofe@64962
   414
lemma (in field) nonzero_idempotent:
berghofe@64962
   415
  "p \<in> set ps \<Longrightarrow> (peval xs p \<noteq> \<zero> \<and> nonzero xs ps) = nonzero xs ps"
berghofe@64962
   416
  by (induct ps) auto
berghofe@64962
   417
berghofe@64962
   418
lemma (in field) nonzero_insert:
berghofe@64962
   419
  "nonzero xs (List.insert p ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
berghofe@64962
   420
  by (simp add: List.insert_def nonzero_idempotent)
berghofe@64962
   421
berghofe@64962
   422
lemma (in field) nonzero_union:
berghofe@64962
   423
  "nonzero xs (List.union ps qs) = (nonzero xs ps \<and> nonzero xs qs)"
berghofe@64962
   424
  by (induct ps rule: rev_induct)
berghofe@64962
   425
    (auto simp add: List.union_def nonzero_insert nonzero_append)
berghofe@64962
   426
berghofe@64962
   427
lemma (in field) fnorm_correct:
berghofe@64962
   428
  assumes "in_carrier xs"
berghofe@64962
   429
  and "nonzero xs (Cond e)"
berghofe@64962
   430
  shows "feval xs e = peval xs (Num e) \<oslash> peval xs (Denom e)"
berghofe@64962
   431
  and "peval xs (Denom e) \<noteq> \<zero>"
berghofe@64962
   432
  using assms
berghofe@64962
   433
proof (induct e)
berghofe@64962
   434
  case (FCnst c) {
berghofe@64962
   435
    case 1
berghofe@64962
   436
    show ?case by simp
berghofe@64962
   437
  next
berghofe@64962
   438
    case 2
berghofe@64962
   439
    show ?case by simp
berghofe@64962
   440
  }
berghofe@64962
   441
next
berghofe@64962
   442
  case (FVar n) {
berghofe@64962
   443
    case 1
berghofe@64962
   444
    then show ?case by simp
berghofe@64962
   445
  next
berghofe@64962
   446
    case 2
berghofe@64962
   447
    show ?case by simp
berghofe@64962
   448
  }
berghofe@64962
   449
next
berghofe@64962
   450
  case (FAdd e1 e2)
berghofe@64962
   451
  note split = split_aux_correct' [where xs=xs and
berghofe@64962
   452
    e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
berghofe@64962
   453
  {
berghofe@64962
   454
    case 1
berghofe@64962
   455
    let ?left = "peval xs (Left (Denom e1) (Denom e2))"
berghofe@64962
   456
    let ?common = "peval xs (Common (Denom e1) (Denom e2))"
berghofe@64962
   457
    let ?right = "peval xs (Right (Denom e1) (Denom e2))"
berghofe@64962
   458
    from 1 FAdd
berghofe@64962
   459
    have "feval xs (FAdd e1 e2) =
berghofe@64962
   460
      (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<oplus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
berghofe@64962
   461
      (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
berghofe@64962
   462
      by (simp add: split_beta split nonzero_union
berghofe@64962
   463
        add_frac_eq r_distr m_ac)
berghofe@64962
   464
    also from 1 FAdd have "\<dots> =
berghofe@64962
   465
      peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))"
berghofe@64962
   466
      by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff)
berghofe@64962
   467
    finally show ?case .
berghofe@64962
   468
  next
berghofe@64962
   469
    case 2
berghofe@64962
   470
    with FAdd show ?case
berghofe@64962
   471
      by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
berghofe@64962
   472
  }
berghofe@64962
   473
next
berghofe@64962
   474
  case (FSub e1 e2)
berghofe@64962
   475
  note split = split_aux_correct' [where xs=xs and
berghofe@64962
   476
    e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
berghofe@64962
   477
  {
berghofe@64962
   478
    case 1
berghofe@64962
   479
    let ?left = "peval xs (Left (Denom e1) (Denom e2))"
berghofe@64962
   480
    let ?common = "peval xs (Common (Denom e1) (Denom e2))"
berghofe@64962
   481
    let ?right = "peval xs (Right (Denom e1) (Denom e2))"
berghofe@64962
   482
    from 1 FSub
berghofe@64962
   483
    have "feval xs (FSub e1 e2) =
berghofe@64962
   484
      (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<ominus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
berghofe@64962
   485
      (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
berghofe@64962
   486
      by (simp add: split_beta split nonzero_union
berghofe@64962
   487
        diff_frac_eq r_diff_distr m_ac)
berghofe@64962
   488
    also from 1 FSub have "\<dots> =
berghofe@64962
   489
      peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))"
berghofe@64962
   490
      by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff)
berghofe@64962
   491
    finally show ?case .
berghofe@64962
   492
  next
berghofe@64962
   493
    case 2
berghofe@64962
   494
    with FSub show ?case
berghofe@64962
   495
      by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
berghofe@64962
   496
  }
berghofe@64962
   497
next
berghofe@64962
   498
  case (FMul e1 e2)
berghofe@64962
   499
  note split =
berghofe@64962
   500
    split_aux_correct' [where xs=xs and
berghofe@64962
   501
      e\<^sub>1="Num e1" and e\<^sub>2="Denom e2"]
berghofe@64962
   502
    split_aux_correct' [where xs=xs and
berghofe@64962
   503
      e\<^sub>1="Num e2" and e\<^sub>2="Denom e1"]
berghofe@64962
   504
  {
berghofe@64962
   505
    case 1
berghofe@64962
   506
    let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))"
berghofe@64962
   507
    let ?common\<^sub>1 = "peval xs (Common (Num e1) (Denom e2))"
berghofe@64962
   508
    let ?right\<^sub>1 = "peval xs (Right (Num e1) (Denom e2))"
berghofe@64962
   509
    let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))"
berghofe@64962
   510
    let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))"
berghofe@64962
   511
    let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))"
berghofe@64962
   512
    from 1 FMul
berghofe@64962
   513
    have "feval xs (FMul e1 e2) =
berghofe@64962
   514
      ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?left\<^sub>2)) \<oslash>
berghofe@64962
   515
      ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?right\<^sub>2 \<otimes> ?right\<^sub>1))"
berghofe@64962
   516
      by (simp add: split_beta split nonzero_union
berghofe@64962
   517
        nonzero_divide_divide_eq_left m_ac)
berghofe@64962
   518
    also from 1 FMul have "\<dots> =
berghofe@64962
   519
      peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))"
berghofe@64962
   520
      by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
berghofe@64962
   521
    finally show ?case .
berghofe@64962
   522
  next
berghofe@64962
   523
    case 2
berghofe@64962
   524
    with FMul show ?case
berghofe@64962
   525
      by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
berghofe@64962
   526
  }
berghofe@64962
   527
next
berghofe@64962
   528
  case (FNeg e)
berghofe@64962
   529
  {
berghofe@64962
   530
    case 1
berghofe@64962
   531
    with FNeg show ?case
berghofe@64962
   532
      by (simp add: split_beta npeneg_correct)
berghofe@64962
   533
  next
berghofe@64962
   534
    case 2
berghofe@64962
   535
    with FNeg show ?case
berghofe@64962
   536
      by (simp add: split_beta)
berghofe@64962
   537
  }
berghofe@64962
   538
next
berghofe@64962
   539
  case (FDiv e1 e2)
berghofe@64962
   540
  note split =
berghofe@64962
   541
    split_aux_correct' [where xs=xs and
berghofe@64962
   542
      e\<^sub>1="Num e1" and e\<^sub>2="Num e2"]
berghofe@64962
   543
    split_aux_correct' [where xs=xs and
berghofe@64962
   544
      e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
berghofe@64962
   545
  {
berghofe@64962
   546
    case 1
berghofe@64962
   547
    let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))"
berghofe@64962
   548
    let ?common\<^sub>1 = "peval xs (Common (Num e1) (Num e2))"
berghofe@64962
   549
    let ?right\<^sub>1 = "peval xs (Right (Num e1) (Num e2))"
berghofe@64962
   550
    let ?left\<^sub>2 = "peval xs (Left (Denom e1) (Denom e2))"
berghofe@64962
   551
    let ?common\<^sub>2 = "peval xs (Common (Denom e1) (Denom e2))"
berghofe@64962
   552
    let ?right\<^sub>2 = "peval xs (Right (Denom e1) (Denom e2))"
berghofe@64962
   553
    from 1 FDiv
berghofe@64962
   554
    have "feval xs (FDiv e1 e2) =
berghofe@64962
   555
      ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?right\<^sub>2)) \<oslash>
berghofe@64962
   556
      ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>2 \<otimes> ?right\<^sub>1))"
berghofe@64962
   557
      by (simp add: split_beta split nonzero_union nonzero_insert
berghofe@64962
   558
        nonzero_divide_divide_eq m_ac)
berghofe@64962
   559
    also from 1 FDiv have "\<dots> =
berghofe@64962
   560
      peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))"
berghofe@64962
   561
      by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
berghofe@64962
   562
    finally show ?case .
berghofe@64962
   563
  next
berghofe@64962
   564
    case 2
berghofe@64962
   565
    with FDiv show ?case
berghofe@64962
   566
      by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
berghofe@64962
   567
  }
berghofe@64962
   568
next
berghofe@64962
   569
  case (FPow e n)
berghofe@64962
   570
  {
berghofe@64962
   571
    case 1
berghofe@64962
   572
    with FPow show ?case
berghofe@64962
   573
      by (simp add: split_beta nonzero_power_divide npepow_correct)
berghofe@64962
   574
  next
berghofe@64962
   575
    case 2
berghofe@64962
   576
    with FPow show ?case
berghofe@64962
   577
      by (simp add: split_beta npepow_correct)
berghofe@64962
   578
  }
berghofe@64962
   579
qed
berghofe@64962
   580
berghofe@64962
   581
lemma (in field) feval_eq0:
berghofe@64962
   582
  assumes "in_carrier xs"
berghofe@64962
   583
  and "fnorm e = (n, d, c)"
berghofe@64962
   584
  and "nonzero xs c"
berghofe@64962
   585
  and "peval xs n = \<zero>"
berghofe@64962
   586
  shows "feval xs e = \<zero>"
berghofe@64962
   587
  using assms fnorm_correct [of xs e]
berghofe@64962
   588
  by simp
berghofe@64962
   589
berghofe@64962
   590
lemma (in field) fexpr_in_carrier:
berghofe@64962
   591
  assumes "in_carrier xs"
berghofe@64962
   592
  and "nonzero xs (Cond e)"
berghofe@64962
   593
  shows "feval xs e \<in> carrier R"
berghofe@64962
   594
  using assms
berghofe@64962
   595
proof (induct e)
berghofe@64962
   596
  case (FDiv e1 e2)
berghofe@64962
   597
  then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R"
berghofe@64962
   598
    "peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)"
berghofe@64962
   599
    by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm)
haftmann@64998
   600
  from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
berghofe@64962
   601
  have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
berghofe@64962
   602
    by (rule fnorm_correct)
haftmann@64998
   603
  moreover from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
berghofe@64962
   604
  have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
haftmann@64998
   605
  ultimately have "feval xs e2 \<noteq> \<zero>" using \<open>peval xs (Num e2) \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
berghofe@64962
   606
    by (simp add: divide_eq_0_iff)
haftmann@64998
   607
  with \<open>feval xs e1 \<in> carrier R\<close> \<open>feval xs e2 \<in> carrier R\<close>
berghofe@64962
   608
  show ?case by simp
berghofe@64962
   609
qed (simp_all add: nonzero_union split: prod.split_asm)
berghofe@64962
   610
berghofe@64962
   611
lemma (in field) feval_eq:
berghofe@64962
   612
  assumes "in_carrier xs"
berghofe@64962
   613
  and "fnorm (FSub e e') = (n, d, c)"
berghofe@64962
   614
  and "nonzero xs c"
berghofe@64962
   615
  shows "(feval xs e = feval xs e') = (peval xs n = \<zero>)"
berghofe@64962
   616
proof -
berghofe@64962
   617
  from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')"
berghofe@64962
   618
    by (auto simp add: nonzero_union split: prod.split_asm)
berghofe@64962
   619
  with assms fnorm_correct [of xs "FSub e e'"]
berghofe@64962
   620
  have "feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d"
berghofe@64962
   621
    "peval xs d \<noteq> \<zero>"
berghofe@64962
   622
    by simp_all
berghofe@64962
   623
  show ?thesis
berghofe@64962
   624
  proof
berghofe@64962
   625
    assume "feval xs e = feval xs e'"
haftmann@64998
   626
    with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close>
haftmann@64998
   627
      \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e')\<close>
berghofe@64962
   628
    have "peval xs n \<oslash> peval xs d = \<zero>"
berghofe@64962
   629
      by (simp add: fexpr_in_carrier minus_eq r_neg)
haftmann@64998
   630
    with \<open>peval xs d \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
berghofe@64962
   631
    show "peval xs n = \<zero>"
berghofe@64962
   632
      by (simp add: divide_eq_0_iff)
berghofe@64962
   633
  next
berghofe@64962
   634
    assume "peval xs n = \<zero>"
haftmann@64998
   635
    with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close> \<open>peval xs d \<noteq> \<zero>\<close>
haftmann@64998
   636
      \<open>nonzero xs (Cond e)\<close> \<open>nonzero xs (Cond e')\<close> \<open>in_carrier xs\<close>
berghofe@64962
   637
    show "feval xs e = feval xs e'"
berghofe@64962
   638
      by (simp add: eq_diff0 fexpr_in_carrier)
berghofe@64962
   639
  qed
berghofe@64962
   640
qed
berghofe@64962
   641
haftmann@64999
   642
ML \<open>
haftmann@64999
   643
val term_of_nat = HOLogic.mk_number @{typ nat} o @{code integer_of_nat};
haftmann@64999
   644
haftmann@64999
   645
val term_of_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
haftmann@64999
   646
haftmann@64999
   647
fun term_of_pexpr (@{code PExpr1} x) = @{term PExpr1} $ term_of_pexpr1 x
haftmann@64999
   648
  | term_of_pexpr (@{code PExpr2} x) = @{term PExpr2} $ term_of_pexpr2 x
haftmann@64999
   649
and term_of_pexpr1 (@{code PCnst} k) = @{term PCnst} $ term_of_int k
haftmann@64999
   650
  | term_of_pexpr1 (@{code PVar} n) = @{term PVar} $ term_of_nat n
haftmann@64999
   651
  | term_of_pexpr1 (@{code PAdd} (x, y)) = @{term PAdd} $ term_of_pexpr x $ term_of_pexpr y
haftmann@64999
   652
  | term_of_pexpr1 (@{code PSub} (x, y)) = @{term PSub} $ term_of_pexpr x $ term_of_pexpr y
haftmann@64999
   653
  | term_of_pexpr1 (@{code PNeg} x) = @{term PNeg} $ term_of_pexpr x
haftmann@64999
   654
and term_of_pexpr2 (@{code PMul} (x, y)) = @{term PMul} $ term_of_pexpr x $ term_of_pexpr y
haftmann@64999
   655
  | term_of_pexpr2 (@{code PPow} (x, n)) = @{term PPow} $ term_of_pexpr x $ term_of_nat n
haftmann@64999
   656
haftmann@64999
   657
fun term_of_result (x, (y, zs)) =
haftmann@64999
   658
  HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod
haftmann@64999
   659
    (term_of_pexpr y, HOLogic.mk_list @{typ pexpr} (map term_of_pexpr zs)));
berghofe@64962
   660
haftmann@64999
   661
local
haftmann@64999
   662
haftmann@64999
   663
fun fnorm (ctxt, ct, t) = Thm.mk_binop @{cterm "Pure.eq :: pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> prop"}
haftmann@64999
   664
  ct (Thm.cterm_of ctxt t);
haftmann@64999
   665
haftmann@64999
   666
val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
haftmann@64999
   667
  (Thm.add_oracle (@{binding fnorm}, fnorm)));
haftmann@64999
   668
haftmann@64999
   669
fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
haftmann@64999
   670
haftmann@64999
   671
in
haftmann@64999
   672
haftmann@64999
   673
val cv = @{computation_conv "pexpr \<times> pexpr \<times> pexpr list"
haftmann@64999
   674
  terms: fnorm nat_of_integer Code_Target_Nat.natural
haftmann@64999
   675
    "0::nat" "1::nat" "2::nat" "3::nat"
haftmann@64999
   676
    "0::int" "1::int" "2::int" "3::int" "-1::int"
haftmann@64999
   677
  datatypes: fexpr int integer num}
haftmann@65043
   678
  (fn ctxt => fn result => fn ct => fnorm_oracle ctxt ct (term_of_result result))
haftmann@64999
   679
haftmann@64999
   680
end
haftmann@64999
   681
\<close>
berghofe@64962
   682
haftmann@64998
   683
ML \<open>
berghofe@64962
   684
signature FIELD_TAC =
berghofe@64962
   685
sig
berghofe@64962
   686
  structure Field_Simps:
berghofe@64962
   687
  sig
berghofe@64962
   688
    type T
berghofe@64962
   689
    val get: Context.generic -> T
berghofe@64962
   690
    val put: T -> Context.generic -> Context.generic
berghofe@64962
   691
    val map: (T -> T) -> Context.generic -> Context.generic
berghofe@64962
   692
  end
berghofe@64962
   693
  val eq_field_simps:
berghofe@64962
   694
    (term * (thm list * thm list * thm list * thm * thm)) *
berghofe@64962
   695
    (term * (thm list * thm list * thm list * thm * thm)) -> bool
berghofe@64962
   696
  val field_tac: bool -> Proof.context -> int -> tactic
berghofe@64962
   697
end
berghofe@64962
   698
berghofe@64962
   699
structure Field_Tac : FIELD_TAC =
berghofe@64962
   700
struct
berghofe@64962
   701
berghofe@64962
   702
open Ring_Tac;
berghofe@64962
   703
berghofe@64962
   704
fun field_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
berghofe@64962
   705
  | field_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
berghofe@64962
   706
  | field_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
berghofe@64962
   707
  | field_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
berghofe@64962
   708
  | field_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
berghofe@64962
   709
  | field_struct (Const (@{const_name Algebra_Aux.m_div}, _) $ R $ _ $ _) = SOME R
berghofe@64962
   710
  | field_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
berghofe@64962
   711
  | field_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
berghofe@64962
   712
  | field_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
berghofe@64962
   713
  | field_struct _ = NONE;
berghofe@64962
   714
berghofe@64962
   715
fun reif_fexpr vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
berghofe@64962
   716
      @{const FAdd} $ reif_fexpr vs a $ reif_fexpr vs b
berghofe@64962
   717
  | reif_fexpr vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
berghofe@64962
   718
      @{const FSub} $ reif_fexpr vs a $ reif_fexpr vs b
berghofe@64962
   719
  | reif_fexpr vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
berghofe@64962
   720
      @{const FMul} $ reif_fexpr vs a $ reif_fexpr vs b
berghofe@64962
   721
  | reif_fexpr vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
berghofe@64962
   722
      @{const FNeg} $ reif_fexpr vs a
berghofe@64962
   723
  | reif_fexpr vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
berghofe@64962
   724
      @{const FPow} $ reif_fexpr vs a $ n
berghofe@64962
   725
  | reif_fexpr vs (Const (@{const_name Algebra_Aux.m_div}, _) $ _ $ a $ b) =
berghofe@64962
   726
      @{const FDiv} $ reif_fexpr vs a $ reif_fexpr vs b
berghofe@64962
   727
  | reif_fexpr vs (Free x) =
berghofe@64962
   728
      @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
berghofe@64962
   729
  | reif_fexpr vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
berghofe@64962
   730
      @{term "FCnst 0"}
berghofe@64962
   731
  | reif_fexpr vs (Const (@{const_name Group.monoid.one}, _) $ _) =
berghofe@64962
   732
      @{term "FCnst 1"}
berghofe@64962
   733
  | reif_fexpr vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
berghofe@64962
   734
      @{const FCnst} $ n
berghofe@64962
   735
  | reif_fexpr _ _ = error "reif_fexpr: bad expression";
berghofe@64962
   736
berghofe@64962
   737
fun reif_fexpr' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
berghofe@64962
   738
      @{const FAdd} $ reif_fexpr' vs a $ reif_fexpr' vs b
berghofe@64962
   739
  | reif_fexpr' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
berghofe@64962
   740
      @{const FSub} $ reif_fexpr' vs a $ reif_fexpr' vs b
berghofe@64962
   741
  | reif_fexpr' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
berghofe@64962
   742
      @{const FMul} $ reif_fexpr' vs a $ reif_fexpr' vs b
berghofe@64962
   743
  | reif_fexpr' vs (Const (@{const_name Groups.uminus}, _) $ a) =
berghofe@64962
   744
      @{const FNeg} $ reif_fexpr' vs a
berghofe@64962
   745
  | reif_fexpr' vs (Const (@{const_name Power.power}, _) $ a $ n) =
berghofe@64962
   746
      @{const FPow} $ reif_fexpr' vs a $ n
berghofe@64962
   747
  | reif_fexpr' vs (Const (@{const_name divide}, _) $ a $ b) =
berghofe@64962
   748
      @{const FDiv} $ reif_fexpr' vs a $ reif_fexpr' vs b
berghofe@64962
   749
  | reif_fexpr' vs (Free x) =
berghofe@64962
   750
      @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
berghofe@64962
   751
  | reif_fexpr' vs (Const (@{const_name zero_class.zero}, _)) =
berghofe@64962
   752
      @{term "FCnst 0"}
berghofe@64962
   753
  | reif_fexpr' vs (Const (@{const_name one_class.one}, _)) =
berghofe@64962
   754
      @{term "FCnst 1"}
berghofe@64962
   755
  | reif_fexpr' vs (Const (@{const_name numeral}, _) $ b) =
berghofe@64962
   756
      @{const FCnst} $ (@{const numeral (int)} $ b)
berghofe@64962
   757
  | reif_fexpr' _ _ = error "reif_fexpr: bad expression";
berghofe@64962
   758
berghofe@64962
   759
fun eq_field_simps
berghofe@64962
   760
  ((t, (ths1, ths2, ths3, th4, th)),
berghofe@64962
   761
   (t', (ths1', ths2', ths3', th4', th'))) =
berghofe@64962
   762
    t aconv t' andalso
berghofe@64962
   763
    eq_list Thm.eq_thm (ths1, ths1') andalso
berghofe@64962
   764
    eq_list Thm.eq_thm (ths2, ths2') andalso
berghofe@64962
   765
    eq_list Thm.eq_thm (ths3, ths3') andalso
berghofe@64962
   766
    Thm.eq_thm (th4, th4') andalso
berghofe@64962
   767
    Thm.eq_thm (th, th');
berghofe@64962
   768
berghofe@64962
   769
structure Field_Simps = Generic_Data
berghofe@64962
   770
(struct
berghofe@64962
   771
  type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net
berghofe@64962
   772
  val empty = Net.empty
berghofe@64962
   773
  val extend = I
berghofe@64962
   774
  val merge = Net.merge eq_field_simps
berghofe@64962
   775
end);
berghofe@64962
   776
berghofe@64962
   777
fun get_field_simps ctxt optcT t =
berghofe@64962
   778
  (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of
berghofe@64962
   779
     SOME (ths1, ths2, ths3, th4, th) =>
berghofe@64962
   780
       let val tr =
berghofe@64962
   781
         Thm.transfer (Proof_Context.theory_of ctxt) #>
berghofe@64962
   782
         (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
berghofe@64962
   783
       in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end
berghofe@64962
   784
   | NONE => error "get_field_simps: lookup failed");
berghofe@64962
   785
berghofe@64962
   786
fun nth_el_conv (_, _, _, nth_el_Cons, _) =
berghofe@64962
   787
  let
berghofe@64962
   788
    val a = type_of_eqn nth_el_Cons;
berghofe@64962
   789
    val If_conv_a = If_conv a;
berghofe@64962
   790
berghofe@64962
   791
    fun conv ys n = (case strip_app ys of
berghofe@64962
   792
      (@{const_name Cons}, [x, xs]) =>
berghofe@64962
   793
        transitive'
berghofe@64962
   794
          (inst [] [x, xs, n] nth_el_Cons)
berghofe@64962
   795
          (If_conv_a (args2 nat_eq_conv)
berghofe@64962
   796
             Thm.reflexive
berghofe@64962
   797
             (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
berghofe@64962
   798
  in conv end;
berghofe@64962
   799
berghofe@64962
   800
fun feval_conv (rls as
berghofe@64962
   801
      ([feval_simps_1, feval_simps_2, feval_simps_3,
berghofe@64962
   802
        feval_simps_4, feval_simps_5, feval_simps_6,
berghofe@64962
   803
        feval_simps_7, feval_simps_8, feval_simps_9,
berghofe@64962
   804
        feval_simps_10, feval_simps_11],
berghofe@64962
   805
       _, _, _, _)) =
berghofe@64962
   806
  let
berghofe@64962
   807
    val nth_el_conv' = nth_el_conv rls;
berghofe@64962
   808
berghofe@64962
   809
    fun conv xs x = (case strip_app x of
berghofe@64962
   810
        (@{const_name FCnst}, [c]) => (case strip_app c of
berghofe@64962
   811
            (@{const_name zero_class.zero}, _) => inst [] [xs] feval_simps_9
berghofe@64962
   812
          | (@{const_name one_class.one}, _) => inst [] [xs] feval_simps_10
berghofe@64962
   813
          | (@{const_name numeral}, [n]) => inst [] [xs, n] feval_simps_11
berghofe@64962
   814
          | _ => inst [] [xs, c] feval_simps_1)
berghofe@64962
   815
      | (@{const_name FVar}, [n]) =>
berghofe@64962
   816
          transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv')
berghofe@64962
   817
      | (@{const_name FAdd}, [a, b]) =>
berghofe@64962
   818
          transitive' (inst [] [xs, a, b] feval_simps_3)
berghofe@64962
   819
            (cong2 (args2 conv) (args2 conv))
berghofe@64962
   820
      | (@{const_name FSub}, [a, b]) =>
berghofe@64962
   821
          transitive' (inst [] [xs, a, b] feval_simps_4)
berghofe@64962
   822
            (cong2 (args2 conv) (args2 conv))
berghofe@64962
   823
      | (@{const_name FMul}, [a, b]) =>
berghofe@64962
   824
          transitive' (inst [] [xs, a, b] feval_simps_5)
berghofe@64962
   825
            (cong2 (args2 conv) (args2 conv))
berghofe@64962
   826
      | (@{const_name FNeg}, [a]) =>
berghofe@64962
   827
          transitive' (inst [] [xs, a] feval_simps_6)
berghofe@64962
   828
            (cong1 (args2 conv))
berghofe@64962
   829
      | (@{const_name FDiv}, [a, b]) =>
berghofe@64962
   830
          transitive' (inst [] [xs, a, b] feval_simps_7)
berghofe@64962
   831
            (cong2 (args2 conv) (args2 conv))
berghofe@64962
   832
      | (@{const_name FPow}, [a, n]) =>
berghofe@64962
   833
          transitive' (inst [] [xs, a, n] feval_simps_8)
berghofe@64962
   834
            (cong2 (args2 conv) Thm.reflexive))
berghofe@64962
   835
  in conv end;
berghofe@64962
   836
berghofe@64962
   837
fun peval_conv (rls as
berghofe@64962
   838
      (_,
berghofe@64962
   839
       [peval_simps_1, peval_simps_2, peval_simps_3,
berghofe@64962
   840
        peval_simps_4, peval_simps_5, peval_simps_6,
berghofe@64962
   841
        peval_simps_7, peval_simps_8, peval_simps_9,
berghofe@64962
   842
        peval_simps_10, peval_simps_11],
berghofe@64962
   843
       _, _, _)) =
berghofe@64962
   844
  let
berghofe@64962
   845
    val nth_el_conv' = nth_el_conv rls;
berghofe@64962
   846
berghofe@64962
   847
    fun conv xs x = (case strip_app x of
berghofe@64962
   848
        (@{const_name PExpr1}, [e]) => (case strip_app e of
berghofe@64962
   849
            (@{const_name PCnst}, [c]) => (case strip_numeral c of
berghofe@64962
   850
                (@{const_name zero_class.zero}, _) => inst [] [xs] peval_simps_8
berghofe@64962
   851
              | (@{const_name one_class.one}, _) => inst [] [xs] peval_simps_9
berghofe@64962
   852
              | (@{const_name numeral}, [n]) => inst [] [xs, n] peval_simps_10
berghofe@64962
   853
              | (@{const_name uminus}, [n]) => inst [] [xs, n] peval_simps_11
berghofe@64962
   854
              | _ => inst [] [xs, c] peval_simps_1)
berghofe@64962
   855
          | (@{const_name PVar}, [n]) =>
berghofe@64962
   856
              transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv')
berghofe@64962
   857
          | (@{const_name PAdd}, [a, b]) =>
berghofe@64962
   858
              transitive' (inst [] [xs, a, b] peval_simps_3)
berghofe@64962
   859
                (cong2 (args2 conv) (args2 conv))
berghofe@64962
   860
          | (@{const_name PSub}, [a, b]) =>
berghofe@64962
   861
              transitive' (inst [] [xs, a, b] peval_simps_4)
berghofe@64962
   862
                (cong2 (args2 conv) (args2 conv))
berghofe@64962
   863
          | (@{const_name PNeg}, [a]) =>
berghofe@64962
   864
              transitive' (inst [] [xs, a] peval_simps_5)
berghofe@64962
   865
                (cong1 (args2 conv)))
berghofe@64962
   866
      | (@{const_name PExpr2}, [e]) => (case strip_app e of
berghofe@64962
   867
            (@{const_name PMul}, [a, b]) =>
berghofe@64962
   868
              transitive' (inst [] [xs, a, b] peval_simps_6)
berghofe@64962
   869
                (cong2 (args2 conv) (args2 conv))
berghofe@64962
   870
          | (@{const_name PPow}, [a, n]) =>
berghofe@64962
   871
              transitive' (inst [] [xs, a, n] peval_simps_7)
berghofe@64962
   872
                (cong2 (args2 conv) Thm.reflexive)))
berghofe@64962
   873
  in conv end;
berghofe@64962
   874
berghofe@64962
   875
fun nonzero_conv (rls as
berghofe@64962
   876
      (_, _,
berghofe@64962
   877
       [nonzero_Nil, nonzero_Cons, nonzero_singleton],
berghofe@64962
   878
       _, _)) =
berghofe@64962
   879
  let
berghofe@64962
   880
    val peval_conv' = peval_conv rls;
berghofe@64962
   881
berghofe@64962
   882
    fun conv xs qs = (case strip_app qs of
berghofe@64962
   883
        (@{const_name Nil}, []) => inst [] [xs] nonzero_Nil
berghofe@64962
   884
      | (@{const_name Cons}, [p, ps]) => (case Thm.term_of ps of
berghofe@64962
   885
            Const (@{const_name Nil}, _) =>
berghofe@64962
   886
              transitive' (inst [] [xs, p] nonzero_singleton)
berghofe@64962
   887
                (cong1 (cong2 (args2 peval_conv') Thm.reflexive))
berghofe@64962
   888
          | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons)
berghofe@64962
   889
              (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv))))
berghofe@64962
   890
  in conv end;
berghofe@64962
   891
berghofe@64962
   892
fun field_tac in_prem ctxt =
berghofe@64962
   893
  SUBGOAL (fn (g, i) =>
berghofe@64962
   894
    let
berghofe@64962
   895
      val (prems, concl) = Logic.strip_horn g;
berghofe@64962
   896
      fun find_eq s = (case s of
berghofe@64962
   897
          (_ $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t $ u)) =>
berghofe@64962
   898
            (case (field_struct t, field_struct u) of
berghofe@64962
   899
               (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
berghofe@64962
   900
             | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
berghofe@64962
   901
             | _ =>
berghofe@64962
   902
                 if Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort field})
berghofe@64962
   903
                 then SOME ((t, u), mk_ring T, T, SOME T, K @{thm in_carrier_trivial}, reif_fexpr')
berghofe@64962
   904
                 else NONE)
berghofe@64962
   905
        | _ => NONE);
berghofe@64962
   906
      val ((t, u), R, T, optT, mkic, reif) =
berghofe@64962
   907
        (case get_first find_eq
berghofe@64962
   908
           (if in_prem then prems else [concl]) of
berghofe@64962
   909
           SOME q => q
berghofe@64962
   910
         | NONE => error "cannot determine field");
berghofe@64962
   911
      val rls as (_, _, _, _, feval_eq) =
berghofe@64962
   912
        get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R;
berghofe@64962
   913
      val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd);
berghofe@64962
   914
      val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
berghofe@64962
   915
      val ce = Thm.cterm_of ctxt (reif xs t);
berghofe@64962
   916
      val ce' = Thm.cterm_of ctxt (reif xs u);
berghofe@64962
   917
      val fnorm = cv ctxt
berghofe@64962
   918
        (Thm.apply @{cterm fnorm} (Thm.apply (Thm.apply @{cterm FSub} ce) ce'));
berghofe@64962
   919
      val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
berghofe@64962
   920
      val (_, [_, c]) = strip_app dc;
berghofe@64962
   921
      val th =
berghofe@64962
   922
        Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv
berghofe@64962
   923
          (binop_conv
berghofe@64962
   924
             (binop_conv
berghofe@64962
   925
                (K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce')))
berghofe@64962
   926
             (Conv.arg1_conv (K (peval_conv rls cxs n))))))
berghofe@64962
   927
        ([mkic xs,
berghofe@64962
   928
          mk_obj_eq fnorm,
berghofe@64962
   929
          mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS
berghofe@64962
   930
         feval_eq);
berghofe@64962
   931
      val th' = Drule.rotate_prems 1
berghofe@64962
   932
        (th RS (if in_prem then @{thm iffD1} else @{thm iffD2}));
berghofe@64962
   933
    in
berghofe@64962
   934
      if in_prem then
berghofe@64962
   935
        dresolve_tac ctxt [th'] 1 THEN defer_tac 1
berghofe@64962
   936
      else
berghofe@64962
   937
        resolve_tac ctxt [th'] 1
berghofe@64962
   938
    end);
berghofe@64962
   939
berghofe@64962
   940
end
haftmann@64998
   941
\<close>
berghofe@64962
   942
berghofe@64962
   943
context field begin
berghofe@64962
   944
haftmann@64998
   945
local_setup \<open>
berghofe@64962
   946
Local_Theory.declaration {syntax = false, pervasive = false}
berghofe@64962
   947
  (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
berghofe@64962
   948
    (Morphism.term phi @{term R},
berghofe@64962
   949
     (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
berghofe@64962
   950
      Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
berghofe@64962
   951
      Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
berghofe@64962
   952
      singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
berghofe@64962
   953
      singleton (Morphism.fact phi) @{thm feval_eq}))))
haftmann@64998
   954
\<close>
berghofe@64962
   955
berghofe@64962
   956
end
berghofe@64962
   957
haftmann@64998
   958
method_setup field = \<open>
berghofe@64962
   959
  Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt =>
berghofe@64962
   960
    SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt))
haftmann@64998
   961
\<close> "reduce equations over fields to equations over rings"
berghofe@64962
   962
berghofe@64962
   963
end