--- a/src/HOL/Imperative_HOL/Ref.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Feb 13 16:30:34 2013 +0100
@@ -216,7 +216,7 @@
by (rule Heap_eqI) (simp add: change_def lookup_chain)
-text {* Non-interaction between imperative array and imperative references *}
+text {* Non-interaction between imperative arrays and imperative references *}
lemma array_get_set [simp]:
"Array.get (set r v h) = Array.get h"
@@ -263,7 +263,7 @@
subsection {* Code generator setup *}
-text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
+text {* Intermediate operation avoids invariance problem in @{text Scala} (similar to value restriction) *}
definition ref' where
[code del]: "ref' = ref"
--- a/src/HOL/Library/Code_Numeral_Types.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy Wed Feb 13 16:30:34 2013 +0100
@@ -83,6 +83,14 @@
"int_of_integer (of_nat n) = of_nat n"
by (induct n) simp_all
+definition integer_of_nat :: "nat \<Rightarrow> integer"
+where
+ "integer_of_nat = of_nat"
+
+lemma int_of_integer_integer_of_nat [simp]:
+ "int_of_integer (integer_of_nat n) = of_nat n"
+ by (simp add: integer_of_nat_def)
+
definition nat_of_integer :: "integer \<Rightarrow> nat"
where
"nat_of_integer k = Int.nat (int_of_integer k)"
@@ -95,7 +103,11 @@
"int_of_integer (of_int k) = k"
by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
-lemma integer_integer_of_int_eq_of_integer_integer_of_int [simp, code_abbrev]:
+lemma nat_of_integer_integer_of_nat [simp]:
+ "nat_of_integer (integer_of_nat n) = n"
+ by (simp add: integer_of_nat_def)
+
+lemma integer_of_int_eq_of_int [simp, code_abbrev]:
"integer_of_int = of_int"
by rule (simp add: integer_eq_iff)
@@ -785,6 +797,12 @@
where
"Nat = natural_of_integer"
+lemma [code_post]:
+ "Nat 0 = 0"
+ "Nat 1 = 1"
+ "Nat (numeral k) = numeral k"
+ by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
+
lemma [code abstype]:
"Nat (integer_of_natural n) = n"
by (unfold Nat_def) (fact natural_of_integer_of_natural)
--- a/src/HOL/Library/Code_Target_Int.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Wed Feb 13 16:30:34 2013 +0100
@@ -26,18 +26,18 @@
by (simp add: integer_of_num_def fun_eq_iff)
lemma [code_abbrev]:
- "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
+ "int_of_integer (numeral k) = Int.Pos k"
by simp
lemma [code_abbrev]:
- "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
+ "int_of_integer (neg_numeral k) = Int.Neg k"
by simp
-
-lemma [code]:
+
+lemma [code, symmetric, code_post]:
"0 = int_of_integer 0"
by simp
-lemma [code]:
+lemma [code, symmetric, code_post]:
"1 = int_of_integer 1"
by simp
--- a/src/HOL/Library/Code_Target_Nat.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Wed Feb 13 16:30:34 2013 +0100
@@ -14,13 +14,15 @@
where
"Nat = nat_of_integer"
-definition integer_of_nat :: "nat \<Rightarrow> integer"
-where
- [code_abbrev]: "integer_of_nat = of_nat"
+lemma [code_post]:
+ "Nat 0 = 0"
+ "Nat 1 = 1"
+ "Nat (numeral k) = numeral k"
+ by (simp_all add: Nat_def nat_of_integer_def)
-lemma int_of_integer_integer_of_nat [simp]:
- "int_of_integer (integer_of_nat n) = of_nat n"
- by (simp add: integer_of_nat_def)
+lemma [code_abbrev]:
+ "integer_of_nat = of_nat"
+ by (fact integer_of_nat_def)
lemma [code_unfold]:
"Int.nat (int_of_integer k) = nat_of_integer k"
@@ -35,7 +37,7 @@
by (simp add: integer_of_nat_def)
lemma [code_abbrev]:
- "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
+ "nat_of_integer (numeral k) = nat_of_num k"
by (simp add: nat_of_integer_def nat_of_num_numeral)
lemma [code abstract]:
--- a/src/HOL/Library/IArray.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Library/IArray.thy Wed Feb 13 16:30:34 2013 +0100
@@ -1,7 +1,7 @@
header "Immutable Arrays with Code Generation"
theory IArray
-imports "~~/src/HOL/Library/Efficient_Nat"
+imports Main
begin
text{* Immutable arrays are lists wrapped up in an additional constructor.
@@ -15,39 +15,69 @@
datatype 'a iarray = IArray "'a list"
-fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
-"of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
-
-fun length :: "'a iarray \<Rightarrow> nat" where
-"length (IArray xs) = List.length xs"
-hide_const (open) length
-
-fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
-"(IArray as) !! n = as!n"
-hide_const (open) sub
-
-fun list_of :: "'a iarray \<Rightarrow> 'a list" where
+primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
"list_of (IArray xs) = xs"
hide_const (open) list_of
+definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+[simp]: "of_fun f n = IArray (map f [0..<n])"
+hide_const (open) of_fun
+
+definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+[simp]: "as !! n = IArray.list_of as ! n"
+hide_const (open) sub
+
+definition length :: "'a iarray \<Rightarrow> nat" where
+[simp]: "length as = List.length (IArray.list_of as)"
+hide_const (open) length
+
+lemma list_of_code [code]:
+"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
+by (cases as) (simp add: map_nth)
+
subsection "Code Generation"
+code_reserved SML Vector
+
code_type iarray
(SML "_ Vector.vector")
code_const IArray
(SML "Vector.fromList")
-code_const IArray.sub
- (SML "Vector.sub(_,_)")
-code_const IArray.length
+
+primrec tabulate :: "code_numeral \<times> (code_numeral \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+"tabulate (n, f) = IArray (map (f \<circ> Code_Numeral.of_nat) [0..<Code_Numeral.nat_of n])"
+hide_const (open) tabulate
+
+lemma [code]:
+"IArray.of_fun f n = IArray.tabulate (Code_Numeral.of_nat n, f \<circ> Code_Numeral.nat_of)"
+by simp
+
+code_const IArray.tabulate
+ (SML "Vector.tabulate")
+
+primrec sub' :: "'a iarray \<times> code_numeral \<Rightarrow> 'a" where
+"sub' (as, n) = IArray.list_of as ! Code_Numeral.nat_of n"
+hide_const (open) sub'
+
+lemma [code]:
+"as !! n = IArray.sub' (as, Code_Numeral.of_nat n)"
+by simp
+
+code_const IArray.sub'
+ (SML "Vector.sub")
+
+definition length' :: "'a iarray \<Rightarrow> code_numeral" where
+[simp]: "length' as = Code_Numeral.of_nat (List.length (IArray.list_of as))"
+hide_const (open) length'
+
+lemma [code]:
+"IArray.length as = Code_Numeral.nat_of (IArray.length' as)"
+by simp
+
+code_const IArray.length'
(SML "Vector.length")
-code_const IArray.of_fun
- (SML "!(fn f => fn n => Vector.tabulate(n,f))")
-
-lemma list_of_code[code]:
- "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
-by (cases A) (simp add: map_nth)
end
+
--- a/src/HOL/List.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/List.thy Wed Feb 13 16:30:34 2013 +0100
@@ -162,6 +162,13 @@
hide_const (open) find
+primrec those :: "'a option list \<Rightarrow> 'a list option"
+where
+"those [] = Some []" |
+"those (x # xs) = (case x of
+ None \<Rightarrow> None
+| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
+
primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"remove1 x [] = []" |
"remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
--- a/src/HOL/Mutabelle/mutabelle.ML Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed Feb 13 16:30:34 2013 +0100
@@ -30,9 +30,6 @@
facts []
end;
-fun thms_of thy = filter (fn (_, th) =>
- Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
-
fun consts_of thy =
let
val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
@@ -128,8 +125,8 @@
let
val revlC = rev longContext
val revsC = rev shortContext
- fun is_prefix [] longList = true
- | is_prefix shList [] = false
+ fun is_prefix [] _ = true
+ | is_prefix _ [] = false
| is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
in
is_prefix revsC revlC
@@ -227,8 +224,8 @@
(*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*)
fun areReplacable [] [] = false
- | areReplacable fstPath [] = false
- | areReplacable [] sndPath = false
+ | areReplacable _ [] = false
+ | areReplacable [] _ = false
| areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true;
@@ -237,21 +234,21 @@
(*substitutes the term at the position of the first list in fstTerm by sndTerm.
The lists represent paths as generated by createSubTermList*)
-fun substitute [] fstTerm sndTerm = sndTerm
+fun substitute [] _ sndTerm = sndTerm
| substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
| substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u
| substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
- | substitute (_::xs) _ sndTerm =
+ | substitute (_::_) _ sndTerm =
raise WrongPath ("The Term could not be found at the specified position");
(*get the subterm with the specified path in myTerm*)
fun getSubTerm myTerm [] = myTerm
- | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
- | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
- | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
- | getSubTerm _ (_::xs) =
+ | getSubTerm (Abs(_,_,subTerm)) (0::xs) = getSubTerm subTerm xs
+ | getSubTerm (t $ _) (0::xs) = getSubTerm t xs
+ | getSubTerm (_ $ u) (1::xs) = getSubTerm u xs
+ | getSubTerm _ (_::_) =
raise WrongPath ("The subterm could not be found at the specified position");
@@ -423,23 +420,4 @@
Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
| freeze t = t;
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
- | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
-
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (freeze t));
-
-fun is_executable thy insts th =
- let
- val ctxt' = Proof_Context.init_global thy
- |> Config.put Quickcheck.size 1
- |> Config.put Quickcheck.iterations 1
- val test = Quickcheck_Common.test_term
- ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false
- in
- case try test (preprocess thy insts (prop_of th), []) of
- SOME _ => (Output.urgent_message "executable"; true)
- | NONE => (Output.urgent_message ("not executable"); false)
- end;
-
end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 13 16:30:34 2013 +0100
@@ -105,7 +105,7 @@
(** quickcheck **)
-fun invoke_quickcheck change_options quickcheck_generator thy t =
+fun invoke_quickcheck change_options thy t =
TimeLimit.timeLimit (seconds 30.0)
(fn _ =>
let
@@ -123,7 +123,7 @@
(Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
fun quickcheck_mtd change_options quickcheck_generator =
- ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
+ ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
(** solve direct **)
@@ -335,8 +335,6 @@
(* andalso is_executable_thm thy th *))
(map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
-fun count x = (length oo filter o equal) x
-
fun elapsed_time description e =
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
@@ -354,27 +352,14 @@
val _ = Output.urgent_message ("Invoking " ^ mtd_name)
val (res, timing) = elapsed_time "total time"
(fn () => case try (invoke_mtd thy) t of
- SOME (res, timing) => res
+ SOME (res, _) => res
| NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
Error))
val _ = Output.urgent_message (" Done")
in (res, [timing]) end
-(* theory -> term list -> mtd -> subentry *)
-
-fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
- let
- val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
- in
- (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
- count Donno res, count Timeout res, count Error res)
- end
-
(* creating entries *)
-fun create_entry thy thm exec mutants mtds =
- (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-
fun create_detailed_entry thy thm exec mutants mtds =
let
fun create_mutant_subentry mutant = (mutant,
@@ -422,15 +407,6 @@
create_entry thy thm exec mutants mtds
end
-(* theory -> mtd list -> thm list -> report *)
-val mutate_theorems = map oooo mutate_theorem
-
-fun string_of_mutant_subentry thy thm_name (t, results) =
- "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
- space_implode "; "
- (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
- "\n"
-
(* string -> string *)
val unyxml = XML.content_of o YXML.parse_body
@@ -457,16 +433,6 @@
Syntax.string_of_term_global thy t ^ "\n" ^
cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
-fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
- "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
- "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
- "\" \nquickcheck\noops\n"
-
-fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
- "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
- cat_lines (map_index
- (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
-
(* subentry -> string *)
fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
timeout, error) =
--- a/src/HOL/Option.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/Option.thy Wed Feb 13 16:30:34 2013 +0100
@@ -101,6 +101,10 @@
qed
qed
+lemma option_case_map [simp]:
+ "option_case g h (Option.map f x) = option_case g (h \<circ> f) x"
+ by (cases x) simp_all
+
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
bind_lzero: "bind None f = None" |
bind_lunit: "bind (Some x) f = f x"
--- a/src/HOL/ROOT Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/ROOT Wed Feb 13 16:30:34 2013 +0100
@@ -446,7 +446,7 @@
Termination
Coherent
PresburgerEx
- ReflectionEx
+ Reflection_Examples
Sqrt
Sqrt_Script
Transfer_Ex
--- a/src/HOL/ex/IArray_Examples.thy Wed Feb 13 15:40:59 2013 +0100
+++ b/src/HOL/ex/IArray_Examples.thy Wed Feb 13 16:30:34 2013 +0100
@@ -1,5 +1,5 @@
theory IArray_Examples
-imports "~~/src/HOL/Library/IArray"
+imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Efficient_Nat"
begin
lemma "IArray [True,False] !! 1 = False"
@@ -24,3 +24,4 @@
by eval
end
+
--- a/src/HOL/ex/ReflectionEx.thy Wed Feb 13 15:40:59 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,422 +0,0 @@
-(* Title: HOL/ex/ReflectionEx.thy
- Author: Amine Chaieb, TU Muenchen
-*)
-
-header {* Examples for generic reflection and reification *}
-
-theory ReflectionEx
-imports "~~/src/HOL/Library/Reflection"
-begin
-
-text{* This theory presents two methods: reify and reflection *}
-
-text{*
-Consider an HOL type 'a, the structure of which is not recongnisable on the theory level. This is the case of bool, arithmetical terms such as int, real etc \dots
-In order to implement a simplification on terms of type 'a we often need its structure.
-Traditionnaly such simplifications are written in ML, proofs are synthesized.
-An other strategy is to declare an HOL-datatype tau and an HOL function (the interpretation) that maps elements of tau to elements of 'a. The functionality of @{text reify} is to compute a term s::tau, which is the representant of t. For this it needs equations for the interpretation.
-
-NB: All the interpretations supported by @{text reify} must have the type @{text "'b list \<Rightarrow> tau \<Rightarrow> 'a"}.
-The method @{text reify} can also be told which subterm of the current subgoal should be reified. The general call for @{text reify} is: @{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation and @{text "(t)"} is an optional parameter which specifies the subterm to which reification should be applied to. If @{text "(t)"} is abscent, @{text reify} tries to reify the whole subgoal.
-
-The method reflection uses @{text reify} and has a very similar signature: @{text "reflection corr_thm eqs (t)"}. Here again @{text eqs} and @{text "(t)"} are as described above and @{text corr_thm} is a thorem proving @{term "I vs (f t) = I vs t"}. We assume that @{text I} is the interpretation and @{text f} is some useful and executable simplification of type @{text "tau \<Rightarrow> tau"}. The method @{text reflection} applies reification and hence the theorem @{term "t = I xs s"} and hence using @{text corr_thm} derives @{term "t = I xs (f s)"}. It then uses normalization by evaluation to prove @{term "f s = s'"} which almost finishes the proof of @{term "t = t'"} where @{term "I xs s' = t'"}.
-*}
-
-text{* Example 1 : Propositional formulae and NNF.*}
-text{* The type @{text fm} represents simple propositional formulae: *}
-
-datatype form = TrueF | FalseF | Less nat nat |
- And form form | Or form form | Neg form | ExQ form
-
-fun interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool" where
-"interp TrueF e = True" |
-"interp FalseF e = False" |
-"interp (Less i j) e = (e!i < e!j)" |
-"interp (And f1 f2) e = (interp f1 e & interp f2 e)" |
-"interp (Or f1 f2) e = (interp f1 e | interp f2 e)" |
-"interp (Neg f) e = (~ interp f e)" |
-"interp (ExQ f) e = (EX x. interp f (x#e))"
-
-lemmas interp_reify_eqs = interp.simps
-declare interp_reify_eqs[reify]
-
-lemma "EX x. x < y & x < z"
- apply (reify )
- oops
-
-datatype 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 = vs!n"
-| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
-| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
-| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
-| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
-| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
-
-lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
-apply (reify Ifm.simps)
-oops
-
- text{* Method @{text reify} maps a bool to an fm. For this it needs the
- semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
-
-
- (* You can also just pick up a subterm to reify \<dots> *)
-lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
-apply (reify Ifm.simps ("((~ D) & (~ F))"))
-oops
-
- text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
-primrec fmsize :: "fm \<Rightarrow> nat" where
- "fmsize (At n) = 1"
-| "fmsize (NOT p) = 1 + fmsize p"
-| "fmsize (And p q) = 1 + fmsize p + fmsize q"
-| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
-| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
-| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
-
-lemma [measure_function]: "is_measure fmsize" ..
-
-fun nnf :: "fm \<Rightarrow> fm"
-where
- "nnf (At n) = At n"
-| "nnf (And p q) = And (nnf p) (nnf q)"
-| "nnf (Or p q) = Or (nnf p) (nnf q)"
-| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
-| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
-| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
-| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
-| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
-| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
-| "nnf (NOT (NOT p)) = nnf p"
-| "nnf (NOT p) = NOT p"
-
- text{* The correctness theorem of nnf: it preserves the semantics of fm *}
-lemma nnf[reflection]: "Ifm (nnf p) vs = Ifm p vs"
- by (induct p rule: nnf.induct) auto
-
- text{* Now let's perform NNF using our @{term nnf} function defined above. First to the whole subgoal. *}
-lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
-apply (reflection Ifm.simps)
-oops
-
- text{* Now we specify on which subterm it should be applied*}
-lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
-apply (reflection Ifm.simps only: "(B | C \<and> (B \<longrightarrow> A | D))")
-oops
-
-
- (* 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
-
-text{* This is just technical to make recursive definitions easier. *}
-primrec num_size :: "num \<Rightarrow> nat"
-where
- "num_size (C c) = 1"
-| "num_size (Var n) = 1"
-| "num_size (Add a b) = 1 + num_size a + num_size b"
-| "num_size (Mul c a) = 1 + num_size a"
-| "num_size (CN n c a) = 4 + num_size a "
-
- text{* The semantics of num *}
-primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
-where
- Inum_C : "Inum (C i) vs = i"
-| Inum_Var: "Inum (Var n) vs = vs!n"
-| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
-| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
-| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
-
-
- text{* Let's reify some nat expressions \dots *}
-lemma "4 * (2*x + (y::nat)) + f a \<noteq> 0"
- apply (reify Inum.simps ("4 * (2*x + (y::nat)) + f a"))
-oops
-text{* We're in a bad situation!! x, y and f a have been recongnized as a constants, which is correct but does not correspond to our intuition of the constructor C. It should encapsulate constants, i.e. numbers, i.e. numerals.*}
-
- text{* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
-lemma "4 * (2*x + (y::nat)) \<noteq> 0"
- apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
-oops
-text{* Hmmm let's specialize @{text Inum_C} with numerals.*}
-
-lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
-lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
-
- text{* Second attempt *}
-lemma "1 * (2*x + (y::nat)) \<noteq> 0"
- apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
-oops
- text{* That was fine, so let's try another one \dots *}
-
-lemma "1 * (2* x + (y::nat) + 0 + 1) \<noteq> 0"
- apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
-oops
- text{* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing. The same for 1. So let's add those equations too *}
-
-lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
- by simp+
-
-lemmas Inum_eqs'= Inum_eqs Inum_01
-
-text{* Third attempt: *}
-
-lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
- apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
-oops
-text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *}
-fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
-where
- "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
- (if n1=n2 then
- (let c = c1 + c2
- in (if c=0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
- else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2)))
- else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
-| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"
-| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)"
-| "lin_add (C b1) (C b2) = C (b1+b2)"
-| "lin_add a b = Add a b"
-lemma lin_add: "Inum (lin_add t s) bs = Inum (Add t s) bs"
-apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
-apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
-by (case_tac "n1 = n2", simp_all add: algebra_simps)
-
-fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
-where
- "lin_mul (C j) i = C (i*j)"
-| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
-| "lin_mul t i = (Mul i t)"
-
-lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
-by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps)
-
-lemma [measure_function]: "is_measure num_size" ..
-
-fun linum:: "num \<Rightarrow> num"
-where
- "linum (C b) = C b"
-| "linum (Var n) = CN n 1 (C 0)"
-| "linum (Add t s) = lin_add (linum t) (linum s)"
-| "linum (Mul c t) = lin_mul (linum t) c"
-| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
-
-lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
-by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
-
- text{* Now we can use linum to simplify nat terms using reflection *}
-lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
- 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 |
- Conj aform aform | Disj aform aform | NEG aform | T | F
-
-primrec linaformsize:: "aform \<Rightarrow> nat"
-where
- "linaformsize T = 1"
-| "linaformsize F = 1"
-| "linaformsize (Lt a b) = 1"
-| "linaformsize (Ge a b) = 1"
-| "linaformsize (Eq a b) = 1"
-| "linaformsize (NEq a b) = 1"
-| "linaformsize (NEG p) = 2 + linaformsize p"
-| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
-| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
-
-lemma [measure_function]: "is_measure linaformsize" ..
-
-primrec is_aform :: "aform => nat list => bool"
-where
- "is_aform T vs = True"
-| "is_aform F vs = False"
-| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
-| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
-| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
-| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
-| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
-| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
-| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
-
- text{* Let's reify and do reflection *}
-lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
- apply (reify Inum_eqs' is_aform.simps)
-oops
-
-text{* Note that reification handles several interpretations at the same time*}
-lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
- apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1")
-oops
-
- text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
-
-fun linaform:: "aform \<Rightarrow> aform"
-where
- "linaform (Lt s t) = Lt (linum s) (linum t)"
-| "linaform (Eq s t) = Eq (linum s) (linum t)"
-| "linaform (Ge s t) = Ge (linum s) (linum t)"
-| "linaform (NEq s t) = NEq (linum s) (linum t)"
-| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
-| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
-| "linaform (NEG T) = F"
-| "linaform (NEG F) = T"
-| "linaform (NEG (Lt a b)) = Ge a b"
-| "linaform (NEG (Ge a b)) = Lt a b"
-| "linaform (NEG (Eq a b)) = NEq a b"
-| "linaform (NEG (NEq a b)) = Eq a b"
-| "linaform (NEG (NEG p)) = linaform p"
-| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
-| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
-| "linaform p = p"
-
-lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
- by (induct p rule: linaform.induct) (auto simp add: linum)
-
-lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0 + Suc 0< 0)"
- apply (reflection Inum_eqs' is_aform.simps rules: linaform)
-oops
-
-declare linaform[reflection]
-lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0 + Suc 0< 0)"
- apply (reflection Inum_eqs' is_aform.simps)
-oops
-
-text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *}
-datatype rb = BC bool| BAnd rb rb | BOr rb rb
-primrec Irb :: "rb \<Rightarrow> bool"
-where
- "Irb (BC p) = p"
-| "Irb (BAnd s t) = (Irb s \<and> Irb t)"
-| "Irb (BOr s t) = (Irb s \<or> 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 | INeg rint | ISub rint rint
-primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
-where
- Irint_Var: "Irint (IVar n) vs = vs!n"
-| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
-| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
-| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
-| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
-| Irint_C: "Irint (IC i) vs = i"
-lemma Irint_C0: "Irint (IC 0) vs = 0"
- by simp
-lemma Irint_C1: "Irint (IC 1) vs = 1"
- by simp
-lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
- by simp
-lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
-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
-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"
-| "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
-| "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
-lemma "[(1::int)] = []"
- apply (reify Irlist.simps Irint_simps ("[1]:: int list"))
- oops
-
-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 | 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)"
-| Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
-| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
-| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
-| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
-| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
-| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
-| Irnat_C: "Irnat (NC i) is ls vs = i"
-lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
-by simp
-lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
-by simp
-lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
-by simp
-lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
- Irnat_C0 Irnat_C1 Irnat_Cnumeral
-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
- | 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
-
-primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
-where
- "Irifm RT ps is ls ns = True"
-| "Irifm RF ps is ls ns = False"
-| "Irifm (RVar n) ps is ls ns = ps!n"
-| "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
-| "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
-| "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
-| "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
-| "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
-| "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
-| "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
-| "Irifm (RNEX p) ps is ls ns = (\<exists>x. Irifm p ps is ls (x#ns))"
-| "Irifm (RIEX p) ps is ls ns = (\<exists>x. Irifm p ps (x#is) ls ns)"
-| "Irifm (RLEX p) ps is ls ns = (\<exists>x. Irifm p ps is (x#ls) ns)"
-| "Irifm (RBEX p) ps is ls ns = (\<exists>x. Irifm p (x#ps) is ls ns)"
-| "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
-| "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
-| "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
-| "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
-
-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)"
- apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
-oops
-
-
-(* An example for equations containing type variables *)
-datatype 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 One vs = 1"
-| "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
- | Or sgn sgn | And sgn sgn
-
-primrec Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
-where
- "Isgn Tr vs = True"
-| "Isgn F vs = False"
-| "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
-| "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
-| "Isgn (Pos t) vs = (Iprod t vs > 0)"
-| "Isgn (Neg t) vs = (Iprod t vs < 0)"
-| "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
-| "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
-
-lemmas eqs = Isgn.simps Iprod.simps
-
-lemma "(x::'a::{linordered_idom})^4 * y * z * y^2 * z^23 > 0"
- apply (reify eqs)
- oops
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Reflection_Examples.thy Wed Feb 13 16:30:34 2013 +0100
@@ -0,0 +1,488 @@
+(* Title: HOL/ex/Reflection_Ex.thy
+ Author: Amine Chaieb, TU Muenchen
+*)
+
+header {* Examples for generic reflection and reification *}
+
+theory Reflection_Examples
+imports Complex_Main "~~/src/HOL/Library/Reflection"
+begin
+
+text {* This theory presents two methods: reify and reflection *}
+
+text {*
+Consider an HOL type @{text \<sigma>}, the structure of which is not recongnisable
+on the theory level. This is the case of @{typ bool}, arithmetical terms such as @{typ int},
+@{typ real} etc \dots In order to implement a simplification on terms of type @{text \<sigma>} we
+often need its structure. Traditionnaly such simplifications are written in ML,
+proofs are synthesized.
+
+An other strategy is to declare an HOL-datatype @{text \<tau>} and an HOL function (the
+interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
+
+The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
+to compute a term @{text s} of type @{text \<tau>}. For this it needs equations for the
+interpretation.
+
+N.B: All the interpretations supported by @{text reify} must have the type
+@{text "'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>"}. The method @{text reify} can also be told which subterm
+of the current subgoal should be reified. The general call for @{text reify} is
+@{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation
+and @{text "(t)"} is an optional parameter which specifies the subterm to which reification
+should be applied to. If @{text "(t)"} is abscent, @{text reify} tries to reify the whole
+subgoal.
+
+The method @{text reflection} uses @{text reify} and has a very similar signature:
+@{text "reflection corr_thm eqs (t)"}. Here again @{text eqs} and @{text "(t)"}
+are as described above and @{text corr_thm} is a theorem proving
+@{prop "I vs (f t) = I vs t"}. We assume that @{text I} is the interpretation
+and @{text f} is some useful and executable simplification of type @{text "\<tau> \<Rightarrow> \<tau>"}.
+The method @{text reflection} applies reification and hence the theorem @{prop "t = I xs s"}
+and hence using @{text corr_thm} derives @{prop "t = I xs (f s)"}. It then uses
+normalization by equational rewriting to prove @{prop "f s = s'"} which almost finishes
+the proof of @{prop "t = t'"} where @{prop "I xs s' = t'"}.
+*}
+
+text {* Example 1 : Propositional formulae and NNF. *}
+text {* The type @{text fm} represents simple propositional formulae: *}
+
+datatype 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"
+| "interp FalseF vs \<longleftrightarrow> False"
+| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j"
+| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs"
+| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs"
+| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs"
+| "interp (ExQ f) vs \<longleftrightarrow> (\<exists>v. interp f (v # vs))"
+
+lemmas interp_reify_eqs = interp.simps
+declare interp_reify_eqs [reify]
+
+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
+
+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"
+| "Ifm (Or p q) vs \<longleftrightarrow> Ifm p vs \<or> Ifm q vs"
+| "Ifm (Imp p q) vs \<longleftrightarrow> Ifm p vs \<longrightarrow> Ifm q vs"
+| "Ifm (Iff p q) vs \<longleftrightarrow> Ifm p vs = Ifm q vs"
+| "Ifm (NOT p) vs \<longleftrightarrow> \<not> Ifm p vs"
+
+lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
+ apply (reify Ifm.simps)
+oops
+
+text {* Method @{text reify} maps a @{typ bool} to an @{typ fm}. For this it needs the
+semantics of @{text fm}, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
+
+text {* You can also just pick up a subterm to reify. *}
+lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
+ apply (reify Ifm.simps ("((\<not> D) \<and> (\<not> F))"))
+oops
+
+text {* Let's perform NNF. This is a version that tends to generate disjunctions *}
+primrec fmsize :: "fm \<Rightarrow> nat"
+where
+ "fmsize (At n) = 1"
+| "fmsize (NOT p) = 1 + fmsize p"
+| "fmsize (And p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
+| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
+| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
+
+lemma [measure_function]: "is_measure fmsize" ..
+
+fun nnf :: "fm \<Rightarrow> fm"
+where
+ "nnf (At n) = At n"
+| "nnf (And p q) = And (nnf p) (nnf q)"
+| "nnf (Or p q) = Or (nnf p) (nnf q)"
+| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
+| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
+| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
+| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
+| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
+| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
+| "nnf (NOT (NOT p)) = nnf p"
+| "nnf (NOT p) = NOT p"
+
+text {* The correctness theorem of @{const nnf}: it preserves the semantics of @{typ fm} *}
+lemma nnf [reflection]:
+ "Ifm (nnf p) vs = Ifm p vs"
+ by (induct p rule: nnf.induct) auto
+
+text {* Now let's perform NNF using our @{const nnf} function defined above. First to the
+ whole subgoal. *}
+lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
+ apply (reflection Ifm.simps)
+oops
+
+text {* Now we specify on which subterm it should be applied *}
+lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
+ apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
+ apply code_simp
+oops
+
+
+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
+
+text {* This is just technical to make recursive definitions easier. *}
+primrec num_size :: "num \<Rightarrow> nat"
+where
+ "num_size (C c) = 1"
+| "num_size (Var n) = 1"
+| "num_size (Add a b) = 1 + num_size a + num_size b"
+| "num_size (Mul c a) = 1 + num_size a"
+| "num_size (CN n c a) = 4 + num_size a "
+
+lemma [measure_function]: "is_measure num_size" ..
+
+text {* The semantics of num *}
+primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
+where
+ Inum_C : "Inum (C i) vs = i"
+| Inum_Var: "Inum (Var n) vs = vs!n"
+| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
+| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
+| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
+
+text {* Let's reify some nat expressions \dots *}
+lemma "4 * (2 * x + (y::nat)) + f a \<noteq> 0"
+ apply (reify Inum.simps ("4 * (2 * x + (y::nat)) + f a"))
+oops
+text {* We're in a bad situation! @{text x}, @{text y} and @{text f} have been recongnized
+as constants, which is correct but does not correspond to our intuition of the constructor C.
+It should encapsulate constants, i.e. numbers, i.e. numerals. *}
+
+text {* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
+lemma "4 * (2 * x + (y::nat)) \<noteq> 0"
+ apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2 * x + (y::nat))"))
+oops
+text {* Hm, let's specialize @{text Inum_C} with numerals.*}
+
+lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
+lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
+
+text {* Second attempt *}
+lemma "1 * (2 * x + (y::nat)) \<noteq> 0"
+ apply (reify Inum_eqs ("1 * (2 * x + (y::nat))"))
+oops
+
+text{* That was fine, so let's try another one \dots *}
+
+lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
+ apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
+oops
+
+text {* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing.
+The same for 1. So let's add those equations, too. *}
+
+lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
+ by simp_all
+
+lemmas Inum_eqs'= Inum_eqs Inum_01
+
+text{* Third attempt: *}
+
+lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
+ apply (reify Inum_eqs' ("1 * (2 * x + (y::nat) + 0 + 1)"))
+oops
+
+text {* Okay, let's try reflection. Some simplifications on @{typ num} follow. You can
+ skim until the main theorem @{text linum}. *}
+
+fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
+where
+ "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
+ (if n1 = n2 then
+ (let c = c1 + c2
+ in (if c = 0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
+ else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2)))
+ else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
+| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"
+| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)"
+| "lin_add (C b1) (C b2) = C (b1 + b2)"
+| "lin_add a b = Add a b"
+
+lemma lin_add:
+ "Inum (lin_add t s) bs = Inum (Add t s) bs"
+ apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
+ apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
+ apply (case_tac "n1 = n2", simp_all add: algebra_simps)
+ done
+
+fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
+where
+ "lin_mul (C j) i = C (i * j)"
+| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i * c) (lin_mul a i))"
+| "lin_mul t i = (Mul i t)"
+
+lemma lin_mul:
+ "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
+ by (induct t i rule: lin_mul.induct) (auto simp add: algebra_simps)
+
+fun linum:: "num \<Rightarrow> num"
+where
+ "linum (C b) = C b"
+| "linum (Var n) = CN n 1 (C 0)"
+| "linum (Add t s) = lin_add (linum t) (linum s)"
+| "linum (Mul c t) = lin_mul (linum t) c"
+| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
+
+lemma linum [reflection]:
+ "Inum (linum t) bs = Inum t bs"
+ by (induct t rule: linum.induct) (simp_all add: lin_mul lin_add)
+
+text {* Now we can use linum to simplify nat terms using reflection *}
+
+lemma "Suc (Suc 1) * (x + Suc 1 * y) = 3 * x + 6 * y"
+ 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 |
+ Conj aform aform | Disj aform aform | NEG aform | T | F
+
+primrec linaformsize:: "aform \<Rightarrow> nat"
+where
+ "linaformsize T = 1"
+| "linaformsize F = 1"
+| "linaformsize (Lt a b) = 1"
+| "linaformsize (Ge a b) = 1"
+| "linaformsize (Eq a b) = 1"
+| "linaformsize (NEq a b) = 1"
+| "linaformsize (NEG p) = 2 + linaformsize p"
+| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
+| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
+
+lemma [measure_function]: "is_measure linaformsize" ..
+
+primrec is_aform :: "aform => nat list => bool"
+where
+ "is_aform T vs = True"
+| "is_aform F vs = False"
+| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
+| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
+| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
+| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
+| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
+| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
+| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
+
+text{* Let's reify and do reflection *}
+lemma "(3::nat) * x + t < 0 \<and> (2 * x + y \<noteq> 17)"
+ apply (reify Inum_eqs' is_aform.simps)
+oops
+
+text {* Note that reification handles several interpretations at the same time*}
+lemma "(3::nat) * x + t < 0 \<and> x * x + t * x + 3 + 1 = z * t * 4 * z \<or> x + x + 1 < 0"
+ apply (reflection Inum_eqs' is_aform.simps only: "x + x + 1")
+oops
+
+text {* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
+
+fun linaform:: "aform \<Rightarrow> aform"
+where
+ "linaform (Lt s t) = Lt (linum s) (linum t)"
+| "linaform (Eq s t) = Eq (linum s) (linum t)"
+| "linaform (Ge s t) = Ge (linum s) (linum t)"
+| "linaform (NEq s t) = NEq (linum s) (linum t)"
+| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
+| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
+| "linaform (NEG T) = F"
+| "linaform (NEG F) = T"
+| "linaform (NEG (Lt a b)) = Ge a b"
+| "linaform (NEG (Ge a b)) = Lt a b"
+| "linaform (NEG (Eq a b)) = NEq a b"
+| "linaform (NEG (NEq a b)) = Eq a b"
+| "linaform (NEG (NEG p)) = linaform p"
+| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
+| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
+| "linaform p = p"
+
+lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
+ by (induct p rule: linaform.induct) (auto simp add: linum)
+
+lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
+ (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
+ apply (reflection Inum_eqs' is_aform.simps rules: linaform)
+oops
+
+declare linaform [reflection]
+
+lemma "(Suc (Suc (Suc 0)) * ((x::nat) + Suc (Suc 0)) + Suc (Suc (Suc 0)) *
+ (Suc (Suc (Suc 0))) * ((x::nat) + Suc (Suc 0))) < 0 \<and> Suc 0 + Suc 0 < 0"
+ apply (reflection Inum_eqs' is_aform.simps)
+oops
+
+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
+
+primrec Irb :: "rb \<Rightarrow> bool"
+where
+ "Irb (BC p) \<longleftrightarrow> p"
+| "Irb (BAnd s t) \<longleftrightarrow> Irb s \<and> Irb t"
+| "Irb (BOr s t) \<longleftrightarrow> Irb s \<or> 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
+ | INeg rint | ISub rint rint
+
+primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
+where
+ Irint_Var: "Irint (IVar n) vs = vs ! n"
+| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
+| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
+| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
+| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
+| Irint_C: "Irint (IC i) vs = i"
+
+lemma Irint_C0: "Irint (IC 0) vs = 0"
+ by simp
+
+lemma Irint_C1: "Irint (IC 1) vs = 1"
+ by simp
+
+lemma Irint_Cnumeral: "Irint (IC (numeral x)) vs = numeral x"
+ by simp
+
+lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumeral
+
+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
+
+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"
+| "Irlist (LCons i t) is vs = Irint i is # Irlist t is vs"
+| "Irlist (LAppend s t) is vs = Irlist s is vs @ Irlist t is vs"
+
+lemma "[(1::int)] = []"
+ apply (reify Irlist.simps Irint_simps ("[1] :: int list"))
+ oops
+
+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
+ | 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)"
+| Irnat_Var: "Irnat (NVar n) is ls vs = vs ! n"
+| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
+| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
+| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
+| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
+| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
+| Irnat_C: "Irnat (NC i) is ls vs = i"
+
+lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
+ by simp
+
+lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
+ by simp
+
+lemma Irnat_Cnumeral: "Irnat (NC (numeral x)) is ls vs = numeral x"
+ by simp
+
+lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth
+ Irnat_C0 Irnat_C1 Irnat_Cnumeral
+
+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
+ | 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
+
+primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
+where
+ "Irifm RT ps is ls ns \<longleftrightarrow> True"
+| "Irifm RF ps is ls ns \<longleftrightarrow> False"
+| "Irifm (RVar n) ps is ls ns \<longleftrightarrow> ps ! n"
+| "Irifm (RNLT s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns < Irnat t is ls ns"
+| "Irifm (RNILT s t) ps is ls ns \<longleftrightarrow> int (Irnat s is ls ns) < Irint t is"
+| "Irifm (RNEQ s t) ps is ls ns \<longleftrightarrow> Irnat s is ls ns = Irnat t is ls ns"
+| "Irifm (RAnd p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<and> Irifm q ps is ls ns"
+| "Irifm (ROr p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<or> Irifm q ps is ls ns"
+| "Irifm (RImp p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns"
+| "Irifm (RIff p q) ps is ls ns \<longleftrightarrow> Irifm p ps is ls ns = Irifm q ps is ls ns"
+| "Irifm (RNEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is ls (x # ns))"
+| "Irifm (RIEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps (x # is) ls ns)"
+| "Irifm (RLEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p ps is (x # ls) ns)"
+| "Irifm (RBEX p) ps is ls ns \<longleftrightarrow> (\<exists>x. Irifm p (x # ps) is ls ns)"
+| "Irifm (RNALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is ls (x#ns))"
+| "Irifm (RIALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps (x # is) ls ns)"
+| "Irifm (RLALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p ps is (x#ls) ns)"
+| "Irifm (RBALL p) ps is ls ns \<longleftrightarrow> (\<forall>x. Irifm p (x # ps) is ls ns)"
+
+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)"
+ 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
+ | Pw prod nat | PNM nat nat prod
+
+primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a"
+where
+ "Iprod Zero vs = 0"
+| "Iprod One vs = 1"
+| "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
+ | Or sgn sgn | And sgn sgn
+
+primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
+where
+ "Isgn Tr vs \<longleftrightarrow> True"
+| "Isgn F vs \<longleftrightarrow> False"
+| "Isgn (ZeroEq t) vs \<longleftrightarrow> Iprod t vs = 0"
+| "Isgn (NZeroEq t) vs \<longleftrightarrow> Iprod t vs \<noteq> 0"
+| "Isgn (Pos t) vs \<longleftrightarrow> Iprod t vs > 0"
+| "Isgn (Neg t) vs \<longleftrightarrow> Iprod t vs < 0"
+| "Isgn (And p q) vs \<longleftrightarrow> Isgn p vs \<and> Isgn q vs"
+| "Isgn (Or p q) vs \<longleftrightarrow> Isgn p vs \<or> Isgn q vs"
+
+lemmas eqs = Isgn.simps Iprod.simps
+
+lemma "(x::'a::{linordered_idom}) ^ 4 * y * z * y ^ 2 * z ^ 23 > 0"
+ apply (reify eqs)
+ oops
+
+end
+
--- a/src/Tools/Code/code_ml.ML Wed Feb 13 15:40:59 2013 +0100
+++ b/src/Tools/Code/code_ml.ML Wed Feb 13 16:30:34 2013 +0100
@@ -833,7 +833,7 @@
check = { env_var = "ISABELLE_PROCESS",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } })
+ "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
#> Code_Target.add_target
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",
--- a/src/Tools/Code/lib/Tools/codegen Wed Feb 13 15:40:59 2013 +0100
+++ b/src/Tools/Code/lib/Tools/codegen Wed Feb 13 16:30:34 2013 +0100
@@ -52,7 +52,7 @@
FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
(SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
- handle _ => Posix.Process.exit 0w1;"
+ handle _ => exit 1;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
val _ = quick_and_dirty := $QUICK_AND_DIRTY; \