# HG changeset patch # User bulwahn # Date 1256408846 -7200 # Node ID 75eddea4abefe3e5d77dd90c510fe108a8ec731b # Parent 2c8f1c450b472b297d9f024cb6cd4e7f29db41a9 further changes due to the previous merge in the predicate compiler diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- 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 = diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- 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 diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- 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) *) diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- 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 diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 2c8f1c450b47 -r 75eddea4abef src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- /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