wenzelm@20319: (*
wenzelm@20319:     ID:         $Id$
wenzelm@20319:     Author:     Amine Chaieb, TU Muenchen
wenzelm@20319: 
wenzelm@20319: A trial for automatical reification.
wenzelm@20319: *)
wenzelm@20319: 
wenzelm@20319: signature REFLECTION = sig
wenzelm@20319:   val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
wenzelm@20319:   val reflection_tac: Proof.context -> thm list -> term option -> int -> tactic
wenzelm@20319: end;
wenzelm@20319: 
wenzelm@20319: structure Reflection : REFLECTION
wenzelm@20319: = struct
wenzelm@20319: 
chaieb@20374: val ext2 = thm "ext2";
chaieb@20374:   (* Make a congruence rule out of a defining equation for the interpretation *)
chaieb@20374:   (* th is one defining equation of f, i.e.
chaieb@20374:      th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
chaieb@20374:   (* Cp is a constructor pattern and P is a pattern *)
chaieb@20374: 
chaieb@20374:   (* The result is:
chaieb@20374:       [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
chaieb@20374:   (*  + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
chaieb@20374: 
chaieb@20374: 
chaieb@20374: fun mk_congeq ctxt fs th = 
chaieb@20374:   let 
chaieb@20374:    val Const(fname,fT)$(vs as Free(_,_))$_ =
chaieb@20374:        (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
chaieb@20374:    val thy = ProofContext.theory_of ctxt
chaieb@20374:    val cert = Thm.cterm_of thy
chaieb@20374:    fun dest_listT (Type ("List.list",[vT])) = vT
chaieb@20374:    val vT = dest_listT (Term.domain_type fT)
chaieb@20374:    val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
chaieb@20374:    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
wenzelm@20319: 
chaieb@20374:    fun add_fterms (t as t1 $ t2 $ t3) =
chaieb@20374:        if exists (fn f => t1 aconv f) fs then insert (op aconv) t
chaieb@20374:        else add_fterms (t1 $ t2) #> add_fterms t3
chaieb@20374:      | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
chaieb@20374:      | add_fterms (t as Abs(xn,xT,t')) = 
chaieb@20374:        if (vs mem (term_frees t)) then (fn _ => [t]) else (fn _ => [])
chaieb@20374:      | add_fterms _ = I
chaieb@20374:    val fterms = add_fterms rhs []
chaieb@20374:    val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt'
chaieb@20374:    val tys = map fastype_of fterms
chaieb@20374:    val vs = map Free (xs ~~ tys)
chaieb@20374:    val env = fterms ~~ vs
chaieb@20374:   
chaieb@20374:    fun replace_fterms (t as t1 $ t2 $ t3) =
chaieb@20374:        (case AList.lookup (op aconv) env t of
chaieb@20374: 	    SOME v => v
chaieb@20374: 	  | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
chaieb@20374:      | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
chaieb@20374:      | replace_fterms t = (case AList.lookup (op aconv) env t of
chaieb@20374: 			       SOME v => v
chaieb@20374: 			     | NONE => t)
chaieb@20374:       
chaieb@20374:    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:      | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
chaieb@20374:    fun tryext x = (x RS ext2 handle _ =>  x)
chaieb@20374:    val cong = (Goal.prove ctxt'' [] (map mk_def env)
chaieb@20374: 			  (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
chaieb@20374: 			  (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) 
chaieb@20374: 							THEN rtac th' 1)) RS sym
chaieb@20374: 	      
chaieb@20374:    val (cong' :: vars') = 
chaieb@20374:        Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
chaieb@20374:    val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'
chaieb@20374: 					      
chaieb@20374:   in  (vs', cong') end; 
chaieb@20374:   
wenzelm@20319: 
chaieb@20374: (*
wenzelm@20319: fun mk_congeq ctxt fs th =
wenzelm@20319:   let
wenzelm@20319:     val Const(fname,fT)$(Free(_,_))$_ =
wenzelm@20319:         (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
wenzelm@20319:     val thy = ProofContext.theory_of ctxt;
wenzelm@20319:     val cert = Thm.cterm_of thy;
wenzelm@20319:     fun dest_listT (Type ("List.list",[vT])) = vT;
wenzelm@20319:     val vT = dest_listT (Term.domain_type fT);
wenzelm@20319:     val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt;
wenzelm@20319:     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
wenzelm@20319: 
wenzelm@20319:     fun add_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319:           if exists (fn f => t1 aconv f) fs then insert (op aconv) t
wenzelm@20319:           else add_fterms (t1 $ t2) #> add_fterms t3
wenzelm@20319:       | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
wenzelm@20319:       | add_fterms (Abs _) = sys_error "FIXME"
wenzelm@20319:       | add_fterms _ = I;
wenzelm@20319:     val fterms = add_fterms rhs [];
wenzelm@20319: 
wenzelm@20319:     val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt';
wenzelm@20319:     val tys = map fastype_of fterms
wenzelm@20319:     val vs = map Free (xs ~~ tys);
wenzelm@20319:     val env = fterms ~~ vs;
wenzelm@20319: 
wenzelm@20319:     fun replace_fterms (t as t1 $ t2 $ t3) =
wenzelm@20319:           (case AList.lookup (op aconv) env t of
wenzelm@20319:             SOME v => v
wenzelm@20319:           | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
wenzelm@20319:       | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
wenzelm@20319:       | replace_fterms t = t;
wenzelm@20319: 
wenzelm@20319:     fun mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t));
wenzelm@20319:     val cong = (Goal.prove ctxt'' [] (map mk_def env)
wenzelm@20319:       (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
wenzelm@20319:       (fn x => LocalDefs.unfold_tac (#context x) (#prems x) THEN rtac th' 1)) RS sym;
wenzelm@20319: 
wenzelm@20319:     val (cong' :: vars') = Variable.export ctxt'' ctxt
wenzelm@20319:       (cong :: map (Drule.mk_term o cert) vs);
wenzelm@20319:     val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
wenzelm@20319:   in (vs', cong') end;
chaieb@20374: *)
wenzelm@20319:  (* congs is a list of pairs (P,th) where th is a theorem for *)
wenzelm@20319:         (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
wenzelm@20319: val FWD = curry (op OF);
wenzelm@20319: 
wenzelm@20319:  (* da is the decomposition for atoms, ie. it returns ([],g) where g
wenzelm@20319:  returns the right instance f (AtC n) = t , where AtC is the Atoms
wenzelm@20319:  constructor and n is the number of the atom corresponding to t *)
wenzelm@20319: 
wenzelm@20319: (* Generic decomp for reification : matches the actual term with the
wenzelm@20319: rhs of one cong rule. The result of the matching guides the
wenzelm@20319: proof synthesis: The matches of the introduced Variables A1 .. An are
wenzelm@20319: processed recursively
wenzelm@20319:  The rest is instantiated in the cong rule,i.e. no reification is needed *)
wenzelm@20319: 
chaieb@20374: exception REIF of string;
chaieb@20374: 
chaieb@20374: val env = ref ([]: (term list));
chaieb@20374: val bnds = ref ([]: (term list));
chaieb@20374: fun env_index t =
chaieb@20374:     let val i = find_index_eq t (!env)
chaieb@20374:         val j = find_index_eq t (!bnds)
chaieb@20374:     in if j = ~1 then if i = ~1 then (env:= (!env)@[t] ; (length ((!bnds)@(!env))) - 1) else i
chaieb@20374:                  else j end;
chaieb@20374: 
chaieb@20374: fun decomp_genreif da cgns (t,ctxt) =
chaieb@20374:   let 
chaieb@20374:    val thy = ProofContext.theory_of ctxt 
chaieb@20374:    val cert = cterm_of thy
chaieb@20374:    fun tryabsdecomp (s,ctxt) = 
chaieb@20374:     (case s of 
chaieb@20374:       Abs(xn,xT,ta) => 
chaieb@20374:        (let
chaieb@20374: 	 val ([xn],ctxt') = Variable.invent_fixes ["x"] ctxt
chaieb@20374: 	 val (xn,ta) = variant_abs (xn,xT,ta)
chaieb@20374:          val x = Free(xn,xT)
chaieb@20374:          val _ = (bnds := x::(!bnds))
chaieb@20374: 	in ([(ta, ctxt')] , fn [th] => 
chaieb@20374: 			       (bnds := tl (!bnds) ; 
chaieb@20374: 				hd (Variable.export ctxt' ctxt 
chaieb@20374: 						    [(forall_intr (cert x) th) COMP allI])))
chaieb@20374: 	end)
chaieb@20374:     | _ => da (s,ctxt))
chaieb@20374:   in 
chaieb@20374:   (case cgns of 
chaieb@20374:     [] => tryabsdecomp (t,ctxt)
chaieb@20374:   | ((vns,cong)::congs) => ((let
chaieb@20374:         val cert = cterm_of thy
chaieb@20374:         val (_, tmenv) =
chaieb@20374:         Pattern.match thy
chaieb@20374:         ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
chaieb@20374:         (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
chaieb@20374:         val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
chaieb@20374:         val (fts,its) = (map (snd o snd) fnvs,
chaieb@20374:                          map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
chaieb@20374:     in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate ([], its) cong))
chaieb@20374:     end)
chaieb@20374:       handle MATCH => decomp_genreif da congs (t,ctxt)))
chaieb@20374:   end;
chaieb@20374: 
chaieb@20374: (*
wenzelm@20319:  fun decomp_genreif thy da ((vns,cong)::congs) t =
wenzelm@20319:     ((let
wenzelm@20319:         val cert = cterm_of thy
wenzelm@20319:         val (_, tmenv) =
wenzelm@20319:         Pattern.match thy
wenzelm@20319:         ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
wenzelm@20319:         (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
wenzelm@20319:         val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
wenzelm@20319:         val (fts,its) = (map (snd o snd) fnvs,
wenzelm@20319:                          map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
wenzelm@20319:     in (fts, FWD (instantiate ([], its) cong))
wenzelm@20319:     end)
wenzelm@20319:       handle MATCH => decomp_genreif thy da congs t)
wenzelm@20319:    | decomp_genreif thy da [] t = da t;
wenzelm@20319: 
wenzelm@20319:      (* We add the atoms here during reification *)
wenzelm@20319: val env = ref ([]: (term list));
wenzelm@20319: 
wenzelm@20319: fun env_index t =
wenzelm@20319:     let val i = find_index_eq t (!env)
wenzelm@20319:     in if i = ~1 then (env:= (!env)@[t] ; (length (!env)) - 1) else i  end;
chaieb@20374: *)
wenzelm@20319: 
wenzelm@20319:           (* looks for the atoms equation and instantiates it with the right number *)
chaieb@20374: 
chaieb@20374: fun mk_decompatom eqs (t,ctxt) =
chaieb@20374:     let 
chaieb@20374:       val thy = ProofContext.theory_of ctxt
chaieb@20374:       fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
chaieb@20374:         | isateq _ = false
chaieb@20374:     in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
chaieb@20374:            NONE => raise REIF "Can not find the atoms equation"
chaieb@20374:          | SOME th =>
chaieb@20374: 	   ([],
chaieb@20374: 	    fn ths =>
chaieb@20374:                let val _ = print_thm th
chaieb@20374:                    val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
chaieb@20374:                    val (Const("List.nth",_)$vs$_) = 
chaieb@20374:                        (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
chaieb@20374:                    val vsT = fastype_of vs
chaieb@20374:                    val Type("List.list",[vT]) = vsT
chaieb@20374:                    val cvs = cterm_of thy (foldr (fn (x,xs) => Const("List.list.Cons", vT --> vsT --> vsT)$x$xs) (Free(x,vsT)) (!bnds))
chaieb@20374:                    val _ = print_thm (th RS sym)
chaieb@20374:                    val _ = print_cterm cvs
chaieb@20374:                    val th' = instantiate' [] 
chaieb@20374: 					  [SOME cvs, 
chaieb@20374:                                            SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
chaieb@20374:                                           (th RS sym)
chaieb@20374:                in hd (Variable.export ctxt' ctxt [th']) end)
chaieb@20374:     end;
chaieb@20374: 
chaieb@20374: (*
wenzelm@20319: fun mk_decompatom thy eqs =
wenzelm@20319:     let fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
wenzelm@20319:           | isateq _ = false
wenzelm@20319:     in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
wenzelm@20319:            NONE => raise REIF "Can not find the atoms equation"
wenzelm@20319:          | SOME th =>
wenzelm@20319:            fn t => ([],
wenzelm@20319:                     fn ths =>
wenzelm@20319:                        instantiate' [] [SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
wenzelm@20319:                                     (th RS sym))
wenzelm@20319:     end;
chaieb@20374: *)
wenzelm@20319:   (* Generic reification procedure: *)
wenzelm@20319:   (* creates all needed cong rules and then just uses the theorem synthesis *)
wenzelm@20319: fun genreif ctxt raw_eqs t =
wenzelm@20319:     let val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
wenzelm@20319:         val thy = ProofContext.theory_of ctxt'
wenzelm@20319:         val cert = cterm_of thy
wenzelm@20319:         val Const(fname,fT)$(Var(_,vT))$_ =
wenzelm@20319:             (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (hd raw_eqs)
wenzelm@20319:         val cv = cert (Free(x, vT))
wenzelm@20319:         val eqs = map (instantiate' [] [SOME cv]) raw_eqs
wenzelm@20319:         val fs =
wenzelm@20319:             foldr (fn (eq,fns) =>
wenzelm@20319:                       let val f$_$_ =  (fst o HOLogic.dest_eq o
wenzelm@20319:                                         HOLogic.dest_Trueprop o prop_of) eq
wenzelm@20319:                       in f ins fns end) [] eqs
wenzelm@20319:         val congs = map (mk_congeq ctxt' fs) eqs
chaieb@20374:         val congs = (map fst congs) ~~ (Variable.export ctxt' ctxt (map snd congs))
wenzelm@20319:         val _ = (env := [])
chaieb@20374:         val _ = (bnds := [])
chaieb@20374:         val da = mk_decompatom raw_eqs
chaieb@20374:         val th = divide_and_conquer (decomp_genreif da congs) (t,ctxt)
wenzelm@20319:         val cv' = cterm_of (ProofContext.theory_of ctxt)
wenzelm@20319:                            (HOLogic.mk_list I (body_type fT) (!env))
wenzelm@20319:         val _ = (env := [])
chaieb@20374:         val _ = (bnds:= [])
wenzelm@20319:         val th' = instantiate' [] [SOME cv'] th
wenzelm@20319:         val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
wenzelm@20319:         val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
wenzelm@20319:                    (fn _ => Simp_tac 1)
wenzelm@20319:     in FWD trans [th'',th']
wenzelm@20319:     end;
wenzelm@20319: 
wenzelm@20319: fun genreflect ctxt corr_thm raw_eqs t =
wenzelm@20319:     let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
wenzelm@20319:         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:         val rth = normalization_conv ft
wenzelm@20319:     in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
wenzelm@20319:                 (simplify (HOL_basic_ss addsimps [rth]) th)
wenzelm@20319:     end
wenzelm@20319: 
wenzelm@20319: fun genreify_tac ctxt eqs to i = (fn st =>
wenzelm@20319:   let
wenzelm@20319:     val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
wenzelm@20319:     val t = (case to of NONE => P | SOME x => x)
wenzelm@20319:     val th = (genreif ctxt eqs t) RS ssubst
wenzelm@20319:   in rtac th i st
wenzelm@20319:   end);
wenzelm@20319: 
wenzelm@20319:     (* Reflection calls reification and uses the correctness *)
wenzelm@20319:         (* theorem assumed to be the dead of the list *)
wenzelm@20319:  fun reflection_tac ctxt (corr_thm::raw_eqs) to i =
wenzelm@20319:     (fn st =>
wenzelm@20319:         let val P = (HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)))
wenzelm@20319:             val t = (case to of NONE => P | SOME x => x)
wenzelm@20319:             val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
wenzelm@20319:         in rtac th i st end);
wenzelm@20319: 
wenzelm@20319: end