including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
--- a/src/HOL/IsaMakefile Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/IsaMakefile Tue Oct 27 09:02:22 2009 +0100
@@ -255,6 +255,7 @@
Map.thy \
Nat_Numeral.thy \
Presburger.thy \
+ Predicate_Compile.thy \
Quickcheck.thy \
Random.thy \
Recdef.thy \
@@ -283,6 +284,13 @@
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
Tools/polyhash.ML \
+ Tools/Predicate_Compile/predicate_compile_aux.ML \
+ Tools/Predicate_Compile/predicate_compile_core.ML \
+ Tools/Predicate_Compile/predicate_compile_data.ML \
+ Tools/Predicate_Compile/predicate_compile_fun.ML \
+ Tools/Predicate_Compile/predicate_compile.ML \
+ Tools/Predicate_Compile/predicate_compile_pred.ML \
+ Tools/Predicate_Compile/predicate_compile_set.ML \
Tools/quickcheck_generators.ML \
Tools/Qelim/cooper_data.ML \
Tools/Qelim/cooper.ML \
@@ -945,7 +953,7 @@
ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
- ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy \
+ ex/Predicate_Compile_ex.thy \
ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.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 \
--- a/src/HOL/Main.thy Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/Main.thy Tue Oct 27 09:02:22 2009 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Nitpick Quickcheck Recdef
+imports Plain Nitpick Predicate_Compile Recdef
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile.thy Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,19 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
+
+header {* A compiler for predicates defined by introduction rules *}
+
+theory Predicate_Compile
+imports Quickcheck
+uses
+ "Tools/Predicate_Compile/predicate_compile_aux.ML"
+ "Tools/Predicate_Compile/predicate_compile_core.ML"
+ "Tools/Predicate_Compile/predicate_compile_set.ML"
+ "Tools/Predicate_Compile/predicate_compile_data.ML"
+ "Tools/Predicate_Compile/predicate_compile_fun.ML"
+ "Tools/Predicate_Compile/predicate_compile_pred.ML"
+ "Tools/Predicate_Compile/predicate_compile.ML"
+begin
+
+setup {* Predicate_Compile.setup *}
+
+end
\ No newline at end of file
--- a/src/HOL/Quickcheck.thy Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/Quickcheck.thy Tue Oct 27 09:02:22 2009 +0100
@@ -126,6 +126,47 @@
shows "random_aux k = rhs k"
using assms by (rule code_numeral.induct)
+subsection {* the Random-Predicate Monad *}
+
+types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+
+definition empty :: "'a randompred"
+ where "empty = Pair (bot_class.bot)"
+
+definition single :: "'a => 'a randompred"
+ where "single x = Pair (Predicate.single x)"
+
+definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
+ where
+ "bind R f = (\<lambda>s. let
+ (P, s') = R s;
+ (s1, s2) = Random.split_seed s'
+ in (Predicate.bind P (%a. fst (f a s1)), s2))"
+
+definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
+where
+ "union R1 R2 = (\<lambda>s. let
+ (P1, s') = R1 s; (P2, s'') = R2 s'
+ in (upper_semilattice_class.sup P1 P2, s''))"
+
+definition if_randompred :: "bool \<Rightarrow> unit randompred"
+where
+ "if_randompred b = (if b then single () else empty)"
+
+definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
+where
+ "not_randompred P = (\<lambda>s. let
+ (P', s') = P s
+ in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
+
+definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
+ where "Random g = scomp g (Pair o (Predicate.single o fst))"
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
+ where "map f P = bind P (single o f)"
+
+subsection {* Code setup *}
+
use "Tools/quickcheck_generators.ML"
setup {* Quickcheck_Generators.setup *}
@@ -137,7 +178,9 @@
code_reserved Quickcheck Quickcheck_Generators
+hide (open) type randompred
hide (open) const random collapse beyond random_fun_aux random_fun_lift
+ empty single bind union if_randompred not_randompred Random map
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-Auxilary functions for predicate compiler
-*)
-
-structure Predicate_Compile_Aux =
-struct
-
-(* general syntactic functions *)
-
-(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
- | conjuncts_aux t conjs = t::conjs;
-
-fun conjuncts t = conjuncts_aux t [];
-
-(* syntactic functions *)
-
-fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
- | is_equationlike_term _ = false
-
-val is_equationlike = is_equationlike_term o prop_of
-
-fun is_pred_equation_term (Const ("==", _) $ u $ v) =
- (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
- | is_pred_equation_term _ = false
-
-val is_pred_equation = is_pred_equation_term o prop_of
-
-fun is_intro_term constname t =
- case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
- Const (c, _) => c = constname
- | _ => false
-
-fun is_intro constname t = is_intro_term constname (prop_of t)
-
-fun is_pred thy constname =
- let
- 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)
- | is_predT _ = false
-
-
-(*** check if a term contains only constructor functions ***)
-fun is_constrt thy =
- let
- val cnstrs = flat (maps
- (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (Datatype.get_all thy)));
- fun check t = (case strip_comb t of
- (Free _, []) => true
- | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
- (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
- | _ => false)
- | _ => false)
- in check end;
-
-fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
- let
- val (xTs, t') = strip_ex t
- in
- ((x, T) :: xTs, t')
- end
- | strip_ex t = ([], t)
-
-fun focus_ex t nctxt =
- let
- val ((xs, Ts), t') = apfst split_list (strip_ex t)
- val (xs', nctxt') = Name.variants xs nctxt;
- val ps' = xs' ~~ Ts;
- val vs = map Free ps';
- val t'' = Term.subst_bounds (rev vs, t');
- in ((ps', t''), nctxt') end;
-
-
-(* introduction rule combinators *)
-
-(* combinators to apply a function to all literals of an introduction rules *)
-
-fun map_atoms f intro =
- let
- val (literals, head) = Logic.strip_horn intro
- fun appl t = (case t of
- (@{term "Not"} $ t') => HOLogic.mk_not (f t')
- | _ => f t)
- in
- Logic.list_implies
- (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
- end
-
-fun fold_atoms f intro s =
- let
- val (literals, head) = Logic.strip_horn intro
- fun appl t s = (case t of
- (@{term "Not"} $ t') => f t' s
- | _ => f t s)
- in fold appl (map HOLogic.dest_Trueprop literals) s end
-
-fun fold_map_atoms f intro s =
- 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)
- | _ => f t s)
- val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
- in
- (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
- end;
-
-fun maps_premises f intro =
- let
- val (premises, head) = Logic.strip_horn intro
- in
- Logic.list_implies (maps f premises, head)
- end
-
-(* lifting term operations to theorems *)
-
-fun map_term thy f th =
- Skip_Proof.make_thm thy (f (prop_of th))
-
-(*
-fun equals_conv lhs_cv rhs_cv ct =
- case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
- | _ => error "equals_conv"
-*)
-
-(* Different options for compiler *)
-
-datatype options = Options of {
- expected_modes : (string * int list list) option,
- show_steps : bool,
- show_mode_inference : bool,
- show_proof_trace : bool,
- show_intermediate_results : bool,
- show_compilation : bool,
- skip_proof : bool,
-
- inductify : bool,
- rpred : bool,
- depth_limited : bool
-};
-
-fun expected_modes (Options opt) = #expected_modes opt
-fun show_steps (Options opt) = #show_steps opt
-fun show_mode_inference (Options opt) = #show_mode_inference opt
-fun show_intermediate_results (Options opt) = #show_intermediate_results opt
-fun show_proof_trace (Options opt) = #show_proof_trace opt
-fun show_compilation (Options opt) = #show_compilation opt
-fun skip_proof (Options opt) = #skip_proof opt
-
-fun is_inductify (Options opt) = #inductify opt
-fun is_rpred (Options opt) = #rpred opt
-fun is_depth_limited (Options opt) = #depth_limited opt
-
-val default_options = Options {
- expected_modes = NONE,
- show_steps = false,
- show_intermediate_results = false,
- show_proof_trace = false,
- show_mode_inference = false,
- show_compilation = false,
- skip_proof = false,
-
- inductify = false,
- rpred = false,
- depth_limited = false
-}
-
-
-fun print_step options s =
- if show_steps options then tracing s else ()
-
-(* tuple processing *)
-
-fun expand_tuples thy intro =
- let
- fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
- | rewrite_args (arg::args) (pats, intro_t, ctxt) =
- (case HOLogic.strip_tupleT (fastype_of arg) of
- (Ts as _ :: _ :: _) =>
- let
- fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, 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)) =
- let
- val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
- val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
- val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
- val args' = map (Pattern.rewrite_term thy [pat] []) args
- in
- rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
- end
- | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
- val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
- (args, (pats, intro_t, ctxt))
- in
- rewrite_args args' (pats, intro_t', ctxt')
- end
- | _ => rewrite_args args (pats, intro_t, ctxt))
- fun rewrite_prem atom =
- let
- val (_, args) = strip_comb atom
- in rewrite_args args end
- val ctxt = ProofContext.init thy
- val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
- val intro_t = prop_of intro'
- val concl = Logic.strip_imp_concl intro_t
- val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
- val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
- val (pats', intro_t', ctxt3) =
- fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
- fun rewrite_pat (ct1, ct2) =
- (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
- val t_insts' = map rewrite_pat t_insts
- val intro'' = Thm.instantiate (T_insts, t_insts') intro
- val [intro'''] = Variable.export ctxt3 ctxt [intro'']
- val intro'''' = Simplifier.full_simplify
- (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
- intro'''
- (* splitting conjunctions introduced by Pair_eq*)
- fun split_conj prem =
- map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
- val intro''''' = map_term thy (maps_premises split_conj) intro''''
- in
- intro'''''
- end
-
-
-
-end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,210 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-Book-keeping datastructure for the predicate compiler
-
-*)
-signature PREDICATE_COMPILE_DATA =
-sig
- type specification_table;
- val make_const_spec_table : theory -> specification_table
- val get_specification : specification_table -> string -> thm list
- val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
- val normalize_equation : theory -> thm -> thm
-end;
-
-structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
-struct
-
-open Predicate_Compile_Aux;
-
-structure Data = TheoryDataFun
-(
- type T =
- {const_spec_table : thm list Symtab.table};
- val empty =
- {const_spec_table = Symtab.empty};
- val copy = I;
- val extend = I;
- fun merge _
- ({const_spec_table = const_spec_table1},
- {const_spec_table = const_spec_table2}) =
- {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
-);
-
-fun mk_data c = {const_spec_table = c}
-fun map_data f {const_spec_table = c} = mk_data (f c)
-
-type specification_table = thm list Symtab.table
-
-fun defining_const_of_introrule_term t =
- let
- val _ $ u = Logic.strip_imp_concl t
- val (pred, all_args) = strip_comb u
- in case pred of
- Const (c, T) => c
- | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
- end
-
-val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
-
-(*TODO*)
-fun is_introlike_term t = true
-
-val is_introlike = is_introlike_term o prop_of
-
-fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
- (case strip_comb u of
- (Const (c, T), args) =>
- if (length (binder_types T) = length args) then
- true
- else
- raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
- | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
- | check_equation_format_term t =
- raise TERM ("check_equation_format_term failed: Not an equation", [t])
-
-val check_equation_format = check_equation_format_term o prop_of
-
-fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
- (case fst (strip_comb u) of
- Const (c, _) => c
- | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
- | defining_const_of_equation_term t =
- raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
-
-val defining_const_of_equation = defining_const_of_equation_term o prop_of
-
-(* Normalizing equations *)
-
-fun mk_meta_equation th =
- case prop_of th of
- Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
- | _ => th
-
-val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
-
-fun full_fun_cong_expand th =
- let
- val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
- val i = length (binder_types (fastype_of f)) - length args
- in funpow i (fn th => th RS meta_fun_cong) th end;
-
-fun declare_names s xs ctxt =
- let
- val res = Name.names ctxt s xs
- in (res, fold Name.declare (map fst res) ctxt) end
-
-fun split_all_pairs thy th =
- let
- val ctxt = ProofContext.init thy
- val ((_, [th']), ctxt') = Variable.import true [th] ctxt
- val t = prop_of th'
- val frees = Term.add_frees t []
- val freenames = Term.add_free_names t []
- val nctxt = Name.make_context freenames
- fun mk_tuple_rewrites (x, T) nctxt =
- let
- val Ts = HOLogic.flatten_tupleT T
- val (xTs, nctxt') = declare_names x Ts nctxt
- val paths = HOLogic.flat_tupleT_paths T
- in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
- val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
- val t' = Pattern.rewrite_term thy rewr [] t
- val tac = Skip_Proof.cheat_tac thy
- val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
- val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
- in
- th'''
- end;
-
-fun normalize_equation thy th =
- mk_meta_equation th
- |> Predicate_Compile_Set.unfold_set_notation
- |> full_fun_cong_expand
- |> split_all_pairs thy
- |> tap check_equation_format
-
-fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
-((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
-
-fun store_thm_in_table ignore_consts thy th=
- let
- val th = th
- |> inline_equations thy
- |> Predicate_Compile_Set.unfold_set_notation
- |> AxClass.unoverload thy
- val (const, th) =
- if is_equationlike th then
- let
- val eq = normalize_equation thy th
- in
- (defining_const_of_equation eq, eq)
- end
- else if (is_introlike th) then (defining_const_of_introrule th, th)
- else error "store_thm: unexpected definition format"
- in
- if not (member (op =) ignore_consts const) then
- Symtab.cons_list (const, th)
- else I
- end
-
-fun make_const_spec_table thy =
- let
- fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
- val table = Symtab.empty
- |> store [] Predicate_Compile_Alternative_Defs.get
- val ignore_consts = Symtab.keys table
- in
- table
- |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
- |> store ignore_consts Nitpick_Simps.get
- |> store ignore_consts Nitpick_Intros.get
- end
-
-fun get_specification table constname =
- case Symtab.lookup table constname of
- SOME thms => thms
- | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
-
-val logic_operator_names =
- [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"},
- @{const_name "op &"}]
-
-val special_cases = member (op =) [
- @{const_name "False"},
- @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
- @{const_name Nat.one_nat_inst.one_nat},
-@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
-@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
-@{const_name Nat.ord_nat_inst.less_eq_nat},
-@{const_name number_nat_inst.number_of_nat},
- @{const_name Int.Bit0},
- @{const_name Int.Bit1},
- @{const_name Int.Pls},
-@{const_name "Int.zero_int_inst.zero_int"},
-@{const_name "List.filter"}]
-
-fun case_consts thy s = is_some (Datatype.info_of_case thy s)
-
-fun obtain_specification_graph thy table constname =
- let
- fun is_nondefining_constname c = member (op =) logic_operator_names c
- val is_defining_constname = member (op =) (Symtab.keys table)
- fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
- fun defiants_of specs =
- fold (Term.add_const_names o prop_of) specs []
- |> filter is_defining_constname
- |> filter_out is_nondefining_constname
- |> filter_out has_code_pred_intros
- |> filter_out (case_consts thy)
- |> filter_out special_cases
- fun extend constname =
- let
- val specs = get_specification table constname
- in (specs, defiants_of specs) end;
- in
- Graph.extend extend constname Graph.empty
- end;
-
-
-end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-Preprocessing definitions of predicates to introduction rules
-*)
-
-signature PREDICATE_COMPILE_PRED =
-sig
- (* preprocesses an equation to a set of intro rules; defines new constants *)
- (*
- val preprocess_pred_equation : thm -> theory -> thm list * theory
- *)
- val preprocess : string -> theory -> (thm list list * theory)
- (* output is the term list of clauses of an unknown predicate *)
- val preprocess_term : term -> theory -> (term list * theory)
-
- (*val rewrite : thm -> thm*)
-
-end;
-(* : PREDICATE_COMPILE_PREPROC_PRED *)
-structure Predicate_Compile_Pred =
-struct
-
-open Predicate_Compile_Aux
-
-fun is_compound ((Const ("Not", _)) $ t) =
- error "is_compound: Negation should not occur; preprocessing is defect"
- | is_compound ((Const ("Ex", _)) $ _) = true
- | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const ("op &", _)) $ _ $ _) =
- error "is_compound: Conjunction should not occur; preprocessing is defect"
- | is_compound _ = false
-
-fun flatten constname atom (defs, thy) =
- if is_compound atom then
- let
- val constname = Name.variant (map (Long_Name.base_name o fst) defs)
- ((Long_Name.base_name constname) ^ "_aux")
- val full_constname = Sign.full_bname thy constname
- val (params, args) = List.partition (is_predT o fastype_of)
- (map Free (Term.add_frees atom []))
- val constT = map fastype_of (params @ args) ---> HOLogic.boolT
- val lhs = list_comb (Const (full_constname, constT), params @ args)
- val def = Logic.mk_equals (lhs, atom)
- val ([definition], thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
- in
- (lhs, ((full_constname, [definition]) :: defs, thy'))
- end
- else
- (atom, (defs, thy))
-
-fun flatten_intros constname intros thy =
- let
- val ctxt = ProofContext.init thy
- val ((_, intros), ctxt') = Variable.import true intros ctxt
- val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
- (flatten constname) (map prop_of intros) ([], thy)
- val tac = fn _ => Skip_Proof.cheat_tac thy'
- val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
- |> Variable.export ctxt' ctxt
- in
- (intros'', (local_defs, thy'))
- end
-
-(* TODO: same function occurs in inductive package *)
-fun select_disj 1 1 = []
- | select_disj _ 1 = [rtac @{thm disjI1}]
- | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
-
-fun introrulify thy ths =
- let
- val ctxt = ProofContext.init thy
- val ((_, ths'), ctxt') = Variable.import true ths ctxt
- fun introrulify' th =
- let
- val (lhs, rhs) = Logic.dest_equals (prop_of th)
- val frees = Term.add_free_names rhs []
- val disjuncts = HOLogic.dest_disj rhs
- val nctxt = Name.make_context frees
- fun mk_introrule t =
- let
- val ((ps, t'), nctxt') = focus_ex t nctxt
- val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
- in
- (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
- end
- val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
- Logic.dest_implies o prop_of) @{thm exI}
- fun prove_introrule (index, (ps, introrule)) =
- let
- val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
- THEN EVERY1 (select_disj (length disjuncts) (index + 1))
- THEN (EVERY (map (fn y =>
- rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
- THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
- THEN TRY (atac 1)
- in
- Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
- end
- in
- map_index prove_introrule (map mk_introrule disjuncts)
- end
- in maps introrulify' ths' |> Variable.export ctxt' ctxt end
-
-val rewrite =
- Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
- #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
- #> Conv.fconv_rule nnf_conv
- #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
-
-val rewrite_intros =
- Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)})
-
-fun preprocess (constname, specs) thy =
- let
- val ctxt = ProofContext.init thy
- val intros =
- if forall is_pred_equation specs then
- introrulify thy (map rewrite specs)
- else if forall (is_intro constname) specs then
- map rewrite_intros specs
- else
- error ("unexpected specification for constant " ^ quote constname ^ ":\n"
- ^ commas (map (quote o Display.string_of_thm_global thy) specs))
- val (intros', (local_defs, thy')) = flatten_intros constname intros thy
- val (intross, thy'') = fold_map preprocess local_defs thy'
- in
- ((constname, intros') :: flat intross,thy'')
- end;
-
-fun preprocess_term t thy = error "preprocess_pred_term: to implement"
-
-fun is_Abs (Abs _) = true
- | is_Abs _ = false
-
-fun flat_higher_order_arguments (intross, thy) =
- let
- fun process constname atom (new_defs, thy) =
- let
- val (pred, args) = strip_comb atom
- val abs_args = filter is_Abs args
- fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
- let
- val _ = tracing ("Introduce new constant for " ^
- Syntax.string_of_term_global thy abs_arg)
- val vars = map Var (Term.add_vars abs_arg [])
- val abs_arg' = Logic.unvarify abs_arg
- val frees = map Free (Term.add_frees abs_arg' [])
- val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
- ((Long_Name.base_name constname) ^ "_hoaux")
- val full_constname = Sign.full_bname thy constname
- val constT = map fastype_of frees ---> (fastype_of abs_arg')
- val const = Const (full_constname, constT)
- val lhs = list_comb (const, frees)
- val def = Logic.mk_equals (lhs, abs_arg')
- val _ = tracing (Syntax.string_of_term_global thy def)
- val ([definition], thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
- in
- (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
- end
- | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
- val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
- in
- (list_comb (pred, args'), (new_defs', thy'))
- end
- fun flat_intro intro (new_defs, thy) =
- let
- val constname = fst (dest_Const (fst (strip_comb
- (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
- val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
- val th = Skip_Proof.make_thm thy intro_ts
- in
- (th, (new_defs, thy))
- end
- fun fold_map_spec f [] s = ([], s)
- | fold_map_spec f ((c, ths) :: specs) s =
- let
- val (ths', s') = f ths s
- val (specs', s'') = fold_map_spec f specs s'
- in ((c, ths') :: specs', s'') end
- val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
- in
- (intross', (new_defs, thy'))
- end
-
-end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-A quickcheck generator based on the predicate compiler
-*)
-
-signature PREDICATE_COMPILE_QUICKCHECK =
-sig
- val quickcheck : Proof.context -> term -> int -> term list option
- val test_ref :
- ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
-end;
-
-structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
-struct
-
-val test_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
-
-val target = "Quickcheck"
-
-fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
-val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
-val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-
-fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
- | mk_split_lambda [x] t = lambda x t
- | mk_split_lambda xs t =
- let
- fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
- | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
- in
- mk_split_lambda' xs t
- end;
-
-fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
- | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
- | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
-
-fun quickcheck ctxt t =
- let
- val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
- val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
- val thy = (ProofContext.theory_of ctxt')
- val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees ctxt' [] vs
- val t'' = subst_bounds (map Free (rev vs'), t')
- val (prems, concl) = strip_horn t''
- val constname = "pred_compile_quickcheck"
- val full_constname = Sign.full_bname thy constname
- val constT = map snd vs' ---> @{typ bool}
- val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
- val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
- HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn _ => Skip_Proof.cheat_tac thy'
- val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
- val _ = tracing (Display.string_of_thm ctxt' intro)
- val thy'' = thy'
- |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
- |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
- (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
- (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
- (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
- val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
- val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname
- val prog =
- if member (op =) modes ([], []) then
- let
- val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
- val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
- in Const (name, T) $ @{term True} $ Bound 0 end
- else if member (op =) depth_limited_modes ([], []) then
- let
- val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
- val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
- in lift_pred (Const (name, T) $ Bound 0) end
- else error "Predicate Compile Quickcheck failed"
- val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
- mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
- val _ = tracing (Syntax.string_of_term ctxt' qc_term)
- val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
- (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
- thy'' qc_term []
- in
- ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield))
- end
-
-end;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen
-
-Preprocessing sets to predicates
-*)
-
-signature PREDICATE_COMPILE_SET =
-sig
-(*
- val preprocess_intro : thm -> theory -> thm * theory
- val preprocess_clause : term -> theory -> term * theory
-*)
- val unfold_set_notation : thm -> thm;
-end;
-
-structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
-struct
-(*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
-@{thm Ball_def}, @{thm Bex_def}]
-
-val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
-
-(*
-fun find_set_theorems ctxt cname =
- let
- val _ = cname
-*)
-
-(*
-fun preprocess_term t ctxt =
- case t of
- Const ("op :", _) $ x $ A =>
- case strip_comb A of
- (Const (cname, T), params) =>
- let
- val _ = find_set_theorems
- in
- (t, ctxt)
- end
- | _ => (t, ctxt)
- | _ => (t, ctxt)
-*)
-(*
-fun preprocess_intro th thy =
- let
- val cnames = find_heads_of_prems
- val set_cname = filter (has_set_definition
- val _ = define_preds
- val _ = prep_pred_def
- in
-*)
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,236 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Auxilary functions for predicate compiler
+*)
+
+structure Predicate_Compile_Aux =
+struct
+
+(* general syntactic functions *)
+
+(*Like dest_conj, but flattens conjunctions however nested*)
+fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+ | conjuncts_aux t conjs = t::conjs;
+
+fun conjuncts t = conjuncts_aux t [];
+
+(* syntactic functions *)
+
+fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
+ | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
+ | is_equationlike_term _ = false
+
+val is_equationlike = is_equationlike_term o prop_of
+
+fun is_pred_equation_term (Const ("==", _) $ u $ v) =
+ (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
+ | is_pred_equation_term _ = false
+
+val is_pred_equation = is_pred_equation_term o prop_of
+
+fun is_intro_term constname t =
+ case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
+ Const (c, _) => c = constname
+ | _ => false
+
+fun is_intro constname t = is_intro_term constname (prop_of t)
+
+fun is_pred thy constname =
+ let
+ 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)
+ | is_predT _ = false
+
+
+(*** check if a term contains only constructor functions ***)
+fun is_constrt thy =
+ let
+ val cnstrs = flat (maps
+ (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+ (Symtab.dest (Datatype.get_all thy)));
+ fun check t = (case strip_comb t of
+ (Free _, []) => true
+ | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+ (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+ | _ => false)
+ | _ => false)
+ in check end;
+
+fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
+ let
+ val (xTs, t') = strip_ex t
+ in
+ ((x, T) :: xTs, t')
+ end
+ | strip_ex t = ([], t)
+
+fun focus_ex t nctxt =
+ let
+ val ((xs, Ts), t') = apfst split_list (strip_ex t)
+ val (xs', nctxt') = Name.variants xs nctxt;
+ val ps' = xs' ~~ Ts;
+ val vs = map Free ps';
+ val t'' = Term.subst_bounds (rev vs, t');
+ in ((ps', t''), nctxt') end;
+
+
+(* introduction rule combinators *)
+
+(* combinators to apply a function to all literals of an introduction rules *)
+
+fun map_atoms f intro =
+ let
+ val (literals, head) = Logic.strip_horn intro
+ fun appl t = (case t of
+ (@{term "Not"} $ t') => HOLogic.mk_not (f t')
+ | _ => f t)
+ in
+ Logic.list_implies
+ (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
+ end
+
+fun fold_atoms f intro s =
+ let
+ val (literals, head) = Logic.strip_horn intro
+ fun appl t s = (case t of
+ (@{term "Not"} $ t') => f t' s
+ | _ => f t s)
+ in fold appl (map HOLogic.dest_Trueprop literals) s end
+
+fun fold_map_atoms f intro s =
+ 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)
+ | _ => f t s)
+ val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
+ in
+ (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
+ end;
+
+fun maps_premises f intro =
+ let
+ val (premises, head) = Logic.strip_horn intro
+ in
+ Logic.list_implies (maps f premises, head)
+ end
+
+(* lifting term operations to theorems *)
+
+fun map_term thy f th =
+ Skip_Proof.make_thm thy (f (prop_of th))
+
+(*
+fun equals_conv lhs_cv rhs_cv ct =
+ case Thm.term_of ct of
+ Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
+ | _ => error "equals_conv"
+*)
+
+(* Different options for compiler *)
+
+datatype options = Options of {
+ expected_modes : (string * int list list) option,
+ show_steps : bool,
+ show_mode_inference : bool,
+ show_proof_trace : bool,
+ show_intermediate_results : bool,
+ show_compilation : bool,
+ skip_proof : bool,
+
+ inductify : bool,
+ rpred : bool,
+ depth_limited : bool
+};
+
+fun expected_modes (Options opt) = #expected_modes opt
+fun show_steps (Options opt) = #show_steps opt
+fun show_mode_inference (Options opt) = #show_mode_inference opt
+fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+fun show_proof_trace (Options opt) = #show_proof_trace opt
+fun show_compilation (Options opt) = #show_compilation opt
+fun skip_proof (Options opt) = #skip_proof opt
+
+fun is_inductify (Options opt) = #inductify opt
+fun is_rpred (Options opt) = #rpred opt
+fun is_depth_limited (Options opt) = #depth_limited opt
+
+val default_options = Options {
+ expected_modes = NONE,
+ show_steps = false,
+ show_intermediate_results = false,
+ show_proof_trace = false,
+ show_mode_inference = false,
+ show_compilation = false,
+ skip_proof = false,
+
+ inductify = false,
+ rpred = false,
+ depth_limited = false
+}
+
+
+fun print_step options s =
+ if show_steps options then tracing s else ()
+
+(* tuple processing *)
+
+fun expand_tuples thy intro =
+ let
+ fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
+ | rewrite_args (arg::args) (pats, intro_t, ctxt) =
+ (case HOLogic.strip_tupleT (fastype_of arg) of
+ (Ts as _ :: _ :: _) =>
+ let
+ fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, 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)) =
+ let
+ val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
+ val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
+ val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
+ val args' = map (Pattern.rewrite_term thy [pat] []) args
+ in
+ rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
+ end
+ | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
+ val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
+ (args, (pats, intro_t, ctxt))
+ in
+ rewrite_args args' (pats, intro_t', ctxt')
+ end
+ | _ => rewrite_args args (pats, intro_t, ctxt))
+ fun rewrite_prem atom =
+ let
+ val (_, args) = strip_comb atom
+ in rewrite_args args end
+ val ctxt = ProofContext.init thy
+ val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
+ val intro_t = prop_of intro'
+ val concl = Logic.strip_imp_concl intro_t
+ val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
+ val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
+ val (pats', intro_t', ctxt3) =
+ fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
+ fun rewrite_pat (ct1, ct2) =
+ (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
+ val t_insts' = map rewrite_pat t_insts
+ val intro'' = Thm.instantiate (T_insts, t_insts') intro
+ val [intro'''] = Variable.export ctxt3 ctxt [intro'']
+ val intro'''' = Simplifier.full_simplify
+ (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
+ intro'''
+ (* splitting conjunctions introduced by Pair_eq*)
+ fun split_conj prem =
+ map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
+ val intro''''' = map_term thy (maps_premises split_conj) intro''''
+ in
+ intro'''''
+ end
+
+
+
+end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 09:02:22 2009 +0100
@@ -49,11 +49,10 @@
mk_sup : term * term -> term,
mk_if : term -> term,
mk_not : term -> term,
- mk_map : typ -> typ -> term -> term -> term,
- lift_pred : term -> term
+ mk_map : typ -> typ -> term -> term -> term
};
val pred_compfuns : compilation_funs
- val rpred_compfuns : compilation_funs
+ val randompred_compfuns : compilation_funs
(* val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
@@ -720,12 +719,6 @@
PredData.map (Graph.map_node pred (map_pred_data set))
end
-(** data structures for generic compilation for different monads **)
-
-(* maybe rename functions more generic:
- mk_predT -> mk_monadT; dest_predT -> dest_monadT
- mk_single -> mk_return (?)
-*)
datatype compilation_funs = CompilationFuns of {
mk_predT : typ -> typ,
dest_predT : typ -> typ,
@@ -735,8 +728,7 @@
mk_sup : term * term -> term,
mk_if : term -> term,
mk_not : term -> term,
- mk_map : typ -> typ -> term -> term -> term,
- lift_pred : term -> term
+ mk_map : typ -> typ -> term -> term -> term
};
fun mk_predT (CompilationFuns funs) = #mk_predT funs
@@ -748,7 +740,6 @@
fun mk_if (CompilationFuns funs) = #mk_if funs
fun mk_not (CompilationFuns funs) = #mk_not funs
fun mk_map (CompilationFuns funs) = #mk_map funs
-fun lift_pred (CompilationFuns funs) = #lift_pred funs
fun funT_of compfuns (iss, is) T =
let
@@ -766,9 +757,9 @@
structure PredicateCompFuns =
struct
-fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
+fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
-fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
+fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
| dest_predT T = raise TYPE ("dest_predT", [T], []);
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
@@ -807,75 +798,65 @@
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
(T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
-val lift_pred = I
-
val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- mk_map = mk_map, lift_pred = lift_pred};
+ mk_map = mk_map};
end;
-structure RPredCompFuns =
+structure RandomPredCompFuns =
struct
-fun mk_rpredT T =
- @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"})
+fun mk_randompredT T =
+ @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
-fun dest_rpredT (Type ("fun", [_,
- Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
- | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []);
+fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
+ [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
+ | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
-fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
+fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
fun mk_single t =
let
val T = fastype_of t
in
- Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
+ Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
end;
fun mk_bind (x, f) =
let
val T as (Type ("fun", [_, U])) = fastype_of f
in
- Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
+ Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
end
-val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
-
-fun mk_if cond = Const (@{const_name RPred.if_rpred},
- HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
-fun mk_not t = let val T = mk_rpredT HOLogic.unitT
- in Const (@{const_name RPred.not_rpred}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map},
- (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp
+fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
+ HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
-fun lift_pred t =
- let
- val T = PredicateCompFuns.dest_predT (fastype_of t)
- val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T
- in
- Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t
- end;
+fun mk_not t = let val T = mk_randompredT HOLogic.unitT
+ in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
-val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
+fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
+ (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
+
+val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot,
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- mk_map = mk_map, lift_pred = lift_pred};
+ mk_map = mk_map};
end;
(* for external use with interactive mode *)
val pred_compfuns = PredicateCompFuns.compfuns
-val rpred_compfuns = RPredCompFuns.compfuns;
+val randompred_compfuns = RandomPredCompFuns.compfuns;
fun lift_random random =
let
val T = dest_randomT (fastype_of random)
in
- Const (@{const_name lift_random}, (@{typ Random.seed} -->
+ Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->
HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
- RPredCompFuns.mk_rpredT T) $ random
+ RandomPredCompFuns.mk_randompredT T) $ random
end;
fun depth_limited_funT_of compfuns (iss, is) T =
@@ -1604,7 +1585,7 @@
val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs
in
(paramTs' @ inargTs @ [@{typ code_numeral}]) --->
- (mk_predT RPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
+ (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
end
fun rpred_create_definitions preds (name, modes) thy =
@@ -2291,7 +2272,7 @@
val add_quickcheck_equations = gen_add_equations
{infer_modes = infer_modes_with_generator,
create_definitions = rpred_create_definitions,
- compile_preds = compile_preds rpred_comp_modifiers RPredCompFuns.compfuns,
+ compile_preds = compile_preds rpred_comp_modifiers RandomPredCompFuns.compfuns,
prove = prove_by_skip,
are_not_defined = fn thy => forall (null o rpred_modes_of thy),
qname = "rpred_equation"}
@@ -2420,7 +2401,7 @@
fun eval thy (options as (depth_limit, random)) t_compr =
let
- val compfuns = if random then RPredCompFuns.compfuns else PredicateCompFuns.compfuns
+ val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
val t = analyze_compr thy compfuns options t_compr;
val T = dest_predT compfuns (fastype_of t);
val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
@@ -2467,12 +2448,10 @@
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val _ = List.app OuterKeyword.keyword ["depth_limit", "random"]
-
val options =
let
- val depth_limit = Scan.optional (P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
- val random = Scan.optional (P.$$$ "random" >> K true) false
+ val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+ val random = Scan.optional (Args.$$$ "random" >> K true) false
in
Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,210 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Book-keeping datastructure for the predicate compiler
+
+*)
+signature PREDICATE_COMPILE_DATA =
+sig
+ type specification_table;
+ val make_const_spec_table : theory -> specification_table
+ val get_specification : specification_table -> string -> thm list
+ val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
+ val normalize_equation : theory -> thm -> thm
+end;
+
+structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
+struct
+
+open Predicate_Compile_Aux;
+
+structure Data = TheoryDataFun
+(
+ type T =
+ {const_spec_table : thm list Symtab.table};
+ val empty =
+ {const_spec_table = Symtab.empty};
+ val copy = I;
+ val extend = I;
+ fun merge _
+ ({const_spec_table = const_spec_table1},
+ {const_spec_table = const_spec_table2}) =
+ {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
+);
+
+fun mk_data c = {const_spec_table = c}
+fun map_data f {const_spec_table = c} = mk_data (f c)
+
+type specification_table = thm list Symtab.table
+
+fun defining_const_of_introrule_term t =
+ let
+ val _ $ u = Logic.strip_imp_concl t
+ val (pred, all_args) = strip_comb u
+ in case pred of
+ Const (c, T) => c
+ | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
+ end
+
+val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
+
+(*TODO*)
+fun is_introlike_term t = true
+
+val is_introlike = is_introlike_term o prop_of
+
+fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
+ (case strip_comb u of
+ (Const (c, T), args) =>
+ if (length (binder_types T) = length args) then
+ true
+ else
+ raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+ | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+ | check_equation_format_term t =
+ raise TERM ("check_equation_format_term failed: Not an equation", [t])
+
+val check_equation_format = check_equation_format_term o prop_of
+
+fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
+ (case fst (strip_comb u) of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
+ | defining_const_of_equation_term t =
+ raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+
+val defining_const_of_equation = defining_const_of_equation_term o prop_of
+
+(* Normalizing equations *)
+
+fun mk_meta_equation th =
+ case prop_of th of
+ Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
+ | _ => th
+
+val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+
+fun full_fun_cong_expand th =
+ let
+ val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
+ val i = length (binder_types (fastype_of f)) - length args
+ in funpow i (fn th => th RS meta_fun_cong) th end;
+
+fun declare_names s xs ctxt =
+ let
+ val res = Name.names ctxt s xs
+ in (res, fold Name.declare (map fst res) ctxt) end
+
+fun split_all_pairs thy th =
+ let
+ val ctxt = ProofContext.init thy
+ val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val t = prop_of th'
+ val frees = Term.add_frees t []
+ val freenames = Term.add_free_names t []
+ val nctxt = Name.make_context freenames
+ fun mk_tuple_rewrites (x, T) nctxt =
+ let
+ val Ts = HOLogic.flatten_tupleT T
+ val (xTs, nctxt') = declare_names x Ts nctxt
+ val paths = HOLogic.flat_tupleT_paths T
+ in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
+ val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
+ val t' = Pattern.rewrite_term thy rewr [] t
+ val tac = Skip_Proof.cheat_tac thy
+ val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
+ val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
+ in
+ th'''
+ end;
+
+fun normalize_equation thy th =
+ mk_meta_equation th
+ |> Predicate_Compile_Set.unfold_set_notation
+ |> full_fun_cong_expand
+ |> split_all_pairs thy
+ |> tap check_equation_format
+
+fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
+((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
+
+fun store_thm_in_table ignore_consts thy th=
+ let
+ val th = th
+ |> inline_equations thy
+ |> Predicate_Compile_Set.unfold_set_notation
+ |> AxClass.unoverload thy
+ val (const, th) =
+ if is_equationlike th then
+ let
+ val eq = normalize_equation thy th
+ in
+ (defining_const_of_equation eq, eq)
+ end
+ else if (is_introlike th) then (defining_const_of_introrule th, th)
+ else error "store_thm: unexpected definition format"
+ in
+ if not (member (op =) ignore_consts const) then
+ Symtab.cons_list (const, th)
+ else I
+ end
+
+fun make_const_spec_table thy =
+ let
+ fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
+ val table = Symtab.empty
+ |> store [] Predicate_Compile_Alternative_Defs.get
+ val ignore_consts = Symtab.keys table
+ in
+ table
+ |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
+ |> store ignore_consts Nitpick_Simps.get
+ |> store ignore_consts Nitpick_Intros.get
+ end
+
+fun get_specification table constname =
+ case Symtab.lookup table constname of
+ SOME thms => thms
+ | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
+
+val logic_operator_names =
+ [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"},
+ @{const_name "op &"}]
+
+val special_cases = member (op =) [
+ @{const_name "False"},
+ @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+ @{const_name Nat.one_nat_inst.one_nat},
+@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
+@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
+@{const_name Nat.ord_nat_inst.less_eq_nat},
+@{const_name number_nat_inst.number_of_nat},
+ @{const_name Int.Bit0},
+ @{const_name Int.Bit1},
+ @{const_name Int.Pls},
+@{const_name "Int.zero_int_inst.zero_int"},
+@{const_name "List.filter"}]
+
+fun case_consts thy s = is_some (Datatype.info_of_case thy s)
+
+fun obtain_specification_graph thy table constname =
+ let
+ fun is_nondefining_constname c = member (op =) logic_operator_names c
+ val is_defining_constname = member (op =) (Symtab.keys table)
+ fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
+ fun defiants_of specs =
+ fold (Term.add_const_names o prop_of) specs []
+ |> filter is_defining_constname
+ |> filter_out is_nondefining_constname
+ |> filter_out has_code_pred_intros
+ |> filter_out (case_consts thy)
+ |> filter_out special_cases
+ fun extend constname =
+ let
+ val specs = get_specification table constname
+ in (specs, defiants_of specs) end;
+ in
+ Graph.extend extend constname Graph.empty
+ end;
+
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,437 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing functions to predicates
+*)
+
+signature PREDICATE_COMPILE_FUN =
+sig
+val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
+ val rewrite_intro : theory -> thm -> thm list
+ val setup_oracle : theory -> theory
+ val pred_of_function : theory -> string -> string option
+end;
+
+structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
+struct
+
+
+(* Oracle for preprocessing *)
+
+val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
+
+fun the_oracle () =
+ case !oracle of
+ NONE => error "Oracle is not setup"
+ | SOME (_, oracle) => oracle
+
+val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
+ (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
+
+
+fun is_funtype (Type ("fun", [_, _])) = true
+ | is_funtype _ = false;
+
+fun is_Type (Type _) = true
+ | is_Type _ = false
+
+(* returns true if t is an application of an datatype constructor *)
+(* which then consequently would be splitted *)
+(* else false *)
+(*
+fun is_constructor thy t =
+ if (is_Type (fastype_of t)) then
+ (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
+ NONE => false
+ | SOME info => (let
+ val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
+ val (c, _) = strip_comb t
+ in (case c of
+ Const (name, _) => name mem_string constr_consts
+ | _ => false) end))
+ else false
+*)
+
+(* must be exported in code.ML *)
+fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
+
+(* Table from constant name (string) to term of inductive predicate *)
+structure Pred_Compile_Preproc = TheoryDataFun
+(
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ = Symtab.merge (op =);
+)
+
+fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
+
+fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy)
+
+
+fun transform_ho_typ (T as Type ("fun", _)) =
+ let
+ val (Ts, T') = strip_type T
+ in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
+| transform_ho_typ t = t
+
+fun transform_ho_arg arg =
+ case (fastype_of arg) of
+ (T as Type ("fun", _)) =>
+ (case arg of
+ Free (name, _) => Free (name, transform_ho_typ T)
+ | _ => error "I am surprised")
+| _ => arg
+
+fun pred_type T =
+ let
+ val (Ts, T') = strip_type T
+ val Ts' = map transform_ho_typ Ts
+ in
+ (Ts' @ [T']) ---> HOLogic.boolT
+ end;
+
+(* FIXME: create new predicate name -- does not avoid nameclashing *)
+fun pred_of f =
+ let
+ val (name, T) = dest_Const f
+ in
+ if (body_type T = @{typ bool}) then
+ (Free (Long_Name.base_name name ^ "P", T))
+ else
+ (Free (Long_Name.base_name name ^ "P", pred_type T))
+ end
+
+fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
+ | mk_param thy lookup_pred t =
+ let
+ val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
+ in if Predicate_Compile_Aux.is_predT (fastype_of t) then
+ t
+ else
+ let
+ val (vs, body) = strip_abs t
+ val names = Term.add_free_names body []
+ val vs_names = Name.variant_list names (map fst vs)
+ val vs' = map2 (curry Free) vs_names (map snd vs)
+ val body' = subst_bounds (rev vs', body)
+ val (f, args) = strip_comb body'
+ val resname = Name.variant (vs_names @ names) "res"
+ val resvar = Free (resname, body_type (fastype_of body'))
+ (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
+ val pred_body = list_comb (P, args @ [resvar])
+ *)
+ val pred_body = HOLogic.mk_eq (body', resvar)
+ val param = fold_rev lambda (vs' @ [resvar]) pred_body
+ in param end
+ end
+(* creates the list of premises for every intro rule *)
+(* theory -> term -> (string list, term list list) *)
+
+fun dest_code_eqn eqn = let
+ val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
+ val (func, args) = strip_comb lhs
+in ((func, args), rhs) end;
+
+fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
+
+fun string_of_term t =
+ case t of
+ Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
+ | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
+ | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
+ | Bound i => "Bound " ^ string_of_int i
+ | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
+ | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
+
+fun ind_package_get_nparams thy name =
+ case try (Inductive.the_inductive (ProofContext.init thy)) name of
+ SOME (_, result) => length (Inductive.params_of (#raw_induct result))
+ | NONE => error ("No such predicate: " ^ quote name)
+
+(* TODO: does not work with higher order functions yet *)
+fun mk_rewr_eq (func, pred) =
+ let
+ val (argTs, resT) = (strip_type (fastype_of func))
+ val nctxt =
+ Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
+ val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
+ val ([resname], nctxt'') = Name.variants ["r"] nctxt'
+ val args = map Free (argnames ~~ argTs)
+ val res = Free (resname, resT)
+ in Logic.mk_equals
+ (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
+ end;
+
+fun has_split_rule_cname @{const_name "nat_case"} = true
+ | has_split_rule_cname @{const_name "list_case"} = true
+ | has_split_rule_cname _ = false
+
+fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
+ | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
+ | has_split_rule_term thy _ = false
+
+fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
+ | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
+ | has_split_rule_term' thy c = has_split_rule_term thy c
+
+fun prepare_split_thm ctxt split_thm =
+ (split_thm RS @{thm iffD2})
+ |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
+
+fun find_split_thm thy (Const (name, typ)) =
+ let
+ fun split_name str =
+ case first_field "." str
+ of (SOME (field, rest)) => field :: split_name rest
+ | NONE => [str]
+ val splitted_name = split_name name
+ in
+ if length splitted_name > 0 andalso
+ String.isSuffix "_case" (List.last splitted_name)
+ then
+ (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
+ |> space_implode "."
+ |> PureThy.get_thm thy
+ |> SOME
+ handle ERROR msg => NONE
+ else NONE
+ end
+ | find_split_thm _ _ = NONE
+
+fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
+ | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
+ | find_split_thm' thy c = find_split_thm thy c
+
+fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
+
+fun folds_map f xs y =
+ let
+ fun folds_map' acc [] y = [(rev acc, y)]
+ | folds_map' acc (x :: xs) y =
+ maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
+ in
+ folds_map' [] xs y
+ end;
+
+fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
+ let
+ fun mk_prems' (t as Const (name, T)) (names, prems) =
+ if is_constr thy name orelse (is_none (try lookup_pred t)) then
+ [(t, (names, prems))]
+ else [(lookup_pred t, (names, prems))]
+ | mk_prems' (t as Free (f, T)) (names, prems) =
+ [(lookup_pred t, (names, prems))]
+ | mk_prems' (t as Abs _) (names, prems) =
+ if Predicate_Compile_Aux.is_predT (fastype_of t) then
+ [(t, (names, prems))] else error "mk_prems': Abs "
+ (* mk_param *)
+ | mk_prems' t (names, prems) =
+ if Predicate_Compile_Aux.is_constrt thy t then
+ [(t, (names, prems))]
+ else
+ if has_split_rule_term' thy (fst (strip_comb t)) then
+ 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 =
+ let
+ val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
+ val var_names = Name.variant_list names (map fst vTs)
+ val vars = map Free (var_names ~~ (map snd vTs))
+ val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
+ val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
+ in
+ mk_prems' inner_t (var_names @ names, prems' @ prems)
+ end
+ in
+ maps mk_prems_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 resname = Name.variant names "res"
+ val resvar = Free (resname, body_type (fastype_of t))
+ val names' = resname :: names
+ fun mk_prems'' (t as Const (c, _)) =
+ if is_constr thy c orelse (is_none (try lookup_pred t)) then
+ folds_map mk_prems' args (names', prems) |>
+ map
+ (fn (argvs, (names'', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
+ in (names'', prem :: prems') end)
+ else
+ let
+ val pred = lookup_pred t
+ val nparams = get_nparams pred
+ val (params, args) = chop nparams args
+ val params' = map (mk_param thy lookup_pred) params
+ in
+ folds_map mk_prems' args (names', prems)
+ |> map (fn (argvs, (names'', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
+ in (names'', prem :: prems') end)
+ end
+ | mk_prems'' (t as Free (_, _)) =
+ let
+ (* higher order argument call *)
+ val pred = lookup_pred t
+ in
+ folds_map mk_prems' args (resname :: names, prems)
+ |> map (fn (argvs, (names', prems')) =>
+ let
+ val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
+ in (names', prem :: prems') end)
+ end
+ | mk_prems'' t =
+ error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
+ in
+ map (pair resvar) (mk_prems'' f)
+ end
+ in
+ mk_prems' t (names, prems)
+ end;
+
+(* assumption: mutual recursive predicates all have the same parameters. *)
+fun define_predicates specs thy =
+ if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get 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*)
+ (* create prednames *)
+ val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+ val argss' = map (map transform_ho_arg) argss
+ val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss'))
+ 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)
+ (* mapping from term (Free or Const) to term *)
+ fun lookup_pred (Const (name, T)) =
+ (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
+ SOME c => Const (c, pred_type T)
+ | NONE =>
+ (case AList.lookup op = fun_pred_names name of
+ SOME f => Free (f, pred_type T)
+ | NONE => Const (name, T)))
+ | lookup_pred (Free (name, T)) =
+ if member op = (map fst pnames) name then
+ Free (name, transform_ho_typ T)
+ else
+ Free (name, T)
+ | lookup_pred t =
+ error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
+
+ (* mapping from term (predicate term, not function term!) to int *)
+ fun get_nparams (Const (name, _)) =
+ the_default 0 (try (ind_package_get_nparams thy) name)
+ | get_nparams (Free (name, _)) =
+ (if member op = prednames name then
+ length pnames
+ else 0)
+ | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy 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, get_nparams) 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 (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
+ NONE => ([], thy)
+ | SOME intr_ts =>
+ if is_some (try (map (cterm_of thy)) intr_ts) then
+ let
+ val (ind_result, thy') =
+ Inductive.add_inductive_global (serial ())
+ {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ 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)))
+ pnames
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts)
+ [] 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'
+ in
+ (specs, thy'')
+ end
+ else
+ let
+ val _ = tracing "Introduction rules of function_predicate are not welltyped"
+ in ([], thy) end
+ end
+
+(* preprocessing intro rules - uses oracle *)
+
+(* theory -> thm -> thm *)
+fun rewrite_intro thy intro =
+ let
+ fun lookup_pred (Const (name, T)) =
+ (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
+ SOME c => Const (c, pred_type T)
+ | NONE => error ("Function " ^ name ^ " is not inductified"))
+ | lookup_pred (Free (name, T)) = Free (name, T)
+ | lookup_pred _ = error "lookup function is not defined!"
+
+ fun get_nparams (Const (name, _)) =
+ the_default 0 (try (ind_package_get_nparams thy) name)
+ | get_nparams (Free _) = 0
+ | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
+
+ val intro_t = (Logic.unvarify o prop_of) intro
+ val (prems, concl) = Logic.strip_horn intro_t
+ val frees = map fst (Term.add_frees intro_t [])
+ fun rewrite prem names =
+ let
+ val t = (HOLogic.dest_Trueprop prem)
+ val (lit, mk_lit) = case try HOLogic.dest_not t of
+ SOME t => (t, HOLogic.mk_not)
+ | NONE => (t, I)
+ val (P, args) = (strip_comb lit)
+ in
+ folds_map (
+ fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
+ else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
+ |> map (fn (resargs, (names', prems')) =>
+ let
+ val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
+ in (prem'::prems', names') end)
+ end
+ val intro_ts' = folds_map rewrite prems frees
+ |> maps (fn (prems', frees') =>
+ rewrite concl frees'
+ |> map (fn (concl'::conclprems, _) =>
+ Logic.list_implies ((flat prems') @ conclprems, concl')))
+ in
+ map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,189 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing definitions of predicates to introduction rules
+*)
+
+signature PREDICATE_COMPILE_PRED =
+sig
+ (* preprocesses an equation to a set of intro rules; defines new constants *)
+ (*
+ val preprocess_pred_equation : thm -> theory -> thm list * theory
+ *)
+ val preprocess : string -> theory -> (thm list list * theory)
+ (* output is the term list of clauses of an unknown predicate *)
+ val preprocess_term : term -> theory -> (term list * theory)
+
+ (*val rewrite : thm -> thm*)
+
+end;
+(* : PREDICATE_COMPILE_PREPROC_PRED *)
+structure Predicate_Compile_Pred =
+struct
+
+open Predicate_Compile_Aux
+
+fun is_compound ((Const ("Not", _)) $ t) =
+ error "is_compound: Negation should not occur; preprocessing is defect"
+ | is_compound ((Const ("Ex", _)) $ _) = true
+ | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
+ | is_compound ((Const ("op &", _)) $ _ $ _) =
+ error "is_compound: Conjunction should not occur; preprocessing is defect"
+ | is_compound _ = false
+
+fun flatten constname atom (defs, thy) =
+ if is_compound atom then
+ let
+ val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ ((Long_Name.base_name constname) ^ "_aux")
+ val full_constname = Sign.full_bname thy constname
+ val (params, args) = List.partition (is_predT o fastype_of)
+ (map Free (Term.add_frees atom []))
+ val constT = map fastype_of (params @ args) ---> HOLogic.boolT
+ val lhs = list_comb (Const (full_constname, constT), params @ args)
+ val def = Logic.mk_equals (lhs, atom)
+ val ([definition], thy') = thy
+ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ in
+ (lhs, ((full_constname, [definition]) :: defs, thy'))
+ end
+ else
+ (atom, (defs, thy))
+
+fun flatten_intros constname intros thy =
+ let
+ val ctxt = ProofContext.init thy
+ val ((_, intros), ctxt') = Variable.import true intros ctxt
+ val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
+ (flatten constname) (map prop_of intros) ([], thy)
+ val tac = fn _ => Skip_Proof.cheat_tac thy'
+ val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
+ |> Variable.export ctxt' ctxt
+ in
+ (intros'', (local_defs, thy'))
+ end
+
+(* TODO: same function occurs in inductive package *)
+fun select_disj 1 1 = []
+ | select_disj _ 1 = [rtac @{thm disjI1}]
+ | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
+
+fun introrulify thy ths =
+ let
+ val ctxt = ProofContext.init thy
+ val ((_, ths'), ctxt') = Variable.import true ths ctxt
+ fun introrulify' th =
+ let
+ val (lhs, rhs) = Logic.dest_equals (prop_of th)
+ val frees = Term.add_free_names rhs []
+ val disjuncts = HOLogic.dest_disj rhs
+ val nctxt = Name.make_context frees
+ fun mk_introrule t =
+ let
+ val ((ps, t'), nctxt') = focus_ex t nctxt
+ val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
+ in
+ (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
+ end
+ val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
+ Logic.dest_implies o prop_of) @{thm exI}
+ fun prove_introrule (index, (ps, introrule)) =
+ let
+ val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
+ THEN EVERY1 (select_disj (length disjuncts) (index + 1))
+ THEN (EVERY (map (fn y =>
+ rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
+ THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
+ THEN TRY (atac 1)
+ in
+ Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
+ end
+ in
+ map_index prove_introrule (map mk_introrule disjuncts)
+ end
+ in maps introrulify' ths' |> Variable.export ctxt' ctxt end
+
+val rewrite =
+ Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
+ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
+ #> Conv.fconv_rule nnf_conv
+ #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
+
+val rewrite_intros =
+ Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)})
+
+fun preprocess (constname, specs) thy =
+ let
+ val ctxt = ProofContext.init thy
+ val intros =
+ if forall is_pred_equation specs then
+ introrulify thy (map rewrite specs)
+ else if forall (is_intro constname) specs then
+ map rewrite_intros specs
+ else
+ error ("unexpected specification for constant " ^ quote constname ^ ":\n"
+ ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+ val (intros', (local_defs, thy')) = flatten_intros constname intros thy
+ val (intross, thy'') = fold_map preprocess local_defs thy'
+ in
+ ((constname, intros') :: flat intross,thy'')
+ end;
+
+fun preprocess_term t thy = error "preprocess_pred_term: to implement"
+
+fun is_Abs (Abs _) = true
+ | is_Abs _ = false
+
+fun flat_higher_order_arguments (intross, thy) =
+ let
+ fun process constname atom (new_defs, thy) =
+ let
+ val (pred, args) = strip_comb atom
+ val abs_args = filter is_Abs args
+ fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
+ let
+ val _ = tracing ("Introduce new constant for " ^
+ Syntax.string_of_term_global thy abs_arg)
+ val vars = map Var (Term.add_vars abs_arg [])
+ val abs_arg' = Logic.unvarify abs_arg
+ val frees = map Free (Term.add_frees abs_arg' [])
+ val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
+ ((Long_Name.base_name constname) ^ "_hoaux")
+ val full_constname = Sign.full_bname thy constname
+ val constT = map fastype_of frees ---> (fastype_of abs_arg')
+ val const = Const (full_constname, constT)
+ val lhs = list_comb (const, frees)
+ val def = Logic.mk_equals (lhs, abs_arg')
+ val _ = tracing (Syntax.string_of_term_global thy def)
+ val ([definition], thy') = thy
+ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ in
+ (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
+ end
+ | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
+ val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
+ in
+ (list_comb (pred, args'), (new_defs', thy'))
+ end
+ fun flat_intro intro (new_defs, thy) =
+ let
+ val constname = fst (dest_Const (fst (strip_comb
+ (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
+ val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
+ val th = Skip_Proof.make_thm thy intro_ts
+ in
+ (th, (new_defs, thy))
+ end
+ fun fold_map_spec f [] s = ([], s)
+ | fold_map_spec f ((c, ths) :: specs) s =
+ let
+ val (ths', s') = f ths s
+ val (specs', s'') = fold_map_spec f specs s'
+ in ((c, ths') :: specs', s'') end
+ val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
+ in
+ (intross', (new_defs, thy'))
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,96 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+A quickcheck generator based on the predicate compiler
+*)
+
+signature PREDICATE_COMPILE_QUICKCHECK =
+sig
+ val quickcheck : Proof.context -> term -> int -> term list option
+ val test_ref :
+ ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
+end;
+
+structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
+struct
+
+val test_ref =
+ Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+
+val target = "Quickcheck"
+
+fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
+val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
+val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
+val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
+val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
+val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
+
+fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
+ | mk_split_lambda [x] t = lambda x t
+ | mk_split_lambda xs t =
+ let
+ fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+ | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+ in
+ mk_split_lambda' xs t
+ end;
+
+fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
+ | strip_imp_prems _ = [];
+
+fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
+ | strip_imp_concl A = A : term;
+
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+
+fun quickcheck ctxt t =
+ let
+ val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
+ val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
+ val thy = (ProofContext.theory_of ctxt')
+ val (vs, t') = strip_abs t
+ val vs' = Variable.variant_frees ctxt' [] vs
+ val t'' = subst_bounds (map Free (rev vs'), t')
+ val (prems, concl) = strip_horn t''
+ val constname = "pred_compile_quickcheck"
+ val full_constname = Sign.full_bname thy constname
+ val constT = map snd vs' ---> @{typ bool}
+ val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+ val t = Logic.list_implies
+ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+ HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
+ val tac = fn _ => Skip_Proof.cheat_tac thy'
+ val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
+ val _ = tracing (Display.string_of_thm ctxt' intro)
+ val thy'' = thy'
+ |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
+ |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
+ (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
+ (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
+ (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
+ val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
+ val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname
+ val prog =
+ if member (op =) modes ([], []) then
+ let
+ val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
+ val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
+ in Const (name, T) $ @{term True} $ Bound 0 end
+ else if member (op =) depth_limited_modes ([], []) then
+ let
+ val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
+ val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
+ in lift_pred (Const (name, T) $ Bound 0) end
+ else error "Predicate Compile Quickcheck failed"
+ val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
+ mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
+ val _ = tracing (Syntax.string_of_term ctxt' qc_term)
+ val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
+ thy'' qc_term []
+ in
+ ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield))
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,52 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing sets to predicates
+*)
+
+signature PREDICATE_COMPILE_SET =
+sig
+(*
+ val preprocess_intro : thm -> theory -> thm * theory
+ val preprocess_clause : term -> theory -> term * theory
+*)
+ val unfold_set_notation : thm -> thm;
+end;
+
+structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
+struct
+(*FIXME: unfolding Ball in pretty adhoc here *)
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
+@{thm Ball_def}, @{thm Bex_def}]
+
+val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
+
+(*
+fun find_set_theorems ctxt cname =
+ let
+ val _ = cname
+*)
+
+(*
+fun preprocess_term t ctxt =
+ case t of
+ Const ("op :", _) $ x $ A =>
+ case strip_comb A of
+ (Const (cname, T), params) =>
+ let
+ val _ = find_set_theorems
+ in
+ (t, ctxt)
+ end
+ | _ => (t, ctxt)
+ | _ => (t, ctxt)
+*)
+(*
+fun preprocess_intro th thy =
+ let
+ val cnames = find_heads_of_prems
+ val set_cname = filter (has_set_definition
+ val _ = define_preds
+ val _ = prep_pred_def
+ in
+*)
+end;
--- a/src/HOL/ex/Predicate_Compile.thy Mon Oct 26 23:27:24 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-theory Predicate_Compile
-imports Complex_Main RPred
-uses
- "../Tools/Predicate_Compile/pred_compile_aux.ML"
- "../Tools/Predicate_Compile/predicate_compile_core.ML"
- "../Tools/Predicate_Compile/pred_compile_set.ML"
- "../Tools/Predicate_Compile/pred_compile_data.ML"
- "../Tools/Predicate_Compile/pred_compile_fun.ML"
- "../Tools/Predicate_Compile/pred_compile_pred.ML"
- "../Tools/Predicate_Compile/predicate_compile.ML"
- "../Tools/Predicate_Compile/pred_compile_quickcheck.ML"
-begin
-
-setup {* Predicate_Compile.setup *}
-setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *}
-
-end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Oct 27 09:02:22 2009 +0100
@@ -1,5 +1,5 @@
theory Predicate_Compile_Alternative_Defs
-imports Predicate_Compile
+imports Main
begin
section {* Set operations *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Oct 27 09:02:22 2009 +0100
@@ -0,0 +1,12 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* A Prototype of Quickcheck based on the Predicate Compiler *}
+
+theory Predicate_Compile_Quickcheck
+imports Main
+uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+begin
+
+setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *}
+
+end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_ex.thy Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Oct 27 09:02:22 2009 +0100
@@ -2,6 +2,64 @@
imports Main Predicate_Compile_Alternative_Defs
begin
+subsection {* Basic predicates *}
+
+inductive False' :: "bool"
+
+code_pred (mode: []) False' .
+code_pred [depth_limited] False' .
+code_pred [rpred, show_compilation] False' .
+
+inductive EmptySet :: "'a \<Rightarrow> bool"
+
+code_pred (mode: [], [1]) EmptySet .
+
+inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+
+code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
+
+inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+code_pred (mode: [], [1], [2], [1, 2])EmptyClosure .
+thm EmptyClosure.equation
+
+inductive False'' :: "bool"
+where
+ "False \<Longrightarrow> False''"
+
+code_pred (mode: []) False'' .
+
+inductive EmptySet' :: "'a \<Rightarrow> bool"
+where
+ "False \<Longrightarrow> EmptySet' x"
+
+code_pred (mode: [1]) EmptySet' .
+code_pred (mode: [], [1]) [inductify] EmptySet' .
+
+inductive True' :: "bool"
+where
+ "True \<Longrightarrow> True'"
+
+code_pred (mode: []) True' .
+
+consts a' :: 'a
+
+inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+"Fact a' a'"
+
+code_pred (mode: [], [1], [2], [1, 2]) Fact .
+
+inductive zerozero :: "nat * nat => bool"
+where
+ "zerozero (0, 0)"
+
+code_pred zerozero .
+code_pred [rpred, show_compilation] zerozero .
+
+subsection {* even predicate *}
+
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
"even 0"
| "even n \<Longrightarrow> odd (Suc n)"
@@ -26,7 +84,6 @@
values [depth_limit = 7] "{x. even 6}"
values [depth_limit = 2] "{x. odd 7}"
values [depth_limit = 8] "{x. odd 7}"
-
values [depth_limit = 7] 10 "{n. even n}"
definition odd' where "odd' x == \<not> even x"
@@ -39,6 +96,14 @@
values [depth_limit = 2] "{x. odd' 7}"
values [depth_limit = 9] "{x. odd' 7}"
+inductive is_even :: "nat \<Rightarrow> bool"
+where
+ "n mod 2 = 0 \<Longrightarrow> is_even n"
+
+code_pred is_even .
+
+subsection {* append predicate *}
+
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
@@ -60,7 +125,7 @@
value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
value [code] "Predicate.the (append_3 ([]::int list))"
-subsection {* Tricky case with alternative rules *}
+text {* tricky case with alternative rules *}
inductive append2
where
@@ -78,15 +143,6 @@
from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
qed
-subsection {* Tricky cases with tuples *}
-
-inductive zerozero :: "nat * nat => bool"
-where
- "zerozero (0, 0)"
-
-code_pred zerozero .
-code_pred [rpred] zerozero .
-
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
where
"tupled_append ([], xs, xs)"
@@ -127,6 +183,8 @@
code_pred [inductify] tupled_append''' .
thm tupled_append'''.equation
+subsection {* map_ofP predicate *}
+
inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
where
"map_ofP ((a, b)#xs) a b"
@@ -135,6 +193,8 @@
code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
thm map_ofP.equation
+subsection {* filter predicate *}
+
inductive filter1
for P
where
@@ -168,7 +228,7 @@
code_pred filter3 .
code_pred [depth_limited] filter3 .
thm filter3.depth_limited_equation
-(*code_pred [rpred] filter3 .*)
+
inductive filter4
where
"List.filter P xs = ys ==> filter4 P xs ys"
@@ -177,7 +237,7 @@
code_pred [depth_limited] filter4 .
code_pred [rpred] filter4 .
-section {* reverse *}
+subsection {* reverse predicate *}
inductive rev where
"rev [] []"
@@ -196,6 +256,8 @@
code_pred tupled_rev .
thm tupled_rev.equation
+subsection {* partition predicate *}
+
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for f where
"partition f [] [] []"
@@ -206,6 +268,11 @@
code_pred [depth_limited] partition .
code_pred [rpred] partition .
+values 10 "{(ys, zs). partition is_even
+ [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
+values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
+values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
+
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
for f where
"tupled_partition f ([], [], [])"
@@ -216,23 +283,13 @@
thm tupled_partition.equation
-
-inductive is_even :: "nat \<Rightarrow> bool"
-where
- "n mod 2 = 0 \<Longrightarrow> is_even n"
-
-code_pred is_even .
-
-values 10 "{(ys, zs). partition is_even
- [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
-values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
-values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
-
lemma [code_pred_intros]:
"r a b \<Longrightarrow> tranclp r a b"
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
by auto
+subsection {* transitive predicate *}
+
code_pred tranclp
proof -
case tranclp
@@ -265,7 +322,7 @@
values 20 "{(n, m). tranclp succ n m}"
*)
-subsection{* IMP *}
+subsection {* IMP *}
types
var = nat
@@ -304,7 +361,7 @@
code_pred tupled_exec .
-subsection{* CCS *}
+subsection {* CCS *}
text{* This example formalizes finite CCS processes without communication or
recursion. For simplicity, labels are natural numbers. *}
@@ -354,18 +411,15 @@
value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
-section {* Executing definitions *}
+subsection {* Minimum *}
definition Min
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
code_pred [inductify] Min .
-subsection {* Examples with lists *}
+subsection {* Lexicographic order *}
-subsubsection {* Lexicographic order *}
-
-thm lexord_def
code_pred [inductify] lexord .
code_pred [inductify, rpred] lexord .
thm lexord.equation
@@ -392,6 +446,7 @@
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
+
(*values [random] "{xys. test_lexord xys}"*)
(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*)
(*
@@ -419,7 +474,7 @@
thm lists.equation
-section {* AVL Tree Example *}
+subsection {* AVL Tree *}
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
fun height :: "'a tree => nat" where
@@ -437,7 +492,6 @@
code_pred [rpred] avl .
thm avl.rpred_equation
-(*values [random] 10 "{t. avl (t::int tree)}"*)
fun set_of
where
@@ -455,10 +509,11 @@
code_pred [inductify] is_ord .
thm is_ord.equation
+
code_pred [rpred] is_ord .
thm is_ord.rpred_equation
-section {* Definitions about Relations *}
+subsection {* Definitions about Relations *}
code_pred [inductify] converse .
thm converse.equation
@@ -467,7 +522,6 @@
code_pred [inductify] Image .
thm Image.equation
(*TODO: *)
-ML {* Toplevel.debug := true *}
declare Id_on_def[unfolded UNION_def, code_pred_def]
code_pred [inductify] Id_on .
@@ -483,10 +537,6 @@
thm refl_on.equation
code_pred [inductify] total_on .
thm total_on.equation
-(*
-code_pred [inductify] sym .
-thm sym.equation
-*)
code_pred [inductify] antisym .
thm antisym.equation
code_pred [inductify] trans .
@@ -496,12 +546,13 @@
code_pred [inductify] inv_image .
thm inv_image.equation
-section {* List functions *}
+subsection {* Inverting list functions *}
code_pred [inductify] length .
+code_pred [inductify, rpred] length .
thm size_listP.equation
-code_pred [inductify, rpred] length .
thm size_listP.rpred_equation
+
values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}"
code_pred [inductify] concat .
@@ -509,7 +560,6 @@
code_pred [inductify] tl .
code_pred [inductify] last .
code_pred [inductify] butlast .
-(*code_pred [inductify] listsum .*)
code_pred [inductify] take .
code_pred [inductify] drop .
code_pred [inductify] zip .
@@ -526,15 +576,8 @@
code_pred [inductify] foldl .
code_pred [inductify] filter .
code_pred [inductify, rpred] filter .
-thm filterP.rpred_equation
-definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs"
-code_pred [inductify] test .
-thm testP.equation
-code_pred [inductify, rpred] test .
-thm testP.rpred_equation
-
-section {* Context Free Grammar *}
+subsection {* Context Free Grammar *}
datatype alphabet = a | b
@@ -553,79 +596,6 @@
values [random] 5 "{x. S\<^isub>1p x}"
-inductive is_a where
- "is_a a"
-
-inductive is_b where
- "is_b b"
-
-code_pred is_a .
-code_pred [depth_limited] is_a .
-code_pred [rpred] is_a .
-
-values [random] "{x. is_a x}"
-code_pred [depth_limited] is_b .
-code_pred [rpred] is_b .
-
-code_pred [inductify, depth_limited] filter .
-
-values [depth_limit=5] "{x. filterP is_a [a, b] x}"
-values [depth_limit=3] "{x. filterP is_b [a, b] x}"
-
-lemma "w \<in> S\<^isub>1 \<Longrightarrow> length (filter (\<lambda>x. x = a) w) = 1"
-(*quickcheck[generator=pred_compile, size=10]*)
-oops
-
-inductive test_lemma where
- "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \<noteq> r4 ==> test_lemma w"
-(*
-code_pred [rpred] test_lemma .
-*)
-(*
-definition test_lemma' where
- "test_lemma' w == (w \<in> S\<^isub>1 \<and> (\<not> length [x <- w. x = a] = length [x <- w. x = b]))"
-
-code_pred [inductify, rpred] test_lemma' .
-thm test_lemma'.rpred_equation
-*)
-(*thm test_lemma'.rpred_equation*)
-(*
-values [depth_limit=3 random] "{x. S\<^isub>1 x}"
-*)
-code_pred [depth_limited] is_b .
-(*
-code_pred [inductify, depth_limited] filter .
-*)
-thm filterP.intros
-thm filterP.equation
-(*
-values [depth_limit=3] "{x. filterP is_b [a, b] x}"
-find_theorems "test_lemma'_hoaux"
-code_pred [depth_limited] test_lemma'_hoaux .
-thm test_lemma'_hoaux.depth_limited_equation
-values [depth_limit=2] "{x. test_lemma'_hoaux b}"
-inductive test1 where
- "\<not> test_lemma'_hoaux x ==> test1 x"
-code_pred test1 .
-code_pred [depth_limited] test1 .
-thm test1.depth_limited_equation
-thm test_lemma'_hoaux.depth_limited_equation
-thm test1.intros
-
-values [depth_limit=2] "{x. test1 b}"
-
-thm filterP.intros
-thm filterP.depth_limited_equation
-values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}"
-values [depth_limit=4 random] "{w. test_lemma w}"
-values [depth_limit=4 random] "{w. test_lemma' w}"
-*)
-(*
-theorem S\<^isub>1_sound:
-"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=pred_compile, size=15]
-oops
-*)
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
"[] \<in> S\<^isub>2"
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
@@ -641,12 +611,6 @@
values [random] 10 "{x. S\<^isub>2 x}"
-theorem S\<^isub>2_sound:
-"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-(*quickcheck[generator=SML]*)
-(*quickcheck[generator=pred_compile, size=15, iterations=1]*)
-oops
-
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
"[] \<in> S\<^isub>3"
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
@@ -659,31 +623,6 @@
thm S\<^isub>3.equation
values 10 "{x. S\<^isub>3 x}"
-(*
-theorem S\<^isub>3_sound:
-"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=pred_compile, size=10, iterations=1]
-oops
-*)
-lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-(*quickcheck[size=10, generator = pred_compile]*)
-oops
-(*
-inductive test
-where
- "length [x \<leftarrow> w. a = x] = length [x \<leftarrow> w. x = b] ==> test w"
-ML {* @{term "[x \<leftarrow> w. x = a]"} *}
-code_pred (inductify_all) test .
-
-thm test.equation
-*)
-(*
-theorem S\<^isub>3_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
-(*quickcheck[generator=SML]*)
-quickcheck[generator=pred_compile, size=10, iterations=100]
-oops
-*)
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
"[] \<in> S\<^isub>4"
@@ -693,25 +632,8 @@
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
-(*
-theorem S\<^isub>4_sound:
-"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = pred_compile, size=2, iterations=1]
-oops
-*)
-theorem S\<^isub>4_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
-oops
-theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
-"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
-"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
-oops
-
-section {* Lambda *}
+subsection {* Lambda *}
datatype type =
Atom nat
@@ -728,7 +650,6 @@
"[]\<langle>i\<rangle> = None"
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
-
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
where
"nth_el' (x # xs) 0 x"
@@ -738,8 +659,7 @@
where
Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
| Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
-(* | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" *)
- | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+ | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
primrec
lift :: "[dB, nat] => dB"
@@ -763,15 +683,4 @@
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
-lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T"
-(*quickcheck[generator = pred_compile, size = 10, iterations = 1]*)
-oops
-
-lemma filter_eq_ConsD:
- "filter P ys = x#xs \<Longrightarrow>
- \<exists>us vs. ys = ts @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
-(*quickcheck[generator = pred_compile]*)
-oops
-
-
end
\ No newline at end of file