--- a/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ROOT.ML Sat Oct 24 16:55:42 2009 +0200
@@ -1,5 +1,6 @@
(* Classical Higher-order Logic -- batteries included *)
+Toplevel.debug := true;
use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200
@@ -73,8 +73,15 @@
(*
fun map_atoms f intro =
-fun fold_atoms f intro =
*)
+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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200
@@ -17,7 +17,73 @@
val priority = tracing;
+(* 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 _ = tracing ("Rewriting term " ^
+ (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^
+ (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^
+ (Syntax.string_of_term_global thy intro_t))*)
+ 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)
+ (*val _ = Output.tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t'))
+ val _ = Output.tracing ("pats : " ^ (commas (map
+ (fn (t1, t2) => (Syntax.string_of_term_global thy t1) ^ " -> " ^
+ Syntax.string_of_term_global thy t2) pats'))*)
+ 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 _ = Output.tracing ("t_insts':" ^ (commas (map
+ (fn (ct1, ct2) => (Syntax.string_of_term_global thy (term_of ct1) ^ " -> " ^
+ Syntax.string_of_term_global thy (term_of ct2))) t_insts')))*)
+ val intro'' = Thm.instantiate (T_insts, t_insts') intro
+ (*val _ = Output.tracing ("intro'':" ^ (Display.string_of_thm_global thy intro''))*)
+ val [intro'''] = Variable.export ctxt3 ctxt [intro'']
+ (*val _ = Output.tracing ("intro''':" ^ (Display.string_of_thm_global thy intro'''))*)
+ in
+ intro'''
+ end
+
+ (* eliminating fst/snd functions *)
+val simplify_fst_snd = Simplifier.full_simplify
+ (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
+
(* Some last processing *)
+
fun remove_pointless_clauses intro =
if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
[]
@@ -35,24 +101,25 @@
thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
(get_specs funnames)
val _ = priority "Compiling predicates to flat introrules..."
- val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
+ val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
(get_specs prednames) thy')
val _ = tracing ("Flattened introduction rules: " ^
- commas (map (Display.string_of_thm_global thy'') (flat intross)))
+ commas (map (Display.string_of_thm_global thy'') (flat intross1)))
val _ = priority "Replacing functions in introrules..."
(* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *)
- val intross' =
+ val intross2 =
if fail_safe_mode then
- case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of
- SOME intross' => intross'
- | NONE => let val _ = warning "Function replacement failed!" in intross end
- else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
+ case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
+ SOME intross => intross
+ | NONE => let val _ = warning "Function replacement failed!" in intross1 end
+ else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
val _ = tracing ("Introduction rules with replaced functions: " ^
- commas (map (Display.string_of_thm_global thy'') (flat intross')))
- val intross'' = burrow (maps remove_pointless_clauses) intross'
- val intross'' = burrow (map (AxClass.overload thy'')) intross''
+ commas (map (Display.string_of_thm_global thy'') (flat intross2)))
+ val intross3 = burrow (maps remove_pointless_clauses) intross2
+ val intross4 = burrow (map (AxClass.overload thy'')) intross3
+ val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4
val _ = priority "Registering intro rules..."
- val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
+ val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy''
in
thy'''
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200
@@ -108,6 +108,7 @@
val is_predT : typ -> bool
val guess_nparams : typ -> int
val cprods_subset : 'a list list -> 'a list list
+ val dest_prem : theory -> term list -> term -> indprem
end;
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
@@ -527,7 +528,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 _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy))
val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
val _ = Output.tracing "Preprocessed elimination rule"
in
@@ -2205,54 +2206,7 @@
forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
end
-fun expand_tuples thy intro =
- let
- fun rewrite_args [] (intro_t, names) = (intro_t, names)
- | rewrite_args (arg::args) (intro_t, names) =
- (case HOLogic.strip_tupleT (fastype_of arg) of
- (Ts as _ :: _ :: _) =>
- let
- fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
- (args, (intro_t, names)) = rewrite_arg' (t2, T2) (args, (intro_t, names))
- | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (intro_t, names)) =
- let
- val [x, y] = Name.variant_list names ["x", "y"]
- val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
- val _ = tracing ("Rewriting term " ^
- (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^
- (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^
- (Syntax.string_of_term_global thy intro_t))
- 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', (intro_t', x::y::names))
- end
- | rewrite_arg' _ (args, (intro_t, names)) = (args, (intro_t, names))
- val (args', (intro_t', names')) = rewrite_arg' (arg, fastype_of arg)
- (args, (intro_t, names))
- in
- rewrite_args args' (intro_t', names')
- end
- | _ => rewrite_args args (intro_t, names))
- fun rewrite_prem (Prem (args, _)) = rewrite_args args
- | rewrite_prem (Negprem (args, _)) = rewrite_args args
- | rewrite_prem _ = I
- val intro_t = Logic.unvarify (prop_of intro)
- val frees = Term.add_free_names intro_t []
- val concl = Logic.strip_imp_concl intro_t
- val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
- val params = List.take (args, nparams_of thy (fst (dest_Const p)))
- val (intro_t', frees') = rewrite_args args (intro_t, frees)
- val (intro_t', _) =
- fold (rewrite_prem o dest_prem thy params o HOLogic.dest_Trueprop)
- (Logic.strip_imp_prems intro_t') (intro_t', frees')
- val _ = tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t'))
- val tac =
- (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy)
- in
- Goal.prove (ProofContext.init thy) (Term.add_free_names intro_t' []) []
- intro_t' tac
- end
+
(** main function of predicate compiler **)
@@ -2260,10 +2214,9 @@
let
val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
- val intros' = map (expand_tuples thy) (maps (intros_of thy) prednames)
- val _ = map (check_format_of_intro_rule thy) intros'
+ val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
- prepare_intrs thy prednames intros'
+ prepare_intrs thy prednames (maps (intros_of thy) prednames)
val _ = Output.tracing "Infering modes..."
val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
--- a/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200
@@ -25,7 +25,7 @@
"set xs x ==> set (x' # xs) x"
unfolding mem_def[symmetric, of _ x]
by auto
-
+(*
code_pred set
proof -
case set
@@ -38,6 +38,7 @@
apply auto
done
qed
+*)
section {* Alternative rules for list_all2 *}
@@ -47,6 +48,7 @@
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
@@ -59,5 +61,5 @@
apply auto
done
qed
-
+*)
end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -55,7 +55,7 @@
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)"
-code_pred tupled_append' .
+code_pred (inductify_all) tupled_append' .
thm tupled_append'.equation
(* TODO: Missing a few modes! *)
@@ -64,7 +64,9 @@
"tupled_append'' ([], xs, xs)"
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
-code_pred tupled_append'' .
+thm tupled_append''.cases
+
+code_pred (inductify_all) tupled_append'' .
thm tupled_append''.equation
(* TODO: Missing a few modes *)
@@ -73,10 +75,19 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
-code_pred tupled_append''' .
+code_pred (inductify_all) tupled_append''' .
thm tupled_append'''.equation
(* TODO: Missing a few modes *)
+thm fst_conv snd_conv
+thm map_of.simps
+term "map_of"
+inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+where
+ "map_ofP ((a, b)#xs) a b"
+| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
+code_pred map_ofP .
+thm map_ofP.equation
section {* reverse *}
inductive rev where
@@ -420,13 +431,13 @@
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"
ML {* @{term "[x \<leftarrow> w. x = a]"} *}
code_pred (inductify_all) test .
-
+(*
theorem S\<^isub>3_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<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"
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"