--- a/NEWS Mon Jul 25 23:26:55 2011 +0200
+++ b/NEWS Mon Jul 25 23:27:20 2011 +0200
@@ -97,7 +97,10 @@
* Code generation:
- theory Library/Code_Char_ord provides native ordering of characters
in the target language.
-
+ - commands code_module and code_library are legacy, use export_code instead.
+ - evaluator "SML" and method evaluation are legacy, use evaluator "code"
+ and method eval instead.
+
* Declare ext [intro] by default. Rare INCOMPATIBILITY.
* Nitpick:
@@ -136,6 +139,8 @@
It requires that the Glasgow Haskell compiler is installed and
its location is known to Isabelle with the environment variable
ISABELLE_GHC.
+ - Removed quickcheck tester "SML" based on the SML code generator
+ from HOL-Library
* Function package: discontinued option "tailrec".
INCOMPATIBILITY. Use partial_function instead.
--- a/src/HOL/IsaMakefile Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 25 23:27:20 2011 +0200
@@ -476,7 +476,7 @@
Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \
Library/README.html \
Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
- Library/Reflection.thy Library/SML_Quickcheck.thy \
+ Library/Reflection.thy \
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
@@ -1062,7 +1062,7 @@
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
- ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy \
+ ex/Quickcheck_Narrowing_Examples.thy \
ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
--- a/src/HOL/Library/Library.thy Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Library/Library.thy Mon Jul 25 23:27:20 2011 +0200
@@ -55,7 +55,6 @@
Reflection
RBT_Mapping
Set_Algebras
- SML_Quickcheck
State_Monad
Sum_of_Squares
Transitive_Closure_Table
--- a/src/HOL/Library/SML_Quickcheck.thy Mon Jul 25 23:26:55 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-
-header {* Install quickcheck of SML code generator *}
-
-theory SML_Quickcheck
-imports Main
-begin
-
-ML {*
-signature SML_QUICKCHECK =
-sig
- val active : bool Config.T
- val setup : theory -> theory
-end;
-
-structure SML_Quickcheck : SML_QUICKCHECK =
-struct
-
-val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true);
-
-fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
- let
- val prop = list_abs_free (Term.add_frees t [], t)
- val test_fun = Codegen.test_term ctxt prop
- val iterations = Config.get ctxt Quickcheck.iterations
- fun iterate size 0 = NONE
- | iterate size j =
- let
- val result = test_fun size handle Match =>
- (if Config.get ctxt Quickcheck.quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE)
- in
- case result of NONE => iterate size (j - 1) | SOME q => SOME q
- end
- in (iterate size iterations, NONE) end
-
-val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
-
-val setup =
- Inductive_Codegen.quickcheck_setup
- #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals)))
-
-end;
-*}
-
-setup {* SML_Quickcheck.setup *}
-
-end
--- a/src/HOL/Library/reflection.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Library/reflection.ML Mon Jul 25 23:27:20 2011 +0200
@@ -305,14 +305,15 @@
in rtac th i end);
(* Reflection calls reification and uses the correctness *)
- (* theorem assumed to be the dead of the list *)
+ (* theorem assumed to be the head of the list *)
fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
let
val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *)
-fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt);
- (*FIXME why Codegen.evaluation_conv? very specific...*)
+fun reflection_tac ctxt = gen_reflection_tac ctxt
+ (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt));
+ (*FIXME why Code_Evaluation.dynamic_conv? very specific...*)
end
--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 23:27:20 2011 +0200
@@ -1155,9 +1155,14 @@
fact_lift (formula_fold NONE
(K (add_iterm_syms_to_table ctxt explicit_apply)))
+val undefined_name = make_fixed_const @{const_name undefined}
+val tvar_a = TVar (("'a", 0), HOLogic.typeS)
+
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
+ (undefined_name,
+ {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
([tptp_equal, tptp_old_equal]
@@ -1258,7 +1263,8 @@
fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
| aux arity (IConst (name as (s, _), T, T_args)) =
(case strip_prefix_and_unascii const_prefix s of
- NONE => (name, T_args)
+ NONE =>
+ (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
| SOME s'' =>
let
val s'' = invert_const s''
@@ -1649,7 +1655,7 @@
fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
let
- fun add_iterm in_conj tm =
+ fun add_iterm_syms in_conj tm =
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, s'), T, T_args) =>
@@ -1661,15 +1667,31 @@
else
I
end
- | IAbs (_, tm) => add_iterm in_conj tm
+ | IAbs (_, tm) => add_iterm_syms in_conj tm
| _ => I)
- #> fold (add_iterm in_conj) args
+ #> fold (add_iterm_syms in_conj) args
end
- fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
+ fun add_fact_syms in_conj =
+ fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
+ fun add_formula_var_types (AQuant (_, xs, phi)) =
+ fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
+ #> add_formula_var_types phi
+ | add_formula_var_types (AConn (_, phis)) =
+ fold add_formula_var_types phis
+ | add_formula_var_types _ = I
+ fun var_types () =
+ if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
+ else fold (fact_lift add_formula_var_types) (conjs @ facts) []
+ fun add_undefined_const T =
+ Symtab.map_default (undefined_name, [])
+ (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0,
+ false))
in
Symtab.empty
|> is_type_enc_fairly_sound type_enc
- ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
+ ? (fold (add_fact_syms true) conjs
+ #> fold (add_fact_syms false) facts
+ #> fold add_undefined_const (var_types ()))
end
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
@@ -1896,7 +1918,7 @@
polymorphism_of_type_enc type_enc <> Polymorphic then
nonmono_Ts
else
- [TVar (("'a", 0), HOLogic.typeS)]
+ [tvar_a]
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
--- a/src/HOL/Tools/Meson/meson.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Mon Jul 25 23:27:20 2011 +0200
@@ -14,7 +14,9 @@
val term_pair_of: indexname * (typ * 'a) -> term * 'a
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
- val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
+ val make_cnf:
+ thm list -> thm -> Proof.context
+ -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
val unfold_set_const_simps : Proof.context -> thm list
val presimplified_consts : Proof.context -> string list
@@ -26,8 +28,8 @@
val extensionalize_conv : Proof.context -> conv
val extensionalize_theorem : Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
- val make_clauses_unsorted: thm list -> thm list
- val make_clauses: thm list -> thm list
+ val make_clauses_unsorted: Proof.context -> thm list -> thm list
+ val make_clauses: Proof.context -> thm list -> thm list
val make_horns: thm list -> thm list
val best_prolog_tac: (thm -> int) -> thm list -> tactic
val depth_prolog_tac: thm list -> tactic
@@ -366,18 +368,18 @@
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using Skolemization theorems. *)
-fun cnf old_skolem_ths ctxt (th, ths) =
- let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
+fun cnf old_skolem_ths ctxt ctxt0 (th, ths) =
+ let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
- then nodups ctxt th :: ths (*no work to do, terminate*)
+ then nodups ctxt0 th :: ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
Const (@{const_name HOL.conj}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
| Const (@{const_name All}, _) => (*universal quantifier*)
- let val (th',ctxt') = freeze_spec th (!ctxtr)
- in ctxtr := ctxt'; cnf_aux (th', ths) end
+ let val (th',ctxt0') = freeze_spec th (!ctxt0r)
+ in ctxt0r := ctxt0'; cnf_aux (th', ths) end
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
@@ -388,15 +390,17 @@
Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
(fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
in Seq.list_of (tac (th RS disj_forward)) @ ths end
- | _ => nodups ctxt th :: ths (*no work to do*)
+ | _ => nodups ctxt0 th :: ths (*no work to do*)
and cnf_nil th = cnf_aux (th,[])
val cls =
- if has_too_many_clauses ctxt (concl_of th)
- then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
- else cnf_aux (th,ths)
- in (cls, !ctxtr) end;
-
-fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
+ if has_too_many_clauses ctxt (concl_of th) then
+ (trace_msg ctxt (fn () =>
+ "cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths)
+ else
+ cnf_aux (th, ths)
+ in (cls, !ctxt0r) end
+fun make_cnf old_skolem_ths th ctxt ctxt0 =
+ cnf old_skolem_ths ctxt ctxt0 (th, [])
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
@@ -657,15 +661,15 @@
Display.string_of_thm ctxt th)
| _ => ()))
-fun add_clauses th cls =
+fun add_clauses ctxt th cls =
let val ctxt0 = Variable.global_thm_context th
- val (cnfs, ctxt) = make_cnf [] th ctxt0
+ val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
in Variable.export ctxt ctxt0 cnfs @ cls end;
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
-val make_clauses = sort_clauses o make_clauses_unsorted;
+fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths [];
+val make_clauses = sort_clauses oo make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
@@ -703,12 +707,13 @@
(** Best-first search versions **)
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
-fun best_meson_tac sizef =
- MESON all_tac make_clauses
+fun best_meson_tac sizef ctxt =
+ MESON all_tac (make_clauses ctxt)
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
- (prolog_step_tac (make_horns cls) 1));
+ (prolog_step_tac (make_horns cls) 1))
+ ctxt
(*First, breaks the goal into independent units*)
fun safe_best_meson_tac ctxt =
@@ -716,10 +721,10 @@
(** Depth-first search version **)
-val depth_meson_tac =
- MESON all_tac make_clauses
- (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
-
+fun depth_meson_tac ctxt =
+ MESON all_tac (make_clauses ctxt)
+ (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
+ ctxt
(** Iterative deepening version **)
@@ -737,7 +742,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 25 23:27:20 2011 +0200
@@ -373,7 +373,7 @@
fun clausify th =
make_cnf (if new_skolemizer orelse null choice_ths then []
else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
- th ctxt
+ th ctxt ctxt
val (cnf_ths, ctxt) = clausify nnf_th
fun intr_imp ct th =
Thm.instantiate ([], map (pairself (cterm_of thy))
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jul 25 23:27:20 2011 +0200
@@ -189,9 +189,9 @@
quote (method_call_for_type_enc fallback_type_syss) ^ "...");
FOL_SOLVE fallback_type_syss ctxt cls ths0)
-val neg_clausify =
+fun neg_clausify ctxt =
single
- #> Meson.make_clauses_unsorted
+ #> Meson.make_clauses_unsorted ctxt
#> map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
@@ -217,7 +217,7 @@
verbose_warning ctxt "Proof state contains the universal sort {}"
else
();
- Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
+ Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
end
fun metis_tac [] = generic_metis_tac partial_type_syss
@@ -249,9 +249,7 @@
fun setup_method (binding, type_syss) =
((Args.parens (Scan.repeat Parse.short_ident)
- >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
- SOME tss => tss
- | NONE => [s]))
+ >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
|> Scan.option |> Scan.lift)
-- Attrib.thms >> (METHOD oo method type_syss)
|> Method.setup binding
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 23:27:20 2011 +0200
@@ -63,6 +63,7 @@
val concealedN : string
val liftingN : string
val combinatorsN : string
+ val hybridN : string
val lambdasN : string
val smartN : string
val dest_dir : string Config.T
@@ -337,6 +338,7 @@
val concealedN = "concealed"
val liftingN = "lifting"
val combinatorsN = "combinators"
+val hybridN = "hybrid"
val lambdasN = "lambdas"
val smartN = "smart"
@@ -525,12 +527,29 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt =
+fun lift_lambdas ctxt type_enc =
map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
- Lambda_Lifting.is_quantifier
+ #-> Lambda_Lifting.lift_lambdas
+ (if polymorphism_of_type_enc type_enc = Polymorphic then
+ SOME polymorphic_free_prefix
+ else
+ NONE)
+ Lambda_Lifting.is_quantifier
#> fst
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+ intentionalize_def t
+ | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let
+ fun lam T t = Abs (Name.uu, T, t)
+ val (head, args) = strip_comb t ||> rev
+ val head_T = fastype_of head
+ val n = length args
+ val arg_Ts = head_T |> binder_types |> take n |> rev
+ val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+ in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+ | intentionalize_def t = t
+
fun translate_atp_lambdas ctxt type_enc =
Config.get ctxt atp_lambda_translation
|> (fn trans =>
@@ -544,11 +563,15 @@
trans)
|> (fn trans =>
if trans = concealedN then
- lift_lambdas ctxt ##> K []
+ lift_lambdas ctxt type_enc ##> K []
else if trans = liftingN then
- lift_lambdas ctxt
+ lift_lambdas ctxt type_enc
else if trans = combinatorsN then
map (introduce_combinators ctxt) #> rpair []
+ else if trans = hybridN then
+ lift_lambdas ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt
+ (intentionalize_def t)])
else if trans = lambdasN then
map (Envir.eta_contract) #> rpair []
else
--- a/src/HOL/ex/Meson_Test.thy Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/ex/Meson_Test.thy Mon Jul 25 23:27:20 2011 +0200
@@ -10,7 +10,7 @@
below and constants declared in HOL!
*}
-hide_const (open) implies union inter subset sum quotient
+hide_const (open) implies union inter subset sum quotient
text {*
Test data for the MESON proof procedure
@@ -31,7 +31,7 @@
apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses25 = Meson.make_clauses [sko25]; (*7 clauses*)
+ val clauses25 = Meson.make_clauses @{context} [sko25]; (*7 clauses*)
val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*)
val go25 :: _ = Meson.gocls clauses25;
@@ -52,7 +52,7 @@
apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses26 = Meson.make_clauses [sko26]; (*9 clauses*)
+ val clauses26 = Meson.make_clauses @{context} [sko26]; (*9 clauses*)
val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*)
val go26 :: _ = Meson.gocls clauses26;
@@ -74,7 +74,7 @@
apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *})
ML_val {*
val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses43 = Meson.make_clauses [sko43]; (*6*)
+ val clauses43 = Meson.make_clauses @{context} [sko43]; (*6*)
val horns43 = Meson.make_horns clauses43; (*16*)
val go43 :: _ = Meson.gocls clauses43;
--- a/src/HOL/ex/ROOT.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Jul 25 23:27:20 2011 +0200
@@ -64,7 +64,6 @@
"HarmonicSeries",
"Refute_Examples",
"Quickcheck_Examples",
- "SML_Quickcheck_Examples",
"Quickcheck_Lattice_Examples",
"Landau",
"Execute_Choice",
--- a/src/HOL/ex/SML_Quickcheck_Examples.thy Mon Jul 25 23:26:55 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(* Title: HOL/ex/SML_Quickcheck_Examples.thy
- Author: Stefan Berghofer, Lukas Bulwahn
- Copyright 2011 TU Muenchen
-*)
-
-theory SML_Quickcheck_Examples
-imports "~~/src/HOL/Library/SML_Quickcheck"
-begin
-
-text {*
-This is a regression test for the 'quickcheck' counterexample generator based on the
-SML code generator.
-
-The counterexample generator has been superseded by counterexample generators based on
-the generic code generator.
-*}
-
-declare [[quickcheck_finite_types = false]]
-declare [[quickcheck_timeout = 600.0]]
-
-subsection {* Lists *}
-
-theorem "map g (map f xs) = map (g o f) xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "map g (map f xs) = map (f o g) xs"
- quickcheck[SML, expect = counterexample]
- oops
-
-theorem "rev (xs @ ys) = rev ys @ rev xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "rev (xs @ ys) = rev xs @ rev ys"
- quickcheck[SML, expect = counterexample]
- oops
-
-theorem "rev (rev xs) = xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "rev xs = xs"
- quickcheck[tester = SML, expect = counterexample]
-oops
-
-
-text {* An example involving functions inside other data structures *}
-
-primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
- "app [] x = x"
- | "app (f # fs) x = app fs (f x)"
-
-lemma "app (fs @ gs) x = app gs (app fs x)"
- quickcheck[SML, expect = no_counterexample]
- by (induct fs arbitrary: x) simp_all
-
-lemma "app (fs @ gs) x = app fs (app gs x)"
- quickcheck[SML, expect = counterexample]
- oops
-
-primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
- "occurs a [] = 0"
- | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
-
-primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "del1 a [] = []"
- | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
-
-text {* A lemma, you'd think to be true from our experience with delAll *}
-lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
- -- {* Wrong. Precondition needed.*}
- quickcheck[SML, expect = counterexample]
- oops
-
-lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[SML, expect = counterexample]
- -- {* Also wrong.*}
- oops
-
-lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[SML, expect = no_counterexample]
- by (induct xs) auto
-
-primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "replace a b [] = []"
- | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
- else (x#(replace a b xs)))"
-
-lemma "occurs a xs = occurs b (replace a b xs)"
- quickcheck[SML, expect = counterexample]
- -- {* Wrong. Precondition needed.*}
- oops
-
-lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
- quickcheck[SML, expect = no_counterexample]
- by (induct xs) simp_all
-
-
-subsection {* Trees *}
-
-datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
-
-primrec leaves :: "'a tree \<Rightarrow> 'a list" where
- "leaves Twig = []"
- | "leaves (Leaf a) = [a]"
- | "leaves (Branch l r) = (leaves l) @ (leaves r)"
-
-primrec plant :: "'a list \<Rightarrow> 'a tree" where
- "plant [] = Twig "
- | "plant (x#xs) = Branch (Leaf x) (plant xs)"
-
-primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
- "mirror (Twig) = Twig "
- | "mirror (Leaf a) = Leaf a "
- | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
-
-theorem "plant (rev (leaves xt)) = mirror xt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
-
-primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
- "inOrder (Tip a)= [a]"
- | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
-
-primrec root :: "'a ntree \<Rightarrow> 'a" where
- "root (Tip a) = a"
- | "root (Node f x y) = f"
-
-theorem "hd (inOrder xt) = root xt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-end
--- a/src/Pure/codegen.ML Mon Jul 25 23:26:55 2011 +0200
+++ b/src/Pure/codegen.ML Mon Jul 25 23:27:20 2011 +0200
@@ -916,6 +916,7 @@
fun eval_term ctxt t =
let
+ val _ = legacy_feature "Old evaluation mechanism -- use evaluator 'code' or method eval instead";
val thy = Proof_Context.theory_of ctxt;
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
error "Term to be evaluated contains type variables";
@@ -1012,6 +1013,7 @@
|| Scan.repeat1 (Parse.term >> pair "")) >>
(fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
let
+ val _ = legacy_feature "Old code generation command -- use export_code instead";
val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
val (code, gr) = generate_code thy mode' modules module xs;
val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>