src/HOL/ex/reflection.ML
author chaieb
Mon Aug 14 11:13:50 2006 +0200 (2006-08-14)
changeset 20374 01b711328990
parent 20319 a8761e8568de
child 20564 6857bd9f1a79
permissions -rw-r--r--
Reification now handels binders.
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
chaieb@20374
    16
val ext2 = thm "ext2";
chaieb@20374
    17
  (* Make a congruence rule out of a defining equation for the interpretation *)
chaieb@20374
    18
  (* th is one defining equation of f, i.e.
chaieb@20374
    19
     th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
chaieb@20374
    20
  (* Cp is a constructor pattern and P is a pattern *)
chaieb@20374
    21
chaieb@20374
    22
  (* The result is:
chaieb@20374
    23
      [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
chaieb@20374
    24
  (*  + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
chaieb@20374
    25
chaieb@20374
    26
chaieb@20374
    27
fun mk_congeq ctxt fs th = 
chaieb@20374
    28
  let 
chaieb@20374
    29
   val Const(fname,fT)$(vs as Free(_,_))$_ =
chaieb@20374
    30
       (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
chaieb@20374
    31
   val thy = ProofContext.theory_of ctxt
chaieb@20374
    32
   val cert = Thm.cterm_of thy
chaieb@20374
    33
   fun dest_listT (Type ("List.list",[vT])) = vT
chaieb@20374
    34
   val vT = dest_listT (Term.domain_type fT)
chaieb@20374
    35
   val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
chaieb@20374
    36
   val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
wenzelm@20319
    37
chaieb@20374
    38
   fun add_fterms (t as t1 $ t2 $ t3) =
chaieb@20374
    39
       if exists (fn f => t1 aconv f) fs then insert (op aconv) t
chaieb@20374
    40
       else add_fterms (t1 $ t2) #> add_fterms t3
chaieb@20374
    41
     | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
chaieb@20374
    42
     | add_fterms (t as Abs(xn,xT,t')) = 
chaieb@20374
    43
       if (vs mem (term_frees t)) then (fn _ => [t]) else (fn _ => [])
chaieb@20374
    44
     | add_fterms _ = I
chaieb@20374
    45
   val fterms = add_fterms rhs []
chaieb@20374
    46
   val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt'
chaieb@20374
    47
   val tys = map fastype_of fterms
chaieb@20374
    48
   val vs = map Free (xs ~~ tys)
chaieb@20374
    49
   val env = fterms ~~ vs
chaieb@20374
    50
  
chaieb@20374
    51
   fun replace_fterms (t as t1 $ t2 $ t3) =
chaieb@20374
    52
       (case AList.lookup (op aconv) env t of
chaieb@20374
    53
	    SOME v => v
chaieb@20374
    54
	  | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
chaieb@20374
    55
     | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
chaieb@20374
    56
     | replace_fterms t = (case AList.lookup (op aconv) env t of
chaieb@20374
    57
			       SOME v => v
chaieb@20374
    58
			     | NONE => t)
chaieb@20374
    59
      
chaieb@20374
    60
   fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
chaieb@20374
    61
     | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
chaieb@20374
    62
   fun tryext x = (x RS ext2 handle _ =>  x)
chaieb@20374
    63
   val cong = (Goal.prove ctxt'' [] (map mk_def env)
chaieb@20374
    64
			  (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
chaieb@20374
    65
			  (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) 
chaieb@20374
    66
							THEN rtac th' 1)) RS sym
chaieb@20374
    67
	      
chaieb@20374
    68
   val (cong' :: vars') = 
chaieb@20374
    69
       Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
chaieb@20374
    70
   val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'
chaieb@20374
    71
					      
chaieb@20374
    72
  in  (vs', cong') end; 
chaieb@20374
    73
  
wenzelm@20319
    74
chaieb@20374
    75
(*
wenzelm@20319
    76
fun mk_congeq ctxt fs th =
wenzelm@20319
    77
  let
wenzelm@20319
    78
    val Const(fname,fT)$(Free(_,_))$_ =
wenzelm@20319
    79
        (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
wenzelm@20319
    80
    val thy = ProofContext.theory_of ctxt;
wenzelm@20319
    81
    val cert = Thm.cterm_of thy;
wenzelm@20319
    82
    fun dest_listT (Type ("List.list",[vT])) = vT;
wenzelm@20319
    83
    val vT = dest_listT (Term.domain_type fT);
wenzelm@20319
    84
    val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt;
wenzelm@20319
    85
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
wenzelm@20319
    86
wenzelm@20319
    87
    fun add_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319
    88
          if exists (fn f => t1 aconv f) fs then insert (op aconv) t
wenzelm@20319
    89
          else add_fterms (t1 $ t2) #> add_fterms t3
wenzelm@20319
    90
      | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
wenzelm@20319
    91
      | add_fterms (Abs _) = sys_error "FIXME"
wenzelm@20319
    92
      | add_fterms _ = I;
wenzelm@20319
    93
    val fterms = add_fterms rhs [];
wenzelm@20319
    94
wenzelm@20319
    95
    val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt';
wenzelm@20319
    96
    val tys = map fastype_of fterms
wenzelm@20319
    97
    val vs = map Free (xs ~~ tys);
wenzelm@20319
    98
    val env = fterms ~~ vs;
wenzelm@20319
    99
wenzelm@20319
   100
    fun replace_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319
   101
          (case AList.lookup (op aconv) env t of
wenzelm@20319
   102
            SOME v => v
wenzelm@20319
   103
          | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
wenzelm@20319
   104
      | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
wenzelm@20319
   105
      | replace_fterms t = t;
wenzelm@20319
   106
wenzelm@20319
   107
    fun mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t));
wenzelm@20319
   108
    val cong = (Goal.prove ctxt'' [] (map mk_def env)
wenzelm@20319
   109
      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
wenzelm@20319
   110
      (fn x => LocalDefs.unfold_tac (#context x) (#prems x) THEN rtac th' 1)) RS sym;
wenzelm@20319
   111
wenzelm@20319
   112
    val (cong' :: vars') = Variable.export ctxt'' ctxt
wenzelm@20319
   113
      (cong :: map (Drule.mk_term o cert) vs);
wenzelm@20319
   114
    val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
wenzelm@20319
   115
  in (vs', cong') end;
chaieb@20374
   116
*)
wenzelm@20319
   117
 (* congs is a list of pairs (P,th) where th is a theorem for *)
wenzelm@20319
   118
        (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
wenzelm@20319
   119
val FWD = curry (op OF);
wenzelm@20319
   120
wenzelm@20319
   121
 (* da is the decomposition for atoms, ie. it returns ([],g) where g
wenzelm@20319
   122
 returns the right instance f (AtC n) = t , where AtC is the Atoms
wenzelm@20319
   123
 constructor and n is the number of the atom corresponding to t *)
wenzelm@20319
   124
wenzelm@20319
   125
(* Generic decomp for reification : matches the actual term with the
wenzelm@20319
   126
rhs of one cong rule. The result of the matching guides the
wenzelm@20319
   127
proof synthesis: The matches of the introduced Variables A1 .. An are
wenzelm@20319
   128
processed recursively
wenzelm@20319
   129
 The rest is instantiated in the cong rule,i.e. no reification is needed *)
wenzelm@20319
   130
chaieb@20374
   131
exception REIF of string;
chaieb@20374
   132
chaieb@20374
   133
val env = ref ([]: (term list));
chaieb@20374
   134
val bnds = ref ([]: (term list));
chaieb@20374
   135
fun env_index t =
chaieb@20374
   136
    let val i = find_index_eq t (!env)
chaieb@20374
   137
        val j = find_index_eq t (!bnds)
chaieb@20374
   138
    in if j = ~1 then if i = ~1 then (env:= (!env)@[t] ; (length ((!bnds)@(!env))) - 1) else i
chaieb@20374
   139
                 else j end;
chaieb@20374
   140
chaieb@20374
   141
fun decomp_genreif da cgns (t,ctxt) =
chaieb@20374
   142
  let 
chaieb@20374
   143
   val thy = ProofContext.theory_of ctxt 
chaieb@20374
   144
   val cert = cterm_of thy
chaieb@20374
   145
   fun tryabsdecomp (s,ctxt) = 
chaieb@20374
   146
    (case s of 
chaieb@20374
   147
      Abs(xn,xT,ta) => 
chaieb@20374
   148
       (let
chaieb@20374
   149
	 val ([xn],ctxt') = Variable.invent_fixes ["x"] ctxt
chaieb@20374
   150
	 val (xn,ta) = variant_abs (xn,xT,ta)
chaieb@20374
   151
         val x = Free(xn,xT)
chaieb@20374
   152
         val _ = (bnds := x::(!bnds))
chaieb@20374
   153
	in ([(ta, ctxt')] , fn [th] => 
chaieb@20374
   154
			       (bnds := tl (!bnds) ; 
chaieb@20374
   155
				hd (Variable.export ctxt' ctxt 
chaieb@20374
   156
						    [(forall_intr (cert x) th) COMP allI])))
chaieb@20374
   157
	end)
chaieb@20374
   158
    | _ => da (s,ctxt))
chaieb@20374
   159
  in 
chaieb@20374
   160
  (case cgns of 
chaieb@20374
   161
    [] => tryabsdecomp (t,ctxt)
chaieb@20374
   162
  | ((vns,cong)::congs) => ((let
chaieb@20374
   163
        val cert = cterm_of thy
chaieb@20374
   164
        val (_, tmenv) =
chaieb@20374
   165
        Pattern.match thy
chaieb@20374
   166
        ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
chaieb@20374
   167
        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
chaieb@20374
   168
        val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
chaieb@20374
   169
        val (fts,its) = (map (snd o snd) fnvs,
chaieb@20374
   170
                         map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
chaieb@20374
   171
    in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate ([], its) cong))
chaieb@20374
   172
    end)
chaieb@20374
   173
      handle MATCH => decomp_genreif da congs (t,ctxt)))
chaieb@20374
   174
  end;
chaieb@20374
   175
chaieb@20374
   176
(*
wenzelm@20319
   177
 fun decomp_genreif thy da ((vns,cong)::congs) t =
wenzelm@20319
   178
    ((let
wenzelm@20319
   179
        val cert = cterm_of thy
wenzelm@20319
   180
        val (_, tmenv) =
wenzelm@20319
   181
        Pattern.match thy
wenzelm@20319
   182
        ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
wenzelm@20319
   183
        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
wenzelm@20319
   184
        val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
wenzelm@20319
   185
        val (fts,its) = (map (snd o snd) fnvs,
wenzelm@20319
   186
                         map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
wenzelm@20319
   187
    in (fts, FWD (instantiate ([], its) cong))
wenzelm@20319
   188
    end)
wenzelm@20319
   189
      handle MATCH => decomp_genreif thy da congs t)
wenzelm@20319
   190
   | decomp_genreif thy da [] t = da t;
wenzelm@20319
   191
wenzelm@20319
   192
     (* We add the atoms here during reification *)
wenzelm@20319
   193
val env = ref ([]: (term list));
wenzelm@20319
   194
wenzelm@20319
   195
fun env_index t =
wenzelm@20319
   196
    let val i = find_index_eq t (!env)
wenzelm@20319
   197
    in if i = ~1 then (env:= (!env)@[t] ; (length (!env)) - 1) else i  end;
chaieb@20374
   198
*)
wenzelm@20319
   199
wenzelm@20319
   200
          (* looks for the atoms equation and instantiates it with the right number *)
chaieb@20374
   201
chaieb@20374
   202
fun mk_decompatom eqs (t,ctxt) =
chaieb@20374
   203
    let 
chaieb@20374
   204
      val thy = ProofContext.theory_of ctxt
chaieb@20374
   205
      fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
chaieb@20374
   206
        | isateq _ = false
chaieb@20374
   207
    in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
chaieb@20374
   208
           NONE => raise REIF "Can not find the atoms equation"
chaieb@20374
   209
         | SOME th =>
chaieb@20374
   210
	   ([],
chaieb@20374
   211
	    fn ths =>
chaieb@20374
   212
               let val _ = print_thm th
chaieb@20374
   213
                   val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
chaieb@20374
   214
                   val (Const("List.nth",_)$vs$_) = 
chaieb@20374
   215
                       (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
chaieb@20374
   216
                   val vsT = fastype_of vs
chaieb@20374
   217
                   val Type("List.list",[vT]) = vsT
chaieb@20374
   218
                   val cvs = cterm_of thy (foldr (fn (x,xs) => Const("List.list.Cons", vT --> vsT --> vsT)$x$xs) (Free(x,vsT)) (!bnds))
chaieb@20374
   219
                   val _ = print_thm (th RS sym)
chaieb@20374
   220
                   val _ = print_cterm cvs
chaieb@20374
   221
                   val th' = instantiate' [] 
chaieb@20374
   222
					  [SOME cvs, 
chaieb@20374
   223
                                           SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
chaieb@20374
   224
                                          (th RS sym)
chaieb@20374
   225
               in hd (Variable.export ctxt' ctxt [th']) end)
chaieb@20374
   226
    end;
chaieb@20374
   227
chaieb@20374
   228
(*
wenzelm@20319
   229
fun mk_decompatom thy eqs =
wenzelm@20319
   230
    let fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
wenzelm@20319
   231
          | isateq _ = false
wenzelm@20319
   232
    in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
wenzelm@20319
   233
           NONE => raise REIF "Can not find the atoms equation"
wenzelm@20319
   234
         | SOME th =>
wenzelm@20319
   235
           fn t => ([],
wenzelm@20319
   236
                    fn ths =>
wenzelm@20319
   237
                       instantiate' [] [SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
wenzelm@20319
   238
                                    (th RS sym))
wenzelm@20319
   239
    end;
chaieb@20374
   240
*)
wenzelm@20319
   241
  (* Generic reification procedure: *)
wenzelm@20319
   242
  (* creates all needed cong rules and then just uses the theorem synthesis *)
wenzelm@20319
   243
fun genreif ctxt raw_eqs t =
wenzelm@20319
   244
    let val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
wenzelm@20319
   245
        val thy = ProofContext.theory_of ctxt'
wenzelm@20319
   246
        val cert = cterm_of thy
wenzelm@20319
   247
        val Const(fname,fT)$(Var(_,vT))$_ =
wenzelm@20319
   248
            (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (hd raw_eqs)
wenzelm@20319
   249
        val cv = cert (Free(x, vT))
wenzelm@20319
   250
        val eqs = map (instantiate' [] [SOME cv]) raw_eqs
wenzelm@20319
   251
        val fs =
wenzelm@20319
   252
            foldr (fn (eq,fns) =>
wenzelm@20319
   253
                      let val f$_$_ =  (fst o HOLogic.dest_eq o
wenzelm@20319
   254
                                        HOLogic.dest_Trueprop o prop_of) eq
wenzelm@20319
   255
                      in f ins fns end) [] eqs
wenzelm@20319
   256
        val congs = map (mk_congeq ctxt' fs) eqs
chaieb@20374
   257
        val congs = (map fst congs) ~~ (Variable.export ctxt' ctxt (map snd congs))
wenzelm@20319
   258
        val _ = (env := [])
chaieb@20374
   259
        val _ = (bnds := [])
chaieb@20374
   260
        val da = mk_decompatom raw_eqs
chaieb@20374
   261
        val th = divide_and_conquer (decomp_genreif da congs) (t,ctxt)
wenzelm@20319
   262
        val cv' = cterm_of (ProofContext.theory_of ctxt)
wenzelm@20319
   263
                           (HOLogic.mk_list I (body_type fT) (!env))
wenzelm@20319
   264
        val _ = (env := [])
chaieb@20374
   265
        val _ = (bnds:= [])
wenzelm@20319
   266
        val th' = instantiate' [] [SOME cv'] th
wenzelm@20319
   267
        val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
wenzelm@20319
   268
        val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
wenzelm@20319
   269
                   (fn _ => Simp_tac 1)
wenzelm@20319
   270
    in FWD trans [th'',th']
wenzelm@20319
   271
    end;
wenzelm@20319
   272
wenzelm@20319
   273
fun genreflect ctxt corr_thm raw_eqs t =
wenzelm@20319
   274
    let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
wenzelm@20319
   275
        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
   276
        val rth = normalization_conv ft
wenzelm@20319
   277
    in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
wenzelm@20319
   278
                (simplify (HOL_basic_ss addsimps [rth]) th)
wenzelm@20319
   279
    end
wenzelm@20319
   280
wenzelm@20319
   281
fun genreify_tac ctxt eqs to i = (fn st =>
wenzelm@20319
   282
  let
wenzelm@20319
   283
    val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
wenzelm@20319
   284
    val t = (case to of NONE => P | SOME x => x)
wenzelm@20319
   285
    val th = (genreif ctxt eqs t) RS ssubst
wenzelm@20319
   286
  in rtac th i st
wenzelm@20319
   287
  end);
wenzelm@20319
   288
wenzelm@20319
   289
    (* Reflection calls reification and uses the correctness *)
wenzelm@20319
   290
        (* theorem assumed to be the dead of the list *)
wenzelm@20319
   291
 fun reflection_tac ctxt (corr_thm::raw_eqs) to i =
wenzelm@20319
   292
    (fn st =>
wenzelm@20319
   293
        let val P = (HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)))
wenzelm@20319
   294
            val t = (case to of NONE => P | SOME x => x)
wenzelm@20319
   295
            val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
wenzelm@20319
   296
        in rtac th i st end);
wenzelm@20319
   297
wenzelm@20319
   298
end