src/HOL/ex/Reflection_Examples.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
bundle lifting_syntax;
wenzelm@51240
     1
(*  Title:      HOL/ex/Reflection_Examples.thy
wenzelm@20319
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     3
*)
wenzelm@20319
     4
wenzelm@61343
     5
section \<open>Examples for generic reflection and reification\<close>
haftmann@29650
     6
haftmann@51093
     7
theory Reflection_Examples
haftmann@51093
     8
imports Complex_Main "~~/src/HOL/Library/Reflection"
wenzelm@20319
     9
begin
wenzelm@20319
    10
wenzelm@61343
    11
text \<open>This theory presents two methods: reify and reflection\<close>
haftmann@51093
    12
wenzelm@61343
    13
text \<open>
wenzelm@61933
    14
Consider an HOL type \<open>\<sigma>\<close>, the structure of which is not recongnisable
haftmann@51093
    15
on the theory level.  This is the case of @{typ bool}, arithmetical terms such as @{typ int},
wenzelm@61933
    16
@{typ real} etc \dots  In order to implement a simplification on terms of type \<open>\<sigma>\<close> we
haftmann@51093
    17
often need its structure.  Traditionnaly such simplifications are written in ML,
haftmann@51093
    18
proofs are synthesized.
haftmann@51093
    19
wenzelm@61933
    20
An other strategy is to declare an HOL datatype \<open>\<tau>\<close> and an HOL function (the
wenzelm@61933
    21
interpretation) that maps elements of \<open>\<tau>\<close> to elements of \<open>\<sigma>\<close>.
haftmann@51093
    22
wenzelm@61933
    23
The functionality of \<open>reify\<close> then is, given a term \<open>t\<close> of type \<open>\<sigma>\<close>,
wenzelm@61933
    24
to compute a term \<open>s\<close> of type \<open>\<tau>\<close>.  For this it needs equations for the
haftmann@51093
    25
interpretation.
wenzelm@20319
    26
wenzelm@61933
    27
N.B: All the interpretations supported by \<open>reify\<close> must have the type
wenzelm@61933
    28
\<open>'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>\<close>.  The method \<open>reify\<close> can also be told which subterm
wenzelm@61933
    29
of the current subgoal should be reified.  The general call for \<open>reify\<close> is
wenzelm@61933
    30
\<open>reify eqs (t)\<close>, where \<open>eqs\<close> are the defining equations of the interpretation
wenzelm@61933
    31
and \<open>(t)\<close> is an optional parameter which specifies the subterm to which reification
wenzelm@61933
    32
should be applied to.  If \<open>(t)\<close> is abscent, \<open>reify\<close> tries to reify the whole
haftmann@51093
    33
subgoal.
chaieb@20337
    34
wenzelm@61933
    35
The method \<open>reflection\<close> uses \<open>reify\<close> and has a very similar signature:
wenzelm@61933
    36
\<open>reflection corr_thm eqs (t)\<close>.  Here again \<open>eqs\<close> and \<open>(t)\<close>
wenzelm@61933
    37
are as described above and \<open>corr_thm\<close> is a theorem proving
wenzelm@61933
    38
@{prop "I vs (f t) = I vs t"}.  We assume that \<open>I\<close> is the interpretation
wenzelm@61933
    39
and \<open>f\<close> is some useful and executable simplification of type \<open>\<tau> \<Rightarrow> \<tau>\<close>.
wenzelm@61933
    40
The method \<open>reflection\<close> applies reification and hence the theorem @{prop "t = I xs s"}
wenzelm@61933
    41
and hence using \<open>corr_thm\<close> derives @{prop "t = I xs (f s)"}.  It then uses
haftmann@51093
    42
normalization by equational rewriting to prove @{prop "f s = s'"} which almost finishes
haftmann@51093
    43
the proof of @{prop "t = t'"} where @{prop "I xs s' = t'"}.
wenzelm@61343
    44
