--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 20:27:26 2009 +0200
@@ -121,7 +121,7 @@
(* lifting term operations to theorems *)
fun map_term thy f th =
- setmp quick_and_dirty true (SkipProof.make_thm thy) (f (prop_of th))
+ Skip_Proof.make_thm thy (f (prop_of th))
(*
fun equals_conv lhs_cv rhs_cv ct =
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 20:27:26 2009 +0200
@@ -119,7 +119,7 @@
fun normalize_equation thy th =
mk_meta_equation th
- |> Pred_Compile_Set.unfold_set_notation
+ |> Predicate_Compile_Set.unfold_set_notation
|> full_fun_cong_expand
|> split_all_pairs thy
|> tap check_equation_format
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 20:27:26 2009 +0200
@@ -64,6 +64,8 @@
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)
@@ -100,23 +102,29 @@
(Free (Long_Name.base_name name ^ "P", pred_type T))
end
-fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t
- | mk_param lookup_pred t =
+fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
+ | mk_param thy lookup_pred t =
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 = lookup_pred f
- val pred_body = list_comb (P, args @ [resvar])
- val param = fold_rev lambda (vs' @ [resvar]) pred_body
- in param end;
-
-
+ 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) *)
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 20:27:26 2009 +0200
@@ -171,7 +171,7 @@
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 = setmp quick_and_dirty true (SkipProof.make_thm thy) intro_ts
+ val th = Skip_Proof.make_thm thy intro_ts
in
(th, (new_defs, thy))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 20:27:26 2009 +0200
@@ -423,7 +423,7 @@
case expected_modes options of
SOME (s, ms) => (case AList.lookup (op =) modes s of
SOME modes =>
- if not (eq_set (map (map (rpair NONE)) ms, map snd modes)) then
+ if not (eq_set (op =) (map (map (rpair NONE)) ms, map snd modes)) then
error ("expected modes were not inferred:\n"
^ "inferred modes for " ^ s ^ ": "
^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes))
@@ -439,8 +439,8 @@
fun varify (t, (i, ts)) =
let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = foldr varify (~1, []) cs;
- val (i', intr_ts') = foldr varify (i, []) intr_ts;
+ val (i, cs') = List.foldr varify (~1, []) cs;
+ val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
val rec_consts = fold add_term_consts_2 cs' [];
val intr_consts = fold add_term_consts_2 intr_ts' [];
fun unify (cname, cT) =
@@ -555,7 +555,7 @@
val bigeq = (Thm.symmetric (Conv.implies_concl_conv
(MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
(cterm_of thy elimrule')))
- val tac = (fn _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy))
+ val tac = (fn _ => Skip_Proof.cheat_tac thy)
val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
in
Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
@@ -599,7 +599,7 @@
(*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams
(expand_tuples_elim pre_elim))*)
val elim =
- (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
+ (Drule.standard o Skip_Proof.make_thm thy)
(mk_casesrule (ProofContext.init thy) pred nparams intros)
val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
in
@@ -702,7 +702,7 @@
val pred = Const (constname, T)
val nparams = guess_nparams T
val pre_elim =
- (Drule.standard o SkipProof.make_thm thy)
+ (Drule.standard o Skip_Proof.make_thm thy)
(mk_casesrule (ProofContext.init thy) pred nparams pre_intros)
in register_predicate (constname, pre_intros, pre_elim, nparams) thy end
@@ -2010,7 +2010,7 @@
THEN print_tac' options "proved one direction"
THEN prove_other_direction options thy modes pred mode moded_clauses
THEN print_tac' options "proved other direction")
- else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
+ else (fn _ => Skip_Proof.cheat_tac thy))
end;
(* composition of mode inference, definition, compilation and proof *)
@@ -2038,7 +2038,7 @@
(join_preds_modes moded_clauses compiled_terms)
fun prove_by_skip options thy _ _ _ _ compiled_terms =
- map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
+ map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
compiled_terms
fun dest_prem thy params t =
@@ -2145,7 +2145,7 @@
val elim = the_elim_of thy predname
val nparams = nparams_of thy predname
val elim' =
- (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
+ (Drule.standard o (Skip_Proof.make_thm thy))
(mk_casesrule (ProofContext.init thy) nparams intros)
in
if not (Thm.equiv_thm (elim, elim')) then
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Sat Oct 24 20:27:26 2009 +0200
@@ -0,0 +1,76 @@
+theory Predicate_Compile_Alternative_Defs
+imports Predicate_Compile
+begin
+
+section {* Set operations *}
+(*
+definition Empty where "Empty == {}"
+declare empty_def[symmetric, code_pred_inline]
+*)
+declare eq_reflection[OF empty_def, code_pred_inline]
+(*
+definition Union where "Union A B == A Un B"
+
+lemma [code_pred_intros]: "A x ==> Union A B x"
+and [code_pred_intros] : "B x ==> Union A B x"
+unfolding Union_def Un_def Collect_def mem_def by auto
+
+code_pred Union
+unfolding Union_def Un_def Collect_def mem_def by auto
+
+declare Union_def[symmetric, code_pred_inline]
+*)
+declare eq_reflection[OF Un_def, code_pred_inline]
+
+section {* Alternative list definitions *}
+
+subsection {* Alternative rules for set *}
+
+lemma set_ConsI1 [code_pred_intros]:
+ "set (x # xs) x"
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+lemma set_ConsI2 [code_pred_intros]:
+ "set xs x ==> set (x' # xs) x"
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+code_pred set
+proof -
+ case set
+ from this show thesis
+ apply (case_tac a1)
+ apply auto
+ unfolding mem_def[symmetric, of _ a2]
+ apply auto
+ unfolding mem_def
+ apply auto
+ done
+qed
+
+
+subsection {* Alternative rules for list_all2 *}
+
+lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+by auto
+
+lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+by auto
+
+code_pred list_all2
+proof -
+ case list_all2
+ from this show thesis
+ apply -
+ apply (case_tac a1)
+ apply (case_tac a2)
+ apply auto
+ apply (case_tac a2)
+ apply auto
+ done
+qed
+
+
+
+end
\ No newline at end of file