1.1 --- a/src/HOL/ex/Reflection.thy	Fri Jan 26 13:59:06 2007 +0100
     1.2 +++ b/src/HOL/ex/Reflection.thy	Sun Jan 28 11:52:52 2007 +0100
     1.3 @@ -7,11 +7,12 @@
     1.4  
     1.5  theory Reflection
     1.6  imports Main
     1.7 -uses ("reflection.ML")
     1.8 +  uses ("reflection.ML")
     1.9  begin
    1.10  
    1.11  lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    1.12    by (blast intro: ext)
    1.13 +
    1.14  use "reflection.ML"
    1.15  
    1.16  method_setup reify = {*

     2.1 --- a/src/HOL/ex/ReflectionEx.thy	Fri Jan 26 13:59:06 2007 +0100
     2.2 +++ b/src/HOL/ex/ReflectionEx.thy	Sun Jan 28 11:52:52 2007 +0100
     2.3 @@ -355,4 +355,38 @@
     2.4    apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
     2.5  oops
     2.6  
     2.7 +
     2.8 +  (* An example for equations containing type variables *)	
     2.9 +datatype prod = Zero | One | Var nat | Mul prod prod 
    2.10 +  | Pw prod nat | PNM nat nat prod
    2.11 +consts Iprod :: "('a::{ordered_idom,recpower}) list \<Rightarrow> prod \<Rightarrow> 'a" 
    2.12 +primrec
    2.13 +  "Iprod vs Zero = 0"
    2.14 +  "Iprod vs One = 1"
    2.15 +  "Iprod vs (Var n) = vs!n"
    2.16 +  "Iprod vs (Mul a b) = (Iprod vs a * Iprod vs b)"
    2.17 +  "Iprod vs (Pw a n) = ((Iprod vs a) ^ n)"
    2.18 +  "Iprod vs (PNM n k t) = (vs ! n)^k * Iprod vs t"
    2.19 +consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
    2.20 +datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
    2.21 +  | Or sgn sgn | And sgn sgn
    2.22 +
    2.23 +consts Isgn :: "('a::{ordered_idom, recpower}) list \<Rightarrow> sgn \<Rightarrow> bool"
    2.24 +primrec 
    2.25 +  "Isgn vs Tr = True"
    2.26 +  "Isgn vs F = False"
    2.27 +  "Isgn vs (ZeroEq t) = (Iprod vs t = 0)"
    2.28 +  "Isgn vs (NZeroEq t) = (Iprod vs t \<noteq> 0)"
    2.29 +  "Isgn vs (Pos t) = (Iprod vs t > 0)"
    2.30 +  "Isgn vs (Neg t) = (Iprod vs t < 0)"
    2.31 +  "Isgn vs (And p q) = (Isgn vs p \<and> Isgn vs q)"
    2.32 +  "Isgn vs (Or p q) = (Isgn vs p \<or> Isgn vs q)"
    2.33 +
    2.34 +lemmas eqs = Isgn.simps Iprod.simps
    2.35 +
    2.36 +lemma "(x::int)^4 * y * z * y^2 * z^23 > 0"
    2.37 +  apply (reify eqs)
    2.38 +  oops
    2.39 +
    2.40 +
    2.41  end

     3.1 --- a/src/HOL/ex/reflection.ML	Fri Jan 26 13:59:06 2007 +0100
     3.2 +++ b/src/HOL/ex/reflection.ML	Sun Jan 28 11:52:52 2007 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4     val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
     3.5     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
     3.6     fun add_fterms (t as t1 $ t2) = 
     3.7 -       if exists (fn f => (t |> strip_comb |> fst) aconv f) fs then insert (op aconv) t
     3.8 +       if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
     3.9         else add_fterms t1 #> add_fterms t2
    3.10       | add_fterms (t as Abs(xn,xT,t')) = 
    3.11         if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
    3.12 @@ -92,7 +92,7 @@
    3.13   let 
    3.14    val tt = HOLogic.listT (fastype_of t)
    3.15   in 
    3.16 -  (case AList.lookup (op =) (!bds) tt of
    3.17 +  (case AList.lookup Type.could_unify (!bds) tt of
    3.18      NONE => error "index_of : type not found in environements!"
    3.19    | SOME (tbs,tats) =>
    3.20      let
    3.21 @@ -160,8 +160,8 @@
    3.22     in exists_Const 
    3.23  	  (fn (n,ty) => n="List.nth" 
    3.24  			andalso 
    3.25 -			AList.defined (op =) (!bds) (domain_type ty)) rhs 
    3.26 -	  andalso fastype_of rhs = tT
    3.27 +			AList.defined Type.could_unify (!bds) (domain_type ty)) rhs 
    3.28 +	  andalso Type.could_unify (fastype_of rhs, tT)
    3.29     end
    3.30    fun get_nth t = 
    3.31     case t of