\<close>
chaieb@20337
    45
wenzelm@61343
    46
text \<open>Example 1 : Propositional formulae and NNF.\<close>
wenzelm@61933
    47
text \<open>The type \<open>fm\<close> represents simple propositional formulae:\<close>
chaieb@20337
    48
blanchet@58310
    49
datatype form = TrueF | FalseF | Less nat nat
haftmann@51093
    50
  | And form form | Or form form | Neg form | ExQ form
chaieb@23547
    51
haftmann@51093
    52
primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
haftmann@51093
    53
where
haftmann@51093
    54
  "interp TrueF vs \<longleftrightarrow> True"
haftmann@51093
    55
| "interp FalseF vs \<longleftrightarrow> False"
haftmann@51093
    56
| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
haftmann@51093
    57
| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
haftmann@51093
    58
| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
haftmann@51093
    59
| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
haftmann@51093
    60
| "interp (ExQ f) vs \<longleftrightarrow> (\<exists>v. interp f (v # vs))"
chaieb@23547
    61
chaieb@23608
    62
lemmas interp_reify_eqs = interp.simps
haftmann@51093
    63
declare interp_reify_eqs [reify]
chaieb@23547
    64
haftmann@51093
    65
lemma "\<exists>x. x < y \<and> x < z"
haftmann@51093
    66
  apply reify
chaieb@23608
    67
  oops
chaieb@23547
    68
blanchet@58310
    69
datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
wenzelm@20319
    70
haftmann@51093
    71
primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
haftmann@51093
    72
where
haftmann@51093
    73
  "Ifm (At n) vs \<longleftrightarrow> vs ! n"
haftmann@51093
    74
| "Ifm (And p q) vs \<longleftrightarrow> Ifm p vs \<and> Ifm q vs"
haftmann@51093
    75
| "Ifm (Or p q) vs \<longleftrightarrow> Ifm p vs \<or> Ifm q vs"
haftmann@51093
    76
| "Ifm (Imp p q) vs \<longleftrightarrow> Ifm p vs \<longrightarrow> Ifm q vs"
haftmann@51093
    77
| "Ifm (Iff p q) vs \<longleftrightarrow> Ifm p vs = Ifm q vs"
haftmann@51093
    78
| "Ifm (NOT p) vs \<longleftrightarrow> \<not> Ifm p vs"
wenzelm@20319
    79
haftmann@51093
    80
lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
haftmann@51093
    81
  apply (reify Ifm.simps)
chaieb@23547
    82
oops
chaieb@23547
    83
wenzelm@61933
    84
text \<open>Method \<open>reify\<close> maps a @{typ bool} to an @{typ fm}.  For this it needs the 
wenzelm@61933
    85
semantics of \<open>fm\<close>, i.e.\ the rewrite rules in \<open>Ifm.simps\<close>.\<close>
chaieb@23547
    86
wenzelm@61343
    87
text \<open>You can also just pick up a subterm to reify.\<close>
haftmann@51093
    88
lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
haftmann@51093
    89
  apply (reify Ifm.simps ("((\<not> D) \<and> (\<not> F))"))
chaieb@23547
    90
oops
chaieb@23547
    91
wenzelm@61343
    92
text \<open>Let's perform NNF. This is a version that tends to generate disjunctions\<close>
haftmann@51093
    93
primrec fmsize :: "fm \<Rightarrow> nat"
haftmann@51093
    94
where
wenzelm@20319
    95
  "fmsize (At n) = 1"
krauss@35419
    96
| "fmsize (NOT p) = 1 + fmsize p"
krauss@35419
    97
| "fmsize (And p q) = 1 + fmsize p + fmsize q"
krauss@35419
    98
| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
krauss@35419
    99
| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
krauss@35419
   100
| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
krauss@35419
   101
krauss@35419
   102
lemma [measure_function]: "is_measure fmsize" ..
wenzelm@20319
   103
