tuned
authorboehmes
Wed Dec 15 08:39:24 2010 +0100 (2010-12-15)
changeset 411233bb9be510a9d
parent 41122 72176ec5e031
child 41124 1de17a2de5ad
tuned
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature SMT_TRANSLATE =
     1.6  sig
     1.7 -  (* intermediate term structure *)
     1.8 +  (*intermediate term structure*)
     1.9    datatype squant = SForall | SExists
    1.10    datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
    1.11    datatype sterm =
    1.12 @@ -15,7 +15,7 @@
    1.13      SLet of string * sterm * sterm |
    1.14      SQua of squant * string list * sterm spattern list * int option * sterm
    1.15  
    1.16 -  (* configuration options *)
    1.17 +  (*configuration options*)
    1.18    type prefixes = {sort_prefix: string, func_prefix: string}
    1.19    type sign = {
    1.20      header: string list,
     2.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 08:39:24 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 08:39:24 2010 +0100
     2.3 @@ -6,17 +6,18 @@
     2.4  
     2.5  signature SMT_UTILS =
     2.6  sig
     2.7 +  (*basic combinators*)
     2.8    val repeat: ('a -> 'a option) -> 'a -> 'a
     2.9    val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
    2.10  
    2.11 -  (* types *)
    2.12 +  (*types*)
    2.13    val dest_funT: int -> typ -> typ list * typ
    2.14  
    2.15 -  (* terms *)
    2.16 +  (*terms*)
    2.17    val dest_conj: term -> term * term
    2.18    val dest_disj: term -> term * term
    2.19  
    2.20 -  (* patterns and instantiations *)
    2.21 +  (*patterns and instantiations*)
    2.22    val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
    2.23    val destT1: ctyp -> ctyp
    2.24    val destT2: ctyp -> ctyp
    2.25 @@ -24,7 +25,7 @@
    2.26    val instT: ctyp -> ctyp * cterm -> cterm
    2.27    val instT': cterm -> ctyp * cterm -> cterm
    2.28  
    2.29 -  (* certified terms *)
    2.30 +  (*certified terms*)
    2.31    val certify: Proof.context -> term -> cterm
    2.32    val typ_of: cterm -> typ
    2.33    val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
    2.34 @@ -35,7 +36,7 @@
    2.35    val dest_cprop: cterm -> cterm
    2.36    val mk_cequals: cterm -> cterm -> cterm
    2.37  
    2.38 -  (* conversions *)
    2.39 +  (*conversions*)
    2.40    val if_conv: (term -> bool) -> conv -> conv -> conv
    2.41    val if_true_conv: (term -> bool) -> conv -> conv
    2.42    val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
    2.43 @@ -45,6 +46,8 @@
    2.44  structure SMT_Utils: SMT_UTILS =
    2.45  struct
    2.46  
    2.47 +(* basic combinators *)
    2.48 +
    2.49  fun repeat f =
    2.50    let fun rep x = (case f x of SOME y => rep y | NONE => x)
    2.51    in rep end
     3.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 08:39:24 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 08:39:24 2010 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  signature Z3_PROOF_LITERALS =
     3.6  sig
     3.7 -  (* literal table *)
     3.8 +  (*literal table*)
     3.9    type littab = thm Termtab.table
    3.10    val make_littab: thm list -> littab
    3.11    val insert_lit: thm -> littab -> littab
    3.12 @@ -14,17 +14,17 @@
    3.13    val lookup_lit: littab -> term -> thm option
    3.14    val get_first_lit: (term -> bool) -> littab -> thm option
    3.15  
    3.16 -  (* rules *)
    3.17 +  (*rules*)
    3.18    val true_thm: thm
    3.19    val rewrite_true: thm
    3.20  
    3.21 -  (* properties *)
    3.22 +  (*properties*)
    3.23    val is_conj: term -> bool
    3.24    val is_disj: term -> bool
    3.25    val exists_lit: bool -> (term -> bool) -> term -> bool
    3.26    val negate: cterm -> cterm
    3.27  
    3.28 -  (* proof tools *)
    3.29 +  (*proof tools*)
    3.30    val explode: bool -> bool -> bool -> term list -> thm -> thm list
    3.31    val join: bool -> littab -> term -> thm
    3.32    val prove_conj_disj_eq: cterm -> thm
    3.33 @@ -37,7 +37,7 @@
    3.34  
    3.35  
    3.36  
    3.37 -(** literal table **)
    3.38 +(* literal table *)
    3.39  
    3.40  type littab = thm Termtab.table
    3.41  
    3.42 @@ -51,14 +51,14 @@
    3.43  
    3.44  
    3.45  
    3.46 -(** rules **)
    3.47 +(* rules *)
    3.48  
    3.49  val true_thm = @{lemma "~False" by simp}
    3.50  val rewrite_true = @{lemma "True == ~ False" by simp}
    3.51  
    3.52  
    3.53  
    3.54 -(** properties and term operations **)
    3.55 +(* properties and term operations *)
    3.56  
    3.57  val is_neg = (fn @{const Not} $ _ => true | _ => false)
    3.58  fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
    3.59 @@ -87,9 +87,9 @@
    3.60  
    3.61  
    3.62  
    3.63 -(** proof tools **)
    3.64 +(* proof tools *)
    3.65  
    3.66 -(* explosion of conjunctions and disjunctions *)
    3.67 +(** explosion of conjunctions and disjunctions **)
    3.68  
    3.69  local
    3.70    fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
    3.71 @@ -117,8 +117,10 @@
    3.72    val dneg_rule = T.precompose destn @{thm notnotD}
    3.73  in
    3.74  
    3.75 -(* explode a term into literals and collect all rules to be able to deduce
    3.76 -   particular literals afterwards *)
    3.77 +(*
    3.78 +  explode a term into literals and collect all rules to be able to deduce
    3.79 +  particular literals afterwards
    3.80 +*)
    3.81  fun explode_term is_conj =
    3.82    let
    3.83      val dest = if is_conj then dest_conj_term else dest_disj_term
    3.84 @@ -144,11 +146,15 @@
    3.85  
    3.86    in explode0 end
    3.87  
    3.88 -(* extract a literal by applying previously collected rules *)
    3.89 +(*
    3.90 +  extract a literal by applying previously collected rules
    3.91 +*)
    3.92  fun extract_lit thm rules = fold T.compose rules thm
    3.93  
    3.94  
    3.95 -(* explode a theorem into its literals *)
    3.96 +(*
    3.97 +  explode a theorem into its literals
    3.98 +*)
    3.99  fun explode is_conj full keep_intermediate stop_lits =
   3.100    let
   3.101      val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
   3.102 @@ -180,7 +186,7 @@
   3.103  
   3.104  
   3.105  
   3.106 -(* joining of literals to conjunctions or disjunctions *)
   3.107 +(** joining of literals to conjunctions or disjunctions **)
   3.108  
   3.109  local
   3.110    fun on_cprem i f thm = f (Thm.cprem_of thm i)
   3.111 @@ -259,7 +265,7 @@
   3.112  
   3.113  
   3.114  
   3.115 -(* proving equality of conjunctions or disjunctions *)
   3.116 +(** proving equality of conjunctions or disjunctions **)
   3.117  
   3.118  fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
   3.119  
     4.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 08:39:24 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 08:39:24 2010 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature Z3_PROOF_PARSER =
     4.6  sig
     4.7 -  (* proof rules *)
     4.8 +  (*proof rules*)
     4.9    datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
    4.10      Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
    4.11      Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
    4.12 @@ -16,7 +16,7 @@
    4.13      CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
    4.14    val string_of_rule: rule -> string
    4.15  
    4.16 -  (* proof parser *)
    4.17 +  (*proof parser*)
    4.18    datatype proof_step = Proof_Step of {
    4.19      rule: rule,
    4.20      prems: int list,
    4.21 @@ -34,7 +34,7 @@
    4.22  
    4.23  
    4.24  
    4.25 -(** proof rules **)
    4.26 +(* proof rules *)
    4.27  
    4.28  datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
    4.29    Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
    4.30 @@ -91,7 +91,7 @@
    4.31  
    4.32  
    4.33  
    4.34 -(** certified terms and variables **)
    4.35 +(* certified terms and variables *)
    4.36  
    4.37  val (var_prefix, decl_prefix) = ("v", "sk")
    4.38  (* "decl_prefix" is for skolem constants (represented by free variables)
    4.39 @@ -171,7 +171,7 @@
    4.40  
    4.41  
    4.42  
    4.43 -(** proof parser **)
    4.44 +(* proof parser *)
    4.45  
    4.46  datatype proof_step = Proof_Step of {
    4.47    rule: rule,
    4.48 @@ -179,7 +179,7 @@
    4.49    prop: cterm }
    4.50  
    4.51  
    4.52 -(* parser context *)
    4.53 +(** parser context **)
    4.54  
    4.55  val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
    4.56  
    4.57 @@ -240,7 +240,7 @@
    4.58  fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt)
    4.59  
    4.60  
    4.61 -(* core parser *)
    4.62 +(** core parser **)
    4.63  
    4.64  fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
    4.65    ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
    4.66 @@ -269,7 +269,7 @@
    4.67  fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
    4.68  
    4.69  
    4.70 -(* parser combinators and parsers for basic entities *)
    4.71 +(** parser combinators and parsers for basic entities **)
    4.72  
    4.73  fun $$ s = Scan.lift (Scan.$$ s)
    4.74  fun this s = Scan.lift (Scan.this_string s)
    4.75 @@ -306,7 +306,7 @@
    4.76  fun id st = ($$ "#" |-- nat_num) st
    4.77  
    4.78  
    4.79 -(* parsers for various parts of Z3 proofs *)
    4.80 +(** parsers for various parts of Z3 proofs **)
    4.81  
    4.82  fun sort st = Scan.first [
    4.83    this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
    4.84 @@ -400,15 +400,17 @@
    4.85    rule SOME ~1)
    4.86  
    4.87  
    4.88 -(* overall parser *)
    4.89 +(** overall parser **)
    4.90  
    4.91 -(* Currently, terms are parsed bottom-up (i.e., along with parsing the proof
    4.92 -   text line by line), but proofs are reconstructed top-down (i.e. by an
    4.93 -   in-order top-down traversal of the proof tree/graph).  The latter approach
    4.94 -   was taken because some proof texts comprise irrelevant proof steps which
    4.95 -   will thus not be reconstructed.  This approach might also be beneficial
    4.96 -   for constructing terms, but it would also increase the complexity of the
    4.97 -   (otherwise rather modular) code. *)
    4.98 +(*
    4.99 +  Currently, terms are parsed bottom-up (i.e., along with parsing the proof
   4.100 +  text line by line), but proofs are reconstructed top-down (i.e. by an
   4.101 +  in-order top-down traversal of the proof tree/graph).  The latter approach
   4.102 +  was taken because some proof texts comprise irrelevant proof steps which
   4.103 +  will thus not be reconstructed.  This approach might also be beneficial
   4.104 +  for constructing terms, but it would also increase the complexity of the
   4.105 +  (otherwise rather modular) code.
   4.106 +*)
   4.107  
   4.108  fun parse ctxt typs terms proof_text =
   4.109    make_context ctxt typs terms
     5.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 08:39:24 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 08:39:24 2010 +0100
     5.3 @@ -6,18 +6,18 @@
     5.4  
     5.5  signature Z3_PROOF_TOOLS =
     5.6  sig
     5.7 -  (* accessing and modifying terms *)
     5.8 +  (*accessing and modifying terms*)
     5.9    val term_of: cterm -> term
    5.10    val prop_of: thm -> term
    5.11    val as_meta_eq: cterm -> cterm
    5.12  
    5.13 -  (* theorem nets *)
    5.14 +  (*theorem nets*)
    5.15    val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
    5.16    val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
    5.17      cterm -> 'a option
    5.18    val net_instance: thm Net.net -> cterm -> thm option
    5.19  
    5.20 -  (* proof combinators *)
    5.21 +  (*proof combinators*)
    5.22    val under_assumption: (thm -> thm) -> cterm -> thm
    5.23    val with_conv: conv -> (cterm -> thm) -> cterm -> thm
    5.24    val discharge: thm -> thm -> thm
    5.25 @@ -29,16 +29,16 @@
    5.26    val by_abstraction: bool * bool -> Proof.context -> thm list ->
    5.27      (Proof.context -> cterm -> thm) -> cterm -> thm
    5.28  
    5.29 -  (* a faster COMP *)
    5.30 +  (*a faster COMP*)
    5.31    type compose_data
    5.32    val precompose: (cterm -> cterm list) -> thm -> compose_data
    5.33    val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    5.34    val compose: compose_data -> thm -> thm
    5.35  
    5.36 -  (* unfolding of 'distinct' *)
    5.37 +  (*unfolding of 'distinct'*)
    5.38    val unfold_distinct_conv: conv
    5.39  
    5.40 -  (* simpset *)
    5.41 +  (*simpset*)
    5.42    val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    5.43    val make_simpset: Proof.context -> thm list -> simpset
    5.44  end
    5.45 @@ -107,7 +107,11 @@
    5.46  
    5.47  fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
    5.48  
    5.49 -(* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
    5.50 +(*
    5.51 +   |- c x == t x ==> P (c x)
    5.52 +  ---------------------------
    5.53 +      c == t |- P (c x)
    5.54 +*) 
    5.55  fun make_hyp_def thm ctxt =
    5.56    let
    5.57      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)