Generic reflection and reification (by Amine Chaieb).
authorwenzelm
Thu Aug 03 15:03:05 2006 +0200 (2006-08-03)
changeset 20319a8761e8568de
parent 20318 0e0ea63fe768
child 20320 a5368278a72c
Generic reflection and reification (by Amine Chaieb).
src/HOL/ex/Reflection.thy
src/HOL/ex/ReflectionEx.thy
src/HOL/ex/reflection.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Reflection.thy	Thu Aug 03 15:03:05 2006 +0200
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Generic reflection and reification *}
    1.10 +
    1.11 +theory Reflection
    1.12 +imports Main
    1.13 +uses "reflection.ML"
    1.14 +begin
    1.15 +
    1.16 +method_setup reify = {*
    1.17 +  fn src =>
    1.18 +    Method.syntax (Attrib.thms --
    1.19 +      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.20 +  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to))
    1.21 +*} "partial automatic reification"
    1.22 +
    1.23 +method_setup reflection = {*
    1.24 +  fn src =>
    1.25 +    Method.syntax (Attrib.thms --
    1.26 +      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.27 +  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to))
    1.28 +*} "reflection method"
    1.29 +
    1.30 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/ReflectionEx.thy	Thu Aug 03 15:03:05 2006 +0200
     2.3 @@ -0,0 +1,252 @@
     2.4 +(*
     2.5 +    ID:         $Id$
     2.6 +    Author:     Amine Chaieb, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Examples for generic reflection and reification *}
    2.10 +
    2.11 +theory ReflectionEx
    2.12 +imports Reflection
    2.13 +begin
    2.14 +
    2.15 +
    2.16 +  (* The type fm represents simple propositional formulae *)
    2.17 +datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
    2.18 +
    2.19 +consts Ifm :: "bool list \<Rightarrow> fm \<Rightarrow> bool"
    2.20 +primrec
    2.21 +  "Ifm vs (At n) = vs!n"
    2.22 +  "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
    2.23 +  "Ifm vs (Or p q) = (Ifm vs p \<or> Ifm vs q)"
    2.24 +  "Ifm vs (Imp p q) = (Ifm vs p \<longrightarrow> Ifm vs q)"
    2.25 +  "Ifm vs (Iff p q) = (Ifm vs p = Ifm vs q)"
    2.26 +  "Ifm vs (NOT p) = (\<not> (Ifm vs p))"
    2.27 +
    2.28 +consts fmsize :: "fm \<Rightarrow> nat"
    2.29 +primrec
    2.30 +  "fmsize (At n) = 1"
    2.31 +  "fmsize (NOT p) = 1 + fmsize p"
    2.32 +  "fmsize (And p q) = 1 + fmsize p + fmsize q"
    2.33 +  "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    2.34 +  "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
    2.35 +  "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
    2.36 +
    2.37 +
    2.38 +
    2.39 +  (* reify maps a bool to an fm, for this it needs the 
    2.40 +  semantics of fm (Ifm.simps)*)
    2.41 +lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
    2.42 +apply (reify Ifm.simps)
    2.43 +oops
    2.44 +
    2.45 +  (* You can also just pick up a subterm to reify \<dots> *)
    2.46 +lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
    2.47 +apply (reify Ifm.simps ("((~ D) & (~ F))"))
    2.48 +oops
    2.49 +
    2.50 +  (* Let's perform NNF, A version that tends to disjunctions *)
    2.51 +consts nnf :: "fm \<Rightarrow> fm"
    2.52 +recdef nnf "measure fmsize"
    2.53 +  "nnf (At n) = At n"
    2.54 +  "nnf (And p q) = And (nnf p) (nnf q)"
    2.55 +  "nnf (Or p q) = Or (nnf p) (nnf q)"
    2.56 +  "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
    2.57 +  "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
    2.58 +  "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
    2.59 +  "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
    2.60 +  "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
    2.61 +  "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
    2.62 +  "nnf (NOT (NOT p)) = nnf p"
    2.63 +  "nnf (NOT p) = NOT p"
    2.64 +
    2.65 +  (* nnf preserves the semantics of fm *)
    2.66 +lemma nnf: "Ifm vs (nnf p) = Ifm vs p"
    2.67 +  by (induct p rule: nnf.induct) auto
    2.68 +
    2.69 +  (* Now let's perform NNF using our function defined above. 
    2.70 +  reflection takes the correctness theorem (nnf) the semantics of fm
    2.71 +  and applies the function to the corresponding of the formula *)
    2.72 +lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
    2.73 +apply (reflection nnf Ifm.simps)
    2.74 +oops
    2.75 +
    2.76 +  (* Here also you can just pick up a subterm \<dots> *)
    2.77 +lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
    2.78 +apply (reflection nnf Ifm.simps ("(B | C \<and> (B \<longrightarrow> A | D))"))
    2.79 +oops
    2.80 +
    2.81 +
    2.82 +  (* Example 2 : simple arithmetics formulae *)
    2.83 +
    2.84 +  (* num reflects linear expressions over natural number  *)
    2.85 +datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
    2.86 +
    2.87 +consts num_size :: "num \<Rightarrow> nat" 
    2.88 +primrec 
    2.89 +  "num_size (C c) = 1"
    2.90 +  "num_size (Var n) = 1"
    2.91 +  "num_size (Add a b) = 1 + num_size a + num_size b"
    2.92 +  "num_size (Mul c a) = 1 + num_size a"
    2.93 +  "num_size (CN n c a) = 4 + num_size a "
    2.94 +
    2.95 +  (* The semantics of num *)
    2.96 +consts Inum:: "nat list \<Rightarrow> num \<Rightarrow> nat"
    2.97 +primrec 
    2.98 +  Inum_C  : "Inum vs (C i) = i"
    2.99 +  Inum_Var: "Inum vs (Var n) = vs!n"
   2.100 +  Inum_Add: "Inum vs (Add s t) = Inum vs s + Inum vs t"
   2.101 +  Inum_Mul: "Inum vs (Mul c t) = c * Inum vs t"
   2.102 +  Inum_CN : "Inum vs (CN n c t) = c*(vs!n) + Inum vs t"
   2.103 +
   2.104 +  (* Let's reify some nat expressions \<dots> *)
   2.105 +lemma "4 * (2*x + (y::nat)) \<noteq> 0"
   2.106 +  apply (reify Inum.simps ("4 * (2*x + (y::nat))"))
   2.107 +    (* We're in a bad situation!!*)
   2.108 +oops
   2.109 +  (* So let's leave the Inum_C equation at the end and see what happens \<dots>*)
   2.110 +lemma "4 * (2*x + (y::nat)) \<noteq> 0"
   2.111 +  apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
   2.112 +    (* We're still in a bad situation!!*)
   2.113 +    (* BUT!! It's better\<dots> Note that the reification depends on the order of the equations\<dots> *)
   2.114 +    (* The problem is that Inum_C has the form : Inum vs (C i) = i *)
   2.115 +    (* So the right handside matches any term of type nat, which makes things bad. *)
   2.116 +    (* We want only numerals \<dots> So let's specialize Inum_C with numerals.*)
   2.117 +oops
   2.118 +
   2.119 +lemma Inum_number: "Inum vs (C (number_of t)) = number_of t" by simp
   2.120 +lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
   2.121 +
   2.122 +  (* Second trial *)
   2.123 +lemma "1 * (2*x + (y::nat)) \<noteq> 0"
   2.124 +  apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
   2.125 +oops
   2.126 +  (* That was fine, so let's try an other one\<dots> *)
   2.127 +
   2.128 +lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
   2.129 +  apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
   2.130 +    (* Oh!! 0 is not a variable \<dots> Oh! 0 is not a number_of .. thing *)
   2.131 +    (* Tha same for 1, so let's add those equations too *)
   2.132 +oops
   2.133 +
   2.134 +lemma Inum_01: "Inum vs (C 0) = 0" "Inum vs (C 1) = 1" "Inum vs (C(Suc n)) = Suc n"
   2.135 +  by simp+
   2.136 +lemmas Inum_eqs'= Inum_eqs Inum_01
   2.137 +  (* Third Trial *)
   2.138 +
   2.139 +lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
   2.140 +  apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
   2.141 +    (* Okay *)
   2.142 +oops
   2.143 +
   2.144 +  (* Some simplifications for num terms, you can skimm untill the main theorem linum *)
   2.145 +consts lin_add :: "num \<times> num \<Rightarrow> num"
   2.146 +recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
   2.147 +  "lin_add (CN n1 c1 r1,CN n2 c2 r2) =
   2.148 +  (if n1=n2 then 
   2.149 +  (let c = c1 + c2
   2.150 +  in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2))))
   2.151 +  else if n1 \<le> n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2))) 
   2.152 +  else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))"
   2.153 +  "lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))"  
   2.154 +  "lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))" 
   2.155 +  "lin_add (C b1, C b2) = C (b1+b2)"
   2.156 +  "lin_add (a,b) = Add a b"
   2.157 +lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)"
   2.158 +apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
   2.159 +apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   2.160 +by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
   2.161 +
   2.162 +consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   2.163 +recdef lin_mul "measure size "
   2.164 +  "lin_mul (C j) = (\<lambda> i. C (i*j))"
   2.165 +  "lin_mul (CN n c a) = (\<lambda> i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
   2.166 +  "lin_mul t = (\<lambda> i. Mul i t)"
   2.167 +
   2.168 +lemma lin_mul: "\<And> i. Inum bs (lin_mul t i) = Inum bs (Mul i t)"
   2.169 +by (induct t rule: lin_mul.induct, auto simp add: ring_eq_simps)
   2.170 +
   2.171 +consts linum:: "num \<Rightarrow> num"
   2.172 +recdef linum "measure num_size"
   2.173 +  "linum (C b) = C b"
   2.174 +  "linum (Var n) = CN n 1 (C 0)"
   2.175 +  "linum (Add t s) = lin_add (linum t, linum s)"
   2.176 +  "linum (Mul c t) = lin_mul (linum t) c"
   2.177 +  "linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)"
   2.178 +
   2.179 +lemma linum : "Inum vs (linum t) = Inum vs t"
   2.180 +by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
   2.181 +
   2.182 +  (* Now we can use linum to simplify nat terms using reflection *)
   2.183 +lemma "(Suc (Suc 1)) * ((x::nat) + (Suc 1)*y) = 3*x + 6*y"
   2.184 +apply (reflection linum Inum_eqs' ("(Suc (Suc 1)) * ((x::nat) + (Suc 1)*y)"))
   2.185 +oops
   2.186 +
   2.187 +  (* Let's list this to formulae \<dots> *)
   2.188 +
   2.189 +datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   2.190 +  Conj aform aform | Disj aform aform | NEG aform | T | F
   2.191 +consts linaformsize:: "aform \<Rightarrow> nat"
   2.192 +recdef linaformsize "measure size"
   2.193 +  "linaformsize T = 1"
   2.194 +  "linaformsize F = 1"
   2.195 +  "linaformsize (Lt a b) = 1"
   2.196 +  "linaformsize (Ge a b) = 1"
   2.197 +  "linaformsize (Eq a b) = 1"
   2.198 +  "linaformsize (NEq a b) = 1"
   2.199 +  "linaformsize (NEG p) = 2 + linaformsize p"
   2.200 +  "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   2.201 +  "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   2.202 +
   2.203 +
   2.204 +consts aform :: "nat list => aform => bool"
   2.205 +primrec
   2.206 +  "aform vs T = True"
   2.207 +  "aform vs F = False"
   2.208 +  "aform vs (Lt a b) = (Inum vs a < Inum vs b)"
   2.209 +  "aform vs (Eq a b) = (Inum vs a = Inum vs b)"
   2.210 +  "aform vs (Ge a b) = (Inum vs a \<ge> Inum vs b)"
   2.211 +  "aform vs (NEq a b) = (Inum vs a \<noteq> Inum vs b)"
   2.212 +  "aform vs (NEG p) = (\<not> (aform vs p))"
   2.213 +  "aform vs (Conj p q) = (aform vs p \<and> aform vs q)"
   2.214 +  "aform vs (Disj p q) = (aform vs p \<or> aform vs q)"
   2.215 +
   2.216 +  (* Let's reify and do reflection .. *)
   2.217 +lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
   2.218 +apply (reify Inum_eqs' aform.simps)
   2.219 +oops
   2.220 +
   2.221 +lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
   2.222 +apply (reflection linum Inum_eqs' aform.simps ("x + x + 1"))
   2.223 +oops
   2.224 +
   2.225 +  (* We now define a simple transformation on aform: NNF + linum on atoms *)
   2.226 +consts linaform:: "aform \<Rightarrow> aform"
   2.227 +recdef linaform "measure linaformsize"
   2.228 +  "linaform (Lt s t) = Lt (linum s) (linum t)"
   2.229 +  "linaform (Eq s t) = Eq (linum s) (linum t)"
   2.230 +  "linaform (Ge s t) = Ge (linum s) (linum t)"
   2.231 +  "linaform (NEq s t) = NEq (linum s) (linum t)"
   2.232 +  "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   2.233 +  "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   2.234 +  "linaform (NEG T) = F"
   2.235 +  "linaform (NEG F) = T"
   2.236 +  "linaform (NEG (Lt a b)) = Ge a b"
   2.237 +  "linaform (NEG (Ge a b)) = Lt a b"
   2.238 +  "linaform (NEG (Eq a b)) = NEq a b"
   2.239 +  "linaform (NEG (NEq a b)) = Eq a b"
   2.240 +  "linaform (NEG (NEG p)) = linaform p"
   2.241 +  "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   2.242 +  "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   2.243 +  "linaform p = p"
   2.244 +
   2.245 +lemma linaform: "aform vs (linaform p) = aform vs p"
   2.246 +  by (induct p rule: linaform.induct, auto simp add: linum)
   2.247 +
   2.248 +lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0  + Suc 0< 0)"
   2.249 +  apply (reflection linaform Inum_eqs' aform.simps) (*  ("Suc 0 + Suc 0< 0")) *)
   2.250 +oops
   2.251 +
   2.252 +    (* etc etc \<dots>*)
   2.253 +
   2.254 +
   2.255 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/reflection.ML	Thu Aug 03 15:03:05 2006 +0200
     3.3 @@ -0,0 +1,172 @@
     3.4 +(*
     3.5 +    ID:         $Id$
     3.6 +    Author:     Amine Chaieb, TU Muenchen
     3.7 +
     3.8 +A trial for automatical reification.
     3.9 +*)
    3.10 +
    3.11 +signature REFLECTION = sig
    3.12 +  val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
    3.13 +  val reflection_tac: Proof.context -> thm list -> term option -> int -> tactic
    3.14 +end;
    3.15 +
    3.16 +structure Reflection : REFLECTION
    3.17 += struct
    3.18 +
    3.19 +    (* Make a congruence rule out of a defining equation for the interpretation *)
    3.20 +        (* th is one defining equation of f, i.e.
    3.21 +           th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
    3.22 +        (* Cp is a constructor pattern and P is a pattern *)
    3.23 +
    3.24 +        (* The result is:
    3.25 +         [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *)
    3.26 +        (*  + the a list of names of the A1 .. An, Those are fresh in the ctxt*)
    3.27 +
    3.28 +fun mk_congeq ctxt fs th =
    3.29 +  let
    3.30 +    val Const(fname,fT)$(Free(_,_))$_ =
    3.31 +        (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
    3.32 +    val thy = ProofContext.theory_of ctxt;
    3.33 +    val cert = Thm.cterm_of thy;
    3.34 +    fun dest_listT (Type ("List.list",[vT])) = vT;
    3.35 +    val vT = dest_listT (Term.domain_type fT);
    3.36 +    val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt;
    3.37 +    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
    3.38 +
    3.39 +    fun add_fterms (t as t1 $ t2 $ t3) =
    3.40 +          if exists (fn f => t1 aconv f) fs then insert (op aconv) t
    3.41 +          else add_fterms (t1 $ t2) #> add_fterms t3
    3.42 +      | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2
    3.43 +      | add_fterms (Abs _) = sys_error "FIXME"
    3.44 +      | add_fterms _ = I;
    3.45 +    val fterms = add_fterms rhs [];
    3.46 +
    3.47 +    val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt';
    3.48 +    val tys = map fastype_of fterms
    3.49 +    val vs = map Free (xs ~~ tys);
    3.50 +    val env = fterms ~~ vs;
    3.51 +
    3.52 +    fun replace_fterms (t as t1 $ t2 $ t3) =
    3.53 +          (case AList.lookup (op aconv) env t of
    3.54 +            SOME v => v
    3.55 +          | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3)
    3.56 +      | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2
    3.57 +      | replace_fterms t = t;
    3.58 +
    3.59 +    fun mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t));
    3.60 +    val cong = (Goal.prove ctxt'' [] (map mk_def env)
    3.61 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    3.62 +      (fn x => LocalDefs.unfold_tac (#context x) (#prems x) THEN rtac th' 1)) RS sym;
    3.63 +
    3.64 +    val (cong' :: vars') = Variable.export ctxt'' ctxt
    3.65 +      (cong :: map (Drule.mk_term o cert) vs);
    3.66 +    val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
    3.67 +  in (vs', cong') end;
    3.68 +
    3.69 + (* congs is a list of pairs (P,th) where th is a theorem for *)
    3.70 +        (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *)
    3.71 +val FWD = curry (op OF);
    3.72 +
    3.73 + (* da is the decomposition for atoms, ie. it returns ([],g) where g
    3.74 + returns the right instance f (AtC n) = t , where AtC is the Atoms
    3.75 + constructor and n is the number of the atom corresponding to t *)
    3.76 +
    3.77 +(* Generic decomp for reification : matches the actual term with the
    3.78 +rhs of one cong rule. The result of the matching guides the
    3.79 +proof synthesis: The matches of the introduced Variables A1 .. An are
    3.80 +processed recursively
    3.81 + The rest is instantiated in the cong rule,i.e. no reification is needed *)
    3.82 +
    3.83 + fun decomp_genreif thy da ((vns,cong)::congs) t =
    3.84 +    ((let
    3.85 +        val cert = cterm_of thy
    3.86 +        val (_, tmenv) =
    3.87 +        Pattern.match thy
    3.88 +        ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    3.89 +        (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
    3.90 +        val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
    3.91 +        val (fts,its) = (map (snd o snd) fnvs,
    3.92 +                         map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    3.93 +    in (fts, FWD (instantiate ([], its) cong))
    3.94 +    end)
    3.95 +      handle MATCH => decomp_genreif thy da congs t)
    3.96 +   | decomp_genreif thy da [] t = da t;
    3.97 +
    3.98 +     (* We add the atoms here during reification *)
    3.99 +val env = ref ([]: (term list));
   3.100 +
   3.101 +fun env_index t =
   3.102 +    let val i = find_index_eq t (!env)
   3.103 +    in if i = ~1 then (env:= (!env)@[t] ; (length (!env)) - 1) else i  end;
   3.104 +
   3.105 +exception REIF of string;
   3.106 +
   3.107 +          (* looks for the atoms equation and instantiates it with the right number *)
   3.108 +fun mk_decompatom thy eqs =
   3.109 +    let fun isateq (_$_$(Const("List.nth",_)$_$_)) = true
   3.110 +          | isateq _ = false
   3.111 +    in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of
   3.112 +           NONE => raise REIF "Can not find the atoms equation"
   3.113 +         | SOME th =>
   3.114 +           fn t => ([],
   3.115 +                    fn ths =>
   3.116 +                       instantiate' [] [SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))]
   3.117 +                                    (th RS sym))
   3.118 +    end;
   3.119 +
   3.120 +  (* Generic reification procedure: *)
   3.121 +  (* creates all needed cong rules and then just uses the theorem synthesis *)
   3.122 +fun genreif ctxt raw_eqs t =
   3.123 +    let val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
   3.124 +        val thy = ProofContext.theory_of ctxt'
   3.125 +        val cert = cterm_of thy
   3.126 +        val Const(fname,fT)$(Var(_,vT))$_ =
   3.127 +            (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (hd raw_eqs)
   3.128 +        val cv = cert (Free(x, vT))
   3.129 +        val eqs = map (instantiate' [] [SOME cv]) raw_eqs
   3.130 +        val fs =
   3.131 +            foldr (fn (eq,fns) =>
   3.132 +                      let val f$_$_ =  (fst o HOLogic.dest_eq o
   3.133 +                                        HOLogic.dest_Trueprop o prop_of) eq
   3.134 +                      in f ins fns end) [] eqs
   3.135 +        val congs = map (mk_congeq ctxt' fs) eqs
   3.136 +        val _ = (env := [])
   3.137 +        val da = mk_decompatom thy eqs
   3.138 +        val [th] = Variable.export ctxt' ctxt
   3.139 +                 [divide_and_conquer (decomp_genreif thy da congs) t]
   3.140 +        val cv' = cterm_of (ProofContext.theory_of ctxt)
   3.141 +                           (HOLogic.mk_list I (body_type fT) (!env))
   3.142 +        val _ = (env := [])
   3.143 +        val th' = instantiate' [] [SOME cv'] th
   3.144 +        val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
   3.145 +        val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
   3.146 +                   (fn _ => Simp_tac 1)
   3.147 +    in FWD trans [th'',th']
   3.148 +    end;
   3.149 +
   3.150 +fun genreflect ctxt corr_thm raw_eqs t =
   3.151 +    let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
   3.152 +        val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th
   3.153 +        val rth = normalization_conv ft
   3.154 +    in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
   3.155 +                (simplify (HOL_basic_ss addsimps [rth]) th)
   3.156 +    end
   3.157 +
   3.158 +fun genreify_tac ctxt eqs to i = (fn st =>
   3.159 +  let
   3.160 +    val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
   3.161 +    val t = (case to of NONE => P | SOME x => x)
   3.162 +    val th = (genreif ctxt eqs t) RS ssubst
   3.163 +  in rtac th i st
   3.164 +  end);
   3.165 +
   3.166 +    (* Reflection calls reification and uses the correctness *)
   3.167 +        (* theorem assumed to be the dead of the list *)
   3.168 + fun reflection_tac ctxt (corr_thm::raw_eqs) to i =
   3.169 +    (fn st =>
   3.170 +        let val P = (HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)))
   3.171 +            val t = (case to of NONE => P | SOME x => x)
   3.172 +            val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
   3.173 +        in rtac th i st end);
   3.174 +
   3.175 +end