krauss@35419
   104
fun nnf :: "fm \<Rightarrow> fm"
krauss@35419
   105
where
wenzelm@20319
   106
  "nnf (At n) = At n"
krauss@35419
   107
| "nnf (And p q) = And (nnf p) (nnf q)"
krauss@35419
   108
| "nnf (Or p q) = Or (nnf p) (nnf q)"
krauss@35419
   109
| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
krauss@35419
   110
| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
krauss@35419
   111
| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
krauss@35419
   112
| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
krauss@35419
   113
| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
krauss@35419
   114
| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
krauss@35419
   115
| "nnf (NOT (NOT p)) = nnf p"
krauss@35419
   116
| "nnf (NOT p) = NOT p"
wenzelm@20319
   117
wenzelm@61343
   118
text \<open>The correctness theorem of @{const nnf}: it preserves the semantics of @{typ fm}\<close>
haftmann@51093
   119
lemma nnf [reflection]:
haftmann@51093
   120
  "Ifm (nnf p) vs = Ifm p vs"
wenzelm@20319
   121
  by (induct p rule: nnf.induct) auto
wenzelm@20319
   122
wenzelm@61343
   123
text \<open>Now let's perform NNF using our @{const nnf} function defined above.  First to the
wenzelm@61343
   124
  whole subgoal.\<close>
haftmann@51093
   125
lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
haftmann@51093
   126
  apply (reflection Ifm.simps)
wenzelm@20319
   127
oops
wenzelm@20319
   128
wenzelm@61343
   129
text \<open>Now we specify on which subterm it should be applied\<close>
haftmann@51093
   130
lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
haftmann@51093
   131
  apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
wenzelm@20319
   132
oops
wenzelm@20319
   133
wenzelm@20319
   134
wenzelm@61343
   135
text \<open>Example 2: Simple arithmetic formulae\<close>
wenzelm@20319
   136
wenzelm@61933
   137
text \<open>The type \<open>num\<close> reflects linear expressions over natural number\<close>
blanchet@58310
   138
datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
wenzelm@20319
   139
wenzelm@61343
   140
text \<open>This is just technical to make recursive definitions easier.\<close>
krauss@35419
   141
primrec num_size :: "num \<Rightarrow> nat" 
krauss@35419
   142
where
wenzelm@20319
   143
  "num_size (C c) = 1"
krauss@35419
   144
| "num_size (Var n) = 1"
krauss@35419
   145
| "num_size (Add a b) = 1 + num_size a + num_size b"
krauss@35419
   146
| "num_size (Mul c a) = 1 + num_size a"
krauss@35419
   147
| "num_size (CN n c a) = 4 + num_size a "
wenzelm@20319
   148
haftmann@51093
   149
lemma [measure_function]: "is_measure num_size" ..
haftmann@51093
   150
wenzelm@61343
   151
text \<open>The semantics of num\<close>
krauss@35419
   152
primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
krauss@35419
   153
where
chaieb@23624
   154
  Inum_C  : "Inum (C i) vs = i"
krauss@35419
   155
| Inum_Var: "Inum (Var n) vs = vs!n"
krauss@35419
   156
| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
krauss@35419
   157
| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
krauss@35419
   158
| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
wenzelm@20319
   159
wenzelm@61343
   160
text \<open>Let's reify some nat expressions \dots\<close>
haftmann@51093
   161
lemma "4 * (2 * x + (y::nat)) + f a \<noteq> 0"
haftmann@51093
   162
  apply (reify Inum.simps ("4 * (2 * x + (y::nat)) + f a"))
wenzelm@20319
   163
oops
wenzelm@61933
   164
text \<open>We're in a bad situation! \<open>x\<close>, \<open>y\<close> and \<open>f\<close> have been recongnized
haftmann@51093
   165
as constants, which is correct but does not correspond to our intuition of the constructor C.
wenzelm@61343
   166
