--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 10:59:25 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 14:32:45 2014 +0100
@@ -11,11 +11,11 @@
val keep_function : theory -> string -> bool
val processed_specs : theory -> string -> (string * thm list) list option
val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
-
+
val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
val obtain_specification_graph :
Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
-
+
val present_graph : thm list Term_Graph.T -> unit
val normalize_equation : theory -> thm -> thm
end;
@@ -66,7 +66,7 @@
let
val _ $ u = Logic.strip_imp_concl t
in fst (strip_comb u) end
-(*
+(*
in case pred of
Const (c, T) => c
| _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
@@ -75,9 +75,9 @@
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
fun defining_const_of_introrule th =
- case defining_term_of_introrule th
- of Const (c, _) => c
- | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+ (case defining_term_of_introrule th of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th]))
(*TODO*)
fun is_introlike_term _ = true
@@ -85,29 +85,29 @@
val is_introlike = is_introlike_term o prop_of
fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
- (case strip_comb u of
- (Const (_, T), args) =>
- if (length (binder_types T) = length args) then
- true
- else
- raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
- | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+ (case strip_comb u of
+ (Const (_, T), args) =>
+ if (length (binder_types T) = length args) then
+ true
+ else
+ raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+ | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
| check_equation_format_term t =
- raise TERM ("check_equation_format_term failed: Not an equation", [t])
+ raise TERM ("check_equation_format_term failed: Not an equation", [t])
val check_equation_format = check_equation_format_term o prop_of
fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
| defining_term_of_equation_term t =
- raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+ raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
val defining_term_of_equation = defining_term_of_equation_term o prop_of
fun defining_const_of_equation th =
- case defining_term_of_equation th
- of Const (c, _) => c
- | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
+ (case defining_term_of_equation th of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]))
@@ -115,9 +115,10 @@
(* Normalizing equations *)
fun mk_meta_equation th =
- case prop_of th of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
- | _ => th
+ (case prop_of th of
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) =>
+ th RS @{thm eq_reflection}
+ | _ => th)
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -131,13 +132,13 @@
let
val res = Name.invent_names ctxt s xs
in (res, fold Name.declare (map fst res) ctxt) end
-
+
fun split_all_pairs thy th =
let
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val ((_, [th']), _) = Variable.import true [th] ctxt
val t = prop_of th'
- val frees = Term.add_frees t []
+ val frees = Term.add_frees t []
val freenames = Term.add_free_names t []
val nctxt = Name.make_context freenames
fun mk_tuple_rewrites (x, T) nctxt =
@@ -146,7 +147,7 @@
val (xTs, nctxt') = declare_names x Ts nctxt
val paths = HOLogic.flat_tupleT_paths T
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
- val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
+ val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
val t' = Pattern.rewrite_term thy rewr [] t
val th'' =
Goal.prove ctxt (Term.add_free_names t' []) [] t'
@@ -162,7 +163,7 @@
val ctxt = Proof_Context.init_global thy
val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
- (*val _ = print_step options
+ (*val _ = print_step options
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
@@ -206,11 +207,13 @@
else
NONE
fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
- val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
- [] => (case Spec_Rules.retrieve ctxt t of
- [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
- | ((_, (_, ths)) :: _) => filter_defs ths)
- | ths => rev ths
+ val spec =
+ (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+ [] =>
+ (case Spec_Rules.retrieve ctxt t of
+ [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
+ | ((_, (_, ths)) :: _) => filter_defs ths)
+ | ths => rev ths)
val _ =
if show_intermediate_results options then
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
@@ -221,38 +224,38 @@
end
val logic_operator_names =
- [@{const_name "=="},
+ [@{const_name "=="},
@{const_name "==>"},
@{const_name Trueprop},
@{const_name Not},
@{const_name HOL.eq},
@{const_name HOL.implies},
@{const_name All},
- @{const_name Ex},
+ @{const_name Ex},
@{const_name HOL.conj},
@{const_name HOL.disj}]
-fun special_cases (c, _) = member (op =) [
- @{const_name Product_Type.Unity},
- @{const_name False},
- @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
- @{const_name Nat.one_nat_inst.one_nat},
- @{const_name Orderings.less}, @{const_name Orderings.less_eq},
- @{const_name Groups.zero},
- @{const_name Groups.one}, @{const_name Groups.plus},
- @{const_name Nat.ord_nat_inst.less_eq_nat},
- @{const_name Nat.ord_nat_inst.less_nat},
-(* FIXME
- @{const_name number_nat_inst.number_of_nat},
-*)
- @{const_name Num.Bit0},
- @{const_name Num.Bit1},
- @{const_name Num.One},
- @{const_name Int.zero_int_inst.zero_int},
- @{const_name List.filter},
- @{const_name HOL.If},
- @{const_name Groups.minus}
- ] c
+fun special_cases (c, _) =
+ member (op =)
+ [@{const_name Product_Type.Unity},
+ @{const_name False},
+ @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
+ @{const_name Nat.one_nat_inst.one_nat},
+ @{const_name Orderings.less}, @{const_name Orderings.less_eq},
+ @{const_name Groups.zero},
+ @{const_name Groups.one}, @{const_name Groups.plus},
+ @{const_name Nat.ord_nat_inst.less_eq_nat},
+ @{const_name Nat.ord_nat_inst.less_nat},
+ (* FIXME
+ @{const_name number_nat_inst.number_of_nat},
+ *)
+ @{const_name Num.Bit0},
+ @{const_name Num.Bit1},
+ @{const_name Num.One},
+ @{const_name Int.zero_int_inst.zero_int},
+ @{const_name List.filter},
+ @{const_name HOL.If},
+ @{const_name Groups.minus}] c
fun obtain_specification_graph options thy t =
@@ -309,13 +312,12 @@
|> map (the o Termtab.lookup mapping)
|> distinct (eq_list eq_cname);
val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-
+
fun namify consts = map string_of_const consts
|> commas;
val prgr = map (fn (consts, constss) =>
- { name = namify consts, ID = namify consts, dir = "", unfold = true,
- path = "", parents = map namify constss, content = [] }) conn;
- in Graph_Display.display_graph prgr end;
+ {name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss, content = [] }) conn
+ in Graph_Display.display_graph prgr end
-
-end;
+end