src/HOL/Import/shuffler.ML
author wenzelm
Tue, 29 Sep 2009 16:24:36 +0200
changeset 32740 9dd0a2f83429
parent 32432 64f30bdd3ba1
child 32957 675c0c7e6a37
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     1
(*  Title:      HOL/Import/shuffler.ML
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
    Author:     Sebastian Skalberg, TU Muenchen
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
Package for proving two terms equal by normalizing (hence the
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
"shuffler" name).  Uses the simplifier for the normalization.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
*)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
signature Shuffler =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
sig
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    10
    val debug      : bool Unsynchronized.ref
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
    val norm_term  : theory -> term -> thm
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
    val make_equal : theory -> term -> term -> thm option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
    val set_prop   : theory -> term -> (string * thm) list -> (string * thm) option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
    val find_potential: theory -> term -> (string * thm) list
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
    18
    val gen_shuffle_tac: Proof.context -> bool -> (string * thm) list -> int -> tactic
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
    19
    val shuffle_tac: Proof.context -> thm list -> int -> tactic
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
    20
    val search_tac : Proof.context -> int -> tactic
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
    val print_shuffles: theory -> unit
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
    val add_shuffle_rule: thm -> theory -> theory
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    25
    val shuffle_attr: attribute
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
    27
    val setup      : theory -> theory
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
structure Shuffler :> Shuffler =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32432
diff changeset
    33
val debug = Unsynchronized.ref false
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
fun if_debug f x = if !debug then f x else ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
val message = if_debug writeln
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
(*Prints exceptions readably to users*)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    39
fun print_sign_exn_unit sign e =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
  case e of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
     THM (msg,i,thms) =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    42
         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31945
diff changeset
    43
          List.app (writeln o Display.string_of_thm_global sign) thms)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
   | THEORY (msg,thys) =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    45
         (writeln ("Exception THEORY raised:\n" ^ msg);
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    46
          List.app (writeln o Context.str_of_thy) thys)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
   | TERM (msg,ts) =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    48
         (writeln ("Exception TERM raised:\n" ^ msg);
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26928
diff changeset
    49
          List.app (writeln o Syntax.string_of_term_global sign) ts)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
   | TYPE (msg,Ts,ts) =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    51
         (writeln ("Exception TYPE raised:\n" ^ msg);
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26928
diff changeset
    52
          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26928
diff changeset
    53
          List.app (writeln o Syntax.string_of_term_global sign) ts)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
   | e => raise e
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
(*Prints an exception, then fails*)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31945
diff changeset
    59
val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
fun mk_meta_eq th =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
    (case concl_of th of
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    63
         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
       | Const("==",_) $ _ $ _ => th
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
       | _ => raise THM("Not an equality",0,[th]))
28397
389c5e494605 handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents: 27865
diff changeset
    66
    handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    67
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
fun mk_obj_eq th =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
    (case concl_of th of
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    70
         Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
       | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
       | _ => raise THM("Not an equality",0,[th]))
28397
389c5e494605 handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents: 27865
diff changeset
    73
    handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    75
