src/HOL/Tools/ATP/recon_translate_proof.ML
author paulson
Fri, 08 Apr 2005 18:43:39 +0200
changeset 15684 5ec4d21889d6
parent 15658 2edb384bf61f
child 15697 681bcb7f0389
permissions -rw-r--r--
Reconstruction code, now packaged to avoid name clashes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     2
fun take n [] = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     3
|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     4
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     5
fun drop n [] = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     6
|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     7
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     8
fun remove n [] = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     9
|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    10
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    11
fun remove_nth n [] = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    12
|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    13
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    14
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    15
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    16
fun add_in_order (x:string) [] = [x]
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    17
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    18
                             then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    19
                                  (x::(y::ys))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    20
                             else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    21
                                  (y::(add_in_order x ys))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    22
fun add_once x [] = [x]
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    23
|   add_once x (y::ys) = if (inlist x (y::ys)) then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    24
                            (y::ys)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    25
                        else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    26
                            add_in_order x (y::ys)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    27
     
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
    28
fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    29
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    30
Goal "False ==> False";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    31
by Auto_tac;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    32
qed "False_imp";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    33
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    34
exception Reflex_equal;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    35
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    36
(********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    37
(* Proofstep datatype           *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    38
(********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    39
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    40
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    41
datatype Side = Left |Right
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    42
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    43
 datatype Proofstep = ExtraAxiom
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    44
                     |OrigAxiom
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    45
                     | Axiom
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    46
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    47
                     | MRR of (int * int) * (int * int) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    48
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    49
                     | Para of (int * int) * (int * int) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    50
                     | Rewrite of (int * int) * (int * int)  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    51
                     | Obvious of (int * int)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    52
                     (*| Hyper of int list*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    53
                     | Unusedstep of unit
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    54
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    55
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    56
datatype Clausesimp = Binary_s of int * int
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    57
                      | Factor_s of unit
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    58
                      | Demod_s of (int * int) list
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    59
                      | Hyper_s of int list
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    60
                      | Unusedstep_s of unit
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    61
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    62
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    63
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    64
datatype Step_label = T_info
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    65
                     |P_info
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    66
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    67
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    68
fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    69
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    70
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    71
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    72
fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    73
                                 val exp_term = explode termstr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    74
                             in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    75
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    76
                             end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    77
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    78
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    79
(****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    80
(* Reconstruct an axiom resolution step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    81
(****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    82
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    83
 fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
    84
                                     let val this_axiom =(Recon_Base.assoc  clausenum clauses)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    85
                                         val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    86
                                         val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    87
                                     in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    88
                                         (res, (Axiom,clause_strs,thmvars )  )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    89
                                     end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    90
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    91
(****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    92
(* Reconstruct a binary resolution step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    93
(****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    94
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    95
                 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    96
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    97
        = let
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
    98
              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
    99
              val thm2 =  Recon_Base.assoc  clause2 thml
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   100
              val res =   thm1 RSN ((lit2 +1), thm2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   101
              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   102
              val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   103
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   104
             (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   105
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   106
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   107
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   108
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   109
(******************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   110
(* Reconstruct a matching replacement resolution step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   111
(******************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   112
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   113
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   114
fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   115
        = let
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   116
              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   117
              val thm2 =  Recon_Base.assoc  clause2 thml
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   118
              val res =   thm1 RSN ((lit2 +1), thm2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   119
              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   120
              val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   121
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   122
             (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   123
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   124
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   125
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   126
(*******************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   127
(* Reconstruct a factoring resolution step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   128
(*******************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   129
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   130
fun mksubstlist [] sublist = sublist
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   131
   |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   132
                                          val avar = Var(a,vartype)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   133
                                          val newlist = ((avar,b)::sublist) in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   134
                                          mksubstlist rest newlist
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   135
                                      end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   136
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   137
(* based on Tactic.distinct_subgoals_tac *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   138
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   139
fun delete_assump_tac state lit =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   140
    let val (frozth,thawfn) = freeze_thaw state
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   141
        val froz_prems = cprems_of frozth
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   142
        val assumed = implies_elim_list frozth (map assume froz_prems)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   143
        val new_prems = remove_nth lit froz_prems
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   144
        val implied = implies_intr_list new_prems assumed
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   145
    in  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   146
        Seq.single (thawfn implied)  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   147
    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   148
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   149
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   150
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   151
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   152
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   153
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   154
(* Reconstruct a factoring step      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   155
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   156
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   157
fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   158
                          let 
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   159
                            val th =  Recon_Base.assoc clause thml
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   160
                            val prems = prems_of th
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   161
                            val fac1 = get_nth (lit1+1) prems
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   162
                            val fac2 = get_nth (lit2+1) prems
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   163
                            val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   164
                            val newenv = getnewenv unif_env
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   165
                            val envlist = Envir.alist_of newenv
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   166
                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   167
                            val newsubsts = mksubstlist envlist []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   168
                          in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   169
                            if (is_Var (fst(hd(newsubsts))))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   170
                            then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   171
                                let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   172
                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   173
                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   174
                                   val facthm = read_instantiate [(str1,str2)] th;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   175
                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   176
                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   177
                                   val thmvars = thm_vars res'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   178
                                in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   179
                                       (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   180
                                end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   181
                            else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   182
                                let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   183
                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   184
                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   185
                                   val facthm = read_instantiate [(str1,str2)] th;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   186
                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   187
                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   188
                                  val thmvars = thm_vars res'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   189
                                in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   190
                                       (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   191
                                end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   192
                         end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   193
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   194
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   195
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   196
Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   197
val prems = it;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   198
br (hd prems) 1;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   199
br (hd(tl(tl prems))) 1;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   200
qed "merge";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   201
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   202
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   203
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   204
fun get_unif_comb t eqterm =
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   205
    if ((type_of t) = (type_of eqterm))
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   206
    then t
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   207
    else
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   208
        let val _ $ rand = t
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   209
        in get_unif_comb rand eqterm end;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   210
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   211
fun get_unif_lit t eqterm =
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   212
    if (can HOLogic.dest_eq t)
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   213
    then
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   214
	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   215
	in lhs end
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   216
    else
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   217
	get_unif_comb t eqterm;
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   218
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   219
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   220
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   221
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   222
(* Reconstruct a paramodulation step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   223
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   224
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   225
val rev_subst = rotate_prems 1 subst;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   226
val rev_ssubst = rotate_prems 1 ssubst;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   227
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   228
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   229
(* have changed from negate_nead to negate_head.  God knows if this will actually work *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   230
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   231
                          let 
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   232
                            val th1 =  Recon_Base.assoc clause1 thml
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   233
                            val th2 =  Recon_Base.assoc clause2 thml 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   234
                            val eq_lit_th = select_literal (lit1+1) th1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   235
                            val mod_lit_th = select_literal (lit2+1) th2
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   236
                            val eqsubst = eq_lit_th RSN (2,rev_subst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   237
                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   238
			    val newth' =negate_head newth 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   239
                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   240
                                handle Not_in_list => let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   241
                                                  val mod_lit_th' = mod_lit_th RS not_sym
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   242
                                                   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   243
			                           val newth' =negate_head newth 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   244
                                               in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   245
                                                  (rearrange_clause newth' clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   246
                                               end)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   247
                            val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   248
                         in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   249
                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   250
                         end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   251
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   252
(*              
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   253
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   254
                          let 
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   255
                            val th1 =  Recon_Base.assoc clause1 thml
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   256
                            val th2 =  Recon_Base.assoc clause2 thml 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   257
                            val eq_lit_th = select_literal (lit1+1) th1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   258
                            val mod_lit_th = select_literal (lit2+1) th2
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   259
                            val eqsubst = eq_lit_th RSN (2,rev_subst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   260
                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   261
			    val newth' =negate_nead newth 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   262
                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   263
                            val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   264
                         in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   265
                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   266
                         end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   267
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   268
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   269
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   270
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   271
(********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   272
(* Reconstruct a rewriting step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   273
(********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   274
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   275
(*
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   276
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   277
val rev_subst = rotate_prems 1 subst;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   278
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   279
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   280
     let  val eq_lit_th = select_literal (lit1+1) cl1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   281
          val mod_lit_th = select_literal (lit2+1) cl2
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   282
          val eqsubst = eq_lit_th RSN (2,rev_subst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   283
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   284
eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   285
     in negated_asm_of_head newth end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   286
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   287
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   288
eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   289
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   290
val mod_lit_th' = mod_lit_th RS not_sym
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   291
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   292
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   293
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   294
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   295
fun delete_assumps 0 th = th 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   296
|   delete_assumps n th = let val th_prems = length (prems_of th)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   297
                              val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   298
                          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   299
                              delete_assumps (n-1) th'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   300
                          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   301
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   302
(* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   303
(* changed negate_nead to negate_head here too*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   304
                    (* clause1, lit1 is thing to rewrite with *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   305
fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   306
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   307
                          let val th1 =  Recon_Base.assoc clause1 thml
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   308
                              val th2 = Recon_Base.assoc clause2 thml
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   309
                              val eq_lit_th = select_literal (lit1+1) th1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   310
                              val mod_lit_th = select_literal (lit2+1) th2
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   311
                              val eqsubst = eq_lit_th RSN (2,rev_subst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   312
                              val eq_lit_prem_num = length (prems_of eq_lit_th)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   313
                              val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   314
                              val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   315
eqsubst)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   316
                         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   317
                              val newthm = negate_head newth
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   318
                              val newthm' = delete_assumps eq_lit_prem_num newthm
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   319
                              val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   320
                              val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   321
                           in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   322
                               (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   323
                           end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   324
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   325
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   326
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   327
(*****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   328
(* Reconstruct an obvious reduction step *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   329
(*****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   330
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   331
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   332
fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15658
diff changeset
   333
                           let val th1 =  Recon_Base.assoc clause1 thml
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   334
                               val prems1 = prems_of th1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   335
                               val newthm = refl RSN ((lit1+ 1), th1)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   336
                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   337
                               val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   338
                               val thmvars = thm_vars res
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   339
                           in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   340
                               (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   341
                           end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   342
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   343
(**************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   344
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   345
(**************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   346
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   347
 fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   348
        = follow_axiom clauses allvars  clausenum thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   349
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   350
      | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   351
        = follow_binary  (a, b)  allvars thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   352
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   353
      | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   354
        = follow_mrr (a, b)  allvars thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   355
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   356
      | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   357
         = follow_factor a b c  allvars thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   358
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   359
      | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   360
        = follow_standard_para (a, b) allvars  thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   361
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   362
      | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   363
        = follow_rewrite (a,b)  allvars thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   364
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   365
      | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   366
        = follow_obvious (a,b)  allvars thml clause_strs
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   367
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   368
      (*| follow_proof clauses  clausenum thml (Hyper l)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   369
        = follow_hyper l thml*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   370
      | follow_proof clauses  allvars clausenum  thml _ _ =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   371
          raise ASSERTION  "proof step not implemented"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   372
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   373
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   374
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   375
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   376
(**************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   377
(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   378
(**************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   379
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   380
    fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   381
        = let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   382
            val (thm, recon_fun) = follow_proof clauses  allvars clause_num thml proof_step clause_strs 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   383
            val recon_step = (recon_fun)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   384
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   385
            (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   386
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   387
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   388
(***************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   389
(* follow through the res. proof, creating an Isabelle theorem *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   390
(***************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   391
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   392
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   393
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   394
(*fun is_proof_char ch = (case ch of 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   395
                       
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   396
                        "(" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   397
                       |  ")" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   398
                         | ":" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   399
                        |  "'" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   400
                        |  "&" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   401
                        | "|" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   402
                        | "~" => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   403
                        |  "." => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   404
                        |(is_alpha ) => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   405
                       |(is_digit) => true
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   406
                         | _ => false)*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   407
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   408
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   409
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   410
fun proofstring x = let val exp = explode x 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   411
                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   412
                        List.filter (is_proof_char ) exp
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   413
                    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   414
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   415
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   416
fun not_newline ch = not (ch = "\n");
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   417
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   418
fun concat_with_and [] str = str
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   419
|   concat_with_and (x::[]) str = str^"("^x^")"
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   420
|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   421
(*
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   422
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   423
fun follow clauses [] allvars thml recons = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   424
                             let (* val _ = reset show_sorts*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   425
                              val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   426
                              val thmproofstring = proofstring ( thmstring)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   427
                            val no_returns =List.filter  not_newline ( thmproofstring)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   428
                            val thmstr = implode no_returns
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15642
diff changeset
   429
                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   430
                               val _ = TextIO.output(outfile, "thmstr is "^thmstr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   431
                               val _ = TextIO.flushOut outfile;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   432
                               val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   433
                                 (*val _ = set show_sorts*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   434
                             in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   435
                                  ((snd( hd thml)), recons)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   436
                             end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   437
      | follow clauses (h::t) allvars thml recons 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   438
        = let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   439
            val (thml', recons') = follow_line clauses allvars  thml h recons
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   440
            val  (thm, recons_list) = follow clauses t  allvars thml' recons'
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   441
            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   442
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   443
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   444
             (thm,recons_list)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   445
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   446
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   447
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   448
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   449
fun replace_clause_strs [] recons newrecons= (newrecons)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   450
|   replace_clause_strs ((thmnum, thm)::thml)  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   451
                           let val new_clause_strs = get_meta_lits_bracket thm
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   452
                           in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   453
                               replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   454
                           end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   455
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   456
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   457
fun follow clauses [] allvars thml recons = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   458
                             let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   459
                                 val new_recons = replace_clause_strs thml recons []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   460
                             in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   461
                                  ((snd( hd thml)), new_recons)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   462
                             end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   463
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   464
 |  follow clauses (h::t) allvars thml recons 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   465
        = let
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   466
            val (thml', recons') = follow_line clauses allvars  thml h recons
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   467
            val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   468
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   469
             (thm,recons_list)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   470
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   471
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   472
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   473
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   474
(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   475
 (* and the proof as a list of the proper datatype *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   476
(* take the cnf clauses of the goal and the proof from the res. prover *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   477
(* as a list of type Proofstep and return the thm goal ==> False *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   478
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   479
fun first_pair (a,b,c) = (a,b);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   480
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   481
fun second_pair (a,b,c) = (b,c);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   482
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   483
(* takes original axioms, proof_steps parsed from spass, variables *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   484
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   485
fun translate_proof clauses proof allvars
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   486
        = let val (thm, recons) = follow clauses proof allvars [] []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   487
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   488
             (thm, (recons))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   489
          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   490
  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   491
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   492
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   493
fun remove_tinfo [] = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   494
|   remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)