--- a/NEWS Wed Nov 17 13:38:53 2010 +0100
+++ b/NEWS Wed Nov 17 13:39:30 2010 +0100
@@ -355,6 +355,9 @@
cvc3_options
yices_options
+* Boogie output files (.b2i files) need to be declared in the
+theory header.
+
* Removed [split_format ... and ... and ...] version of
[split_format]. Potential INCOMPATIBILITY.
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Nov 17 13:39:30 2010 +0100
@@ -80,7 +80,7 @@
*}
-boogie_open "Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra.b2i"
declare [[smt_certificates="Boogie_Dijkstra.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Nov 17 13:39:30 2010 +0100
@@ -37,7 +37,7 @@
\end{verbatim}
*}
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
declare [[smt_certificates="Boogie_Max.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Wed Nov 17 13:39:30 2010 +0100
@@ -37,7 +37,7 @@
\end{verbatim}
*}
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
boogie_status -- {* gives an overview of all verification conditions *}
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Wed Nov 17 13:39:30 2010 +0100
@@ -45,7 +45,7 @@
\end{verbatim}
*}
-boogie_open (quiet) "VCC_Max"
+boogie_open (quiet) "VCC_Max.b2i"
declare [[smt_certificates="VCC_Max.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Wed Nov 17 13:39:30 2010 +0100
@@ -17,8 +17,11 @@
fun boogie_open ((quiet, base_name), offsets) thy =
let
val ext = "b2i"
- fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
- val base_path = add_ext (Path.explode base_name)
+ fun check_ext path = snd (Path.split_ext path) = ext orelse
+ error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^
+ "expected file ending " ^ quote ext)
+
+ val base_path = Path.explode base_name |> tap check_ext
val (full_path, _) =
Thy_Load.check_file [Thy_Load.master_directory thy] base_path
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Nov 17 13:39:30 2010 +0100
@@ -25,6 +25,7 @@
val monomorph_limit: int Config.T
val drop_bad_facts: bool Config.T
val filter_only_facts: bool Config.T
+ val debug_files: string Config.T
(*tools*)
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -131,6 +132,10 @@
val (filter_only_facts, setup_filter_only_facts) =
Attrib.config_bool filter_only_factsN (K false)
+val debug_filesN = "smt_debug_files"
+val (debug_files, setup_debug_files) =
+ Attrib.config_string debug_filesN (K "")
+
val setup_options =
setup_oracle #>
setup_datatypes #>
@@ -141,7 +146,8 @@
setup_monomorph_limit #>
setup_drop_bad_facts #>
setup_filter_only_facts #>
- setup_trace_used_facts
+ setup_trace_used_facts #>
+ setup_debug_files
(* diagnostics *)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 17 13:39:30 2010 +0100
@@ -162,10 +162,12 @@
addsimps [@{thm Nat_Numeral.int_nat_number_of}]
addsimps @{thms neg_simps}
+ val int_eq = Thm.cterm_of @{theory} @{const "==" (int)}
+
fun cancel_int_nat_simproc _ ss ct =
let
val num = Thm.dest_arg (Thm.dest_arg ct)
- val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
+ val goal = Thm.mk_binop int_eq ct num
val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
fun tac _ = Simplifier.simp_tac simpset 1
in on_positive num (Goal.prove_internal [] goal) tac end
@@ -180,8 +182,8 @@
fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
- val uses_nat_int =
- Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
+ val uses_nat_int = Term.exists_subterm (member (op aconv)
+ [@{const of_nat (int)}, @{const nat}])
in
fun nat_as_int ctxt =
map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
@@ -285,7 +287,7 @@
fun norm_def ctxt thm =
(case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
+ @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def ctxt (thm RS @{thm fun_cong})
| Const (@{const_name "=="}, _) $ _ $ Abs _ =>
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
@@ -293,7 +295,7 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{term "op ==>"} $ _ $ _ =>
+ @{const "==>"} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
| Const (@{const_name "=="}, _) $ _ $ _ =>
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 13:39:30 2010 +0100
@@ -63,7 +63,7 @@
(* Z3 builtins *)
local
- fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
+ fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
| z3_builtin_fun _ _ = NONE
in
@@ -86,13 +86,13 @@
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
else NONE
- val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
- val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
- val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
- val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
- val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
- val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
- val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
+ val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
+ val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
+ val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
+ val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
+ val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
+ val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
+ val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 13:39:30 2010 +0100
@@ -108,7 +108,17 @@
fun run ctxt cmd args input =
(case C.certificates_of ctxt of
- NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+ NONE =>
+ if Config.get ctxt C.debug_files = "" then
+ Cache_IO.run (make_cmd (choose cmd) args) input
+ else
+ let
+ val base_path = Path.explode (Config.get ctxt C.debug_files)
+ val in_path = Path.ext "smt_in" base_path
+ val out_path = Path.ext "smt_out" base_path
+ in
+ Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path
+ end
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
@@ -254,6 +264,8 @@
in
raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
end)
+
+ val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
in
fun add_solver cfg =
@@ -261,7 +273,7 @@
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
reconstruct} = cfg
- fun core_oracle () = @{cprop False}
+ fun core_oracle () = cfalse
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
interface=interface,
@@ -302,6 +314,8 @@
"contains the universal sort {}"))
else solver_of ctxt rm ctxt irules
+val cnot = Thm.cterm_of @{theory} @{const Not}
+
fun smt_filter run_remote time_limit st xrules i =
let
val {facts, goal, ...} = Proof.goal st
@@ -312,10 +326,8 @@
|> Config.put C.drop_bad_facts true
|> Config.put C.filter_only_facts true
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
- val cprop =
- concl
- |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
- |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+ fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+ val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 13:39:30 2010 +0100
@@ -134,7 +134,7 @@
| (ps, [false]) => cons (SNoPat ps)
| _ => raise TERM ("dest_pats", ts))
-fun dest_trigger (@{term trigger} $ tl $ t) =
+fun dest_trigger (@{const trigger} $ tl $ t) =
(rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
| dest_trigger t = ([], t)
@@ -161,8 +161,8 @@
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
Const (@{const_name Let}, _) => true
- | @{term "op = :: bool => _"} $ _ $ @{term True} => true
- | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+ | @{const HOL.eq (bool)} $ _ $ @{const True} => true
+ | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
| _ => false)
val rewrite_rules = [
@@ -199,11 +199,11 @@
fun conn (n, T) = (n, mapTs as_propT as_propT T)
fun pred (n, T) = (n, mapTs I as_propT T)
- val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
- fun as_term t = Const term_eq $ t $ @{term True}
+ val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
+ fun as_term t = Const term_eq $ t $ @{const True}
val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
- fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+ fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
@@ -225,7 +225,7 @@
and in_pats ps =
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
- and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+ and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
| in_trig t = in_form t
and in_form t =
--- a/src/HOL/Tools/SMT/smt_word.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_word.ML Wed Nov 17 13:39:30 2010 +0100
@@ -60,7 +60,7 @@
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
| dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
- fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+ fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
| dest_nat ts = raise TERM ("dest_nat", ts)
fun dest_nat_word_funT (T, ts) =
(dest_word_funT (Term.range_type T), dest_nat ts)
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 13:39:30 2010 +0100
@@ -70,8 +70,8 @@
val {is_builtin_pred, ...}= the strict
val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
- fun is_int_div_mod @{term "op div :: int => _"} = true
- | is_int_div_mod @{term "op mod :: int => _"} = true
+ fun is_int_div_mod @{const div (int)} = true
+ | is_int_div_mod @{const mod (int)} = true
| is_int_div_mod _ = false
fun add_div_mod irules =
@@ -170,11 +170,13 @@
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
-val mk_true = @{cterm "~False"}
-val mk_false = @{cterm False}
-val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm HOL.implies}
-val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
+val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{theory} @{const False}
+val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{theory} @{const HOL.conj}
+val disj = Thm.cterm_of @{theory} @{const HOL.disj}
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -205,22 +207,22 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
-val mk_uminus = Thm.capply @{cterm "uminus :: int => _"}
-val mk_add = Thm.mk_binop @{cterm "op + :: int => _"}
-val mk_sub = Thm.mk_binop @{cterm "op - :: int => _"}
-val mk_mul = Thm.mk_binop @{cterm "op * :: int => _"}
-val mk_div = Thm.mk_binop @{cterm "z3div :: int => _"}
-val mk_mod = Thm.mk_binop @{cterm "z3mod :: int => _"}
-val mk_lt = Thm.mk_binop @{cterm "op < :: int => _"}
-val mk_le = Thm.mk_binop @{cterm "op <= :: int => _"}
+val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
+val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)})
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_model.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Wed Nov 17 13:39:30 2010 +0100
@@ -115,7 +115,7 @@
fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
val (default_int, ints) =
- (case find_first (match [@{term int}]) vs of
+ (case find_first (match [@{const of_nat (int)}]) vs of
NONE => (NONE, [])
| SOME (_, cases) =>
let val (cs, (_, e)) = split_last cases
@@ -138,7 +138,7 @@
| SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
in
map subst_nats vs
- |> filter_out (match [@{term int}, @{term nat}])
+ |> filter_out (match [@{const of_nat (int)}, @{const nat}])
end
fun filter_valid_valuations terms = map_filter (fn
@@ -179,8 +179,8 @@
fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
-fun trans_expr _ True = pair @{term True}
- | trans_expr _ False = pair @{term False}
+fun trans_expr _ True = pair @{const True}
+ | trans_expr _ False = pair @{const False}
| trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
| trans_expr T (Number (i, SOME j)) =
pair (Const (@{const_name divide}, [T, T] ---> T) $
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Nov 17 13:39:30 2010 +0100
@@ -22,6 +22,7 @@
val is_conj: term -> bool
val is_disj: term -> bool
val exists_lit: bool -> (term -> bool) -> term -> bool
+ val negate: cterm -> cterm
(* proof tools *)
val explode: bool -> bool -> bool -> term list -> thm -> thm list
@@ -59,19 +60,19 @@
(** properties and term operations **)
-val is_neg = (fn @{term Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
+val is_neg = (fn @{const Not} $ _ => true | _ => false)
+fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
fun dest_disj_term' f = (fn
- @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
+ @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
| _ => NONE)
-val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
val dest_disj_term =
- dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
+ dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
fun exists_lit is_conj P =
let
@@ -82,6 +83,8 @@
| NONE => false)
in exists end
+val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+
(** proof tools **)
@@ -135,7 +138,7 @@
end
| NONE => add (t, rev rules))
- fun explode0 (@{term Not} $ (@{term Not} $ t)) =
+ fun explode0 (@{const Not} $ (@{const Not} $ t)) =
Termtab.make [(t, [dneg_rule])]
| explode0 t = explode1 [] t Termtab.empty
@@ -202,23 +205,23 @@
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
- fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
+ fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
| dest_conj t = raise TERM ("dest_conj", [t])
- val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
+ val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t))
+ fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
- fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
+ fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
fun dni f = apsnd f o Thm.dest_binop o f o d1
val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
- val iff_const = @{term "op = :: bool => _"}
- fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
- f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
+ val iff_const = @{const HOL.eq (bool)}
+ fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
+ f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
| as_negIff _ _ = NONE
in
@@ -231,12 +234,12 @@
fun lookup_rule t =
(case t of
- @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
- | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
- (T.compose negIffI, lookup (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
+ @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+ | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
+ (T.compose negIffI, lookup (iff_const $ u $ t))
+ | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
- in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
+ in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
| _ =>
(case as_dneg lookup t of
NONE => (T.compose negIffE, as_negIff lookup t)
@@ -264,11 +267,10 @@
val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
- val neg = Thm.capply @{cterm Not}
in
-fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
+fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
+fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2
+fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3
end
@@ -279,10 +281,10 @@
val rules = explode_term conj (T.prop_of thm)
fun contra_lits (t, rs) =
(case t of
- @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
+ @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
| _ => NONE)
in
- (case Termtab.lookup rules @{term False} of
+ (case Termtab.lookup rules @{const False} of
SOME rs => extract_lit thm rs
| NONE =>
the (Termtab.get_first contra_lits rules)
@@ -322,8 +324,9 @@
let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
in
(case (kind_of (Thm.term_of cl), Thm.term_of cr) of
- (SOME CONJ, @{term False}) => contradict true cl
- | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
+ (SOME CONJ, @{const False}) => contradict true cl
+ | (SOME DISJ, @{const Not} $ @{const False}) =>
+ contrapos2 (contradict false o fst) cp
| (kl, _) =>
(case (kl, kind_of (Thm.term_of cr)) of
(SOME CONJ, SOME CONJ) => prove_eq true true cp
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Nov 17 13:39:30 2010 +0100
@@ -113,10 +113,11 @@
fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
fun close ctxt (ct, vars) =
let
val inst = mk_inst ctxt vars
- val mk_prop = Thm.capply @{cterm Trueprop}
val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
@@ -182,6 +183,8 @@
(* parser context *)
+val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+
fun make_context ctxt typs terms =
let
val ctxt' =
@@ -189,7 +192,7 @@
|> Symtab.fold (Variable.declare_typ o snd) typs
|> Symtab.fold (Variable.declare_term o snd) terms
- fun cert @{term True} = @{cterm "~False"}
+ fun cert @{const True} = not_false
| cert t = certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
@@ -357,8 +360,10 @@
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+val ctrue = Thm.cterm_of @{theory} @{const True}
+
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
- (the o mk_fun (K (SOME @{cterm True})))) st
+ (the o mk_fun (K (SOME ctrue)))) st
fun quant_kind st = st |> (
this "forall" >> K (mk_forall o theory_of) ||
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 17 13:39:30 2010 +0100
@@ -231,7 +231,7 @@
in
fun lemma thm ct =
let
- val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ val cu = L.negate (Thm.dest_arg ct)
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
end
@@ -243,7 +243,7 @@
val explode_disj = L.explode false true false
val join_disj = L.join false
fun unit thm thms th =
- let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
+ let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -251,7 +251,7 @@
val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
in
fun unit_resolution thm thms ct =
- Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ L.negate (Thm.dest_arg ct)
|> T.under_assumption (unit thm thms)
|> Thm o T.discharge thm o T.compose contrapos
end
@@ -295,14 +295,14 @@
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
in
(case Thm.term_of ct1 of
- @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
+ @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term HOL.conj} $ _ $ _ =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term HOL.disj} $ _ $ _ =>
- prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
+ | @{const HOL.conj} $ _ $ _ =>
+ prove disjI3 (L.negate ct2, false) (ct1, true)
+ | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
+ prove disjI3 (L.negate ct2, false) (ct1, false)
+ | @{const HOL.disj} $ _ $ _ =>
+ prove disjI2 (L.negate ct1, false) (ct2, true)
| Const (@{const_name SMT.distinct}, _) $ _ =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
@@ -310,7 +310,7 @@
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
- | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
+ | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
fun prv cu =
@@ -392,7 +392,7 @@
if l aconv r
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
- | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
+ | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
| _ =>
let
@@ -474,8 +474,8 @@
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
- | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
+ @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
| Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
@@ -589,8 +589,8 @@
|> Conv.fconv_rule (Thm.beta_conversion true)
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
- | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
- (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
+ | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
+ (sk_all_rule, Thm.dest_arg, L.negate)
| kind t = raise TERM ("skolemize", [t])
fun dest_abs_type (Abs (_, T, _)) = T
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 17 13:39:30 2010 +0100
@@ -53,12 +53,12 @@
(* accessing terms *)
-val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
-val mk_prop = Thm.capply @{cterm Trueprop}
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
@@ -195,14 +195,14 @@
and abstr cvs ct =
(case Thm.term_of ct of
- @{term Trueprop} $ _ => abstr1 cvs ct
- | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
- | @{term True} => pair ct
- | @{term False} => pair ct
- | @{term Not} $ _ => abstr1 cvs ct
- | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
+ @{const Trueprop} $ _ => abstr1 cvs ct
+ | @{const "==>"} $ _ $ _ => abstr2 cvs ct
+ | @{const True} => pair ct
+ | @{const False} => pair ct
+ | @{const Not} $ _ => abstr1 cvs ct
+ | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name SMT.distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
@@ -221,8 +221,10 @@
else fresh_abstraction cvs ct cx))
in abstr [] end
+val cimp = Thm.cterm_of @{theory} @{const "==>"}
+
fun with_prems thms f ct =
- fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
+ fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
|> f
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms
--- a/src/HOLCF/ConvexPD.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy Wed Nov 17 13:39:30 2010 +0100
@@ -289,7 +289,8 @@
apply (erule insert [OF unit])
done
-lemma convex_pd_induct:
+lemma convex_pd_induct
+ [case_names adm convex_unit convex_plus, induct type: convex_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<natural>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
@@ -374,6 +375,9 @@
"convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
unfolding convex_map_def by simp
+lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>"
+unfolding convex_map_def by simp
+
lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: convex_pd_induct, simp_all)
@@ -516,6 +520,9 @@
"convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
unfolding convex_join_def by simp
+lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>"
+unfolding convex_join_def by simp
+
lemma convex_join_map_unit:
"convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
by (induct xs rule: convex_pd_induct, simp_all)
--- a/src/HOLCF/Domain.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/Domain.thy Wed Nov 17 13:39:30 2010 +0100
@@ -7,7 +7,7 @@
theory Domain
imports Bifinite Domain_Aux
uses
- ("Tools/repdef.ML")
+ ("Tools/domaindef.ML")
("Tools/Domain/domain_isomorphism.ML")
("Tools/Domain/domain_axioms.ML")
("Tools/Domain/domain.ML")
@@ -94,7 +94,7 @@
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
*}
-lemma typedef_rep_class:
+lemma typedef_liftdomain_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
fixes t :: defl
@@ -156,7 +156,7 @@
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
*}
-use "Tools/repdef.ML"
+use "Tools/domaindef.ML"
subsection {* Isomorphic deflations *}
--- a/src/HOLCF/IsaMakefile Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/IsaMakefile Wed Nov 17 13:39:30 2010 +0100
@@ -77,9 +77,9 @@
Tools/Domain/domain_induction.ML \
Tools/Domain/domain_isomorphism.ML \
Tools/Domain/domain_take_proofs.ML \
+ Tools/domaindef.ML \
Tools/fixrec.ML \
Tools/pcpodef.ML \
- Tools/repdef.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
--- a/src/HOLCF/LowerPD.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/LowerPD.thy Wed Nov 17 13:39:30 2010 +0100
@@ -281,7 +281,8 @@
apply (erule insert [OF unit])
done
-lemma lower_pd_induct:
+lemma lower_pd_induct
+ [case_names adm lower_unit lower_plus, induct type: lower_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<flat>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
@@ -367,6 +368,9 @@
"lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
unfolding lower_map_def by simp
+lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>"
+unfolding lower_map_def by simp
+
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: lower_pd_induct, simp_all)
@@ -507,6 +511,9 @@
"lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
unfolding lower_join_def by simp
+lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>"
+unfolding lower_join_def by simp
+
lemma lower_join_map_unit:
"lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs"
by (induct xs rule: lower_pd_induct, simp_all)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 17 13:39:30 2010 +0100
@@ -523,7 +523,7 @@
let
val spec = (tbind, map (rpair dummyS) vs, mx);
val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
- Repdef.add_repdef false NONE spec defl NONE thy;
+ Domaindef.add_domaindef false NONE spec defl NONE thy;
(* declare domain_defl_simps rules *)
val thy = Context.theory_map (RepData.add_thm DEFL) thy;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/domaindef.ML Wed Nov 17 13:39:30 2010 +0100
@@ -0,0 +1,236 @@
+(* Title: HOLCF/Tools/repdef.ML
+ Author: Brian Huffman
+
+Defining representable domains using algebraic deflations.
+*)
+
+signature DOMAINDEF =
+sig
+ type rep_info =
+ {
+ emb_def : thm,
+ prj_def : thm,
+ defl_def : thm,
+ liftemb_def : thm,
+ liftprj_def : thm,
+ liftdefl_def : thm,
+ DEFL : thm
+ }
+
+ val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ term -> (binding * binding) option -> theory ->
+ (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
+
+ val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
+ * (binding * binding) option -> theory -> theory
+end;
+
+structure Domaindef :> DOMAINDEF =
+struct
+
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+
+(** type definitions **)
+
+type rep_info =
+ {
+ emb_def : thm,
+ prj_def : thm,
+ defl_def : thm,
+ liftemb_def : thm,
+ liftprj_def : thm,
+ liftdefl_def : thm,
+ DEFL : thm
+ };
+
+(* building types and terms *)
+
+val udomT = @{typ udom};
+val deflT = @{typ defl};
+fun emb_const T = Const (@{const_name emb}, T ->> udomT);
+fun prj_const T = Const (@{const_name prj}, udomT ->> T);
+fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
+fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT);
+fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T);
+fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT);
+
+fun mk_u_map t =
+ let
+ val (T, U) = dest_cfunT (fastype_of t);
+ val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U);
+ val u_map_const = Const (@{const_name u_map}, u_map_type);
+ in
+ mk_capply (u_map_const, t)
+ end;
+
+fun mk_cast (t, x) =
+ capply_const (udomT, udomT)
+ $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
+ $ x;
+
+(* manipulating theorems *)
+
+(* proving class instances *)
+
+fun declare_type_name a =
+ Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun gen_add_domaindef
+ (prep_term: Proof.context -> 'a -> term)
+ (def: bool)
+ (name: binding)
+ (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
+ (raw_defl: 'a)
+ (opt_morphs: (binding * binding) option)
+ (thy: theory)
+ : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
+ let
+ val _ = Theory.requires thy "Domain" "domaindefs";
+
+ (*rhs*)
+ val tmp_ctxt =
+ ProofContext.init_global thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val defl = prep_term tmp_ctxt raw_defl;
+ val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
+
+ val deflT = Term.fastype_of defl;
+ val _ = if deflT = @{typ "defl"} then ()
+ else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
+
+ (*lhs*)
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
+ val lhs_sorts = map snd lhs_tfrees;
+ val full_tname = Sign.full_name thy tname;
+ val newT = Type (full_tname, map TFree lhs_tfrees);
+
+ (*morphisms*)
+ val morphs = opt_morphs
+ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
+
+ (*set*)
+ val set = @{const defl_set} $ defl;
+
+ (*pcpodef*)
+ val tac1 = rtac @{thm defl_set_bottom} 1;
+ val tac2 = rtac @{thm adm_defl_set} 1;
+ val ((info, cpo_info, pcpo_info), thy) = thy
+ |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
+
+ (*definitions*)
+ val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
+ val Abs_const = Const (#Abs_name (#1 info), udomT --> newT);
+ val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
+ val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
+ Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
+ val defl_eqn = Logic.mk_equals (defl_const newT,
+ Abs ("x", Term.itselfT newT, defl));
+ val liftemb_eqn =
+ Logic.mk_equals (liftemb_const newT,
+ mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT)));
+ val liftprj_eqn =
+ Logic.mk_equals (liftprj_const newT,
+ mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"}));
+ val liftdefl_eqn =
+ Logic.mk_equals (liftdefl_const newT,
+ Abs ("t", Term.itselfT newT,
+ mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT)));
+
+ val name_def = Binding.suffix_name "_def" name;
+ val emb_bind = (Binding.prefix_name "emb_" name_def, []);
+ val prj_bind = (Binding.prefix_name "prj_" name_def, []);
+ val defl_bind = (Binding.prefix_name "defl_" name_def, []);
+ val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []);
+ val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []);
+ val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []);
+
+ (*instantiate class rep*)
+ val lthy = thy
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain});
+ val ((_, (_, emb_ldef)), lthy) =
+ Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
+ val ((_, (_, prj_ldef)), lthy) =
+ Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
+ val ((_, (_, defl_ldef)), lthy) =
+ Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
+ val ((_, (_, liftemb_ldef)), lthy) =
+ Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy;
+ val ((_, (_, liftprj_ldef)), lthy) =
+ Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy;
+ val ((_, (_, liftdefl_ldef)), lthy) =
+ Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy;
+ val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
+ val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
+ val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
+ val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
+ val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef;
+ val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef;
+ val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef;
+ val type_definition_thm =
+ MetaSimplifier.rewrite_rule
+ (the_list (#set_def (#2 info)))
+ (#type_definition (#2 info));
+ val typedef_thms =
+ [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
+ liftemb_def, liftprj_def, liftdefl_def];
+ val thy = lthy
+ |> Class.prove_instantiation_instance
+ (K (Tactic.rtac (@{thm typedef_liftdomain_class} OF typedef_thms) 1))
+ |> Local_Theory.exit_global;
+
+ (*other theorems*)
+ val defl_thm' = Thm.transfer thy defl_def;
+ val (DEFL_thm, thy) = thy
+ |> Sign.add_path (Binding.name_of name)
+ |> Global_Theory.add_thm
+ ((Binding.prefix_name "DEFL_" name,
+ Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
+ ||> Sign.restore_naming thy;
+
+ val rep_info =
+ { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
+ liftemb_def = liftemb_def, liftprj_def = liftprj_def,
+ liftdefl_def = liftdefl_def, DEFL = DEFL_thm };
+ in
+ ((info, cpo_info, pcpo_info, rep_info), thy)
+ end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in domaindef " ^ quote (Binding.str_of name));
+
+fun add_domaindef def opt_name typ defl opt_morphs thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ in
+ gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy
+ end;
+
+fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
+ let
+ val ctxt = ProofContext.init_global thy;
+ val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
+ in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end;
+
+
+(** outer syntax **)
+
+val domaindef_decl =
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
+
+fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
+ domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
+
+val _ =
+ Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl
+ (domaindef_decl >>
+ (Toplevel.print oo (Toplevel.theory o mk_domaindef)));
+
+end;
--- a/src/HOLCF/Tools/repdef.ML Wed Nov 17 13:38:53 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(* Title: HOLCF/Tools/repdef.ML
- Author: Brian Huffman
-
-Defining representable domains using algebraic deflations.
-*)
-
-signature REPDEF =
-sig
- type rep_info =
- {
- emb_def : thm,
- prj_def : thm,
- defl_def : thm,
- liftemb_def : thm,
- liftprj_def : thm,
- liftdefl_def : thm,
- DEFL : thm
- }
-
- val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> theory ->
- (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
-
- val repdef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> theory
-end;
-
-structure Repdef :> REPDEF =
-struct
-
-open HOLCF_Library;
-
-infixr 6 ->>;
-infix -->>;
-
-(** type definitions **)
-
-type rep_info =
- {
- emb_def : thm,
- prj_def : thm,
- defl_def : thm,
- liftemb_def : thm,
- liftprj_def : thm,
- liftdefl_def : thm,
- DEFL : thm
- };
-
-(* building types and terms *)
-
-val udomT = @{typ udom};
-val deflT = @{typ defl};
-fun emb_const T = Const (@{const_name emb}, T ->> udomT);
-fun prj_const T = Const (@{const_name prj}, udomT ->> T);
-fun defl_const T = Const (@{const_name defl}, Term.itselfT T --> deflT);
-fun liftemb_const T = Const (@{const_name liftemb}, mk_upT T ->> udomT);
-fun liftprj_const T = Const (@{const_name liftprj}, udomT ->> mk_upT T);
-fun liftdefl_const T = Const (@{const_name liftdefl}, Term.itselfT T --> deflT);
-
-fun mk_u_map t =
- let
- val (T, U) = dest_cfunT (fastype_of t);
- val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U);
- val u_map_const = Const (@{const_name u_map}, u_map_type);
- in
- mk_capply (u_map_const, t)
- end;
-
-fun mk_cast (t, x) =
- capply_const (udomT, udomT)
- $ (capply_const (deflT, udomT ->> udomT) $ @{const cast} $ t)
- $ x;
-
-(* manipulating theorems *)
-
-(* proving class instances *)
-
-fun declare_type_name a =
- Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
-fun gen_add_repdef
- (prep_term: Proof.context -> 'a -> term)
- (def: bool)
- (name: binding)
- (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
- (raw_defl: 'a)
- (opt_morphs: (binding * binding) option)
- (thy: theory)
- : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
- let
- val _ = Theory.requires thy "Domain" "repdefs";
-
- (*rhs*)
- val tmp_ctxt =
- ProofContext.init_global thy
- |> fold (Variable.declare_typ o TFree) raw_args;
- val defl = prep_term tmp_ctxt raw_defl;
- val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
-
- val deflT = Term.fastype_of defl;
- val _ = if deflT = @{typ "defl"} then ()
- else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
-
- (*lhs*)
- val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
- val lhs_sorts = map snd lhs_tfrees;
- val full_tname = Sign.full_name thy tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
-
- (*morphisms*)
- val morphs = opt_morphs
- |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
-
- (*set*)
- val set = @{const defl_set} $ defl;
-
- (*pcpodef*)
- val tac1 = rtac @{thm defl_set_bottom} 1;
- val tac2 = rtac @{thm adm_defl_set} 1;
- val ((info, cpo_info, pcpo_info), thy) = thy
- |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
-
- (*definitions*)
- val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
- val Abs_const = Const (#Abs_name (#1 info), udomT --> newT);
- val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
- val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
- Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
- val defl_eqn = Logic.mk_equals (defl_const newT,
- Abs ("x", Term.itselfT newT, defl));
- val liftemb_eqn =
- Logic.mk_equals (liftemb_const newT,
- mk_cfcomp (@{term "udom_emb u_approx"}, mk_u_map (emb_const newT)));
- val liftprj_eqn =
- Logic.mk_equals (liftprj_const newT,
- mk_cfcomp (mk_u_map (prj_const newT), @{term "udom_prj u_approx"}));
- val liftdefl_eqn =
- Logic.mk_equals (liftdefl_const newT,
- Abs ("t", Term.itselfT newT,
- mk_capply (@{const u_defl}, defl_const newT $ Logic.mk_type newT)));
-
- val name_def = Binding.suffix_name "_def" name;
- val emb_bind = (Binding.prefix_name "emb_" name_def, []);
- val prj_bind = (Binding.prefix_name "prj_" name_def, []);
- val defl_bind = (Binding.prefix_name "defl_" name_def, []);
- val liftemb_bind = (Binding.prefix_name "liftemb_" name_def, []);
- val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []);
- val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []);
-
- (*instantiate class rep*)
- val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain});
- val ((_, (_, emb_ldef)), lthy) =
- Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
- val ((_, (_, prj_ldef)), lthy) =
- Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
- val ((_, (_, defl_ldef)), lthy) =
- Specification.definition (NONE, (defl_bind, defl_eqn)) lthy;
- val ((_, (_, liftemb_ldef)), lthy) =
- Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy;
- val ((_, (_, liftprj_ldef)), lthy) =
- Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy;
- val ((_, (_, liftdefl_ldef)), lthy) =
- Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy;
- val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
- val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
- val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
- val defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef;
- val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef;
- val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef;
- val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef;
- val type_definition_thm =
- MetaSimplifier.rewrite_rule
- (the_list (#set_def (#2 info)))
- (#type_definition (#2 info));
- val typedef_thms =
- [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
- liftemb_def, liftprj_def, liftdefl_def];
- val thy = lthy
- |> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
- |> Local_Theory.exit_global;
-
- (*other theorems*)
- val defl_thm' = Thm.transfer thy defl_def;
- val (DEFL_thm, thy) = thy
- |> Sign.add_path (Binding.name_of name)
- |> Global_Theory.add_thm
- ((Binding.prefix_name "DEFL_" name,
- Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
- ||> Sign.restore_naming thy;
-
- val rep_info =
- { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
- liftemb_def = liftemb_def, liftprj_def = liftprj_def,
- liftdefl_def = liftdefl_def, DEFL = DEFL_thm };
- in
- ((info, cpo_info, pcpo_info, rep_info), thy)
- end
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name));
-
-fun add_repdef def opt_name typ defl opt_morphs thy =
- let
- val name = the_default (#1 typ) opt_name;
- in
- gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy
- end;
-
-fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
- let
- val ctxt = ProofContext.init_global thy;
- val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
- in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end;
-
-
-(** outer syntax **)
-
-val repdef_decl =
- Scan.optional (Parse.$$$ "(" |--
- ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
- Parse.binding >> (fn s => (true, SOME s)))
- --| Parse.$$$ ")") (true, NONE) --
- (Parse.type_args_constrained -- Parse.binding) --
- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
-
-fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
- repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
-
-val _ =
- Outer_Syntax.command "repdef" "HOLCF definition of representable domains" Keyword.thy_decl
- (repdef_decl >>
- (Toplevel.print oo (Toplevel.theory o mk_repdef)));
-
-end;
--- a/src/HOLCF/UpperPD.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/UpperPD.thy Wed Nov 17 13:39:30 2010 +0100
@@ -276,7 +276,8 @@
apply (erule insert [OF unit])
done
-lemma upper_pd_induct:
+lemma upper_pd_induct
+ [case_names adm upper_unit upper_plus, induct type: upper_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<sharp>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
@@ -362,6 +363,9 @@
"upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
unfolding upper_map_def by simp
+lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>"
+unfolding upper_map_def by simp
+
lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: upper_pd_induct, simp_all)
@@ -502,6 +506,9 @@
"upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
unfolding upper_join_def by simp
+lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>"
+unfolding upper_join_def by simp
+
lemma upper_join_map_unit:
"upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs"
by (induct xs rule: upper_pd_induct, simp_all)
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 17 13:38:53 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 17 13:39:30 2010 +0100
@@ -116,7 +116,7 @@
"liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
instance
-apply (rule typedef_rep_class)
+apply (rule typedef_liftdomain_class)
apply (rule type_definition_foo)
apply (rule below_foo_def)
apply (rule emb_foo_def)
@@ -151,7 +151,7 @@
"liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
instance
-apply (rule typedef_rep_class)
+apply (rule typedef_liftdomain_class)
apply (rule type_definition_bar)
apply (rule below_bar_def)
apply (rule emb_bar_def)
@@ -186,7 +186,7 @@
"liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
instance
-apply (rule typedef_rep_class)
+apply (rule typedef_liftdomain_class)
apply (rule type_definition_baz)
apply (rule below_baz_def)
apply (rule emb_baz_def)
--- a/src/Tools/cache_io.ML Wed Nov 17 13:38:53 2010 +0100
+++ b/src/Tools/cache_io.ML Wed Nov 17 13:39:30 2010 +0100
@@ -13,6 +13,8 @@
output: string list,
redirected_output: string list,
return_code: int}
+ val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
+ result
val run: (Path.T -> Path.T -> string) -> string -> result
(*cache*)
@@ -52,14 +54,16 @@
redirected_output: string list,
return_code: int}
+fun raw_run make_cmd str in_path out_path =
+ let
+ val _ = File.write in_path str
+ val (out2, rc) = bash_output (make_cmd in_path out_path)
+ val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+ in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+
fun run make_cmd str =
with_tmp_file cache_io_prefix (fn in_path =>
- with_tmp_file cache_io_prefix (fn out_path =>
- let
- val _ = File.write in_path str
- val (out2, rc) = bash_output (make_cmd in_path out_path)
- val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+ with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
(* cache *)