It should encapsulate constants, i.e. numbers, i.e. numerals.\<close>
chaieb@20337
   167
wenzelm@61933
   168
text \<open>So let's leave the \<open>Inum_C\<close> equation at the end and see what happens \dots\<close>
haftmann@51093
   169
lemma "4 * (2 * x + (y::nat)) \<noteq> 0"
haftmann@51093
   170
  apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2 * x + (y::nat))"))
wenzelm@20319
   171
oops
wenzelm@61933
   172
text \<open>Hm, let's specialize \<open>Inum_C\<close> with numerals.\<close>
wenzelm@20319
   173
huffman@47108
   174
lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
wenzelm@20319
   175
lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
wenzelm@20319
   176
wenzelm@61343
   177
text \<open>Second attempt\<close>
haftmann@51093
   178
lemma "1 * (2 * x + (y::nat)) \<noteq> 0"
haftmann@51093
   179
  apply (reify Inum_eqs ("1 * (2 * x + (y::nat))"))
wenzelm@20319
   180
oops
haftmann@51093
   181
wenzelm@61343
   182
text\<open>That was fine, so let's try another one \dots\<close>
wenzelm@20319
   183
haftmann@51093
   184
lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
haftmann@51093
   185
  apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
wenzelm@20319
   186
oops
haftmann@51093
   187
wenzelm@61933
   188
text \<open>Oh!! 0 is not a variable \dots\ Oh! 0 is not a \<open>numeral\<close> \dots\ thing.
wenzelm@61343
   189
The same for 1. So let's add those equations, too.\<close>
wenzelm@20319
   190
chaieb@23624
   191
lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
haftmann@51093
   192
  by simp_all
chaieb@20337
   193
wenzelm@20319
   194
lemmas Inum_eqs'= Inum_eqs Inum_01
chaieb@20337
   195
wenzelm@61343
   196
text\<open>Third attempt:\<close>
wenzelm@20319
   197
haftmann@51093
   198
lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
haftmann@51093
   199
  apply (reify Inum_eqs' ("1 * (2 * x + (y::nat) + 0 + 1)"))
wenzelm@20319
   200
oops
haftmann@51093
   201
wenzelm@61343
   202
text \<open>Okay, let's try reflection. Some simplifications on @{typ num} follow. You can
wenzelm@61933
   203
  skim until the main theorem \<open>linum\<close>.\<close>
haftmann@51093
   204
  
krauss@35419
   205
fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
krauss@35419
   206
where
krauss@35419
   207
  "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
haftmann@51093
   208
    (if n1 = n2 then 
haftmann@51093
   209
      (let c = c1 + c2
haftmann@51093
   210
       in (if c = 0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
haftmann@51093
   211
     else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
haftmann@51093
   212
     else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
krauss@35419
   213
| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
krauss@35419
   214
| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
haftmann@51093
   215
| "lin_add (C b1) (C b2) = C (b1 + b2)"
krauss@35419
   216
| "lin_add a b = Add a b"
haftmann@51093
   217
haftmann@51093
   218
lemma lin_add:
haftmann@51093
   219
  "Inum (lin_add t s) bs = Inum (Add t s) bs"
haftmann@51093
   220
  apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
haftmann@51093
   221
  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
haftmann@51093
   222
  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
haftmann@51093
   223
  done
wenzelm@20319
   224
krauss@35419
   225
fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
krauss@35419
   226
where
haftmann@51093
   227
  "lin_mul (C j) i = C (i * j)"
haftmann@51093
   228
| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i * c) (lin_mul a i))"
krauss@35419
   229
| "lin_mul t i = (Mul i t)"
wenzelm@20319
   230
haftmann@51093
   231
lemma lin_mul:
haftmann@51093
   232
  "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
haftmann@51093
   233
  by (induct t i rule: lin_mul.induct) (auto simp add: algebra_simps)
krauss@35419
   234
krauss@35419
   235
fun linum:: "num \<Rightarrow> num"
krauss@35419
   236
where
wenzelm@20319
   237
  "linum (C b) = C b"
krauss@35419
   238
| "linum (Var n) = CN n 1 (C 0)"
krauss@35419
   239
| "linum (Add t s) = lin_add (linum t) (linum s)"
krauss@35419
   240
| "linum (Mul c t) = lin_mul (linum t) c"
krauss@35419
   241
| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
wenzelm@20319
   242
haftmann@51093
   243
lemma linum [reflection]:
haftmann@51093
   244
  "Inum (linum t) bs = Inum t bs"
haftmann@51093
   245
  by (induct t rule: linum.induct) (simp_all add: lin_mul lin_add)
wenzelm@20319
   246
wenzelm@61343
   247
text \<open>Now we can use linum to simplify nat terms using reflection\<close>
haftmann@51093
   248
haftmann@51093
   249
lemma "Suc (Suc 1) * (x + Suc 1 * y) = 3 * x + 6 * y"
haftmann@51093
   250
  apply (reflection Inum_eqs' only: "Suc (Suc 1) * (x + Suc 1 * y)")
wenzelm@20319
   251
oops
wenzelm@20319
   252
wenzelm@61343
   253
text \<open>Let's lift this to formulae and see what happens\<close>
wenzelm@20319
   254
blanchet@58310
   255
datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
wenzelm@20319
   256
  Conj aform aform | Disj aform aform | NEG aform | T | F
krauss@35419
   257
krauss@35419
   258
primrec linaformsize:: "aform \<Rightarrow> nat"
krauss@35419
   259
where
wenzelm@20319
   260
  "linaformsize T = 1"
krauss@35419
   261
| "linaformsize F = 1"
krauss@35419
   262
| "linaformsize (Lt a b) = 1"
krauss@35419
   263
| "linaformsize (Ge a b) = 1"
krauss@35419
   264
| "linaformsize (Eq a b) = 1"
krauss@35419
   265
| "linaformsize (NEq a b) = 1"
krauss@35419
   266
| "linaformsize (NEG p) = 2 + linaformsize p"
krauss@35419
   267
| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
krauss@35419
   268
| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
wenzelm@20319
   269
krauss@35419
   270
lemma [measure_function]: "is_measure linaformsize" ..
wenzelm@20319
   271
krauss@35419
   272
primrec is_aform :: "aform => nat list => bool"
krauss@35419
   273
where
wenzelm@28866
   274
  "is_aform T vs = True"
krauss@35419
   275
| "is_aform F vs = False"
krauss@35419
   276
| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
krauss@35419
   277
| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
krauss@35419
   278
| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
krauss@35419
   279
| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
krauss@35419
   280
| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
krauss@35419
   281
| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
krauss@35419
   282
| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
wenzelm@20319
   283
wenzelm@61343
   284
text\<open>Let's reify and do reflection\<close>
haftmann@51093
   285
lemma "(3::nat) * x + t < 0 \<and> (2 * x + y \<noteq> 17)"
haftmann@51093
   286
  apply (reify Inum_eqs' is_aform.simps) 
wenzelm@20319
   287
oops
wenzelm@20319
   288
wenzelm@61343
   289
text \<open>Note that reification handles several interpretations at the same time\<close>
haftmann@51093
   290
lemma "(3::nat) * x + t < 0 \<and> x * x + t * x + 3 + 1 = z * t * 4 * z \<or> x + x + 1 < 0"
haftmann@51093
   291
  apply (reflection Inum_eqs' is_aform.simps only: "x + x + 1") 
wenzelm@20319
   292
oops
wenzelm@20319
   293
wenzelm@61343
   294
text \<open>For reflection we now define a simple transformation on aform: NNF + linum on atoms\<close>
krauss@35419
   295
krauss@35419
   296
fun linaform:: "aform \<Rightarrow> aform"
krauss@35419
   297
where
wenzelm@20319
   298
  "linaform (Lt s t) = Lt (linum s) (linum t)"
krauss@35419
   299
| "linaform (Eq s t) = Eq (linum s) (linum t)"
krauss@35419
   300
| "linaform (Ge s t) = Ge (linum s) (linum t)"
krauss@35419
   301
| "linaform (NEq s t) = NEq (linum s) (linum t)"
krauss@35419
   302
| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
krauss@35419
   303
| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
krauss@35419
   304
| "linaform (NEG T) = F"
krauss@35419
   305
| "linaform (NEG F) = T"
krauss@35419
   306
| "linaform (NEG (Lt a b)) = Ge a b"
krauss@35419
   307
| "linaform (NEG (Ge a b)) = Lt a b"
krauss@35419
   308
| "linaform (NEG (Eq a b)) = NEq a b"
krauss@35419
   309
| "linaform (NEG (NEq a b)) = Eq a b"
krauss@35419
   310
| "linaform (NEG (NEG p)) = linaform p"
krauss@35419
   311
| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
krauss@35419
   312
| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
krauss@35419
   313
| "linaform p = p"
wenzelm@20319
   314
wenzelm@28866
   315
lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
wenzelm@28866
   316
  by (induct p rule: linaform.induct) (auto simp add: linum)
wenzelm@20319
   317
haftmann@51093
   318
lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
haftmann@51093
   319
  (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
haftmann@51093
   320
  apply (reflection Inum_eqs' is_aform.simps rules: linaform)  
chaieb@23650
   321
oops
chaieb@23650
   322
haftmann@51093
   323
declare linaform [reflection]
haftmann@51093
   324
haftmann@51093
   325
lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
haftmann@51093
   326
  (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
haftmann@51093
   327
  apply (reflection Inum_eqs' is_aform.simps)
chaieb@20564
   328
oops
chaieb@20564
   329
wenzelm@61343
   330
text \<open>We now give an example where interpretaions have zero or more than only
haftmann@51093
   331
  one envornement of different types and show that automatic reification also deals with
wenzelm@61343
   332
  bindings\<close>
haftmann@51093
   333
  
blanchet@58310
   334
datatype rb = BC bool | BAnd rb rb | BOr rb rb
haftmann@51093
   335
krauss@35419
   336
primrec Irb :: "rb \<Rightarrow> bool"
krauss@35419
   337
where
haftmann@51093
   338
  "Irb (BC p) \<longleftrightarrow> p"
haftmann@51093
   339
| "Irb (BAnd s t) \<longleftrightarrow> Irb s \<and> Irb t"
haftmann@51093
   340
| "Irb (BOr s t) \<longleftrightarrow> Irb s \<or> Irb t"
chaieb@20564
   341
chaieb@20564
   342
lemma "A \<and> (B \<or> D \<and> B) \<and> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B)"
haftmann@51093
   343
  apply (reify Irb.simps)
wenzelm@20319
   344
oops
wenzelm@20319
   345
blanchet@58310
   346
datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
haftmann@51093
   347
  | INeg rint | ISub rint rint
chaieb@23650
   348
krauss@35419
   349
primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
krauss@35419
   350
where
haftmann@51093
   351
  Irint_Var: "Irint (IVar n) vs = vs ! n"
krauss@35419
   352
| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
krauss@35419
   353
| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
krauss@35419
   354
| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
krauss@35419
   355
| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
krauss@35419
   356
| Irint_C: "Irint (IC i) vs = i"
haftmann@51093
   357
chaieb@23624
   358
lemma Irint_C0: "Irint (IC 0) vs = 0"
chaieb@20564
   359
  by simp
haftmann@51093
   360
chaieb@23624
   361
lemma Irint_C1: "Irint (IC 1) vs = 1"
chaieb@20564
   362
  by simp
haftmann@51093
   363
huffman@47108
   364
lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
chaieb@20564
   365
  by simp
haftmann@51093
   366
huffman@47108
   367
lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
haftmann@51093
   368
haftmann@51093
   369
lemma "(3::int) * x + y * y - 9 + (- z) = 0"
haftmann@51093
   370
  apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
chaieb@20564
   371
  oops
haftmann@51093
   372
blanchet@58310
   373
datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
haftmann@51093
   374
haftmann@51093
   375
primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
krauss@35419
   376
where
chaieb@23624
   377
  "Irlist (LEmpty) is vs = []"
haftmann@51093
   378
| "Irlist (LVar n) is vs = vs ! n"
haftmann@51093
   379
| "Irlist (LCons i t) is vs = Irint i is # Irlist t is vs"
haftmann@51093
   380
| "Irlist (LAppend s t) is vs = Irlist s is vs @ Irlist t is vs"
haftmann@51093
   381
chaieb@20564
   382
lemma "[(1::int)] = []"
haftmann@51093
   383
  apply (reify Irlist.simps Irint_simps ("[1] :: int list"))
chaieb@20564
   384
  oops
chaieb@20374
   385
haftmann@51093
   386
lemma "([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs = [y * y - z - 9 + (3::int) * x]"
haftmann@51093
   387
  apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
chaieb@20564
   388
  oops
chaieb@20374
   389
blanchet@58310
   390
datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
haftmann@51093
   391
  | NNeg rnat | NSub rnat rnat | Nlgth rlist
haftmann@51093
   392
haftmann@51093
   393
primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
krauss@35419
   394
where
krauss@35419
   395
  Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
haftmann@51093
   396
| Irnat_Var: "Irnat (NVar n) is ls vs = vs ! n"
krauss@35419
   397
| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
krauss@35419
   398
| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
krauss@35419
   399
| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
krauss@35419
   400
| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
krauss@35419
   401
| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
krauss@35419
   402
| Irnat_C: "Irnat (NC i) is ls vs = i"
haftmann@51093
   403
chaieb@23624
   404
lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
haftmann@51093
   405
  by simp
haftmann@51093
   406
chaieb@23624
   407
lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
haftmann@51093
   408
  by simp
haftmann@51093
   409
huffman@47108
   410
lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
haftmann@51093
   411
  by simp
haftmann@51093
   412
chaieb@20564
   413
lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
huffman@47108
   414
  Irnat_C0 Irnat_C1 Irnat_Cnumeral
haftmann@51093
   415
haftmann@51093
   416
lemma "Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs) = length xs"
haftmann@51093
   417
  apply (reify Irnat_simps Irlist.simps Irint_simps
haftmann@51093
   418
     ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
chaieb@20564
   419
  oops
haftmann@51093
   420
blanchet@58310
   421
datatype rifm = RT | RF | RVar nat
chaieb@20564
   422
  | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
haftmann@51093
   423
  | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
haftmann@51093
   424
  | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
chaieb@20564
   425
  | RBEX rifm | RBALL rifm
chaieb@23624
   426
krauss@35419
   427
primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
krauss@35419
   428
where
haftmann@51093
   429
  "Irifm RT ps is ls ns \<longleftrightarrow> True"
haftmann@51093
   430
| "Irifm RF ps is ls ns \<longleftrightarrow> False"
haftmann@51093
   431
| "Irifm (RVar n) ps is ls ns \<longleftrightarrow> ps ! n"
haftmann@51093
   432
| "Irifm (RNLT s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns < Irnat t is ls ns"
haftmann@51093
   433
| "Irifm (RNILT s t) ps is ls ns \<longleftrightarrow> int (Irnat s is ls ns) < Irint t is"
haftmann@51093
   434
| "Irifm (RNEQ s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns = Irnat t is ls ns"
haftmann@51093
   435
| "Irifm (RAnd p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<and> Irifm q ps is ls ns"
haftmann@51093
   436
| "Irifm (ROr p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<or> Irifm q ps is ls ns"
haftmann@51093
   437
| "Irifm (RImp p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns"
haftmann@51093
   438
| "Irifm (RIff p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns = Irifm q ps is ls ns"
haftmann@51093
   439
| "Irifm (RNEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is ls (x # ns))"
haftmann@51093
   440
| "Irifm (RIEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps (x # is) ls ns)"
haftmann@51093
   441
| "Irifm (RLEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is (x # ls) ns)"
haftmann@51093
   442
| "Irifm (RBEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p (x # ps) is ls ns)"
haftmann@51093
   443
| "Irifm (RNALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is ls (x#ns))"
haftmann@51093
   444
| "Irifm (RIALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps (x # is) ls ns)"
haftmann@51093
   445
| "Irifm (RLALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is (x#ls) ns)"
haftmann@51093
   446
| "Irifm (RBALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p (x # ps) is ls ns)"
chaieb@20374
   447
haftmann@51093
   448
lemma " \<forall>x. \<exists>n. ((Suc n) * length (([(3::int) * x + f t * y - 9 + (- z)] @ []) @ xs) = length xs) \<and> m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \<longrightarrow> (\<exists>p. \<forall>q. p \<and> q \<longrightarrow> r)"
chaieb@20564
   449
  apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
chaieb@20374
   450
oops
chaieb@20374
   451
wenzelm@61343
   452
text \<open>An example for equations containing type variables\<close>
chaieb@22199
   453
blanchet@58310
   454
datatype prod = Zero | One | Var nat | Mul prod prod 
chaieb@22199
   455
  | Pw prod nat | PNM nat nat prod
haftmann@51093
   456
haftmann@51093
   457
primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
krauss@35419
   458
where
chaieb@23624
   459
  "Iprod Zero vs = 0"
krauss@35419
   460
| "Iprod One vs = 1"
haftmann@51093
   461
| "Iprod (Var n) vs = vs ! n"
haftmann@51093
   462
| "Iprod (Mul a b) vs = Iprod a vs * Iprod b vs"
haftmann@51093
   463
| "Iprod (Pw a n) vs = Iprod a vs ^ n"
haftmann@51093
   464
| "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
haftmann@39246
   465
blanchet@58310
   466
datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
chaieb@22199
   467
  | Or sgn sgn | And sgn sgn
chaieb@22199
   468
haftmann@51093
   469
primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
krauss@35419
   470
where 
haftmann@51093
   471
  "Isgn Tr vs \<longleftrightarrow> True"
haftmann@51093
   472
| "Isgn F vs \<longleftrightarrow> False"
haftmann@51093
   473
| "Isgn (ZeroEq t) vs \<longleftrightarrow> Iprod t vs = 0"
haftmann@51093
   474
| "Isgn (NZeroEq t) vs \<longleftrightarrow> Iprod t vs \<noteq> 0"
haftmann@51093
   475
| "Isgn (Pos t) vs \<longleftrightarrow> Iprod t vs > 0"
haftmann@51093
   476
| "Isgn (Neg t) vs \<longleftrightarrow> Iprod t vs < 0"
haftmann@51093
   477
| "Isgn (And p q) vs \<longleftrightarrow> Isgn p vs \<and> Isgn q vs"
haftmann@51093
   478
| "Isgn (Or p q) vs \<longleftrightarrow> Isgn p vs \<or> Isgn q vs"
chaieb@22199
   479
chaieb@22199
   480
lemmas eqs = Isgn.simps Iprod.simps
chaieb@22199
   481
haftmann@51093
   482
lemma "(x::'a::{linordered_idom}) ^ 4 * y * z * y ^ 2 * z ^ 23 > 0"
chaieb@22199
   483
  apply (reify eqs)
chaieb@22199
   484
  oops
chaieb@22199
   485
wenzelm@20319
   486
end
haftmann@51093
   487