src/HOL/ex/reflection.ML
author wenzelm
Thu Aug 03 15:03:05 2006 +0200 (2006-08-03)
changeset 20319 a8761e8568de
child 20374 01b711328990
permissions -rw-r--r--
Generic reflection and reification (by Amine Chaieb).
wenzelm@20319
     1
(*
wenzelm@20319
     2
    ID:         $Id$
wenzelm@20319
     3
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     4
wenzelm@20319
     5
A trial for automatical reification.
wenzelm@20319
     6
*)
wenzelm@20319
     7
wenzelm@20319
     8
signature REFLECTION = sig
wenzelm@20319
     9
  val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
wenzelm@20319
    10
  val reflection_tac: Proof.context -> thm list -> term option -> int -> tactic
wenzelm@20319
    11
end;
wenzelm@20319
    12
wenzelm@20319
    13
structure Reflection : REFLECTION
wenzelm@20319
    14
= struct
wenzelm@20319
    15
wenzelm@20319
    16
    (* Make a congruence rule out of a defining equation for the interpretation *)
wenzelm@20319
    17
        (* th is one defining equation of f, i.e.
wenzelm@20319
    18
           th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
wenzelm@20319
    19
        (* Cp is a constructor pattern and P is a pattern *)
wenzelm@20319
    20
wenzelm@20319
    21
        (* The result is:
wenzelm@20319
    22
         [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
wenzelm@20319
    23
        (*  + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
wenzelm@20319
    24
wenzelm@20319
    25
fun mk_congeq ctxt fs th =
wenzelm@20319
    26
  let
wenzelm@20319
    27
    val Const(fname,fT)$(Free(_,_))$_ =
wenzelm@20319
    28
        (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
wenzelm@20319
    29
    val thy = ProofContext.theory_of ctxt;
wenzelm@20319
    30
    val cert = Thm.cterm_of thy;
wenzelm@20319
    31
    fun dest_listT (Type ("List.list",[vT])) = vT;
wenzelm@20319
    32
    val vT = dest_listT (Term.domain_type fT);
wenzelm@20319
    33
    val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt;
wenzelm@20319
    34
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
wenzelm@20319
    35
wenzelm@20319
    36
    fun add_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319
    37
          if exists (fn f => t1 aconv f) fs then insert (op aconv) t
wenzelm@20319
    38
          else add_fterms (t1 $ t2) #> add_fterms t3
wenzelm@20319
    39
      | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
wenzelm@20319
    40
      | add_fterms (Abs _) = sys_error "FIXME"
wenzelm@20319
    41
      | add_fterms _ = I;
wenzelm@20319
    42
    val fterms = add_fterms rhs [];
wenzelm@20319
    43
wenzelm@20319
    44
    val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt';
wenzelm@20319
    45
    val tys = map fastype_of fterms
wenzelm@20319
    46
    val vs = map Free (xs ~~ tys);
wenzelm@20319
    47
    val env = fterms ~~ vs;
wenzelm@20319
    48
wenzelm@20319
    49
    fun replace_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319
    50
          (case AList.lookup (op aconv) env t of
wenzelm@20319
    51
            SOME v => v
wenzelm@20319
    52
          | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
wenzelm@20319
    53
      | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
wenzelm@20319
    54
      | replace_fterms t = t;
wenzelm@20319
    55
wenzelm@20319
    56
    fun mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t));
wenzelm@20319
    57
    val cong = (Goal.prove ctxt'' [] (map mk_def env)
wenzelm@20319
    58
      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
wenzelm@20319
    59
      (fn x => LocalDefs.unfold_tac (#context x) (#prems x) THEN rtac th' 1)) RS sym;
wenzelm@20319
    60
wenzelm@20319
    61
    val (cong' :: vars') = Variable.export ctxt'' ctxt
wenzelm@20319
    62
      (cong :: map (Drule.mk_term o cert) vs);
wenzelm@20319
    63
    val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
wenzelm@20319
    64
  in (vs', cong') end;
wenzelm@20319
    65
wenzelm@20319
    66
 (* congs is a list of pairs (P,th) where th is a theorem for *)
wenzelm@20319
    67
        (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
wenzelm@20319
    68
val FWD = curry (op OF);
wenzelm@20319
    69
wenzelm@20319
    70
 (* da is the decomposition for atoms, ie. it returns ([],g) where g
wenzelm@20319
    71
 returns the right instance f (AtC n) = t , where AtC is the Atoms
wenzelm@20319
    72
 constructor and n is the number of the atom corresponding to t *)
wenzelm@20319
    73
wenzelm@20319
    74
(* Generic decomp for reification : matches the actual term with the
wenzelm@20319
    75
rhs of one cong rule. The result of the matching guides the
wenzelm@20319
    76
proof synthesis: The matches of the introduced Variables A1 .. An are
wenzelm@20319
    77
processed recursively
wenzelm@20319
    78
 The rest is instantiated in the cong rule,i.e. no reification is needed *)
wenzelm@20319
    79
wenzelm@20319
    80
 fun decomp_genreif thy da ((vns,cong)::congs) t =
wenzelm@20319
    81
    ((let
wenzelm@20319
    82
        val cert = cterm_of thy
wenzelm@20319
    83
        val (_, tmenv) =
wenzelm@20319
    84
        Pattern.match thy
wenzelm@20319
    85
        ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
wenzelm@20319
    86
        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
wenzelm@20319
    87
        val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
wenzelm@20319
    88
        val (fts,its) = (map (snd o snd) fnvs,
wenzelm@20319
    89
                         map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
wenzelm@20319
    90
    in (fts, FWD (instantiate ([], its) cong))
wenzelm@20319
    91
    end)
wenzelm@20319
    92
      handle MATCH => decomp_genreif thy da congs t)
wenzelm@20319
    93
   | decomp_genreif thy da [] t = da t;
wenzelm@20319
    94
wenzelm@20319
    95
     (* We add the atoms here during reification *)
wenzelm@20319
    96
val env = ref ([]: (term list));
wenzelm@20319
    97
wenzelm@20319
    98
fun env_index t =
wenzelm@20319
    99
    let val i = find_index_eq t (!env)
wenzelm@20319
   100
    in if i = ~1 then (env:= (!env)@[t] ; (length (!env)) - 1) else i  end;
wenzelm@20319
   101
wenzelm@20319
   102
exception REIF of string;
wenzelm@20319
   103
wenzelm@20319
   104
          (* looks for the atoms equation and instantiates it with the right number *)
wenzelm@20319
   105
fun mk_decompatom thy eqs =
wenzelm@20319
   106
    let fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
wenzelm@20319
   107
          | isateq _ = false
wenzelm@20319
   108
    in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
wenzelm@20319
   109
           NONE => raise REIF "Can not find the atoms equation"
wenzelm@20319
   110
         | SOME th =>
wenzelm@20319
   111
           fn t => ([],
wenzelm@20319
   112
                    fn ths =>
wenzelm@20319
   113
                       instantiate' [] [SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
wenzelm@20319
   114
                                    (th RS sym))
wenzelm@20319
   115
    end;
wenzelm@20319
   116
wenzelm@20319
   117
  (* Generic reification procedure: *)
wenzelm@20319
   118
  (* creates all needed cong rules and then just uses the theorem synthesis *)
wenzelm@20319
   119
fun genreif ctxt raw_eqs t =
wenzelm@20319
   120
    let val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
wenzelm@20319
   121
        val thy = ProofContext.theory_of ctxt'
wenzelm@20319
   122
        val cert = cterm_of thy
wenzelm@20319
   123
        val Const(fname,fT)$(Var(_,vT))$_ =
wenzelm@20319
   124
            (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (hd raw_eqs)
wenzelm@20319
   125
        val cv = cert (Free(x, vT))
wenzelm@20319
   126
        val eqs = map (instantiate' [] [SOME cv]) raw_eqs
wenzelm@20319
   127
        val fs =
wenzelm@20319
   128
            foldr (fn (eq,fns) =>
wenzelm@20319
   129
                      let val f$_$_ =  (fst o HOLogic.dest_eq o
wenzelm@20319
   130
                                        HOLogic.dest_Trueprop o prop_of) eq
wenzelm@20319
   131
                      in f ins fns end) [] eqs
wenzelm@20319
   132
        val congs = map (mk_congeq ctxt' fs) eqs
wenzelm@20319
   133
        val _ = (env := [])
wenzelm@20319
   134
        val da = mk_decompatom thy eqs
wenzelm@20319
   135
        val [th] = Variable.export ctxt' ctxt
wenzelm@20319
   136
                 [divide_and_conquer (decomp_genreif thy da congs) t]
wenzelm@20319
   137
        val cv' = cterm_of (ProofContext.theory_of ctxt)
wenzelm@20319
   138
                           (HOLogic.mk_list I (body_type fT) (!env))
wenzelm@20319
   139
        val _ = (env := [])
wenzelm@20319
   140
        val th' = instantiate' [] [SOME cv'] th
wenzelm@20319
   141
        val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
wenzelm@20319
   142
        val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
wenzelm@20319
   143
                   (fn _ => Simp_tac 1)
wenzelm@20319
   144
    in FWD trans [th'',th']
wenzelm@20319
   145
    end;
wenzelm@20319
   146
wenzelm@20319
   147
fun genreflect ctxt corr_thm raw_eqs t =
wenzelm@20319
   148
    let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
wenzelm@20319
   149
        val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th
wenzelm@20319
   150
        val rth = normalization_conv ft
wenzelm@20319
   151
    in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
wenzelm@20319
   152
                (simplify (HOL_basic_ss addsimps [rth]) th)
wenzelm@20319
   153
    end
wenzelm@20319
   154
wenzelm@20319
   155
fun genreify_tac ctxt eqs to i = (fn st =>
wenzelm@20319
   156
  let
wenzelm@20319
   157
    val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
wenzelm@20319
   158
    val t = (case to of NONE => P | SOME x => x)
wenzelm@20319
   159
    val th = (genreif ctxt eqs t) RS ssubst
wenzelm@20319
   160
  in rtac th i st
wenzelm@20319
   161
  end);
wenzelm@20319
   162
wenzelm@20319
   163
    (* Reflection calls reification and uses the correctness *)
wenzelm@20319
   164
        (* theorem assumed to be the dead of the list *)
wenzelm@20319
   165
 fun reflection_tac ctxt (corr_thm::raw_eqs) to i =
wenzelm@20319
   166
    (fn st =>
wenzelm@20319
   167
        let val P = (HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)))
wenzelm@20319
   168
            val t = (case to of NONE => P | SOME x => x)
wenzelm@20319
   169
            val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
wenzelm@20319
   170
        in rtac th i st end);
wenzelm@20319
   171
wenzelm@20319
   172
end