--- 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
@@ -137,4 +137,57 @@
if is_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'''
+ in
+ intro''''
+ end
+
+
+
end;
--- 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,71 +17,6 @@
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 =
@@ -145,8 +80,8 @@
val _ = print_intross thy''' "Introduction rules with new constants: " intross3
val intross4 = map (maps remove_pointless_clauses) intross3
val _ = print_intross thy''' "After removing pointless clauses: " intross4
- val intross5 = burrow (map (AxClass.overload thy''')) intross4
- val intross6 = burrow (map (simplify_fst_snd o expand_tuples thy''')) intross5
+ val intross5 = map (map (AxClass.overload thy''')) intross4
+ val intross6 = burrow (map (expand_tuples thy''')) intross5
val _ = print_intross thy''' "introduction rules before registering: " intross6
val _ = print_step options "Registering introduction rules..."
val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
--- 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
@@ -592,6 +592,8 @@
([intro], elim)
end
+fun expand_tuples_elim th = th
+
fun fetch_pred_data thy name =
case try (Inductive.the_inductive (ProofContext.init thy)) name of
SOME (info as (_, result)) =>
@@ -600,17 +602,21 @@
let
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
in (fst (dest_Const const) = name) end;
- val intros = ind_set_codegen_preproc thy ((map (preprocess_intro thy))
- (filter is_intro_of (#intrs result)))
+ val intros = ind_set_codegen_preproc thy
+ (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
val nparams = length (Inductive.params_of (#raw_induct result))
- val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
+ (*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)))
+ (mk_casesrule (ProofContext.init thy) nparams intros)
val (intros, elim) = if null intros then noclause thy name elim else (intros, elim)
in
mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
end
| NONE => error ("No such predicate: " ^ quote name)
-
+
(* updaters *)
fun apfst3 f (x, y, z) = (f x, y, z)
@@ -2243,6 +2249,26 @@
forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
end
+(*
+fun check_intros_elim_match thy prednames =
+ let
+ fun check predname =
+ let
+ val intros = intros_of thy predname
+ 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)))
+ (mk_casesrule (ProofContext.init thy) nparams intros)
+ val _ = Output.tracing (Display.string_of_thm_global thy elim)
+ val _ = Output.tracing (Display.string_of_thm_global thy elim')
+ in
+ if not (Thm.equiv_thm (elim, elim')) then
+ error "Introduction and elimination rules do not match!"
+ else true
+ end
+ in forall check prednames end
+*)
(** main function of predicate compiler **)
@@ -2251,6 +2277,7 @@
let
val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+ (*val _ = check_intros_elim_match thy prednames*)
(*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 (maps (intros_of thy) prednames)
--- 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
@@ -7,7 +7,7 @@
| "even n \<Longrightarrow> odd (Suc n)"
| "odd n \<Longrightarrow> even (Suc n)"
-code_pred (mode: [], [1]) even .
+code_pred (mode: [], [1]) [show_steps, inductify] even .
thm odd.equation
thm even.equation
@@ -38,22 +38,23 @@
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) [inductify] append .
thm append.equation
-code_pred (inductify_all) (rpred) append .
+code_pred [rpred] append .
thm append.equation
thm append.rpred_equation
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
-values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
+values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
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 {* This cannot be handled correctly yet *}
(*
inductive append2
@@ -92,8 +93,8 @@
"tupled_append' ([], xs, xs)"
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)"
-
-code_pred (inductify_all) tupled_append' .
+ML {* aconv *}
+code_pred tupled_append' .
thm tupled_append'.equation
(* TODO: Modeanalysis returns mode [2] ?? *)
@@ -104,7 +105,7 @@
thm tupled_append''.cases
-code_pred (inductify_all) tupled_append'' .
+code_pred [inductify] tupled_append'' .
thm tupled_append''.equation
(* TODO: Modeanalysis returns mode [2] ?? *)
@@ -113,7 +114,7 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
-code_pred (inductify_all) tupled_append''' .
+code_pred [inductify] tupled_append''' .
thm tupled_append'''.equation
(* TODO: Missing a few modes *)
@@ -130,7 +131,7 @@
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-code_pred rev .
+code_pred (mode: [1], [2], [1, 2]) rev .
thm rev.equation
@@ -149,7 +150,7 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-code_pred partition .
+code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition .
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
for f where
@@ -197,11 +198,10 @@
case tranclp
from this converse_tranclpE[OF this(1)] show thesis by metis
qed
-(*
-code_pred (inductify_all) (rpred) tranclp .
+
+code_pred [inductify, rpred] tranclp .
thm tranclp.equation
thm tranclp.rpred_equation
-*)
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
@@ -223,8 +223,6 @@
values 20 "{(n, m). tranclp succ n m}"
*)
-subsection{* *}
-
subsection{* IMP *}
types
@@ -319,7 +317,7 @@
definition Min
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
-code_pred (inductify_all) Min .
+code_pred [inductify] Min .
subsection {* Examples with lists *}
(*
@@ -334,7 +332,7 @@
thm filterP.rpred_equation
*)
-code_pred (inductify_all) lexord .
+code_pred [inductify] lexord .
thm lexord.equation
@@ -344,20 +342,22 @@
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
-code_pred (inductify_all) lexn .
+code_pred [inductify] lexn .
thm lexn.equation
-code_pred (inductify_all) lenlex .
+code_pred [inductify] lenlex .
thm lenlex.equation
-(*
-code_pred (inductify_all) (rpred) lenlex .
+
+code_pred [inductify, rpred] lenlex .
thm lenlex.rpred_equation
-*)
+
thm lists.intros
-code_pred (inductify_all) lists .
+code_pred [inductify] lists .
thm lists.equation
+section {* AVL Tree Example *}
+
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
fun height :: "'a tree => nat" where
"height ET = 0"
@@ -369,9 +369,9 @@
"avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
-code_pred (inductify_all) avl .
+code_pred [inductify] avl .
thm avl.equation
-(*
+
fun set_of
where
"set_of ET = {}"
@@ -383,11 +383,10 @@
"is_ord ET = True"
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-ML {* *}
-code_pred (inductify_all) set_of .
+code_pred [inductify] set_of .
thm set_of.equation
-*)
+
text {* expected mode: [1], [1, 2] *}
(* FIXME *)
(*
@@ -396,50 +395,47 @@
*)
section {* Definitions about Relations *}
-code_pred (inductify_all) converse .
+code_pred [inductify] converse .
thm converse.equation
-code_pred (inductify_all) Domain .
+code_pred [inductify] Domain .
thm Domain.equation
section {* List functions *}
-code_pred (inductify_all) length .
+code_pred [inductify] length .
thm size_listP.equation
-code_pred (inductify_all) concat .
+code_pred [inductify] concat .
thm concatP.equation
-code_pred (inductify_all) hd .
-code_pred (inductify_all) tl .
-code_pred (inductify_all) last .
-code_pred (inductify_all) butlast .
-(*code_pred (inductify_all) listsum .*)
-code_pred (inductify_all) take .
-code_pred (inductify_all) drop .
-code_pred (inductify_all) zip .
-code_pred (inductify_all) upt .
-code_pred set sorry
-code_pred (inductify_all) remdups .
-code_pred (inductify_all) remove1 .
-code_pred (inductify_all) removeAll .
-code_pred (inductify_all) distinct .
-code_pred (inductify_all) replicate .
-code_pred (inductify_all) splice .
-code_pred (inductify_all) List.rev .
-thm revP.equation
-
-code_pred (inductify_all) foldl .
-thm foldlP.equation
-
-code_pred (inductify_all) filter .
+code_pred [inductify] hd .
+code_pred [inductify] tl .
+code_pred [inductify] last .
+code_pred [inductify] butlast .
+thm listsum.simps
+(*code_pred [inductify] listsum .*)
+code_pred [inductify] take .
+code_pred [inductify] drop .
+code_pred [inductify] zip .
+code_pred [inductify] upt .
+code_pred [inductify] remdups .
+code_pred [inductify] remove1 .
+code_pred [inductify] removeAll .
+code_pred [inductify] distinct .
+code_pred [inductify] replicate .
+code_pred [inductify] splice .
+code_pred [inductify] List.rev .
+code_pred [inductify] foldr .
+code_pred [inductify] foldl .
+code_pred [inductify] filter .
definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs"
-term "one_nat_inst.one_nat"
-code_pred (inductify_all) test .
+(*
+TODO: implement higher-order replacement correctly
+code_pred [inductify] test .
thm testP.equation
-(*
-code_pred (inductify_all) (rpred) test .
+code_pred [inductify, rpred] test .
*)
section {* Handling set operations *}
@@ -457,7 +453,7 @@
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
-code_pred (inductify_all) S\<^isub>1p .
+code_pred [inductify] S\<^isub>1p .
thm S\<^isub>1p.equation
(*
@@ -473,10 +469,12 @@
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
-(*
-code_pred (inductify_all) (rpred) S\<^isub>2 .
-ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name "B\<^isub>2"} *}
-*)
+
+code_pred [inductify, rpred] S\<^isub>2 .
+thm S\<^isub>2.rpred_equation
+thm A\<^isub>2.rpred_equation
+thm B\<^isub>2.rpred_equation
+
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]*)
@@ -491,7 +489,7 @@
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
-code_pred (inductify_all) S\<^isub>3 .
+code_pred [inductify] S\<^isub>3 .
theorem S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
@@ -598,21 +596,6 @@
lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T"
quickcheck[generator = pred_compile, size = 10, iterations = 100]
oops
-(* FIXME *)
-
-inductive test' for P where
-"[| filter P vs = res |]
-==> test' P vs res"
-
-code_pred (inductify_all) test' .
-thm test'.equation
-
-(*
-export_code test_for_1_yields_1_2 in SML file -
-code_pred (inductify_all) (rpred) test .
-
-thm test.equation
-*)
lemma filter_eq_ConsD:
"filter P ys = x#xs \<Longrightarrow>