src/HOL/Library/reflection.ML
changeset 32960 69916a850301
parent 32149 ef59550a55d3
child 32978 a473ba9a221d
     1.1 --- a/src/HOL/Library/reflection.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -48,22 +48,22 @@
     1.4     val tys = map fastype_of fterms
     1.5     val vs = map Free (xs ~~ tys)
     1.6     val env = fterms ~~ vs
     1.7 -		    (* FIXME!!!!*)
     1.8 +                    (* FIXME!!!!*)
     1.9     fun replace_fterms (t as t1 $ t2) =
    1.10         (case AList.lookup (op aconv) env t of
    1.11 -	    SOME v => v
    1.12 -	  | NONE => replace_fterms t1 $ replace_fterms t2)
    1.13 +            SOME v => v
    1.14 +          | NONE => replace_fterms t1 $ replace_fterms t2)
    1.15       | replace_fterms t = (case AList.lookup (op aconv) env t of
    1.16 -			       SOME v => v
    1.17 -			     | NONE => t)
    1.18 +                               SOME v => v
    1.19 +                             | NONE => t)
    1.20  
    1.21     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)))
    1.22       | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
    1.23     fun tryext x = (x RS ext2 handle THM _ =>  x)
    1.24     val cong = (Goal.prove ctxt'' [] (map mk_def env)
    1.25 -			  (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    1.26 -			  (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
    1.27 -							THEN rtac th' 1)) RS sym
    1.28 +                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    1.29 +                          (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
    1.30 +                                                        THEN rtac th' 1)) RS sym
    1.31  
    1.32     val (cong' :: vars') =
    1.33         Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
    1.34 @@ -134,15 +134,15 @@
    1.35                   val (xn,ta) = variant_abs (xn,xT,ta)
    1.36                   val x = Free(xn,xT)
    1.37                   val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT)
    1.38 -		          of NONE => error "tryabsdecomp: Type not found in the Environement"
    1.39 +                          of NONE => error "tryabsdecomp: Type not found in the Environement"
    1.40                             | SOME (bsT,atsT) =>
    1.41                               (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
    1.42                 in (([(ta, ctxt')],
    1.43                      fn ([th], bds) =>
    1.44                        (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
    1.45                         let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
    1.46 -		       in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
    1.47 -		       end)),
    1.48 +                       in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
    1.49 +                       end)),
    1.50                     bds)
    1.51                 end)
    1.52             | _ => da (s,ctxt) bds)
    1.53 @@ -157,9 +157,9 @@
    1.54                  (Vartab.empty, Vartab.empty)
    1.55              val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
    1.56              val (fts,its) =
    1.57 -	      (map (snd o snd) fnvs,
    1.58 +              (map (snd o snd) fnvs,
    1.59                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    1.60 -	    val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    1.61 +            val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    1.62            in ((fts ~~ (replicate (length fts) ctxt),
    1.63                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    1.64            end)
    1.65 @@ -174,9 +174,9 @@
    1.66            let
    1.67              val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
    1.68            in exists_Const
    1.69 -	    (fn (n,ty) => n = @{const_name "List.nth"}
    1.70 +            (fn (n,ty) => n = @{const_name "List.nth"}
    1.71                            andalso
    1.72 -			  AList.defined Type.could_unify bds (domain_type ty)) rhs
    1.73 +                          AList.defined Type.could_unify bds (domain_type ty)) rhs
    1.74              andalso Type.could_unify (fastype_of rhs, tT)
    1.75            end
    1.76  
    1.77 @@ -266,7 +266,7 @@
    1.78  
    1.79          val bds = AList.make (fn _ => ([],[])) tys
    1.80          val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop
    1.81 -  	                           |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
    1.82 +                                   |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl
    1.83                                     |> (insteq eq)) raw_eqs
    1.84          val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
    1.85        in (ps ~~ (Variable.export ctxt' ctxt congs), bds)
    1.86 @@ -278,14 +278,14 @@
    1.87      fun is_listVar (Var (_,t)) = can dest_listT t
    1.88           | is_listVar _ = false
    1.89      val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
    1.90 -	          |> strip_comb |> snd |> filter is_listVar
    1.91 +                  |> strip_comb |> snd |> filter is_listVar
    1.92      val cert = cterm_of (ProofContext.theory_of ctxt)
    1.93      val cvs = map (fn (v as Var(n,t)) => (cert v,
    1.94                    the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
    1.95      val th' = instantiate ([], cvs) th
    1.96      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
    1.97      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
    1.98 -	       (fn _ => simp_tac (simpset_of ctxt) 1)
    1.99 +               (fn _ => simp_tac (simpset_of ctxt) 1)
   1.100    in FWD trans [th'',th']
   1.101    end
   1.102