structure ShuffleData = TheoryDataFun
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    76
(
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    77
  type T = thm list
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    78
  val empty = []
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    79
  val copy = I
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    80
  val extend = I
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    81
  fun merge _ = Library.gen_union Thm.eq_thm
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    82
)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    84
fun print_shuffles thy =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    85
  Pretty.writeln (Pretty.big_list "Shuffle theorems:"
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31945
diff changeset
    86
    (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
val weaken =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 26277
diff changeset
    90
        val cert = cterm_of Pure.thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    91
        val P = Free("P",propT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    92
        val Q = Free("Q",propT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    93
        val PQ = Logic.mk_implies(P,Q)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    94
        val PPQ = Logic.mk_implies(P,PQ)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    95
        val cP = cert P
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    96
        val cQ = cert Q
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    97
        val cPQ = cert PQ
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    98
        val cPPQ = cert PPQ
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
    99
        val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   100
        val th3 = assume cP
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   101
        val th4 = implies_elim_list (assume cPPQ) [th3,th3]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   102
                                    |> implies_intr_list [cPPQ,cP]
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   104
        equal_intr th4 th1 |> standard
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
val imp_comm =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 26277
diff changeset
   109
        val cert = cterm_of Pure.thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   110
        val P = Free("P",propT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   111
        val Q = Free("Q",propT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   112
        val R = Free("R",propT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   113
        val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   114
        val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   115
        val cP = cert P
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   116
        val cQ = cert Q
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   117
        val cPQR = cert PQR
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   118
        val cQPR = cert QPR
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   119
        val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   120
                                    |> implies_intr_list [cPQR,cQ,cP]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   121
        val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   122
                                    |> implies_intr_list [cQPR,cP,cQ]
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   124
        equal_intr th1 th2 |> standard
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
val def_norm =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 26277
diff changeset
   129
        val cert = cterm_of Pure.thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   130
        val aT = TFree("'a",[])
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   131
        val bT = TFree("'b",[])
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   132
        val v = Free("v",aT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   133
        val P = Free("P",aT-->bT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   134
        val Q = Free("Q",aT-->bT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   135
        val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   136
        val cPQ = cert (Logic.mk_equals(P,Q))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   137
        val cv = cert v
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   138
        val rew = assume cvPQ
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   139
                         |> forall_elim cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   140
                         |> abstract_rule "v" cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   141
        val (lhs,rhs) = Logic.dest_equals(concl_of rew)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   142
        val th1 = transitive (transitive
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   143
                                  (eta_conversion (cert lhs) |> symmetric)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   144
                                  rew)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   145
                             (eta_conversion (cert rhs))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   146
                             |> implies_intr cvPQ
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   147
        val th2 = combination (assume cPQ) (reflexive cv)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   148
                              |> forall_intr cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   149
                              |> implies_intr cPQ
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   151
        equal_intr th1 th2 |> standard
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
val all_comm =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   155
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 26277
diff changeset
   156
        val cert = cterm_of Pure.thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   157
        val xT = TFree("'a",[])
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   158
        val yT = TFree("'b",[])
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   159
        val x = Free("x",xT)
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   160
        val y = Free("y",yT)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   161
        val P = Free("P",xT-->yT-->propT)
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   162
        val lhs = Logic.all x (Logic.all y (P $ x $ y))
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   163
        val rhs = Logic.all y (Logic.all x (P $ x $ y))
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   164
        val cl = cert lhs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   165
        val cr = cert rhs
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   166
        val cx = cert x
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   167
        val cy = cert y
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   168
        val th1 = assume cr
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   169
                         |> forall_elim_list [cy,cx]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   170
                         |> forall_intr_list [cx,cy]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   171
                         |> implies_intr cr
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   172
        val th2 = assume cl
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   173
                         |> forall_elim_list [cx,cy]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   174
                         |> forall_intr_list [cy,cx]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   175
                         |> implies_intr cl
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   177
        equal_intr th1 th2 |> standard
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   179
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
val equiv_comm =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 26277
diff changeset
   182
        val cert = cterm_of Pure.thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   183
        val T    = TFree("'a",[])
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   184
        val t    = Free("t",T)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   185
        val u    = Free("u",T)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   186
        val ctu  = cert (Logic.mk_equals(t,u))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   187
        val cut  = cert (Logic.mk_equals(u,t))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   188
        val th1  = assume ctu |> symmetric |> implies_intr ctu
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   189
        val th2  = assume cut |> symmetric |> implies_intr cut
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   191
        equal_intr th1 th2 |> standard
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
(* This simplification procedure rewrites !!x y. P x y
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
deterministicly, in order for the normalization function, defined
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
below, to handle nested quantifiers robustly *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
local
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   199
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   200
exception RESULT of int
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   201
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   202
fun find_bound n (Bound i) = if i = n then raise RESULT 0
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   203
                             else if i = n+1 then raise RESULT 1
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   204
                             else ()
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   205
  | find_bound n (t $ u) = (find_bound n t; find_bound n u)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   206
  | find_bound n (Abs(_,_,t)) = find_bound (n+1) t
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   207
  | find_bound _ _ = ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   208
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   209
fun swap_bound n (Bound i) = if i = n then Bound (n+1)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   210
                             else if i = n+1 then Bound n
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   211
                             else Bound i
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   212
  | swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   213
  | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   214
  | swap_bound n t = t
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   215
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   216
fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   217
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   218
        val lhs = list_all ([xv,yv],t)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   219
        val rhs = list_all ([yv,xv],swap_bound 0 t)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   220
        val rew = Logic.mk_equals (lhs,rhs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   221
        val init = trivial (cterm_of thy rew)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   222
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   223
        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   224
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   225
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   226
fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   227
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   228
        val res = (find_bound 0 body;2) handle RESULT i => i
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   229
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   230
        case res of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   231
            0 => SOME (rew_th thy (x,xT) (y,yT) body)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   232
          | 1 => if string_ord(y,x) = LESS
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   233
                 then
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   234
                     let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   235
                         val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   236
                         val t_th    = reflexive (cterm_of thy t)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   237
                         val newt_th = reflexive (cterm_of thy newt)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   238
                     in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   239
                         SOME (transitive t_th newt_th)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   240
                     end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   241
                 else NONE
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   242
          | _ => error "norm_term (quant_rewrite) internal error"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   243
     end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14854
diff changeset
   244
  | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   245
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   246
fun freeze_thaw_term t =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   247
    let
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
   248
        val tvars = OldTerm.term_tvars t
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
   249
        val tfree_names = OldTerm.add_term_tfree_names(t,[])
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   250
        val (type_inst,_) =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   251
            Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   252
                      let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   253
                          val v' = Name.variant used v
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   254
                      in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   255
                          ((w,TFree(v',S))::inst,v'::used)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   256
                      end)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   257
                  (([],tfree_names),tvars)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   258
        val t' = subst_TVars type_inst t
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   259
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   260
        (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   261
                  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   262
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   263
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   264
fun inst_tfrees thy [] thm = thm
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   265
  | inst_tfrees thy ((name,U)::rest) thm =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   266
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   267
        val cU = ctyp_of thy U
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29269
diff changeset
   268
        val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   269
        val (rens, thm') = Thm.varifyT'
20951
868120282837 gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents: 20897
diff changeset
   270
    (remove (op = o apsnd fst) name tfrees) thm
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   271
        val mid =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   272
            case rens of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   273
                [] => thm'
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   274
              | [((_, S), idx)] => instantiate
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   275
            ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   276
              | _ => error "Shuffler.inst_tfrees internal error"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   277
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   278
        inst_tfrees thy rest mid
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   279
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   280
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   281
fun is_Abs (Abs _) = true
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   282
  | is_Abs _ = false
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   283
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   284
fun eta_redex (t $ Bound 0) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   285
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   286
        fun free n (Bound i) = i = n
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   287
          | free n (t $ u) = free n t orelse free n u
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   288
          | free n (Abs(_,_,t)) = free (n+1) t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   289
          | free n _ = false
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   290
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   291
        not (free 0 t)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   292
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   293
  | eta_redex _ = false
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   294
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   295
fun eta_contract thy assumes origt =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   296
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   297
        val (typet,Tinst) = freeze_thaw_term origt
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   298
        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   299
        val final = inst_tfrees thy Tinst o thaw
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   300
        val t = #1 (Logic.dest_equals (prop_of init))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   301
        val _ =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   302
            let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   303
                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   304
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   305
                if not (lhs aconv origt)
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   306
                then
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   307
                  writeln (cat_lines
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   308
                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   309
                      Syntax.string_of_term_global thy origt,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   310
                      Syntax.string_of_term_global thy lhs,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   311
                      Syntax.string_of_term_global thy typet,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   312
                      Syntax.string_of_term_global thy t] @
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   313
                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   314
                else ()
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   315
            end
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   316
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   317
        case t of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   318
            Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   319
            ((if eta_redex P andalso eta_redex Q
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   320
              then
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   321
                  let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   322
                      val cert = cterm_of thy
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   323
                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   324
                      val cv = cert v
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   325
                      val ct = cert t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   326
                      val th = (assume ct)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   327
                                   |> forall_elim cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   328
                                   |> abstract_rule x cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   329
                      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   330
                      val th' = transitive (symmetric ext_th) th
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   331
                      val cu = cert (prop_of th')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   332
                      val uth = combination (assume cu) (reflexive cv)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   333
                      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   334
                                     |> transitive uth
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   335
                                     |> forall_intr cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   336
                                     |> implies_intr cu
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   337
                      val rew_th = equal_intr (th' |> implies_intr ct) uth'
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   338
                      val res = final rew_th
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   339
                      val lhs = (#1 (Logic.dest_equals (prop_of res)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   340
                  in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   341
                       SOME res
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   342
                  end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   343
              else NONE)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   344
             handle e => OldGoals.print_exn e)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   345
          | _ => NONE
17440
df77edc4f5d0 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents: 17188
diff changeset
   346
       end
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   347
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   348
fun beta_fun thy assume t =
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   349
    SOME (beta_conversion true (cterm_of thy t))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   350
17188
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   351
val meta_sym_rew = thm "refl"
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   352
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   353
fun equals_fun thy assume t =
17188
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   354
    case t of
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 29265
diff changeset
   355
        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
17188
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   356
      | _ => NONE
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   357
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   358
fun eta_expand thy assumes origt =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   359
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   360
        val (typet,Tinst) = freeze_thaw_term origt
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   361
        val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   362
        val final = inst_tfrees thy Tinst o thaw
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   363
        val t = #1 (Logic.dest_equals (prop_of init))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   364
        val _ =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   365
            let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   366
                val lhs = #1 (Logic.dest_equals (prop_of (final init)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   367
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   368
                if not (lhs aconv origt)
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   369
                then
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   370
                  writeln (cat_lines
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   371
                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   372
                      Syntax.string_of_term_global thy origt,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   373
                      Syntax.string_of_term_global thy lhs,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   374
                      Syntax.string_of_term_global thy typet,
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   375
                      Syntax.string_of_term_global thy t] @
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   376
                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   377
                else ()
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   378
            end
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   379
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   380
        case t of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   381
            Const("==",T) $ P $ Q =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   382
            if is_Abs P orelse is_Abs Q
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   383
            then (case domain_type T of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   384
                      Type("fun",[aT,bT]) =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   385
                      let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   386
                          val cert = cterm_of thy
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29270
diff changeset
   387
                          val vname = Name.variant (Term.add_free_names t []) "v"
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   388
                          val v = Free(vname,aT)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   389
                          val cv = cert v
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   390
                          val ct = cert t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   391
                          val th1 = (combination (assume ct) (reflexive cv))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   392
                                        |> forall_intr cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   393
                                        |> implies_intr ct
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   394
                          val concl = cert (concl_of th1)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   395
                          val th2 = (assume concl)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   396
                                        |> forall_elim cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   397
                                        |> abstract_rule vname cv
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   398
                          val (lhs,rhs) = Logic.dest_equals (prop_of th2)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   399
                          val elhs = eta_conversion (cert lhs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   400
                          val erhs = eta_conversion (cert rhs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   401
                          val th2' = transitive
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   402
                                         (transitive (symmetric elhs) th2)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   403
                                         erhs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   404
                          val res = equal_intr th1 (th2' |> implies_intr concl)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   405
                          val res' = final res
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   406
                      in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   407
                          SOME res'
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   408
                      end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   409
                    | _ => NONE)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   410
            else NONE
32432
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   411
          | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
64f30bdd3ba1 modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents: 32091
diff changeset
   412
    end;
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   413
14854
61bdf2ae4dc5 removed obsolete sort 'logic';
wenzelm
parents: 14848
diff changeset
   414
fun mk_tfree s = TFree("'"^s,[])
20326
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   415
fun mk_free s t = Free (s,t)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   416
val xT = mk_tfree "a"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   417
val yT = mk_tfree "b"
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   418
val x = Free ("x", xT)
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   419
val y = Free ("y", yT)
20326
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   420
val P  = mk_free "P" (xT-->yT-->propT)
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   421
val Q  = mk_free "Q" (xT-->yT)
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   422
val R  = mk_free "R" (xT-->yT)
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   423
val S  = mk_free "S" xT
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   424
val S'  = mk_free "S'" xT
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   425
in
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   426
fun beta_simproc thy = Simplifier.simproc_i
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   427
                      thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   428
                      "Beta-contraction"
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   429
                      [Abs("x",xT,Q) $ S]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   430
                      beta_fun
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   431
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   432
fun equals_simproc thy = Simplifier.simproc_i
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   433
                      thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   434
                      "Ordered rewriting of meta equalities"
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   435
                      [Const("op ==",xT) $ S $ S']
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   436
                      equals_fun
17188
a26a4fc323ed Updated import.
obua
parents: 16428
diff changeset
   437
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   438
fun quant_simproc thy = Simplifier.simproc_i
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   439
                           thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   440
                           "Ordered rewriting of nested quantifiers"
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   441
                           [Logic.all x (Logic.all y (P $ x $ y))]
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   442
                           quant_rewrite
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   443
fun eta_expand_simproc thy = Simplifier.simproc_i
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   444
                         thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   445
                         "Smart eta-expansion by equivalences"
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   446
                         [Logic.mk_equals(Q,R)]
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   447
                         eta_expand
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   448
fun eta_contract_simproc thy = Simplifier.simproc_i
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   449
                         thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   450
                         "Smart handling of eta-contractions"
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   451
                         [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   452
                         eta_contract
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   453
end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   454
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   455
(* Disambiguates the names of bound variables in a term, returning t
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   456
== t' where all the names of bound variables in t' are unique *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   457
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   458
fun disamb_bound thy t =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   459
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   460
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   461
        fun F (t $ u,idx) =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   462
            let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   463
                val (t',idx') = F (t,idx)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   464
                val (u',idx'') = F (u,idx')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   465
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   466
                (t' $ u',idx'')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   467
            end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   468
          | F (Abs(x,xT,t),idx) =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   469
            let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   470
                val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   471
                val (t',idx') = F (t,idx+1)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   472
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   473
                (Abs(x',xT,t'),idx')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   474
            end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   475
          | F arg = arg
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   476
        val (t',_) = F (t,0)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   477
        val ct = cterm_of thy t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   478
        val ct' = cterm_of thy t'
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   479
        val res = transitive (reflexive ct) (reflexive ct')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   480
        val _ = message ("disamb_term: " ^ (string_of_thm res))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   481
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   482
        res
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   483
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   484
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   485
(* Transforms a term t to some normal form t', returning the theorem t
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   486
== t'.  This is originally a help function for make_equal, but might
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   487
be handy in its own right, for example for indexing terms. *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   488
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   489
fun norm_term thy t =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   490
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   491
        val norms = ShuffleData.get thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   492
        val ss = Simplifier.theory_context thy empty_ss
17892
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17463
diff changeset
   493
          setmksimps single
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   494
          addsimps (map (Thm.transfer thy) norms)
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   495
          addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   496
        fun chain f th =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   497
            let
22902
ac833b4bb7ee moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents: 22846
diff changeset
   498
                val rhs = Thm.rhs_of th
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   499
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   500
                transitive th (f rhs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   501
            end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   502
        val th =
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   503
            t |> disamb_bound thy
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   504
              |> chain (Simplifier.full_rewrite ss)
20326
cbf31171c147 fixed generator
obua
parents: 20224
diff changeset
   505
              |> chain eta_conversion
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   506
              |> strip_shyps
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   507
        val _ = message ("norm_term: " ^ (string_of_thm th))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   508
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   509
        th
17463
e9c1574d0caf removed spurious PolyML.exception_trace;
wenzelm
parents: 17440
diff changeset
   510
    end
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   511
    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   512
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   513
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   514
(* Closes a theorem with respect to free and schematic variables (does
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   515
not touch type variables, though). *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   517
fun close_thm th =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   518
    let
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21588
diff changeset
   519
        val thy = Thm.theory_of_thm th
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   520
        val c = prop_of th
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 28397
diff changeset
   521
        val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   522
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   523
        Drule.forall_intr_list (map (cterm_of thy) vars) th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   524
    end
17959
8db36a108213 OldGoals;
wenzelm
parents: 17892
diff changeset
   525
    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   526
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   527
(* Normalizes a theorem's conclusion using norm_term. *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   528
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   529
fun norm_thm thy th =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   530
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   531
        val c = prop_of th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   532
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   533
        equal_elim (norm_term thy c) th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   534
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   535
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   536
(* make_equal thy t u tries to construct the theorem t == u under the
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   537
signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14854
diff changeset
   538
NONE is returned. *)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   539
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   540
fun make_equal thy t u =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   541
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   542
        val t_is_t' = norm_term thy t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   543
        val u_is_u' = norm_term thy u
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   544
        val th = transitive t_is_t' (symmetric u_is_u')
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   545
        val _ = message ("make_equal: SOME " ^ (string_of_thm th))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   546
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   547
        SOME th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   548
    end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14854
diff changeset
   549
    handle e as THM _ => (message "make_equal: NONE";NONE)
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   550
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   551
fun match_consts ignore t (* th *) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   552
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   553
        fun add_consts (Const (c, _), cs) =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   554
            if c mem_string ignore
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   555
            then cs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   556
            else insert (op =) c cs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   557
          | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   558
          | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   559
          | add_consts (_, cs) = cs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   560
        val t_consts = add_consts(t,[])
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   561
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   562
     fn (name,th) =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   563
        let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   564
            val th_consts = add_consts(prop_of th,[])
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   565
        in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   566
            eq_set(t_consts,th_consts)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   567
        end
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   568
    end
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   569
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   570
val collect_ignored =
21078
101aefd61aac slight cleanup
haftmann
parents: 20951
diff changeset
   571
    fold_rev (fn thm => fn cs =>
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   572
              let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   573
                  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
29287
5b0bfd63b5da eliminated OldTerm.(add_)term_consts;
wenzelm
parents: 29281
diff changeset
   574
                  val ignore_lhs = Term.add_const_names lhs [] \\ Term.add_const_names rhs []
5b0bfd63b5da eliminated OldTerm.(add_)term_consts;
wenzelm
parents: 29281
diff changeset
   575
                  val ignore_rhs = Term.add_const_names rhs [] \\ Term.add_const_names lhs []
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   576
              in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   577
                  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   578
              end)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   579
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   580
(* set_prop t thms tries to make a theorem with the proposition t from
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   581
one of the theorems thms, by shuffling the propositions around.  If it
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14854
diff changeset
   582
succeeds, SOME theorem is returned, otherwise NONE.  *)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   583
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   584
fun set_prop thy t =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   585
    let
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 28397
diff changeset
   586
        val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
27330
1af2598b5f7d Logic.all/mk_equals/mk_implies;
wenzelm
parents: 27173
diff changeset
   587
        val closed_t = fold_rev Logic.all vars t
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   588
        val rew_th = norm_term thy closed_t
22902
ac833b4bb7ee moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents: 22846
diff changeset
   589
        val rhs = Thm.rhs_of rew_th
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   590
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   591
        val shuffles = ShuffleData.get thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   592
        fun process [] = NONE
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   593
          | process ((name,th)::thms) =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   594
            let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   595
                val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   596
                val triv_th = trivial rhs
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   597
                val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
31945
d5f186aa0bed structure Thm: less pervasive names;
wenzelm
parents: 31244
diff changeset
   598
                val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   599
                                 SOME(th,_) => SOME th
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   600
                               | NONE => NONE
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   601
            in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   602
                case mod_th of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   603
                    SOME mod_th =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   604
                    let
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   605
                        val closed_th = equal_elim (symmetric rew_th) mod_th
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   606
                    in
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   607
                        message ("Shuffler.set_prop succeeded by " ^ name);
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   608
                        SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   609
                    end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   610
                  | NONE => process thms
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   611
            end
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   612
            handle e as THM _ => process thms
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   613
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   614
        fn thms =>
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   615
           case process thms of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   616
               res as SOME (name,th) => if (prop_of th) aconv t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   617
                                        then res
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   618
                                        else error "Internal error in set_prop"
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   619
             | NONE => NONE
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   620
    end
17959
8db36a108213 OldGoals;
wenzelm
parents: 17892
diff changeset
   621
    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   622
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   623
fun find_potential thy t =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   624
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   625
        val shuffles = ShuffleData.get thy
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   626
        val ignored = collect_ignored shuffles []
26662
39483503705f Facts.dest_table;
wenzelm
parents: 26424
diff changeset
   627
        val all_thms =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27330
diff changeset
   628
          map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   629
    in
26277
461e11226111 removed obsolete PureThy.thms_containing_consts;
wenzelm
parents: 24634
diff changeset
   630
        List.filter (match_consts ignored t) all_thms
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   631
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   632
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   633
fun gen_shuffle_tac ctxt search thms i st =
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   634
    let
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   635
        val thy = ProofContext.theory_of ctxt
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   636
        val _ = message ("Shuffling " ^ (string_of_thm st))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   637
        val t = List.nth(prems_of st,i-1)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   638
        val set = set_prop thy t
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   639
        fun process_tac thms st =
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   640
            case set thms of
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   641
                SOME (_,th) => Seq.of_list (compose (th,i,st))
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   642
              | NONE => Seq.empty
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   643
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   644
        (process_tac thms APPEND (if search
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   645
                                  then process_tac (find_potential thy t)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   646
                                  else no_tac)) st
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   647
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   648
31244
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   649
fun shuffle_tac ctxt thms =
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   650
  gen_shuffle_tac ctxt false (map (pair "") thms);
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   651
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   652
fun search_tac ctxt =
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   653
  gen_shuffle_tac ctxt true (map (pair "premise") (Assumption.all_prems_of ctxt));
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   654
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   655
fun add_shuffle_rule thm thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   656
    let
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   657
        val shuffles = ShuffleData.get thy
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   658
    in
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   659
        if exists (curry Thm.eq_thm thm) shuffles
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   660
        then (warning ((string_of_thm thm) ^ " already known to the shuffler");
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   661
              thy)
cd0dc678a205 simplified method setup;
wenzelm
parents: 21078
diff changeset
   662
        else ShuffleData.put (thm::shuffles) thy
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   663
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   664
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20854
diff changeset
   665
val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   666
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   667
val setup =
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   668
  Method.setup @{binding shuffle_tac}
31244
4ed31c673baf fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents: 31241
diff changeset
   669
    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt ths)))
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   670
    "solve goal by shuffling terms around" #>
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   671
  Method.setup @{binding search_tac}
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30528
diff changeset
   672
    (Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #>
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   673
  add_shuffle_rule weaken #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   674
  add_shuffle_rule equiv_comm #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   675
  add_shuffle_rule imp_comm #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   676
  add_shuffle_rule Drule.norm_hhf_eq #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   677
  add_shuffle_rule Drule.triv_forall_equality #>
30528
7173bf123335 simplified attribute setup;
wenzelm
parents: 30510
diff changeset
   678
  Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18127
diff changeset
   679
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   680
end