src/HOL/ex/Reflection_Examples.thy

 *}
 
 text {* Example 1 : Propositional formulae and NNF. *}
 text {* The type @{text fm} represents simple propositional formulae: *}
 
-datatype form = TrueF | FalseF | Less nat nat
+datatype_new form = TrueF | FalseF | Less nat nat
   | And form form | Or form form | Neg form | ExQ form
 
 primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
 where
   "interp TrueF vs \<longleftrightarrow> True"

 
 lemma "\<exists>x. x < y \<and> x < z"
   apply reify
   oops
 
-datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
+datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
 
 primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
 where
   "Ifm (At n) vs \<longleftrightarrow> vs ! n"
 | "Ifm (And p q) vs \<longleftrightarrow> Ifm p vs \<and> Ifm q vs"

 
 
 text {* Example 2: Simple arithmetic formulae *}
 
 text {* The type @{text num} reflects linear expressions over natural number *}
-datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
+datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
 
 text {* This is just technical to make recursive definitions easier. *}
 primrec num_size :: "num \<Rightarrow> nat" 
 where
   "num_size (C c) = 1"

   apply (reflection Inum_eqs' only: "Suc (Suc 1) * (x + Suc 1 * y)")
 oops
 
 text {* Let's lift this to formulae and see what happens *}
 
-datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
+datatype_new aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   Conj aform aform | Disj aform aform | NEG aform | T | F
 
 primrec linaformsize:: "aform \<Rightarrow> nat"
 where
   "linaformsize T = 1"

 
 text {* We now give an example where interpretaions have zero or more than only
   one envornement of different types and show that automatic reification also deals with
   bindings *}
   
-datatype rb = BC bool | BAnd rb rb | BOr rb rb
+datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
 
 primrec Irb :: "rb \<Rightarrow> bool"
 where
   "Irb (BC p) \<longleftrightarrow> p"
 | "Irb (BAnd s t) \<longleftrightarrow> Irb s \<and> Irb t"

 
 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)"
   apply (reify Irb.simps)
 oops
 
-datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
+datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
   | INeg rint | ISub rint rint
 
 primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
 where
   Irint_Var: "Irint (IVar n) vs = vs ! n"

 
 lemma "(3::int) * x + y * y - 9 + (- z) = 0"
   apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
   oops
 
-datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
+datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
 
 primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
 where
   "Irlist (LEmpty) is vs = []"
 | "Irlist (LVar n) is vs = vs ! n"

 
 lemma "([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs = [y * y - z - 9 + (3::int) * x]"
   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
   oops
 
-datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
+datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
   | NNeg rnat | NSub rnat rnat | Nlgth rlist
 
 primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
 where
   Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"

 lemma "Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs) = length xs"
   apply (reify Irnat_simps Irlist.simps Irint_simps
      ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
   oops
 
-datatype rifm = RT | RF | RVar nat
+datatype_new rifm = RT | RF | RVar nat
   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
   | RBEX rifm | RBALL rifm
 

   apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
 oops
 
 text {* An example for equations containing type variables *}
 
-datatype prod = Zero | One | Var nat | Mul prod prod 
+datatype_new prod = Zero | One | Var nat | Mul prod prod 
   | Pw prod nat | PNM nat nat prod
 
 primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
 where
   "Iprod Zero vs = 0"

 | "Iprod (Var n) vs = vs ! n"
 | "Iprod (Mul a b) vs = Iprod a vs * Iprod b vs"
 | "Iprod (Pw a n) vs = Iprod a vs ^ n"
 | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
 
-datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
+datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   | Or sgn sgn | And sgn sgn
 
 primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
 where 
   "Isgn Tr vs \<longleftrightarrow> True"