src/Tools/IsaPlanner/rw_inst.ML
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43324 2b47822868e4
child 44121 44adaa6db327
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     1
(*  Title:      Tools/IsaPlanner/rw_inst.ML
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     2
    Author:     Lucas Dixon, University of Edinburgh
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     3
23175
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     4
Rewriting using a conditional meta-equality theorem which supports
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     5
schematic variable instantiation.
267ba70e7a9d tuned headers -- adapted to usual conventions;
wenzelm
parents: 23171
diff changeset
     6
*)   
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     7
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     8
signature RW_INST =
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
     9
sig
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    10
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    11
  (* Rewrite: give it instantiation infromation, a rule, and the
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    12
  target thm, and it will return the rewritten target thm *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    13
  val rw :
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    14
      ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    15
       (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    16
      * (string * Term.typ) list           (* Fake named bounds + types *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    17
      * (string * Term.typ) list           (* names of bound + types *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    18
      * Term.term ->                       (* outer term for instantiation *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    19
      Thm.thm ->                           (* rule with indexies lifted *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    20
      Thm.thm ->                           (* target thm *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    21
      Thm.thm                              (* rewritten theorem possibly 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    22
                                              with additional premises for 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    23
                                              rule conditions *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    24
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    25
  (* used tools *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    26
  val mk_abstractedrule :
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    27
      (string * Term.typ) list (* faked outer bound *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    28
      -> (string * Term.typ) list (* hopeful name of outer bounds *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    29
      -> Thm.thm -> Thm.cterm list * Thm.thm
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    30
  val mk_fixtvar_tyinsts :
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    31
      (Term.indexname * (Term.sort * Term.typ)) list ->
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    32
      Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    33
                        * (string * Term.sort) list
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    34
  val mk_renamings :
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    35
      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    36
  val new_tfree :
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    37
      ((string * int) * Term.sort) *
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    38
      (((string * int) * (Term.sort * Term.typ)) list * string list) ->
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    39
      ((string * int) * (Term.sort * Term.typ)) list * string list
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    40
  val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    41
                   -> (Term.indexname *(Term.typ * Term.term)) list
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    42
  val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    43
                   -> (Term.indexname * (Term.sort * Term.typ)) list
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    44
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    45
  val beta_contract : Thm.thm -> Thm.thm
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    46
  val beta_eta_contract : Thm.thm -> Thm.thm
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    47
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    48
end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    49
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    50
structure RWInst 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    51
: RW_INST
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    52
= struct
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    53
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    54
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    55
(* beta contract the theorem *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    56
fun beta_contract thm = 
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35845
diff changeset
    57
    Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    58
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    59
(* beta-eta contract the theorem *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    60
fun beta_eta_contract thm = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    61
    let
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35845
diff changeset
    62
      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35845
diff changeset
    63
      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    64
    in thm3 end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    65
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    66
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    67
(* to get the free names of a theorem (including hyps and flexes) *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    68
fun usednames_of_thm th =
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    69
    let val rep = Thm.rep_thm th
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    70
      val hyps = #hyps rep
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    71
      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    72
      val prop = #prop rep
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    73
    in
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
    74
      List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    75
    end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    76
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    77
(* Given a list of variables that were bound, and a that has been
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    78
instantiated with free variable placeholders for the bound vars, it
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    79
creates an abstracted version of the theorem, with local bound vars as
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    80
lambda-params:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    81
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    82
Ts: 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    83
("x", ty)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    84
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    85
rule::
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    86
C :x ==> P :x = Q :x
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    87
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    88
results in:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    89
("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    90
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    91
note: assumes rule is instantiated
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    92
*)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    93
(* Note, we take abstraction in the order of last abstraction first *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    94
fun mk_abstractedrule TsFake Ts rule = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    95
    let 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    96
      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    97
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    98
      (* now we change the names of temporary free vars that represent 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
    99
         bound vars with binders outside the redex *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   100
      val prop = Thm.prop_of rule;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   101
      val names = usednames_of_thm rule;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   102
      val (fromnames,tonames,names2,Ts') = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   103
          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 36945
diff changeset
   104
                    let val n2 = singleton (Name.variant_list names) n in
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   105
                      (ctermify (Free(faken,ty)) :: rnf,
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   106
                       ctermify (Free(n2,ty)) :: rnt, 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   107
                       n2 :: names,
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   108
                       (n2,ty) :: Ts'')
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   109
                    end)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   110
                (([],[],names, []), TsFake~~Ts);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   111
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   112
      (* rename conflicting free's in the rule to avoid cconflicts
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   113
      with introduced vars from bounds outside in redex *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   114
      val rule' = rule |> Drule.forall_intr_list fromnames
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   115
                       |> Drule.forall_elim_list tonames;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   116
      
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   117
      (* make unconditional rule and prems *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   118
      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   119
                                                          rule';
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   120
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   121
      (* using these names create lambda-abstracted version of the rule *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   122
      val abstractions = rev (Ts' ~~ tonames);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   123
      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   124
                                    Thm.abstract_rule n ct th)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   125
                                (uncond_rule, abstractions);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   126
    in (cprems, abstract_rule) end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   127
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   128
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   129
(* given names to avoid, and vars that need to be fixed, it gives
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   130
unique new names to the vars so that they can be fixed as free
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   131
variables *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   132
(* make fixed unique free variable instantiations for non-ground vars *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   133
(* Create a table of vars to be renamed after instantiation - ie
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   134
      other uninstantiated vars in the hyps of the rule 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   135
      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   136
fun mk_renamings tgt rule_inst = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   137
    let
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   138
      val rule_conds = Thm.prems_of rule_inst
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29270
diff changeset
   139
      val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   140
      val (conds_tyvs,cond_vs) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   141
          Library.foldl (fn ((tyvs, vs), t) => 
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33038
diff changeset
   142
                    (union (op =) (OldTerm.term_tvars t) tyvs,
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33038
diff changeset
   143
                     union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   144
                (([],[]), rule_conds);
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 23175
diff changeset
   145
      val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33038
diff changeset
   146
      val vars_to_fix = union (op =) termvars cond_vs;
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   147
      val (renamings, names2) = 
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29270
diff changeset
   148
          List.foldr (fn (((n,i),ty), (vs, names')) => 
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 36945
diff changeset
   149
                    let val n' = singleton (Name.variant_list names') n in
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   150
                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   151
                    end)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   152
                ([], names) vars_to_fix;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   153
    in renamings end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   154
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   155
(* make a new fresh typefree instantiation for the given tvar *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   156
fun new_tfree (tv as (ix,sort), (pairs,used)) =
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 36945
diff changeset
   157
      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   158
      in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   159
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   160
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   161
(* make instantiations to fix type variables that are not 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   162
   already instantiated (in ignore_ixs) from the list of terms. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   163
fun mk_fixtvar_tyinsts ignore_insts ts = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   164
    let 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   165
      val ignore_ixs = map fst ignore_insts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   166
      val (tvars, tfrees) = 
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29270
diff changeset
   167
            List.foldr (fn (t, (varixs, tfrees)) => 
29270
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   168
                      (OldTerm.add_term_tvars (t,varixs),
0eade173f77e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   169
                       OldTerm.add_term_tfrees (t,tfrees)))
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   170
                  ([],[]) ts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   171
        val unfixed_tvars = 
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33042
diff changeset
   172
            filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29270
diff changeset
   173
        val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   174
    in (fixtyinsts, tfrees) end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   175
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   176
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   177
(* cross-instantiate the instantiations - ie for each instantiation
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   178
replace all occurances in other instantiations - no loops are possible
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   179
and thus only one-parsing of the instantiations is necessary. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   180
fun cross_inst insts = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   181
    let 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   182
      fun instL (ix, (ty,t)) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   183
          map (fn (ix2,(ty2,t2)) => 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   184
                  (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   185
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   186
      fun cross_instL ([], l) = rev l
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   187
        | cross_instL ((ix, t) :: insts, l) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   188
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   189
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   190
    in cross_instL (insts, []) end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   191
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   192
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   193
fun cross_inst_typs insts = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   194
    let 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   195
      fun instL (ix, (srt,ty)) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   196
          map (fn (ix2,(srt2,ty2)) => 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   197
                  (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   198
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   199
      fun cross_instL ([], l) = rev l
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   200
        | cross_instL ((ix, t) :: insts, l) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   201
          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   202
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   203
    in cross_instL (insts, []) end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   204
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   205
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   206
(* assume that rule and target_thm have distinct var names. THINK:
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   207
efficient version with tables for vars for: target vars, introduced
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   208
vars, and rule vars, for quicker instantiation?  The outerterm defines
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   209
which part of the target_thm was modified.  Note: we take Ts in the
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   210
upterm order, ie last abstraction first., and with an outeterm where
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   211
the abstracted subterm has the arguments in the revered order, ie
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   212
first abstraction first.  FakeTs has abstractions using the fake name
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   213
- ie the name distinct from all other abstractions. *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   214
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   215
fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   216
    let 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   217
      (* general signature info *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   218
      val target_sign = (Thm.theory_of_thm target_thm);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   219
      val ctermify = Thm.cterm_of target_sign;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   220
      val ctypeify = Thm.ctyp_of target_sign;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   221
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   222
      (* fix all non-instantiated tvars *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   223
      val (fixtyinsts, othertfrees) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   224
          mk_fixtvar_tyinsts nonfixed_typinsts
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   225
                             [Thm.prop_of rule, Thm.prop_of target_thm];
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   226
      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   227
                               fixtyinsts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   228
      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   229
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   230
      (* certified instantiations for types *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   231
      val ctyp_insts = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   232
          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   233
              typinsts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   234
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   235
      (* type instantiated versions *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   236
      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   237
      val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   238
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   239
      val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   240
      (* type instanitated outer term *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   241
      val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   242
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   243
      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   244
                              FakeTs;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   245
      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   246
                          Ts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   247
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   248
      (* type-instantiate the var instantiations *)
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29270
diff changeset
   249
      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => 
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   250
                            (ix, (Term.typ_subst_TVars term_typ_inst ty, 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   251
                                  Term.subst_TVars term_typ_inst t))
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   252
                            :: insts_tyinst)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   253
                        [] unprepinsts;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   254
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   255
      (* cross-instantiate *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   256
      val insts_tyinst_inst = cross_inst insts_tyinst;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   257
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   258
      (* create certms of instantiations *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   259
      val cinsts_tyinst = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   260
          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   261
                                  ctermify t)) insts_tyinst_inst;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   262
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   263
      (* The instantiated rule *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   264
      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   265
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   266
      (* Create a table of vars to be renamed after instantiation - ie
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   267
      other uninstantiated vars in the hyps the *instantiated* rule 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   268
      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   269
      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   270
                                   rule_inst;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   271
      val cterm_renamings = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   272
          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   273
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   274
      (* Create the specific version of the rule for this target application *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   275
      val outerterm_inst = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   276
          outerterm_tyinst 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   277
            |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   278
            |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   279
      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   280
      val (cprems, abstract_rule_inst) = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   281
          rule_inst |> Thm.instantiate ([], cterm_renamings)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   282
                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   283
      val specific_tgt_rule = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   284
          beta_eta_contract
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   285
            (Thm.combination couter_inst abstract_rule_inst);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   286
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   287
      (* create an instantiated version of the target thm *)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   288
      val tgt_th_inst = 
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   289
          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   290
                        |> Thm.instantiate ([], cterm_renamings);
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   291
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   292
      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   293
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   294
    in
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   295
      (beta_eta_contract tgt_th_inst)
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   296
        |> Thm.equal_elim specific_tgt_rule
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   297
        |> Drule.implies_intr_list cprems
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   298
        |> Drule.forall_intr_list frees_of_fixed_vars
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   299
        |> Drule.forall_elim_list vars
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 33317
diff changeset
   300
        |> Thm.varifyT_global' othertfrees
23171
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   301
        |-> K Drule.zero_var_indexes
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   302
    end;
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   303
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   304
861f63a35d31 moved IsaPlanner from Provers to Tools;
wenzelm
parents:
diff changeset
   305
end; (* struct *)