author | wenzelm |
Thu, 30 May 2013 12:35:40 +0200 | |
changeset 52230 | 1105b3b5aa77 |
parent 52131 | 366fa32ee2a3 |
child 54742 | 7a86358a3c0b |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_pred.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
|
33265 | 4 |
Preprocessing definitions of predicates to introduction rules. |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
5 |
*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_PRED = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
sig |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
(* preprocesses an equation to a set of intro rules; defines new constants *) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
10 |
val preprocess : Predicate_Compile_Aux.options -> (string * thm list) -> theory |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
11 |
-> ((string * thm list) list * theory) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
12 |
val flat_higher_order_arguments : ((string * thm list) list * theory) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
13 |
-> ((string * thm list) list * ((string * thm list) list * theory)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
14 |
end; |
33265 | 15 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
16 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
17 |
structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
18 |
struct |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
open Predicate_Compile_Aux |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
|
50056 | 22 |
fun is_compound ((Const (@{const_name Not}, _)) $ _) = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
error "is_compound: Negation should not occur; preprocessing is defect" |
38558 | 24 |
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38558
diff
changeset
|
25 |
| is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38558
diff
changeset
|
26 |
| is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
27 |
error "is_compound: Conjunction should not occur; preprocessing is defect" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
28 |
| is_compound _ = false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
29 |
|
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
30 |
fun try_destruct_case thy names atom = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
31 |
case find_split_thm thy (fst (strip_comb atom)) of |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
32 |
NONE => NONE |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
33 |
| SOME raw_split_thm => |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
34 |
let |
42361 | 35 |
val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
36 |
(* TODO: contextify things - this line is to unvarify the split_thm *) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
37 |
(*val ((_, [isplit_thm]), _) = |
42361 | 38 |
Variable.import true [split_thm] (Proof_Context.init_global thy)*) |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
39 |
val (assms, concl) = Logic.strip_horn (prop_of split_thm) |
50056 | 40 |
val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) |
39802
7cadad6a18cc
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
bulwahn
parents:
39787
diff
changeset
|
41 |
val atom' = case_betapply thy atom |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
42 |
val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
43 |
val names' = Term.add_free_names atom' names |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
44 |
fun mk_subst_rhs assm = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
45 |
let |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
46 |
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
47 |
val var_names = Name.variant_list names' (map fst vTs) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
48 |
val vars = map Free (var_names ~~ (map snd vTs)) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
49 |
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
50 |
fun partition_prem_subst prem = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
51 |
case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
52 |
(Free (x, T), r) => (NONE, SOME ((x, T), r)) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
53 |
| _ => (SOME prem, NONE) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
54 |
fun partition f xs = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
55 |
let |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
56 |
fun partition' acc1 acc2 [] = (rev acc1, rev acc2) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
57 |
| partition' acc1 acc2 (x :: xs) = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
58 |
let |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
59 |
val (y, z) = f x |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
60 |
val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1 |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
61 |
val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2 |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
62 |
in partition' acc1' acc2' xs end |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
63 |
in partition' [] [] xs end |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
64 |
val (prems'', subst) = partition partition_prem_subst prems' |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
65 |
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
66 |
val pre_rhs = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
67 |
fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
68 |
val rhs = Envir.expand_term_frees subst pre_rhs |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
69 |
in |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
70 |
case try_destruct_case thy (var_names @ names') rhs of |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
71 |
NONE => [(subst, rhs)] |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
72 |
| SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
73 |
end |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
74 |
in SOME (atom', maps mk_subst_rhs assms) end |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
75 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
fun flatten constname atom (defs, thy) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
77 |
if is_compound atom then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
78 |
let |
52131 | 79 |
val atom = Envir.beta_norm (Envir.eta_long [] atom) |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
80 |
val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
81 |
((Long_Name.base_name constname) ^ "_aux") |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
val full_constname = Sign.full_bname thy constname |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
val (params, args) = List.partition (is_predT o fastype_of) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
84 |
(map Free (Term.add_frees atom [])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
85 |
val constT = map fastype_of (params @ args) ---> HOLogic.boolT |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
86 |
val lhs = list_comb (Const (full_constname, constT), params @ args) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
val def = Logic.mk_equals (lhs, atom) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
88 |
val ([definition], thy') = thy |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
89 |
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |
46909 | 90 |
|> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
91 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
92 |
(lhs, ((full_constname, [definition]) :: defs, thy')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
93 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
94 |
else |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35897
diff
changeset
|
95 |
case (fst (strip_comb atom)) of |
37908
05bf021b093c
putting proof in the right context; adding if rewriting; tuned
bulwahn
parents:
36610
diff
changeset
|
96 |
(Const (@{const_name If}, _)) => |
05bf021b093c
putting proof in the right context; adding if rewriting; tuned
bulwahn
parents:
36610
diff
changeset
|
97 |
let |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
98 |
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39802
diff
changeset
|
99 |
val atom' = Raw_Simplifier.rewrite_term thy |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
100 |
(map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom |
42816
ba14eafef077
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents:
42361
diff
changeset
|
101 |
val _ = @{assert} (not (atom = atom')) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
102 |
in |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
103 |
flatten constname atom' (defs, thy) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
104 |
end |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35897
diff
changeset
|
105 |
| _ => |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
106 |
case try_destruct_case thy [] atom of |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35897
diff
changeset
|
107 |
NONE => (atom, (defs, thy)) |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
108 |
| SOME (atom', srs) => |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
109 |
let |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
110 |
val frees = map Free (Term.add_frees atom' []) |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
111 |
val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
112 |
((Long_Name.base_name constname) ^ "_aux") |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
113 |
val full_constname = Sign.full_bname thy constname |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
114 |
val constT = map fastype_of frees ---> HOLogic.boolT |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
115 |
val lhs = list_comb (Const (full_constname, constT), frees) |
39723
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
116 |
fun mk_def (subst, rhs) = |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
117 |
Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs) |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
118 |
val new_defs = map mk_def srs |
12cc713036d6
handling nested cases more elegant by requiring less new constants
bulwahn
parents:
39557
diff
changeset
|
119 |
val (definition, thy') = thy |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
120 |
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |
35897
8758895ea413
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
wenzelm
parents:
35882
diff
changeset
|
121 |
|> fold_map Specification.axiom (map_index |
8758895ea413
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
wenzelm
parents:
35882
diff
changeset
|
122 |
(fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
123 |
in |
35897
8758895ea413
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
wenzelm
parents:
35882
diff
changeset
|
124 |
(lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy')) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
125 |
end |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35897
diff
changeset
|
126 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
127 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
128 |
fun flatten_intros constname intros thy = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
129 |
let |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
130 |
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
131 |
val ((_, intros), ctxt') = Variable.import true intros ctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
132 |
val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
133 |
(flatten constname) (map prop_of intros) ([], thy) |
42361 | 134 |
val ctxt'' = Proof_Context.transfer thy' ctxt' |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
135 |
val intros'' = |
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
136 |
map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros' |
37908
05bf021b093c
putting proof in the right context; adding if rewriting; tuned
bulwahn
parents:
36610
diff
changeset
|
137 |
|> Variable.export ctxt'' ctxt |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
138 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
139 |
(intros'', (local_defs, thy')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
140 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
141 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
142 |
(* TODO: same function occurs in inductive package *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
143 |
fun select_disj 1 1 = [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
144 |
| select_disj _ 1 = [rtac @{thm disjI1}] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
145 |
| select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1)); |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
146 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
147 |
fun introrulify thy ths = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
148 |
let |
42361 | 149 |
val ctxt = Proof_Context.init_global thy |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
150 |
val ((_, ths'), ctxt') = Variable.import true ths ctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
151 |
fun introrulify' th = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
152 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
153 |
val (lhs, rhs) = Logic.dest_equals (prop_of th) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
154 |
val frees = Term.add_free_names rhs [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
155 |
val disjuncts = HOLogic.dest_disj rhs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
156 |
val nctxt = Name.make_context frees |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
157 |
fun mk_introrule t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
158 |
let |
50056 | 159 |
val ((ps, t'), _) = focus_ex t nctxt |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
160 |
val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
161 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
162 |
(ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
163 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
164 |
val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
165 |
Logic.dest_implies o prop_of) @{thm exI} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
166 |
fun prove_introrule (index, (ps, introrule)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
167 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
168 |
val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
169 |
THEN EVERY1 (select_disj (length disjuncts) (index + 1)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
170 |
THEN (EVERY (map (fn y => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
171 |
rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
172 |
THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
173 |
THEN TRY (atac 1) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
174 |
in |
33441
99a5f22a967d
eliminated funny record patterns and made SML/NJ happy;
wenzelm
parents:
33403
diff
changeset
|
175 |
Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
176 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
177 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
178 |
map_index prove_introrule (map mk_introrule disjuncts) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
179 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
180 |
in maps introrulify' ths' |> Variable.export ctxt' ctxt end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
181 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
182 |
fun rewrite ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
183 |
Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm Ball_def}, @{thm Bex_def}]) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
184 |
#> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
185 |
#> Conv.fconv_rule (nnf_conv ctxt) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
186 |
#> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}]) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
187 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
188 |
fun rewrite_intros thy = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
189 |
Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [@{thm all_not_ex}]) |
38952
694d0c88d86a
avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler
bulwahn
parents:
38795
diff
changeset
|
190 |
#> Simplifier.full_simplify |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
191 |
(Simplifier.global_context thy HOL_basic_ss |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
192 |
addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) |
42361 | 193 |
#> split_conjuncts_in_assms (Proof_Context.init_global thy) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
194 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
195 |
fun print_specs options thy msg ths = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
196 |
if show_intermediate_results options then |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
197 |
(tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
198 |
else |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
199 |
() |
39787
a44f6b11cdc4
adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
bulwahn
parents:
39723
diff
changeset
|
200 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
201 |
fun preprocess options (constname, specs) thy = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
202 |
(* case Predicate_Compile_Data.processed_specs thy constname of |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
203 |
SOME specss => (specss, thy) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
204 |
| NONE =>*) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
205 |
let |
42361 | 206 |
val ctxt = Proof_Context.init_global thy |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
207 |
val intros = |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
208 |
if forall is_pred_equation specs then |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
209 |
map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs)) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
210 |
else if forall (is_intro constname) specs then |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
211 |
map (rewrite_intros thy) specs |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
212 |
else |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
213 |
error ("unexpected specification for constant " ^ quote constname ^ ":\n" |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
214 |
^ commas (map (quote o Display.string_of_thm_global thy) specs)) |
37908
05bf021b093c
putting proof in the right context; adding if rewriting; tuned
bulwahn
parents:
36610
diff
changeset
|
215 |
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} |
52230 | 216 |
val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
217 |
val _ = print_specs options thy "normalized intros" intros |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
218 |
(*val intros = maps (split_cases thy) intros*) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
219 |
val (intros', (local_defs, thy')) = flatten_intros constname intros thy |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
220 |
val (intross, thy'') = fold_map (preprocess options) local_defs thy' |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
221 |
val full_spec = (constname, intros') :: flat intross |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
222 |
(*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
223 |
in |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
224 |
(full_spec, thy'') |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
225 |
end; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
226 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
227 |
fun flat_higher_order_arguments (intross, thy) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
228 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
229 |
fun process constname atom (new_defs, thy) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
230 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
231 |
val (pred, args) = strip_comb atom |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
232 |
fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
233 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
234 |
val vars = map Var (Term.add_vars abs_arg []) |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
235 |
val abs_arg' = Logic.unvarify_global abs_arg |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
236 |
val frees = map Free (Term.add_frees abs_arg' []) |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
237 |
val constname = |
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
238 |
singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs)) |
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
239 |
((Long_Name.base_name constname) ^ "_hoaux") |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
240 |
val full_constname = Sign.full_bname thy constname |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
241 |
val constT = map fastype_of frees ---> (fastype_of abs_arg') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
242 |
val const = Const (full_constname, constT) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
243 |
val lhs = list_comb (const, frees) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
244 |
val def = Logic.mk_equals (lhs, abs_arg') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
245 |
val ([definition], thy') = thy |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
246 |
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |
46909 | 247 |
|> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
248 |
in |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
249 |
(list_comb (Logic.varify_global const, vars), |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
250 |
((full_constname, [definition])::new_defs, thy')) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
251 |
end |
33403
a9b6497391b0
recursively replacing abstractions by new definitions in the predicate compiler
bulwahn
parents:
33375
diff
changeset
|
252 |
| replace_abs_arg arg (new_defs, thy) = |
39468
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
253 |
if is_some (try HOLogic.dest_prodT (fastype_of arg)) then |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
254 |
(case try HOLogic.dest_prod arg of |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
255 |
SOME (t1, t2) => |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
256 |
(new_defs, thy) |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
257 |
|> process constname t1 |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
258 |
||>> process constname t2 |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
259 |
|>> HOLogic.mk_prod |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
260 |
| NONE => (warning ("Replacing higher order arguments " ^ |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
261 |
"is not applied in an undestructable product type"); (arg, (new_defs, thy)))) |
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
262 |
else if (is_predT (fastype_of arg)) then |
33403
a9b6497391b0
recursively replacing abstractions by new definitions in the predicate compiler
bulwahn
parents:
33375
diff
changeset
|
263 |
process constname arg (new_defs, thy) |
a9b6497391b0
recursively replacing abstractions by new definitions in the predicate compiler
bulwahn
parents:
33375
diff
changeset
|
264 |
else |
a9b6497391b0
recursively replacing abstractions by new definitions in the predicate compiler
bulwahn
parents:
33375
diff
changeset
|
265 |
(arg, (new_defs, thy)) |
39468
3cb3b1668c5d
improving replacing higher order arguments to work with tuples
bulwahn
parents:
38952
diff
changeset
|
266 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
267 |
val (args', (new_defs', thy')) = fold_map replace_abs_arg |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
268 |
(map Envir.beta_eta_contract args) (new_defs, thy) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
269 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
270 |
(list_comb (pred, args'), (new_defs', thy')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
271 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
272 |
fun flat_intro intro (new_defs, thy) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
273 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
274 |
val constname = fst (dest_Const (fst (strip_comb |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
275 |
(HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro)))))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
276 |
val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
277 |
val th = Skip_Proof.make_thm thy intro_ts |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
278 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
279 |
(th, (new_defs, thy)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
280 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
281 |
fun fold_map_spec f [] s = ([], s) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
282 |
| fold_map_spec f ((c, ths) :: specs) s = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
283 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
284 |
val (ths', s') = f ths s |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
285 |
val (specs', s'') = fold_map_spec f specs s' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
286 |
in ((c, ths') :: specs', s'') end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
287 |
val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
288 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
289 |
(intross', (new_defs, thy')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
290 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
291 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
292 |
end; |