--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 11:45:09 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 13:48:15 2010 +0100
@@ -20,14 +20,15 @@
| comb_option f (SOME x1, NONE) = SOME x1
| comb_option f (NONE, NONE) = NONE
-fun map2_optional f (x :: xs) (y :: ys) = (f x (SOME y)) :: (map2_optional f xs ys)
+fun map2_optional f (x :: xs) (y :: ys) = f x (SOME y) :: (map2_optional f xs ys)
| map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs [])
| map2_optional f [] [] = []
fun find_indices f xs =
map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
-fun assert check = if check then () else error "Assertion failed!"
+fun assert check = if check then () else raise Fail "Assertion failed!"
+
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
@@ -48,7 +49,7 @@
(* name: binder_modes? *)
fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
| strip_fun_mode Bool = []
- | strip_fun_mode _ = error "Bad mode for strip_fun_mode"
+ | strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode"
fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
| dest_fun_mode mode = [mode]
@@ -67,51 +68,36 @@
else
[Input, Output]
end
- | all_modes_of_typ' (Type ("*", [T1, T2])) =
+ | all_modes_of_typ' (Type (@{type_name "*"}, [T1, T2])) =
map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
| all_modes_of_typ' _ = [Input, Output]
fun all_modes_of_typ (T as Type ("fun", _)) =
- let
- val (S, U) = strip_type T
- in
- if U = HOLogic.boolT then
- fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
- (map all_modes_of_typ' S) [Bool]
- else
- [Input, Output]
- end
- | all_modes_of_typ (Type ("bool", [])) = [Bool]
+ let
+ val (S, U) = strip_type T
+ in
+ if U = @{typ bool} then
+ fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
+ (map all_modes_of_typ' S) [Bool]
+ else
+ [Input, Output]
+ end
+ | all_modes_of_typ @{typ bool} = [Bool]
| all_modes_of_typ T = all_modes_of_typ' T
fun all_smodes_of_typ (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
- fun all_smodes (Type ("*", [T1, T2])) =
+ fun all_smodes (Type (@{type_name "*"}, [T1, T2])) =
map_product (curry Pair) (all_smodes T1) (all_smodes T2)
| all_smodes _ = [Input, Output]
in
if U = HOLogic.boolT then
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
else
- error "all_smodes_of_typ: invalid type for predicate"
+ raise Fail "all_smodes_of_typ: invalid type for predicate"
end
-(*
-fun extract_params arg =
- case fastype_of arg of
- (T as Type ("fun", _)) =>
- (if (body_type T = HOLogic.boolT) then
- (case arg of
- Free _ => [arg] | _ => error "extract_params: Unexpected term")
- else [])
- | (Type ("*", [T1, T2])) =>
- let
- val (t1, t2) = HOLogic.dest_prod arg
- in
- extract_params t1 @ extract_params t2
- end
- | _ => []
-*)
+
fun ho_arg_modes_of mode =
let
fun ho_arg_mode (m as Fun _) = [m]
@@ -125,7 +111,7 @@
let
fun ho_arg (Fun _) (SOME t) = [t]
| ho_arg (Fun _) NONE = error "ho_arg_of"
- | ho_arg (Pair (m1, m2)) (SOME (Const ("Pair", _) $ t1 $ t2)) =
+ | ho_arg (Pair (m1, m2)) (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2)
| ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE
| ho_arg _ _ = []
@@ -146,13 +132,13 @@
end
| replace (_, t) hoargs = (t, hoargs)
in
- fst (fold_map replace ((strip_fun_mode mode) ~~ ts) hoargs)
+ fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs)
end
fun ho_argsT_of mode Ts =
let
fun ho_arg (Fun _) T = [T]
- | ho_arg (Pair (m1, m2)) (Type ("*", [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
+ | ho_arg (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
| ho_arg _ _ = []
in
flat (map2 ho_arg (strip_fun_mode mode) Ts)
@@ -172,7 +158,7 @@
| split_arg_mode' m t =
if eq_mode (m, Input) then (SOME t, NONE)
else if eq_mode (m, Output) then (NONE, SOME t)
- else error "split_map_mode: mode and term do not match"
+ else raise Fail "split_map_mode: mode and term do not match"
in
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
end
@@ -181,7 +167,7 @@
fun split_map_modeT f mode Ts =
let
fun split_arg_mode' (m as Fun _) T = f m T
- | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) =
+ | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
let
val (i1, o1) = split_arg_mode' m1 T1
val (i2, o2) = split_arg_mode' m2 T2
@@ -190,14 +176,14 @@
end
| split_arg_mode' Input T = (SOME T, NONE)
| split_arg_mode' Output T = (NONE, SOME T)
- | split_arg_mode' _ _ = error "split_modeT': mode and type do not match"
+ | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
in
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
end
fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
-fun fold_map_aterms_prodT comb f (Type ("*", [T1, T2])) s =
+fun fold_map_aterms_prodT comb f (Type (@{type_name "*"}, [T1, T2])) s =
let
val (x1, s') = fold_map_aterms_prodT comb f T1 s
val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
@@ -215,7 +201,7 @@
fun split_modeT' mode Ts =
let
fun split_arg_mode' (Fun _) T = ([], [])
- | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) =
+ | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
let
val (i1, o1) = split_arg_mode' m1 T1
val (i2, o2) = split_arg_mode' m2 T2
@@ -224,7 +210,7 @@
end
| split_arg_mode' Input T = ([T], [])
| split_arg_mode' Output T = ([], [T])
- | split_arg_mode' _ _ = error "split_modeT': mode and type do not match"
+ | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
in
(pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
end
@@ -296,7 +282,7 @@
val T = (Sign.the_const_type thy constname)
in body_type T = @{typ "bool"} end;
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
+fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
| is_predT _ = false
(*** check if a term contains only constructor functions ***)
@@ -339,7 +325,7 @@
else false
*)
-val is_constr = Code.is_constr;
+val is_constr = Code.is_constr o ProofContext.theory_of;
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
let
@@ -366,7 +352,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t = (case t of
- (@{term "Not"} $ t') => HOLogic.mk_not (f t')
+ (@{term Not} $ t') => HOLogic.mk_not (f t')
| _ => f t)
in
Logic.list_implies
@@ -377,7 +363,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t s = (case t of
- (@{term "Not"} $ t') => f t' s
+ (@{term Not} $ t') => f t' s
| _ => f t s)
in fold appl (map HOLogic.dest_Trueprop literals) s end
@@ -385,7 +371,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t s = (case t of
- (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
+ (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
| _ => f t s)
val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
in
@@ -399,6 +385,18 @@
Logic.list_implies (maps f premises, head)
end
+fun map_concl f intro =
+ let
+ val (premises, head) = Logic.strip_horn intro
+ in
+ Logic.list_implies (premises, f head)
+ end
+
+(* combinators to apply a function to all basic parts of nested products *)
+
+fun map_products f (Const ("Pair", T) $ t1 $ t2) =
+ Const ("Pair", T) $ map_products f t1 $ map_products f t2
+ | map_products f t = f t
(* split theorems of case expressions *)
@@ -466,7 +464,7 @@
(* Different options for compiler *)
-datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated
+datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
| Pos_Random_DSeq | Neg_Random_DSeq
@@ -477,10 +475,12 @@
fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
| compilation_for_polarity _ c = c
-fun string_of_compilation c = case c of
+fun string_of_compilation c =
+ case c of
Pred => ""
| Random => "random"
| Depth_Limited => "depth limited"
+ | Depth_Limited_Random => "depth limited random"
| DSeq => "dseq"
| Annotated => "annotated"
| Pos_Random_DSeq => "pos_random dseq"
@@ -558,7 +558,10 @@
"no_topmost_reordering"]
val compilation_names = [("pred", Pred),
- (*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*)
+ ("random", Random),
+ ("depth_limited", Depth_Limited),
+ ("depth_limited_random", Depth_Limited_Random),
+ (*("annotated", Annotated),*)
("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
fun print_step options s =
@@ -573,9 +576,9 @@
(case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
let
- fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
+ fun rewrite_arg' (Const (@{const_name "Pair"}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
- | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
+ | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
let
val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
@@ -619,4 +622,15 @@
intro'''''
end
+(* eta contract higher-order arguments *)
+
+
+fun eta_contract_ho_arguments thy intro =
+ let
+ fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))
+ in
+ map_term thy (map_concl f o map_atoms f) intro
+ end
+
+
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 11:45:09 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 13:48:15 2010 +0100
@@ -17,8 +17,8 @@
val is_registered : theory -> string -> bool
val function_name_of : Predicate_Compile_Aux.compilation -> theory
-> string -> bool * Predicate_Compile_Aux.mode -> string
- val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
- val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
+ val predfun_intro_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
+ val predfun_elim_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
val all_preds_of : theory -> string list
val modes_of: Predicate_Compile_Aux.compilation
-> theory -> string -> Predicate_Compile_Aux.mode list
@@ -72,19 +72,15 @@
(* debug stuff *)
-fun print_tac s = Seq.single;
-
-fun print_tac' options s =
+fun print_tac options s =
if show_proof_trace options then Tactical.print_tac s else Seq.single;
-fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
-
-fun assert b = if not b then error "Assertion failed" else warning "Assertion holds"
+fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
datatype assertion = Max_number_of_subgoals of int
fun assert_tac (Max_number_of_subgoals i) st =
if (nprems_of st <= i) then Seq.single st
- else error ("assert_tac: Numbers of subgoals mismatch at goal state :"
+ else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
^ "\n" ^ Pretty.string_of (Pretty.chunks
(Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
@@ -153,8 +149,8 @@
| mode_of (Term m) = m
| mode_of (Mode_App (d1, d2)) =
(case mode_of d1 of Fun (m, m') =>
- (if eq_mode (m, mode_of d2) then m' else error "mode_of")
- | _ => error "mode_of2")
+ (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of")
+ | _ => raise Fail "mode_of2")
| mode_of (Mode_Pair (d1, d2)) =
Pair (mode_of d1, mode_of d2)
@@ -189,13 +185,14 @@
datatype predfun_data = PredfunData of {
definition : thm,
intro : thm,
- elim : thm
+ elim : thm,
+ neg_intro : thm option
};
fun rep_predfun_data (PredfunData data) = data;
-fun mk_predfun_data (definition, intro, elim) =
- PredfunData {definition = definition, intro = intro, elim = elim}
+fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
+ PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
datatype pred_data = PredData of {
intros : thm list,
@@ -207,20 +204,20 @@
fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim), (function_names, predfun_data, needs_random)) =
+fun mk_pred_data ((intros, elim), (function_names, (predfun_data, needs_random))) =
PredData {intros = intros, elim = elim,
function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) =
- mk_pred_data (f ((intros, elim), (function_names, predfun_data, needs_random)))
+ mk_pred_data (f ((intros, elim), (function_names, (predfun_data, needs_random))))
fun eq_option eq (NONE, NONE) = true
| eq_option eq (SOME x, SOME y) = eq (x, y)
| eq_option eq _ = false
fun eq_pred_data (PredData d1, PredData d2) =
- eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
- eq_option (Thm.eq_thm) (#elim d1, #elim d2)
+ eq_list Thm.eq_thm (#intros d1, #intros d2) andalso
+ eq_option Thm.eq_thm (#elim d1, #elim d2)
structure PredData = Theory_Data
(
@@ -247,7 +244,7 @@
fun the_elim_of thy name = case #elim (the_pred_data thy name)
of NONE => error ("No elimination rule for predicate " ^ quote name)
- | SOME thm => Thm.transfer thy thm
+ | SOME thm => Thm.transfer thy thm
val has_elim = is_some o #elim oo the_pred_data;
@@ -285,11 +282,13 @@
" of predicate " ^ name)
| SOME data => data;
-val predfun_definition_of = #definition ooo the_predfun_data
+val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of
+
+val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of
-val predfun_intro_of = #intro ooo the_predfun_data
+val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of
-val predfun_elim_of = #elim ooo the_predfun_data
+val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of
(* diagnostic display functions *)
@@ -315,7 +314,7 @@
(Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)"
| string_of_prem thy (Sidecond t) =
(Syntax.string_of_term_global thy t) ^ "(sidecondition)"
- | string_of_prem thy _ = error "string_of_prem: unexpected input"
+ | string_of_prem thy _ = raise Fail "string_of_prem: unexpected input"
fun string_of_clause thy pred (ts, prems) =
(space_implode " --> "
@@ -446,7 +445,7 @@
let
val (pred', _) = strip_intro_concl th
val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
- error "Trying to instantiate another predicate" else ()
+ raise Fail "Trying to instantiate another predicate" else ()
in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
fun instantiate_ho_args th =
let
@@ -470,7 +469,7 @@
in
(HOLogic.mk_prod (t1, t2), st'')
end
- | mk_args2 (T as Type ("fun", _)) (params, ctxt) =
+ (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
let
val (S, U) = strip_type T
in
@@ -482,36 +481,80 @@
in
(Free (x, T), (params, ctxt'))
end
- end
+ end*)
| mk_args2 T (params, ctxt) =
let
val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
in
(Free (x, T), (params, ctxt'))
end
-
+
fun mk_casesrule ctxt pred introrules =
let
+ (* TODO: can be simplified if parameters are not treated specially ? *)
val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
+ (* TODO: distinct required ? -- test case with more than one parameter! *)
+ val params = distinct (op aconv) params
val intros = map prop_of intros_th
val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
val argsT = binder_types (fastype_of pred)
+ (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
fun mk_case intro =
let
val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
val prems = Logic.strip_imp_prems intro
- val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
- val frees = (fold o fold_aterms)
- (fn t as Free _ =>
- if member (op aconv) params t then I else insert (op aconv) t
- | _ => I) (args @ prems) []
+ val eqprems =
+ map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
+ val frees = map Free (fold Term.add_frees (args @ prems) [])
in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
val cases = map mk_case intros
in Logic.list_implies (assm :: cases, prop) end;
+fun dest_conjunct_prem th =
+ case HOLogic.dest_Trueprop (prop_of th) of
+ (Const ("op &", _) $ t $ t') =>
+ dest_conjunct_prem (th RS @{thm conjunct1})
+ @ dest_conjunct_prem (th RS @{thm conjunct2})
+ | _ => [th]
+
+fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val nargs = length (binder_types (fastype_of pred))
+ fun PEEK f dependent_tactic st = dependent_tactic (f st) st
+ fun meta_eq_of th = th RS @{thm eq_reflection}
+ val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
+ fun instantiate i n {context = ctxt, params = p, prems = prems,
+ asms = a, concl = cl, schematics = s} =
+ let
+ val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
+ val case_th = MetaSimplifier.simplify true
+ (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs)
+ (nth cases (i - 1))
+ val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
+ val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
+ val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty)
+ fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
+ val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
+ val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems'
+ in
+ (rtac thesis 1)
+ end
+ val tac =
+ etac pre_cases_rule 1
+ THEN
+ (PEEK nprems_of
+ (fn n =>
+ ALLGOALS (fn i =>
+ MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+ THEN (SUBPROOF (instantiate i n) ctxt i))))
+ in
+ Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
+ end
+
(** preprocessing rules **)
fun imp_prems_conv cv ct =
@@ -522,7 +565,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
- | _ => error "Trueprop_conv"
+ | _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
Conv.fconv_rule
@@ -552,7 +595,7 @@
val bigeq = (Thm.symmetric (Conv.implies_concl_conv
(MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
(cterm_of thy elimrule')))
- val tac = (fn _ => Skip_Proof.cheat_tac thy)
+ val tac = (fn _ => Skip_Proof.cheat_tac thy)
val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
in
Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
@@ -560,7 +603,7 @@
fun expand_tuples_elim th = th
-val no_compilation = ([], [], [])
+val no_compilation = ([], ([], []))
fun fetch_pred_data thy name =
case try (Inductive.the_inductive (ProofContext.init thy)) name of
@@ -575,11 +618,11 @@
val index = find_index (fn s => s = name) (#names (fst info))
val pre_elim = nth (#elims result) index
val pred = nth (#preds result) index
- (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams
- (expand_tuples_elim pre_elim))*)
+ val nparams = length (Inductive.params_of (#raw_induct result))
+ val ctxt = ProofContext.init thy
+ val elim_t = mk_casesrule ctxt pred intros
val elim =
- (Drule.export_without_context o Skip_Proof.make_thm thy)
- (mk_casesrule (ProofContext.init thy) pred intros)
+ prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
in
mk_pred_data ((intros, SOME elim), no_compilation)
end
@@ -587,7 +630,7 @@
fun add_predfun_data name mode data =
let
- val add = (apsnd o apsnd3) (cons (mode, mk_predfun_data data))
+ val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
in PredData.map (Graph.map_node name (map_pred_data add)) end
fun is_inductive_predicate thy name =
@@ -648,14 +691,14 @@
fun defined_function_of compilation pred =
let
- val set = (apsnd o apfst3) (cons (compilation, []))
+ val set = (apsnd o apfst) (cons (compilation, []))
in
PredData.map (Graph.map_node pred (map_pred_data set))
end
fun set_function_name compilation pred mode name =
let
- val set = (apsnd o apfst3)
+ val set = (apsnd o apfst)
(AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
in
PredData.map (Graph.map_node pred (map_pred_data set))
@@ -663,7 +706,7 @@
fun set_needs_random name modes =
let
- val set = (apsnd o aptrd3) (K modes)
+ val set = (apsnd o apsnd o apsnd) (K modes)
in
PredData.map (Graph.map_node name (map_pred_data set))
end
@@ -717,7 +760,9 @@
fun mk_if cond = Const (@{const_name Predicate.if_pred},
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_predT HOLogic.unitT
+fun mk_not t =
+ let
+ val T = mk_predT HOLogic.unitT
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
fun mk_Enum f =
@@ -775,7 +820,9 @@
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_randompredT HOLogic.unitT
+fun mk_not t =
+ let
+ val T = mk_randompredT HOLogic.unitT
in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
@@ -791,33 +838,33 @@
struct
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])) = T
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
| dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
-fun mk_bot T = Const ("DSequence.empty", mk_dseqT T);
+fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
fun mk_single t =
let val T = fastype_of t
- in Const("DSequence.single", T --> mk_dseqT T) $ t end;
+ in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
in
- Const ("DSequence.bind", fastype_of x --> T --> U) $ x $ f
+ Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_sup = HOLogic.mk_binop "DSequence.union";
+val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
-fun mk_if cond = Const ("DSequence.if_seq",
+fun mk_if cond = Const (@{const_name DSequence.if_seq},
HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
fun mk_not t = let val T = mk_dseqT HOLogic.unitT
- in Const ("DSequence.not_seq", T --> T) $ t end
+ in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-fun mk_map T1 T2 tf tp = Const ("DSequence.map",
+fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
(T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
@@ -838,28 +885,31 @@
Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
| dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
-fun mk_bot T = Const ("Random_Sequence.empty", mk_random_dseqT T);
+fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
fun mk_single t =
- let val T = fastype_of t
- in Const("Random_Sequence.single", T --> mk_random_dseqT T) $ t end;
+ let
+ val T = fastype_of t
+ in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
- Const ("Random_Sequence.bind", fastype_of x --> T --> U) $ x $ f
+ Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_sup = HOLogic.mk_binop "Random_Sequence.union";
+val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
-fun mk_if cond = Const ("Random_Sequence.if_random_dseq",
+fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_random_dseqT HOLogic.unitT
- in Const ("Random_Sequence.not_random_dseq", T --> T) $ t end
+fun mk_not t =
+ let
+ val T = mk_random_dseqT HOLogic.unitT
+ in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
-fun mk_map T1 T2 tf tp = Const ("Random_Sequence.map",
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
(T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
@@ -868,19 +918,6 @@
end;
-
-
-fun mk_random T =
- let
- val random = Const ("Quickcheck.random_class.random",
- @{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
- in
- Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
- Random_Sequence_CompFuns.mk_random_dseqT T) $ random
- end;
-
(* for external use with interactive mode *)
val pred_compfuns = PredicateCompFuns.compfuns
val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
@@ -945,8 +982,8 @@
else ()
fun error_of p (pol, m) is =
- (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m)
+ " Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode m
fun is_all_input mode =
let
@@ -967,7 +1004,7 @@
if U = HOLogic.boolT then
fold_rev (curry Fun) (map input_of Ts) Bool
else
- error "all_input_of: not a predicate"
+ raise Fail "all_input_of: not a predicate"
end
fun partial_hd [] = NONE
@@ -990,24 +1027,27 @@
fold_rev (curry Fun) (map (K Output) Ts) Output
end
-fun is_invertible_function thy (Const (f, _)) = is_constr thy f
- | is_invertible_function thy _ = false
+fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
+ | is_invertible_function ctxt _ = false
-fun non_invertible_subterms thy (t as Free _) = []
- | non_invertible_subterms thy t =
- case (strip_comb t) of (f, args) =>
- if is_invertible_function thy f then
- maps (non_invertible_subterms thy) args
+fun non_invertible_subterms ctxt (t as Free _) = []
+ | non_invertible_subterms ctxt t =
+ let
+ val (f, args) = strip_comb t
+ in
+ if is_invertible_function ctxt f then
+ maps (non_invertible_subterms ctxt) args
else
[t]
+ end
-fun collect_non_invertible_subterms thy (f as Free _) (names, eqs) = (f, (names, eqs))
- | collect_non_invertible_subterms thy t (names, eqs) =
+fun collect_non_invertible_subterms ctxt (f as Free _) (names, eqs) = (f, (names, eqs))
+ | collect_non_invertible_subterms ctxt t (names, eqs) =
case (strip_comb t) of (f, args) =>
- if is_invertible_function thy f then
+ if is_invertible_function ctxt f then
let
val (args', (names', eqs')) =
- fold_map (collect_non_invertible_subterms thy) args (names, eqs)
+ fold_map (collect_non_invertible_subterms ctxt) args (names, eqs)
in
(list_comb (f, args'), (names', eqs'))
end
@@ -1029,18 +1069,21 @@
fun is_possible_output thy vs t =
forall
(fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
- (non_invertible_subterms thy t)
+ (non_invertible_subterms (ProofContext.init thy) t)
andalso
(forall (is_eqT o snd)
(inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
-fun vars_of_destructable_term thy (Free (x, _)) = [x]
- | vars_of_destructable_term thy t =
- case (strip_comb t) of (f, args) =>
- if is_invertible_function thy f then
- maps (vars_of_destructable_term thy) args
+fun vars_of_destructable_term ctxt (Free (x, _)) = [x]
+ | vars_of_destructable_term ctxt t =
+ let
+ val (f, args) = strip_comb t
+ in
+ if is_invertible_function ctxt f then
+ maps (vars_of_destructable_term ctxt) args
else
[]
+ end
fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t)
@@ -1062,7 +1105,7 @@
SOME ms => SOME (map (fn m => (Context m , [])) ms)
| NONE => NONE)
-fun derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
+fun derivations_of (thy : theory) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
map_product
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
(derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2)
@@ -1109,11 +1152,11 @@
case mode_of d1 of
Fun (m', _) => map (fn (d2, mvars2) =>
(Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
- | _ => error "Something went wrong") derivs1
+ | _ => raise Fail "Something went wrong") derivs1
end
| all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
| all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
- | all_derivations_of _ modes vs _ = error "all_derivations_of"
+ | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of"
fun rev_option_ord ord (NONE, NONE) = EQUAL
| rev_option_ord ord (NONE, SOME _) = GREATER
@@ -1178,7 +1221,7 @@
tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
-fun select_mode_prem (mode_analysis_options : mode_analysis_options) thy pol (modes, (pos_modes, neg_modes)) vs ps =
+fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pol (modes, (pos_modes, neg_modes)) vs ps =
let
fun choose_mode_of_prem (Prem t) = partial_hd
(sort (deriv_ord2 thy modes t) (all_derivations_of thy pos_modes vs t))
@@ -1186,7 +1229,7 @@
| choose_mode_of_prem (Negprem t) = partial_hd
(sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
(all_derivations_of thy neg_modes vs t)))
- | choose_mode_of_prem p = error ("choose_mode_of_prem: " ^ string_of_prem thy p)
+ | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
in
if #reorder_premises mode_analysis_options then
partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps))
@@ -1209,13 +1252,13 @@
val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
in (modes, modes) end
val (in_ts, out_ts) = split_mode mode ts
- val in_vs = maps (vars_of_destructable_term thy) in_ts
+ val in_vs = maps (vars_of_destructable_term (ProofContext.init thy)) in_ts
val out_vs = terms_vs out_ts
fun known_vs_after p vs = (case p of
Prem t => union (op =) vs (term_vs t)
| Sidecond t => union (op =) vs (term_vs t)
| Negprem t => union (op =) vs (term_vs t)
- | _ => error "I do not know")
+ | _ => raise Fail "I do not know")
fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
| check_mode_prems acc_ps rnd vs ps =
(case
@@ -1447,6 +1490,8 @@
compilation : compilation,
function_name_prefix : string,
compfuns : compilation_funs,
+ mk_random : typ -> term list -> term,
+ modify_funT : typ -> typ,
additional_arguments : string list -> term list,
wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
transform_additional_arguments : indprem -> term list -> term list
@@ -1457,7 +1502,12 @@
val compilation = #compilation o dest_comp_modifiers
val function_name_prefix = #function_name_prefix o dest_comp_modifiers
val compfuns = #compfuns o dest_comp_modifiers
-val funT_of = funT_of o compfuns
+
+val mk_random = #mk_random o dest_comp_modifiers
+val funT_of' = funT_of o compfuns
+val modify_funT = #modify_funT o dest_comp_modifiers
+fun funT_of comp mode = modify_funT comp o funT_of' comp mode
+
val additional_arguments = #additional_arguments o dest_comp_modifiers
val wrap_compilation = #wrap_compilation o dest_comp_modifiers
val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
@@ -1465,7 +1515,7 @@
end;
(* TODO: uses param_vs -- change necessary for compilation with new modes *)
-fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg =
+fun compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss arg =
let
fun map_params (t as Free (f, T)) =
if member (op =) param_vs f then
@@ -1481,11 +1531,11 @@
in map_aterms map_params arg end
fun compile_match compilation_modifiers compfuns additional_arguments
- param_vs iss thy eqs eqs' out_ts success_t =
+ param_vs iss ctxt eqs eqs' out_ts success_t =
let
val eqs'' = maps mk_eq eqs @ eqs'
val eqs'' =
- map (compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss) eqs''
+ map (compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss) eqs''
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
val name = Name.variant names "x";
val name' = Name.variant (name :: names) "y";
@@ -1495,8 +1545,7 @@
val v = Free (name, T);
val v' = Free (name', T);
in
- lambda v (fst (Datatype.make_case
- (ProofContext.init thy) Datatype_Case.Quiet [] v
+ lambda v (fst (Datatype.make_case ctxt Datatype_Case.Quiet [] v
[(HOLogic.mk_tuple out_ts,
if null eqs'' then success_t
else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
@@ -1505,25 +1554,25 @@
(v', mk_bot compfuns U')]))
end;
-fun string_of_tderiv thy (t, deriv) =
+fun string_of_tderiv ctxt (t, deriv) =
(case (t, deriv) of
(t1 $ t2, Mode_App (deriv1, deriv2)) =>
- string_of_tderiv thy (t1, deriv1) ^ " $ " ^ string_of_tderiv thy (t2, deriv2)
+ string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
| (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
- "(" ^ string_of_tderiv thy (t1, deriv1) ^ ", " ^ string_of_tderiv thy (t2, deriv2) ^ ")"
- | (t, Term Input) => Syntax.string_of_term_global thy t ^ "[Input]"
- | (t, Term Output) => Syntax.string_of_term_global thy t ^ "[Output]"
- | (t, Context m) => Syntax.string_of_term_global thy t ^ "[" ^ string_of_mode m ^ "]")
+ "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
+ | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
+ | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
+ | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
-fun compile_expr compilation_modifiers compfuns thy pol (t, deriv) additional_arguments =
+fun compile_expr compilation_modifiers compfuns ctxt pol (t, deriv) additional_arguments =
let
fun expr_of (t, deriv) =
(case (t, deriv) of
(t, Term Input) => SOME t
| (t, Term Output) => NONE
| (Const (name, T), Context mode) =>
- SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy name
- (pol, mode),
+ SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+ (ProofContext.theory_of ctxt) name (pol, mode),
Comp_Mod.funT_of compilation_modifiers mode T))
| (Free (s, T), Context m) =>
SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
@@ -1544,22 +1593,22 @@
| (SOME t, SOME u) => SOME (t $ u)
| _ => error "something went wrong here!"))
in
- the (expr_of (t, deriv))
+ list_comb (the (expr_of (t, deriv)), additional_arguments)
end
-fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments
+fun compile_clause compilation_modifiers compfuns ctxt all_vs param_vs additional_arguments
(pol, mode) inp (ts, moded_ps) =
let
val iss = ho_arg_modes_of mode
val compile_match = compile_match compilation_modifiers compfuns
- additional_arguments param_vs iss thy
+ additional_arguments param_vs iss ctxt
val (in_ts, out_ts) = split_mode mode ts;
val (in_ts', (all_vs', eqs)) =
- fold_map (collect_non_invertible_subterms thy) in_ts (all_vs, []);
+ fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
fun compile_prems out_ts' vs names [] =
let
val (out_ts'', (names', eqs')) =
- fold_map (collect_non_invertible_subterms thy) out_ts' (names, []);
+ fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
out_ts'' (names', map (rpair []) vs);
in
@@ -1570,7 +1619,7 @@
let
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
val (out_ts', (names', eqs)) =
- fold_map (collect_non_invertible_subterms thy) out_ts (names, [])
+ fold_map (collect_non_invertible_subterms ctxt) out_ts (names, [])
val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
out_ts' ((names', map (rpair []) vs))
val mode = head_mode_of deriv
@@ -1580,7 +1629,7 @@
Prem t =>
let
val u =
- compile_expr compilation_modifiers compfuns thy
+ compile_expr compilation_modifiers compfuns ctxt
pol (t, deriv) additional_arguments'
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
@@ -1590,7 +1639,7 @@
| Negprem t =>
let
val u = mk_not compfuns
- (compile_expr compilation_modifiers compfuns thy
+ (compile_expr compilation_modifiers compfuns ctxt
(not pol) (t, deriv) additional_arguments')
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
@@ -1600,15 +1649,14 @@
| Sidecond t =>
let
val t = compile_arg compilation_modifiers compfuns additional_arguments
- thy param_vs iss t
+ ctxt param_vs iss t
val rest = compile_prems [] vs' names'' ps;
in
(mk_if compfuns t, rest)
end
| Generator (v, T) =>
let
- val u = mk_random T
-
+ val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
val rest = compile_prems [Free (v, T)] vs' names'' ps;
in
(u, rest)
@@ -1624,14 +1672,13 @@
fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
let
- (* TODO: val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
+ val ctxt = ProofContext.init thy
+ val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
(all_vs @ param_vs)
- *)
val compfuns = Comp_Mod.compfuns compilation_modifiers
fun is_param_type (T as Type ("fun",[_ , T'])) =
is_some (try (dest_predT compfuns) T) orelse is_param_type T'
| is_param_type T = is_some (try (dest_predT compfuns) T)
- val additional_arguments = []
val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
(binder_types T)
val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
@@ -1639,7 +1686,7 @@
val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
(fn T => fn (param_vs, names) =>
- if is_param_type T then
+ if is_param_type T then
(Free (hd param_vs, T), (tl param_vs, names))
else
let
@@ -1650,14 +1697,15 @@
(fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
val cl_ts =
map (compile_clause compilation_modifiers compfuns
- thy all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
+ ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
s T mode additional_arguments
(if null cl_ts then
mk_bot compfuns (HOLogic.mk_tupleT outTs)
else foldr1 (mk_sup compfuns) cl_ts)
val fun_const =
- Const (function_name_of (Comp_Mod.compilation compilation_modifiers) thy s (pol, mode), funT)
+ Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+ (ProofContext.theory_of ctxt) s (pol, mode), funT)
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -1752,8 +1800,24 @@
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
val elimthm = Goal.prove (ProofContext.init thy)
(argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
+ val opt_neg_introthm =
+ if is_all_input mode then
+ let
+ val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
+ val neg_funpropI =
+ HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval
+ (PredicateCompFuns.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
+ val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
+ val tac =
+ Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
+ (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
+ THEN rtac @{thm Predicate.singleI} 1
+ in SOME (Goal.prove (ProofContext.init thy) (argnames @ hoarg_names') []
+ neg_introtrm (fn _ => tac))
+ end
+ else NONE
in
- (introthm, elimthm)
+ ((introthm, elimthm), opt_neg_introthm)
end
fun create_constname_of_mode options thy prefix name T mode =
@@ -1789,11 +1853,11 @@
val ([definition], thy') = thy |>
Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
- val (intro, elim) =
+ val rules as ((intro, elim), _) =
create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
in thy'
|> set_function_name Pred name mode mode_cname
- |> add_predfun_data name mode (definition, intro, elim)
+ |> add_predfun_data name mode (definition, rules)
|> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
|> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
|> Theory.checkpoint
@@ -1843,7 +1907,7 @@
(* MAJOR FIXME: prove_params should be simple
- different form of introrule for parameters ? *)
-fun prove_param options thy t deriv =
+fun prove_param options ctxt nargs t deriv =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val mode = head_mode_of deriv
@@ -1851,54 +1915,72 @@
val ho_args = ho_args_of mode args
val f_tac = case f of
Const (name, T) => simp_tac (HOL_basic_ss addsimps
- ([@{thm eval_pred}, (predfun_definition_of thy name mode),
- @{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
- @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
- | Free _ => TRY (rtac @{thm refl} 1)
- | Abs _ => error "prove_param: No valid parameter term"
+ [@{thm eval_pred}, predfun_definition_of ctxt name mode,
+ @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
+ @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+ | Free _ =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+ let
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ in
+ MetaSimplifier.rewrite_goal_tac
+ (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end) ctxt 1
+ | Abs _ => raise Fail "prove_param: No valid parameter term"
in
REPEAT_DETERM (rtac @{thm ext} 1)
- THEN print_tac' options "prove_param"
- THEN f_tac
- THEN print_tac' options "after simplification in prove_args"
+ THEN print_tac options "prove_param"
+ THEN f_tac
+ THEN print_tac options "after prove_param"
THEN (REPEAT_DETERM (atac 1))
- THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations))
+ THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
+ THEN REPEAT_DETERM (rtac @{thm refl} 1)
end
-fun prove_expr options thy (premposition : int) (t, deriv) =
+fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
case strip_comb t of
(Const (name, T), args) =>
let
val mode = head_mode_of deriv
- val introrule = predfun_intro_of thy name mode
+ val introrule = predfun_intro_of ctxt name mode
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
- print_tac' options "before intro rule:"
+ print_tac options "before intro rule:"
+ THEN rtac introrule 1
+ THEN print_tac options "after intro rule"
(* for the right assumption in first position *)
THEN rotate_tac premposition 1
- THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
- THEN rtac introrule 1
- THEN print_tac' options "after intro rule"
+ THEN atac 1
+ THEN print_tac options "parameter goal"
(* work with parameter arguments *)
- THEN atac 1
- THEN print_tac' options "parameter goal"
- THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations))
+ THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
THEN (REPEAT_DETERM (atac 1))
end
- | _ =>
- asm_full_simp_tac
- (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
- @{thm "snd_conv"}, @{thm pair_collapse}]) 1
- THEN (atac 1)
- THEN print_tac' options "after prove parameter call"
-
+ | (Free _, _) =>
+ print_tac options "proving parameter call.."
+ THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+ let
+ val param_prem = nth prems premposition
+ val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ fun param_rewrite prem =
+ param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
+ val SOME rew_eq = find_first param_rewrite prems'
+ val param_prem' = MetaSimplifier.rewrite_rule
+ (map (fn th => th RS @{thm eq_reflection})
+ [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
+ param_prem
+ in
+ rtac param_prem' 1
+ end) ctxt 1
+ THEN print_tac options "after prove parameter call"
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
-fun check_format thy st =
+fun check_format ctxt st =
let
val concl' = Logic.strip_assums_concl (hd (prems_of st))
val concl = HOLogic.dest_Trueprop concl'
@@ -1913,8 +1995,9 @@
((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*)
end
-fun prove_match options thy (out_ts : term list) =
+fun prove_match options ctxt out_ts =
let
+ val thy = ProofContext.theory_of ctxt
fun get_case_rewrite t =
if (is_constructor thy t) then let
val case_rewrites = (#case_rewrites (Datatype.the_info thy
@@ -1926,20 +2009,21 @@
in
(* make this simpset better! *)
asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
- THEN print_tac' options "after prove_match:"
- THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
+ THEN print_tac options "after prove_match:"
+ THEN (DETERM (TRY (EqSubst.eqsubst_tac ctxt [0] [@{thm HOL.if_P}] 1
THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
- THEN print_tac' options "if condition to be solved:"
- THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
+ THEN print_tac options "if condition to be solved:"
+ THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
THEN check_format thy
- THEN print_tac' options "after if simplification - a TRY block")))
- THEN print_tac' options "after if simplification"
+ THEN print_tac options "after if simplification - a TRY block")))
+ THEN print_tac options "after if simplification"
end;
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
-fun prove_sidecond thy t =
+fun prove_sidecond ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
fun preds_of t nameTs = case strip_comb t of
(f as Const (name, T), args) =>
if is_registered thy name then (name, T) :: nameTs
@@ -1947,7 +2031,7 @@
| _ => nameTs
val preds = preds_of t []
val defs = map
- (fn (pred, T) => predfun_definition_of thy pred
+ (fn (pred, T) => predfun_definition_of ctxt pred
(all_input_of T))
preds
in
@@ -1957,14 +2041,14 @@
(* need better control here! *)
end
-fun prove_clause options thy nargs mode (_, clauses) (ts, moded_ps) =
+fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
let
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems out_ts [] =
- (prove_match options thy out_ts)
- THEN print_tac' options "before simplifying assumptions"
+ (prove_match options ctxt out_ts)
+ THEN print_tac options "before simplifying assumptions"
THEN asm_full_simp_tac HOL_basic_ss' 1
- THEN print_tac' options "before single intro rule"
+ THEN print_tac options "before single intro rule"
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, deriv) :: ps) =
let
@@ -1978,11 +2062,11 @@
val (_, out_ts''') = split_mode mode us
val rec_tac = prove_prems out_ts''' ps
in
- print_tac' options "before clause:"
+ print_tac options "before clause:"
(*THEN asm_simp_tac HOL_basic_ss 1*)
- THEN print_tac' options "before prove_expr:"
- THEN prove_expr options thy premposition (t, deriv)
- THEN print_tac' options "after prove_expr:"
+ THEN print_tac options "before prove_expr:"
+ THEN prove_expr options ctxt nargs premposition (t, deriv)
+ THEN print_tac options "after prove_expr:"
THEN rec_tac
end
| Negprem t =>
@@ -1991,45 +2075,44 @@
val (_, out_ts''') = split_mode mode args
val rec_tac = prove_prems out_ts''' ps
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
+ val neg_intro_rule =
+ Option.map (fn name =>
+ the (predfun_neg_intro_of ctxt name mode)) name
val param_derivations = param_derivations_of deriv
val params = ho_args_of mode args
in
- print_tac' options "before prove_neg_expr:"
+ print_tac options "before prove_neg_expr:"
THEN full_simp_tac (HOL_basic_ss addsimps
[@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
THEN (if (is_some name) then
- print_tac' options ("before unfolding definition " ^
- (Display.string_of_thm_global thy
- (predfun_definition_of thy (the name) mode)))
-
- THEN simp_tac (HOL_basic_ss addsimps
- [predfun_definition_of thy (the name) mode]) 1
- THEN rtac @{thm not_predI} 1
- THEN print_tac' options "after applying rule not_predI"
- THEN full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True},
- @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
- @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
- THEN (REPEAT_DETERM (atac 1))
- THEN (EVERY (map2 (prove_param options thy) params param_derivations))
+ print_tac options "before applying not introduction rule"
+ THEN rotate_tac premposition 1
+ THEN etac (the neg_intro_rule) 1
+ THEN rotate_tac (~premposition) 1
+ THEN print_tac options "after applying not introduction rule"
+ THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
THEN (REPEAT_DETERM (atac 1))
else
- rtac @{thm not_predI'} 1)
+ rtac @{thm not_predI'} 1
+ (* test: *)
+ THEN dtac @{thm sym} 1
+ THEN asm_full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1)
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN rec_tac
end
| Sidecond t =>
rtac @{thm if_predI} 1
- THEN print_tac' options "before sidecond:"
- THEN prove_sidecond thy t
- THEN print_tac' options "after sidecond:"
+ THEN print_tac options "before sidecond:"
+ THEN prove_sidecond ctxt t
+ THEN print_tac options "after sidecond:"
THEN prove_prems [] ps)
- in (prove_match options thy out_ts)
+ in (prove_match options ctxt out_ts)
THEN rest_tac
end;
val prems_tac = prove_prems in_ts moded_ps
in
- print_tac' options "Proving clause..."
+ print_tac options "Proving clause..."
THEN rtac @{thm bindI} 1
THEN rtac @{thm singleI} 1
THEN prems_tac
@@ -2039,50 +2122,50 @@
| select_sup _ 1 = [rtac @{thm supI1}]
| select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
-fun prove_one_direction options thy clauses preds pred mode moded_clauses =
+fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
let
+ val thy = ProofContext.theory_of ctxt
val T = the (AList.lookup (op =) preds pred)
val nargs = length (binder_types T)
val pred_case_rule = the_elim_of thy pred
in
REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
- THEN print_tac' options "before applying elim rule"
- THEN etac (predfun_elim_of thy pred mode) 1
+ THEN print_tac options "before applying elim rule"
+ THEN etac (predfun_elim_of ctxt pred mode) 1
THEN etac pred_case_rule 1
+ THEN print_tac options "after applying elim rule"
THEN (EVERY (map
(fn i => EVERY' (select_sup (length moded_clauses) i) i)
(1 upto (length moded_clauses))))
- THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses))
- THEN print_tac' options "proved one direction"
+ THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
+ THEN print_tac options "proved one direction"
end;
(** Proof in the other direction **)
-fun prove_match2 thy out_ts = let
- fun split_term_tac (Free _) = all_tac
- | split_term_tac t =
- if (is_constructor thy t) then let
- val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
- val num_of_constrs = length (#case_rewrites info)
- (* special treatment of pairs -- because of fishing *)
- val split_rules = case (fst o dest_Type o fastype_of) t of
- "*" => [@{thm prod.split_asm}]
- | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
- val (_, ts) = strip_comb t
- in
- (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^
- "splitting with rules \n" ^
- commas (map (Display.string_of_thm_global thy) split_rules)))
- THEN TRY ((Splitter.split_asm_tac split_rules 1)
- THEN (print_tac "after splitting with split_asm rules")
- (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
- THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
- THEN (REPEAT_DETERM_N (num_of_constrs - 1)
- (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
- THEN (assert_tac (Max_number_of_subgoals 2))
- THEN (EVERY (map split_term_tac ts))
- end
- else all_tac
+fun prove_match2 options ctxt out_ts =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun split_term_tac (Free _) = all_tac
+ | split_term_tac t =
+ if (is_constructor thy t) then
+ let
+ val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
+ val num_of_constrs = length (#case_rewrites info)
+ val (_, ts) = strip_comb t
+ in
+ print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
+ "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info))
+ THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1)
+ THEN (print_tac options "after splitting with split_asm rules")
+ (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
+ THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
+ THEN (REPEAT_DETERM_N (num_of_constrs - 1)
+ (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
+ THEN (assert_tac (Max_number_of_subgoals 2))
+ THEN (EVERY (map split_term_tac ts))
+ end
+ else all_tac
in
split_term_tac (HOLogic.mk_tuple out_ts)
THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
@@ -2094,7 +2177,7 @@
*)
(* TODO: remove function *)
-fun prove_param2 thy t deriv =
+fun prove_param2 options ctxt t deriv =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val mode = head_mode_of deriv
@@ -2102,18 +2185,18 @@
val ho_args = ho_args_of mode args
val f_tac = case f of
Const (name, T) => full_simp_tac (HOL_basic_ss addsimps
- (@{thm eval_pred}::(predfun_definition_of thy name mode)
+ (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term"
in
- print_tac "before simplification in prove_args:"
+ print_tac options "before simplification in prove_args:"
THEN f_tac
- THEN print_tac "after simplification in prove_args"
- THEN EVERY (map2 (prove_param2 thy) ho_args param_derivations)
+ THEN print_tac options "after simplification in prove_args"
+ THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
end
-fun prove_expr2 thy (t, deriv) =
+fun prove_expr2 options ctxt (t, deriv) =
(case strip_comb t of
(Const (name, T), args) =>
let
@@ -2123,59 +2206,54 @@
in
etac @{thm bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
- THEN print_tac "prove_expr2-before"
- THEN (debug_tac (Syntax.string_of_term_global thy
- (prop_of (predfun_elim_of thy name mode))))
- THEN (etac (predfun_elim_of thy name mode) 1)
- THEN print_tac "prove_expr2"
- THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations))
- THEN print_tac "finished prove_expr2"
+ THEN print_tac options "prove_expr2-before"
+ THEN etac (predfun_elim_of ctxt name mode) 1
+ THEN print_tac options "prove_expr2"
+ THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
+ THEN print_tac options "finished prove_expr2"
end
| _ => etac @{thm bindE} 1)
-(* FIXME: what is this for? *)
-(* replace defined by has_mode thy pred *)
-(* TODO: rewrite function *)
-fun prove_sidecond2 thy t = let
+fun prove_sidecond2 options ctxt t = let
fun preds_of t nameTs = case strip_comb t of
(f as Const (name, T), args) =>
- if is_registered thy name then (name, T) :: nameTs
+ if is_registered (ProofContext.theory_of ctxt) name then (name, T) :: nameTs
else fold preds_of args nameTs
| _ => nameTs
val preds = preds_of t []
val defs = map
- (fn (pred, T) => predfun_definition_of thy pred
+ (fn (pred, T) => predfun_definition_of ctxt pred
(all_input_of T))
preds
in
(* only simplify the one assumption *)
full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1
(* need better control here! *)
- THEN print_tac "after sidecond2 simplification"
+ THEN print_tac options "after sidecond2 simplification"
end
-fun prove_clause2 thy pred mode (ts, ps) i =
+fun prove_clause2 options ctxt pred mode (ts, ps) i =
let
- val pred_intro_rule = nth (intros_of thy pred) (i - 1)
+ val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1)
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems2 out_ts [] =
- print_tac "before prove_match2 - last call:"
- THEN prove_match2 thy out_ts
- THEN print_tac "after prove_match2 - last call:"
+ print_tac options "before prove_match2 - last call:"
+ THEN prove_match2 options ctxt out_ts
+ THEN print_tac options "after prove_match2 - last call:"
THEN (etac @{thm singleE} 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN SOLVED (print_tac "state before applying intro rule:"
+ THEN SOLVED (print_tac options "state before applying intro rule:"
THEN (rtac pred_intro_rule 1)
(* How to handle equality correctly? *)
- THEN (print_tac "state before assumption matching")
+ THEN (print_tac options "state before assumption matching")
THEN (REPEAT (atac 1 ORELSE
(CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
[@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
@{thm "snd_conv"}, @{thm pair_collapse}]) 1)
- THEN print_tac "state after simp_tac:"))))
+ THEN print_tac options "state after simp_tac:"))))
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
@@ -2186,7 +2264,7 @@
val (_, out_ts''') = split_mode mode us
val rec_tac = prove_prems2 out_ts''' ps
in
- (prove_expr2 thy (t, deriv)) THEN rec_tac
+ (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
end
| Negprem t =>
let
@@ -2197,14 +2275,14 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
- print_tac "before neg prem 2"
+ print_tac options "before neg prem 2"
THEN etac @{thm bindE} 1
THEN (if is_some name then
full_simp_tac (HOL_basic_ss addsimps
- [predfun_definition_of thy (the name) mode]) 1
+ [predfun_definition_of ctxt (the name) mode]) 1
THEN etac @{thm not_predE} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
- THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations))
+ THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
else
etac @{thm not_predE'} 1)
THEN rec_tac
@@ -2212,32 +2290,32 @@
| Sidecond t =>
etac @{thm bindE} 1
THEN etac @{thm if_predE} 1
- THEN prove_sidecond2 thy t
+ THEN prove_sidecond2 options ctxt t
THEN prove_prems2 [] ps)
- in print_tac "before prove_match2:"
- THEN prove_match2 thy out_ts
- THEN print_tac "after prove_match2:"
+ in print_tac options "before prove_match2:"
+ THEN prove_match2 options ctxt out_ts
+ THEN print_tac options "after prove_match2:"
THEN rest_tac
end;
val prems_tac = prove_prems2 in_ts ps
in
- print_tac "starting prove_clause2"
+ print_tac options "starting prove_clause2"
THEN etac @{thm bindE} 1
THEN (etac @{thm singleE'} 1)
THEN (TRY (etac @{thm Pair_inject} 1))
- THEN print_tac "after singleE':"
+ THEN print_tac options "after singleE':"
THEN prems_tac
end;
-fun prove_other_direction options thy pred mode moded_clauses =
+fun prove_other_direction options ctxt pred mode moded_clauses =
let
fun prove_clause clause i =
(if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
- THEN (prove_clause2 thy pred mode clause i)
+ THEN (prove_clause2 options ctxt pred mode clause i)
in
(DETERM (TRY (rtac @{thm unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
- THEN (rtac (predfun_intro_of thy pred mode) 1)
+ THEN (rtac (predfun_intro_of ctxt pred mode) 1)
THEN (REPEAT_DETERM (rtac @{thm refl} 2))
THEN (if null moded_clauses then
etac @{thm botE} 1
@@ -2255,11 +2333,11 @@
(if not (skip_proof options) then
(fn _ =>
rtac @{thm pred_iffI} 1
- THEN print_tac' options "after pred_iffI"
- THEN prove_one_direction options thy clauses preds pred mode moded_clauses
- THEN print_tac' options "proved one direction"
- THEN prove_other_direction options thy pred mode moded_clauses
- THEN print_tac' options "proved other direction")
+ THEN print_tac options "after pred_iffI"
+ THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
+ THEN print_tac options "proved one direction"
+ THEN prove_other_direction options ctxt pred mode moded_clauses
+ THEN print_tac options "proved other direction")
else (fn _ => Skip_Proof.cheat_tac thy))
end;
@@ -2402,6 +2480,7 @@
fun add_code_equations thy preds result_thmss =
let
+ val ctxt = ProofContext.init thy
fun add_code_equation (predname, T) (pred, result_thms) =
let
val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
@@ -2417,10 +2496,10 @@
val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
val eq_term = HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
- val def = predfun_definition_of thy predname full_mode
+ val def = predfun_definition_of ctxt predname full_mode
val tac = fn _ => Simplifier.simp_tac
(HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
- val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
+ val eq = Goal.prove ctxt arg_names [] eq_term tac
in
(pred, result_thms @ [eq])
end
@@ -2451,11 +2530,12 @@
fun add_equations_of steps mode_analysis_options options prednames thy =
let
fun dest_steps (Steps s) = s
+ val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
val _ = print_step options
- ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+ ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
+ ^ ") for predicates " ^ commas prednames ^ "...")
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
- val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
val _ =
if show_intermediate_results options then
tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
@@ -2533,58 +2613,111 @@
else thy)
scc thy' |> Theory.checkpoint
in thy'' end
-(*
+
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
{
compilation = Depth_Limited,
- function_name_of = function_name_of Depth_Limited,
- set_function_name = set_function_name Depth_Limited,
- funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ),
function_name_prefix = "depth_limited_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
additional_arguments = fn names =>
let
- val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
- in [Free (polarity_name, @{typ "bool"}), Free (depth_name, @{typ "code_numeral"})] end,
+ val depth_name = Name.variant names "depth"
+ in [Free (depth_name, @{typ code_numeral})] end,
+ modify_funT = (fn T => let val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
wrap_compilation =
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
let
- val [polarity, depth] = additional_arguments
- val (_, Ts2) = chop (length (fst mode)) (binder_types T)
- val (_, Us2) = split_smodeT (snd mode) Ts2
- val T' = mk_predT compfuns (HOLogic.mk_tupleT Us2)
+ val [depth] = additional_arguments
+ val (_, Ts) = split_modeT' mode (binder_types T)
+ val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
- val full_mode = null Us2
in
if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
- $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T')
- $ (if full_mode then mk_single compfuns HOLogic.unit else
- Const (@{const_name undefined}, T')))
+ $ mk_bot compfuns (dest_predT compfuns T')
$ compilation
end,
transform_additional_arguments =
fn prem => fn additional_arguments =>
let
- val [polarity, depth] = additional_arguments
- val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
+ val [depth] = additional_arguments
val depth' =
Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
$ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
- in [polarity', depth'] end
+ in [depth'] end
}
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
{
compilation = Random,
- function_name_of = function_name_of Random,
- set_function_name = set_function_name Random,
function_name_prefix = "random_",
- funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
- additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ list_comb (Const(@{const_name Quickcheck.iter},
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
+ PredicateCompFuns.mk_predT T), additional_arguments)),
+ modify_funT = (fn T =>
+ let
+ val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
+ in (Ts @ Ts') ---> U end),
+ additional_arguments = (fn names =>
+ let
+ val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
+ in
+ [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
+ Free (seed, @{typ "code_numeral * code_numeral"})]
+ end),
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-*)
+
+val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Depth_Limited_Random,
+ function_name_prefix = "depth_limited_random_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ list_comb (Const(@{const_name Quickcheck.iter},
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
+ PredicateCompFuns.mk_predT T), tl additional_arguments)),
+ modify_funT = (fn T =>
+ let
+ val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+ @{typ "code_numeral * code_numeral"}]
+ in (Ts @ Ts') ---> U end),
+ additional_arguments = (fn names =>
+ let
+ val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
+ in
+ [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
+ Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
+ end),
+ wrap_compilation =
+ fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+ let
+ val depth = hd (additional_arguments)
+ val (_, Ts) = split_modeT' mode (binder_types T)
+ val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+ val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+ in
+ if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+ $ mk_bot compfuns (dest_predT compfuns T')
+ $ compilation
+ end,
+ transform_additional_arguments =
+ fn prem => fn additional_arguments =>
+ let
+ val [depth, nrandom, size, seed] = additional_arguments
+ val depth' =
+ Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+ $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+ in [depth', nrandom, size, seed] end
+}
+
(* different instantiantions of the predicate compiler *)
val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
@@ -2592,6 +2725,8 @@
compilation = Pred,
function_name_prefix = "",
compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
additional_arguments = K [],
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
@@ -2615,6 +2750,8 @@
compilation = Annotated,
function_name_prefix = "annotated_",
compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
additional_arguments = K [],
wrap_compilation =
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
@@ -2628,6 +2765,8 @@
compilation = DSeq,
function_name_prefix = "dseq_",
compfuns = DSequence_CompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
additional_arguments = K [],
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
@@ -2639,6 +2778,18 @@
compilation = Pos_Random_DSeq,
function_name_prefix = "random_dseq_",
compfuns = Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ let
+ val random = Const ("Quickcheck.random_class.random",
+ @{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+ in
+ Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+ Random_Sequence_CompFuns.mk_random_dseqT T) $ random
+ end),
+
+ modify_funT = I,
additional_arguments = K [],
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
@@ -2650,22 +2801,26 @@
compilation = Neg_Random_DSeq,
function_name_prefix = "random_dseq_neg_",
compfuns = Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
additional_arguments = K [],
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-(*
val add_depth_limited_equations = gen_add_equations
- (Steps {infer_modes = infer_modes,
- define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns,
- compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns
+ options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
prove = prove_by_skip,
add_code_equations = K (K I),
- defined = defined_functions Depth_Limited,
+ comp_modifiers = depth_limited_comp_modifiers,
+ use_random = false,
qname = "depth_limited_equation"})
-*)
+
val add_annotated_equations = gen_add_equations
(Steps {
define_functions =
@@ -2677,16 +2832,31 @@
comp_modifiers = annotated_comp_modifiers,
use_random = false,
qname = "annotated_equation"})
-(*
-val add_quickcheck_equations = gen_add_equations
- (Steps {infer_modes = infer_modes_with_generator,
- define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
- compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
+
+val add_random_equations = gen_add_equations
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
+ (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
+ comp_modifiers = random_comp_modifiers,
prove = prove_by_skip,
add_code_equations = K (K I),
- defined = defined_functions Random,
+ use_random = true,
qname = "random_equation"})
-*)
+
+val add_depth_limited_random_equations = gen_add_equations
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
+ (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
+ comp_modifiers = depth_limited_random_comp_modifiers,
+ prove = prove_by_skip,
+ add_code_equations = K (K I),
+ use_random = true,
+ qname = "depth_limited_random_equation"})
+
val add_dseq_equations = gen_add_equations
(Steps {
define_functions =
@@ -2769,11 +2939,11 @@
((case compilation options of
Pred => add_equations
| DSeq => add_dseq_equations
- | Random_DSeq => add_random_dseq_equations
+ | Pos_Random_DSeq => add_random_dseq_equations
+ | Depth_Limited => add_depth_limited_equations
+ | Random => add_random_equations
+ | Depth_Limited_Random => add_depth_limited_random_equations
| compilation => error ("Compilation not supported")
- (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs)
- | Depth_Limited => add_depth_limited_equations
- | Annotated => add_annotated_equations*)
) options [const]))
end
in
@@ -2852,20 +3022,25 @@
val additional_arguments =
case compilation of
Pred => []
- | Random => [@{term "5 :: code_numeral"}]
+ | Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
+ [@{term "(1, 1) :: code_numeral * code_numeral"}]
| Annotated => []
- | Depth_Limited => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
+ | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
+ | Depth_Limited_Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
+ [@{term "(1, 1) :: code_numeral * code_numeral"}]
| DSeq => []
- | Random_DSeq => []
+ | Pos_Random_DSeq => []
val comp_modifiers =
case compilation of
Pred => predicate_comp_modifiers
- (*| Random => random_comp_modifiers
+ | Random => random_comp_modifiers
| Depth_Limited => depth_limited_comp_modifiers
- | Annotated => annotated_comp_modifiers*)
+ | Depth_Limited_Random => depth_limited_random_comp_modifiers
+ (*| Annotated => annotated_comp_modifiers*)
| DSeq => dseq_comp_modifiers
- | Random_DSeq => pos_random_dseq_comp_modifiers
- val t_pred = compile_expr comp_modifiers compfuns thy true (body, deriv) additional_arguments;
+ | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
+ val t_pred = compile_expr comp_modifiers compfuns (ProofContext.init thy)
+ true (body, deriv) additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
in
@@ -2879,7 +3054,7 @@
let
val compfuns =
case compilation of
- Random => RandomPredCompFuns.compfuns
+ Random => PredicateCompFuns.compfuns
| DSeq => DSequence_CompFuns.compfuns
| Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
| _ => PredicateCompFuns.compfuns
@@ -2888,12 +3063,12 @@
val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
val ts =
case compilation of
- Random =>
+ (* Random =>
fst (Predicate.yieldn k
(Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
(fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
- |> Random_Engine.run))
- | Pos_Random_DSeq =>
+ |> Random_Engine.run))*)
+ Pos_Random_DSeq =>
let
val [nrandom, size, depth] = arguments
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 22 11:45:09 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 22 13:48:15 2010 +0100
@@ -9,7 +9,6 @@
val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
val rewrite_intro : theory -> thm -> thm list
val pred_of_function : theory -> string -> string option
-
val add_function_predicate_translation : (term * term) -> theory -> theory
end;
@@ -37,7 +36,7 @@
in
SOME (Envir.subst_term subst p)
end
- | _ => error ("Multiple matches possible for lookup of " ^ Syntax.string_of_term_global thy t)
+ | _ => NONE
fun pred_of_function thy name =
case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
@@ -61,8 +60,8 @@
(T as Type ("fun", _)) =>
(case arg of
Free (name, _) => Free (name, transform_ho_typ T)
- | _ => error "I am surprised")
-| _ => arg
+ | _ => raise Fail "A non-variable term at a higher-order position")
+ | _ => arg
fun pred_type T =
let
@@ -119,23 +118,12 @@
SOME (c, _) => Predicate_Compile_Data.keep_function thy c
| _ => false
-fun mk_prems thy lookup_pred t (names, prems) =
+fun flatten thy lookup_pred t (names, prems) =
let
- fun mk_prems' (t as Const (name, T)) (names, prems) =
- (if is_constr thy name orelse (is_none (lookup_pred t)) then
- [(t, (names, prems))]
- else
- (*(if is_none (try lookup_pred t) then
- [(Abs ("uu", fastype_of t, HOLogic.mk_eq (t, Bound 0)), (names, prems))]
- else*) [(the (lookup_pred t), (names, prems))])
- | mk_prems' (t as Free (f, T)) (names, prems) =
- (case lookup_pred t of
- SOME t' => [(t', (names, prems))]
- | NONE => [(t, (names, prems))])
- | mk_prems' (t as Abs _) (names, prems) =
- if Predicate_Compile_Aux.is_predT (fastype_of t) then
- ([(Envir.eta_contract t, (names, prems))])
- else
+ fun lift t (names, prems) =
+ case lookup_pred (Envir.eta_contract t) of
+ SOME pred => [(pred, (names, prems))]
+ | NONE =>
let
val (vars, body) = strip_abs t
val _ = assert (fastype_of body = body_type (fastype_of body))
@@ -144,7 +132,7 @@
val body' = subst_bounds (rev frees, body)
val resname = Name.variant (absnames @ names) "res"
val resvar = Free (resname, fastype_of body)
- val t = mk_prems' body' ([], [])
+ val t = flatten' body' ([], [])
|> map (fn (res, (inner_names, inner_prems)) =>
let
fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
@@ -153,7 +141,7 @@
|> filter (fn (x, T) => member (op =) inner_names x)
val t =
fold mk_exists vTs
- (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (resvar, res) ::
+ (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
map HOLogic.dest_Trueprop inner_prems))
in
t
@@ -163,7 +151,20 @@
in
[(t, (names, prems))]
end
- | mk_prems' t (names, prems) =
+ and flatten_or_lift (t, T) (names, prems) =
+ if fastype_of t = T then
+ flatten' t (names, prems)
+ else
+ (* note pred_type might be to general! *)
+ if (pred_type (fastype_of t) = T) then
+ lift t (names, prems)
+ else
+ error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
+ ", " ^ Syntax.string_of_typ_global thy T)
+ and flatten' (t as Const (name, T)) (names, prems) = [(t, (names, prems))]
+ | flatten' (t as Free (f, T)) (names, prems) = [(t, (names, prems))]
+ | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
+ | flatten' (t as _ $ _) (names, prems) =
if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
[(t, (names, prems))]
else
@@ -172,28 +173,31 @@
(let
val (_, [B, x, y]) = strip_comb t
in
- (mk_prems' x (names, prems)
- |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B) :: prems))))
- @ (mk_prems' y (names, prems)
- |> map (fn (res, (names, prems)) =>
- (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B)) :: prems))))
+ flatten' B (names, prems)
+ |> maps (fn (B', (names, prems)) =>
+ (flatten' x (names, prems)
+ |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B') :: prems))))
+ @ (flatten' y (names, prems)
+ |> map (fn (res, (names, prems)) =>
+ (* in general unsound! *)
+ (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems)))))
end)
| Const (@{const_name "Let"}, _) =>
(let
val (_, [f, g]) = strip_comb t
in
- mk_prems' f (names, prems)
+ flatten' f (names, prems)
|> maps (fn (res, (names, prems)) =>
- mk_prems' (betapply (g, res)) (names, prems))
+ flatten' (betapply (g, res)) (names, prems))
end)
| Const (@{const_name "split"}, _) =>
(let
- val (_, [g, res]) = strip_comb t
+ val (_, g :: res :: args) = strip_comb t
val [res1, res2] = Name.variant_list names ["res1", "res2"]
val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
in
- mk_prems' (betapplys (g, [resv1, resv2]))
+ flatten' (betapplys (g, (resv1 :: resv2 :: args)))
(res1 :: res2 :: names,
HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
end)
@@ -202,14 +206,12 @@
let
val (f, args) = strip_comb t
val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
- (* TODO: contextify things - this line is to unvarify the split_thm *)
- (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
val (_, split_args) = strip_comb split_t
val match = split_args ~~ args
- fun mk_prems_of_assm assm =
+ fun flatten_of_assm assm =
let
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
val var_names = Name.variant_list names (map fst vTs)
@@ -219,183 +221,119 @@
val (lhss : term list, rhss) =
split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems')
in
- folds_map mk_prems' lhss (var_names @ names, prems)
+ folds_map flatten' lhss (var_names @ names, prems)
|> map (fn (ress, (names, prems)) =>
let
val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss)
in (names, prems' @ prems) end)
- |> maps (mk_prems' inner_t)
+ |> maps (flatten' inner_t)
end
in
- maps mk_prems_of_assm assms
+ maps flatten_of_assm assms
end
else
let
val (f, args) = strip_comb t
- (* TODO: special procedure for higher-order functions: split arguments in
- simple types and function types *)
val args = map (Pattern.eta_long []) args
- val resname = Name.variant names "res"
- val resvar = Free (resname, body_type (fastype_of t))
val _ = assert (fastype_of t = body_type (fastype_of t))
- val names' = resname :: names
- fun mk_prems'' (t as Const (c, _)) =
- if is_constr thy c orelse (is_none (lookup_pred t)) then
- let
- val _ = ()(*tracing ("not translating function " ^ Syntax.string_of_term_global thy t)*)
- in
- folds_map mk_prems' args (names', prems) |>
- map
- (fn (argvs, (names'', prems')) =>
+ val f' = lookup_pred f
+ val Ts = case f' of
+ SOME pred => (fst (split_last (binder_types (fastype_of pred))))
+ | NONE => binder_types (fastype_of f)
+ in
+ folds_map flatten_or_lift (args ~~ Ts) (names, prems) |>
+ (case f' of
+ NONE =>
+ map (fn (argvs, (names', prems')) => (list_comb (f, argvs), (names', prems')))
+ | SOME pred =>
+ map (fn (argvs, (names', prems')) =>
let
- val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
- in (names'', prem :: prems') end)
- end
- else
- let
- (* lookup_pred is falsch für polymorphe Argumente und bool. *)
- val pred = the (lookup_pred t)
- val Ts = binder_types (fastype_of pred)
- in
- folds_map mk_prems' args (names', prems)
- |> map (fn (argvs, (names'', prems')) =>
- let
- fun lift_arg T t =
- if (fastype_of t) = T then t
- else
- let
- val _ = assert (T =
- (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
- fun mk_if T (b, t, e) =
- Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
- val Ts = binder_types (fastype_of t)
- val t =
- list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
- mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
- HOLogic.mk_eq (@{term True}, Bound 0),
- HOLogic.mk_eq (@{term False}, Bound 0)))
- in
- t
- end
- (*val _ = tracing ("Ts: " ^ commas (map (Syntax.string_of_typ_global thy) Ts))
- val _ = map2 check_arity Ts (map fastype_of (argvs @ [resvar]))*)
- val argvs' = map2 lift_arg (fst (split_last Ts)) argvs
- val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
- in (names'', prem :: prems') end)
- end
- | mk_prems'' (t as Free (_, _)) =
- folds_map mk_prems' args (names', prems) |>
- map
- (fn (argvs, (names'', prems')) =>
- let
- val prem =
- case lookup_pred t of
- NONE => HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
- | SOME p => HOLogic.mk_Trueprop (list_comb (p, argvs @ [resvar]))
- in (names'', prem :: prems') end)
- | mk_prems'' t =
- error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
- in
- map (pair resvar) (mk_prems'' f)
+ fun lift_arg T t =
+ if (fastype_of t) = T then t
+ else
+ let
+ val _ = assert (T =
+ (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
+ fun mk_if T (b, t, e) =
+ Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
+ val Ts = binder_types (fastype_of t)
+ in
+ list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
+ mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
+ HOLogic.mk_eq (@{term True}, Bound 0),
+ HOLogic.mk_eq (@{term False}, Bound 0)))
+ end
+ val argvs' = map2 lift_arg Ts argvs
+ val resname = Name.variant names' "res"
+ val resvar = Free (resname, body_type (fastype_of t))
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
+ in (resvar, (resname :: names', prem :: prems')) end))
end
in
- mk_prems' (Pattern.eta_long [] t) (names, prems)
+ map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
end;
-(* assumption: mutual recursive predicates all have the same parameters. *)
+(* assumption: mutual recursive predicates all have the same parameters. *)
fun define_predicates specs thy =
if forall (fn (const, _) => defined_const thy const) specs then
([], thy)
else
- let
- val consts = map fst specs
- val eqns = maps snd specs
- (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
+ let
+ val consts = map fst specs
+ val eqns = maps snd specs
(* create prednames *)
- val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
- val argss' = map (map transform_ho_arg) argss
- (* TODO: higher order arguments also occur in tuples! *)
- val ho_argss = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss)
- val params = distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')
- val pnames = map dest_Free params
- val preds = map pred_of funs
- val prednames = map (fst o dest_Free) preds
- val funnames = map (fst o dest_Const) funs
- val fun_pred_names = (funnames ~~ prednames)
+ val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+ val argss' = map (map transform_ho_arg) argss
+ fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1))
+ (* FIXME: higher order arguments also occur in tuples! *)
+ val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss'))
+ val preds = map pred_of funs
(* mapping from term (Free or Const) to term *)
- fun map_Free f = Free o f o dest_Free
- val net = fold Item_Net.update
- ((funs ~~ preds) @ (ho_argss ~~ params))
- (Fun_Pred.get thy)
- fun lookup_pred t = lookup thy net t
- (* create intro rules *)
-
- fun mk_intros ((func, pred), (args, rhs)) =
- if (body_type (fastype_of func) = @{typ bool}) then
- (*TODO: preprocess predicate definition of rhs *)
- [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
- else
- let
- val names = Term.add_free_names rhs []
- in mk_prems thy lookup_pred rhs (names, [])
- |> map (fn (resultt, (names', prems)) =>
- Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
- end
- fun mk_rewr_thm (func, pred) = @{thm refl}
- in
- case (*try *)SOME (maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))) of
- NONE =>
- let val _ = tracing "error occured!" in ([], thy) end
- | SOME intr_ts =>
- if is_some (try (map (cterm_of thy)) intr_ts) then
- let
- val (ind_result, thy') =
- thy
- |> Sign.map_naming Name_Space.conceal
- |> Inductive.add_inductive_global
- {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
- no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
- (map (fn (s, T) =>
- ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
- []
- (map (fn x => (Attrib.empty_binding, x)) intr_ts)
- []
- ||> Sign.restore_naming thy
- val prednames = map (fst o dest_Const) (#preds ind_result)
- (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
- (* add constants to my table *)
-
- val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
- (#intrs ind_result))) prednames
- (*
- val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
- *)
-
- val thy'' = Fun_Pred.map
- (fold Item_Net.update (map (apfst Logic.varify_global)
- (distinct (op =) funs ~~ (#preds ind_result)))) thy'
- (*val _ = print_specs thy'' specs*)
- in
- (specs, thy'')
- end
+ val net = fold Item_Net.update
+ ((funs ~~ preds) @ lifted_args)
+ (Fun_Pred.get thy)
+ fun lookup_pred t = lookup thy net t
+ (* create intro rules *)
+ fun mk_intros ((func, pred), (args, rhs)) =
+ if (body_type (fastype_of func) = @{typ bool}) then
+ (* TODO: preprocess predicate definition of rhs *)
+ [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
else
let
- val _ = Output.tracing (
- "Introduction rules of function_predicate are not welltyped: " ^
- commas (map (Syntax.string_of_term_global thy) intr_ts))
- in ([], thy) end
- end
+ val names = Term.add_free_names rhs []
+ in flatten thy lookup_pred rhs (names, [])
+ |> map (fn (resultt, (names', prems)) =>
+ Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
+ end
+ fun mk_rewr_thm (func, pred) = @{thm refl}
+ val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
+ val (ind_result, thy') =
+ thy
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global
+ {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
+ no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+ (map (fn (s, T) =>
+ ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
+ (map (dest_Free o snd) lifted_args)
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts)
+ []
+ ||> Sign.restore_naming thy
+ val prednames = map (fst o dest_Const) (#preds ind_result)
+ (* add constants to my table *)
+ val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
+ (#intrs ind_result))) prednames
+ val thy'' = Fun_Pred.map
+ (fold Item_Net.update (map (apfst Logic.varify_global)
+ (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+ in
+ (specs, thy'')
+ end
fun rewrite_intro thy intro =
let
(*val _ = tracing ("Rewriting intro with registered mapping for: " ^
commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*)
- (*fun lookup_pred (Const (name, T)) =
- (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
- SOME c => SOME (Const (c, pred_type T))
- | NONE => NONE)
- | lookup_pred _ = NONE
- *)
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
val intro_t = Logic.unvarify_global (prop_of intro)
val (prems, concl) = Logic.strip_horn intro_t
@@ -409,7 +347,7 @@
| NONE => (t, I)
val (P, args) = (strip_comb lit)
in
- folds_map (mk_prems thy lookup_pred) args (names, [])
+ folds_map (flatten thy lookup_pred) args (names, [])
|> map (fn (resargs, (names', prems')) =>
let
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))