# HG changeset patch # User chaieb # Date 1158566997 -7200 # Node ID 6857bd9f1a7961a0363f1afb0756b1fec51e40ec # Parent 44eda2314aab9d6cfc6e145c78ae28990a5d6cd8 Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n) instead of only ... = xs!n. diff -r 44eda2314aab -r 6857bd9f1a79 src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Mon Sep 18 07:48:07 2006 +0200 +++ b/src/HOL/ex/ReflectionEx.thy Mon Sep 18 10:09:57 2006 +0200 @@ -113,8 +113,8 @@ Inum_CN : "Inum vs (CN n c t) = c*(vs!n) + Inum vs t" text{* Let's reify some nat expressions \ *} -lemma "4 * (2*x + (y::nat)) \ 0" - apply (reify Inum.simps ("4 * (2*x + (y::nat))")) +lemma "4 * (2*x + (y::nat)) + f a \ 0" + apply (reify Inum.simps ("4 * (2*x + (y::nat)) + f a")) oops text{* We're in a bad situation!! The term above has been recongnized as a constant, which is correct but does not correspond to our intuition of the constructor C. It should encapsulate constants, i.e. numbers, i.e. numerals.*} @@ -173,7 +173,7 @@ "lin_mul t = (\ i. Mul i t)" lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)" -by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps) +by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_eq_simps) consts linum:: "num \ num" recdef linum "measure num_size" @@ -188,7 +188,7 @@ text{* Now we can use linum to simplify nat terms using reflection *} lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y" -apply (reflection linum Inum_eqs' ("(Suc (Suc 1)) * (x + (Suc 1)*y)")) +(* apply (reflection linum Inum_eqs' ("(Suc (Suc 1)) * (x + (Suc 1)*y)")) *) oops text{* Let's lift this to formulae and see what happens *} @@ -220,14 +220,14 @@ "aform vs (Conj p q) = (aform vs p \ aform vs q)" "aform vs (Disj p q) = (aform vs p \ aform vs q)" - text{* Let's reify and do reflection. *} + text{* Let's reify and do reflection *} lemma "(3::nat)*x + t < 0 \ (2 * x + y \ 17)" -apply (reify Inum_eqs' aform.simps) +(* apply (reify Inum_eqs' aform.simps) *) oops text{* Note that reification handles several interpretations at the same time*} lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0" -apply (reflection linum Inum_eqs' aform.simps ("x + x + 1")) +(* apply (reflection linum Inum_eqs' aform.simps ("x + x + 1")) *) oops text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *} @@ -254,28 +254,105 @@ by (induct p rule: linaform.induct, auto simp add: linum) lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \ (Suc 0 + Suc 0< 0)" - apply (reflection linaform Inum_eqs' aform.simps) +(* apply (reflection linaform Inum_eqs' aform.simps) *) +oops + +text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *} +datatype rb = BC bool| BAnd rb rb | BOr rb rb +consts Irb :: "rb \ bool" +primrec + "Irb (BAnd s t) = (Irb s \ Irb t)" + "Irb (BOr s t) = (Irb s \ Irb t)" + "Irb (BC p) = p" + +lemma "A \ (B \ D \ B) \ A \ (B \ D \ B) \ A \ (B \ D \ B) \ A \ (B \ D \ B)" +apply (reify Irb.simps) oops - -text{* And finally an example for binders. Here we have an existential quantifier. Binding is trough de Bruijn indices, the index of the varibles. *} +datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint +consts Irint :: "int list \ rint \ int" +primrec +Irint_Var: "Irint vs (IVar n) = vs!n" +Irint_Neg: "Irint vs (INeg t) = - Irint vs t" +Irint_Add: "Irint vs (IAdd s t) = Irint vs s + Irint vs t" +Irint_Sub: "Irint vs (ISub s t) = Irint vs s - Irint vs t" +Irint_Mult: "Irint vs (IMult s t) = Irint vs s * Irint vs t" +Irint_C: "Irint vs (IC i) = i" +lemma Irint_C0: "Irint vs (IC 0) = 0" + by simp +lemma Irint_C1: "Irint vs (IC 1) = 1" + by simp +lemma Irint_Cnumberof: "Irint vs (IC (number_of x)) = number_of x" + by simp +lemmas Irint_simps = Irint_Var Irint_Neg Irint_Add Irint_Sub Irint_Mult Irint_C0 Irint_C1 Irint_Cnumberof +lemma "(3::int) * x + y*y - 9 + (- z) = 0" + apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)")) + oops +datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist +consts Irlist :: "int list \ (int list) list \ rlist \ (int list)" +primrec + "Irlist is vs (LEmpty) = []" + "Irlist is vs (LVar n) = vs!n" + "Irlist is vs (LCons i t) = ((Irint is i)#(Irlist is vs t))" + "Irlist is vs (LAppend s t) = (Irlist is vs s) @ (Irlist is vs t)" +lemma "[(1::int)] = []" + apply (reify Irlist.simps Irint_simps ("[1]:: int list")) + oops -datatype afm = LT num num | EQ num | AND afm afm | OR afm afm | E afm | A afm +lemma "([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs = [y*y - z - 9 + (3::int) * x]" + apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs")) + oops -consts Iafm:: "nat list \ afm \ bool" - +datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist +consts Irnat :: "int list \ (int list) list \ nat list \ rnat \ nat" primrec - "Iafm vs (LT s t) = (Inum vs s < Inum vs t)" - "Iafm vs (EQ t) = (Inum vs t = 0)" - "Iafm vs (AND p q) = (Iafm vs p \ Iafm vs q)" - "Iafm vs (OR p q) = (Iafm vs p \ Iafm vs q)" - "Iafm vs (E p) = (\x. Iafm (x#vs) p)" - "Iafm vs (A p) = (\x. Iafm (x#vs) p)" +Irnat_Suc: "Irnat is ls vs (NSuc t) = Suc (Irnat is ls vs t)" +Irnat_Var: "Irnat is ls vs (NVar n) = vs!n" +Irnat_Neg: "Irnat is ls vs (NNeg t) = - Irnat is ls vs t" +Irnat_Add: "Irnat is ls vs (NAdd s t) = Irnat is ls vs s + Irnat is ls vs t" +Irnat_Sub: "Irnat is ls vs (NSub s t) = Irnat is ls vs s - Irnat is ls vs t" +Irnat_Mult: "Irnat is ls vs (NMult s t) = Irnat is ls vs s * Irnat is ls vs t" +Irnat_lgth: "Irnat is ls vs (Nlgth rxs) = length (Irlist is ls rxs)" +Irnat_C: "Irnat is ls vs (NC i) = i" +lemma Irnat_C0: "Irnat is ls vs (NC 0) = 0" +by simp +lemma Irnat_C1: "Irnat is ls vs (NC 1) = 1" +by simp +lemma Irnat_Cnumberof: "Irnat is ls vs (NC (number_of x)) = number_of x" +by simp +lemmas Irnat_simps = Irnat_Suc Irnat_Var Irnat_Neg Irnat_Add Irnat_Sub Irnat_Mult Irnat_lgth + Irnat_C0 Irnat_C1 Irnat_Cnumberof +lemma "(Suc n) * length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs) = length xs" + apply (reify Irnat_simps Irlist.simps Irint_simps ("(Suc n) *length (([(3::int) * x + y*y - 9 + (- z)] @ []) @ xs)")) + oops +datatype rifm = RT | RF | RVar nat + | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat + |RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm + | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm + | RBEX rifm | RBALL rifm +consts Irifm :: "bool list \ int list \ (int list) list \ nat list \ rifm \ bool" +primrec +"Irifm ps is ls ns RT = True" +"Irifm ps is ls ns RF = False" + "Irifm ps is ls ns (RVar n) = ps!n" +"Irifm ps is ls ns (RNLT s t) = (Irnat is ls ns s < Irnat is ls ns t)" +"Irifm ps is ls ns (RNILT s t) = (int (Irnat is ls ns s) < Irint is t)" +"Irifm ps is ls ns (RNEQ s t) = (Irnat is ls ns s = Irnat is ls ns t)" +"Irifm ps is ls ns (RAnd p q) = (Irifm ps is ls ns p \ Irifm ps is ls ns q)" +"Irifm ps is ls ns (ROr p q) = (Irifm ps is ls ns p \ Irifm ps is ls ns q)" +"Irifm ps is ls ns (RImp p q) = (Irifm ps is ls ns p \ Irifm ps is ls ns q)" +"Irifm ps is ls ns (RIff p q) = (Irifm ps is ls ns p = Irifm ps is ls ns q)" +"Irifm ps is ls ns (RNEX p) = (\x. Irifm ps is ls (x#ns) p)" +"Irifm ps is ls ns (RIEX p) = (\x. Irifm ps (x#is) ls ns p)" +"Irifm ps is ls ns (RLEX p) = (\x. Irifm ps is (x#ls) ns p)" +"Irifm ps is ls ns (RBEX p) = (\x. Irifm (x#ps) is ls ns p)" +"Irifm ps is ls ns (RNALL p) = (\x. Irifm ps is ls (x#ns) p)" +"Irifm ps is ls ns (RIALL p) = (\x. Irifm ps (x#is) ls ns p)" +"Irifm ps is ls ns (RLALL p) = (\x. Irifm ps is (x#ls) ns p)" +"Irifm ps is ls ns (RBALL p) = (\x. Irifm (x#ps) is ls ns p)" -lemma " \(x::nat) y. \ z. z < x + 3*y \ x + y = 0" -apply (reify Inum_eqs' Iafm.simps) +lemma " \x. \n. ((Suc n) * length (([(3::int) * x + (f t)*y - 9 + (- z)] @ []) @ xs) = length xs) \ m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \ (\p. \q. p \ q \ r)" + apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps) oops - - end diff -r 44eda2314aab -r 6857bd9f1a79 src/HOL/ex/reflection.ML --- a/src/HOL/ex/reflection.ML Mon Sep 18 07:48:07 2006 +0200 +++ b/src/HOL/ex/reflection.ML Mon Sep 18 10:09:57 2006 +0200 @@ -26,33 +26,28 @@ fun mk_congeq ctxt fs th = let - val Const(fname,fT)$(vs as Free(_,_))$_ = - (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th + val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq + |> fst |> strip_comb |> fst val thy = ProofContext.theory_of ctxt val cert = Thm.cterm_of thy - fun dest_listT (Type ("List.list",[vT])) = vT - val vT = dest_listT (Term.domain_type fT) val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) - - fun add_fterms (t as t1 $ t2 $ t3) = - if exists (fn f => t1 aconv f) fs then insert (op aconv) t - else add_fterms (t1 $ t2) #> add_fterms t3 - | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2 + fun add_fterms (t as t1 $ t2) = + if exists (fn f => (t |> strip_comb |> fst) aconv f) fs then insert (op aconv) t + else add_fterms t1 #> add_fterms t2 | add_fterms (t as Abs(xn,xT,t')) = - if (vs mem (term_frees t)) then (fn _ => [t]) else (fn _ => []) + if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => []) | add_fterms _ = I val fterms = add_fterms rhs [] val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt' val tys = map fastype_of fterms val vs = map Free (xs ~~ tys) val env = fterms ~~ vs - - fun replace_fterms (t as t1 $ t2 $ t3) = + (* FIXME!!!!*) + fun replace_fterms (t as t1 $ t2) = (case AList.lookup (op aconv) env t of SOME v => v - | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3) - | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2 + | NONE => replace_fterms t1 $ replace_fterms t2) | replace_fterms t = (case AList.lookup (op aconv) env t of SOME v => v | NONE => t) @@ -70,50 +65,6 @@ val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' in (vs', cong') end; - - -(* -fun mk_congeq ctxt fs th = - let - val Const(fname,fT)$(Free(_,_))$_ = - (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - fun dest_listT (Type ("List.list",[vT])) = vT; - val vT = dest_listT (Term.domain_type fT); - val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt; - val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')); - - fun add_fterms (t as t1 $ t2 $ t3) = - if exists (fn f => t1 aconv f) fs then insert (op aconv) t - else add_fterms (t1 $ t2) #> add_fterms t3 - | add_fterms (t1 $ t2) = add_fterms t1 #> add_fterms t2 - | add_fterms (Abs _) = sys_error "FIXME" - | add_fterms _ = I; - val fterms = add_fterms rhs []; - - val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt'; - val tys = map fastype_of fterms - val vs = map Free (xs ~~ tys); - val env = fterms ~~ vs; - - fun replace_fterms (t as t1 $ t2 $ t3) = - (case AList.lookup (op aconv) env t of - SOME v => v - | NONE => replace_fterms (t1 $ t2) $ replace_fterms t3) - | replace_fterms (t1 $ t2) = replace_fterms t1 $ replace_fterms t2 - | replace_fterms t = t; - - fun mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)); - val cong = (Goal.prove ctxt'' [] (map mk_def env) - (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) - (fn x => LocalDefs.unfold_tac (#context x) (#prems x) THEN rtac th' 1)) RS sym; - - val (cong' :: vars') = Variable.export ctxt'' ctxt - (cong :: map (Drule.mk_term o cert) vs); - val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'; - in (vs', cong') end; -*) (* congs is a list of pairs (P,th) where th is a theorem for *) (* [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *) val FWD = curry (op OF); @@ -130,30 +81,48 @@ exception REIF of string; -val env = ref ([]: (term list)); -val bnds = ref ([]: (term list)); -fun env_index t = - let val i = find_index_eq t (!env) - val j = find_index_eq t (!bnds) - in if j = ~1 then if i = ~1 then (env:= (!env)@[t] ; (length ((!bnds)@(!env))) - 1) else i - else j end; +val bds = ref ([]: (typ * ((term list) * (term list))) list); + +fun index_of t = + let + val tt = HOLogic.listT (fastype_of t) + in + (case AList.lookup (op =) (!bds) tt of + NONE => error "index_of : type not found in environements!" + | SOME (tbs,tats) => + let + val i = find_index_eq t tats + val j = find_index_eq t tbs + in (if j= ~1 then + if i= ~1 + then (bds := AList.update (op =) (tt,(tbs,tats@[t])) (!bds) ; + length tbs + length tats) + else i else j) + end) + end; + +fun dest_listT (Type ("List.list", [T])) = T; fun decomp_genreif da cgns (t,ctxt) = - let - val thy = ProofContext.theory_of ctxt - val cert = cterm_of thy - fun tryabsdecomp (s,ctxt) = - (case s of - Abs(xn,xT,ta) => - (let - val ([xn],ctxt') = Variable.invent_fixes ["x"] ctxt - val (xn,ta) = variant_abs (xn,xT,ta) - val x = Free(xn,xT) - val _ = (bnds := x::(!bnds)) - in ([(ta, ctxt')] , fn [th] => - (bnds := tl (!bnds) ; - hd (Variable.export ctxt' ctxt - [(forall_intr (cert x) th) COMP allI]))) + let + val thy = ProofContext.theory_of ctxt + val cert = cterm_of thy + fun tryabsdecomp (s,ctxt) = + (case s of + Abs(xn,xT,ta) => + (let + val ([xn],ctxt') = Variable.invent_fixes ["x"] ctxt + val (xn,ta) = variant_abs (xn,xT,ta) + val x = Free(xn,xT) + val _ = (case AList.lookup (op =) (!bds) (HOLogic.listT xT) + of NONE => error "tryabsdecomp: Type not found in the Environement" + | SOME (bsT,atsT) => + (bds := AList.update (op =) (HOLogic.listT xT, ((x::bsT), atsT)) (!bds))) + in ([(ta, ctxt')] , + fn [th] => ((let val (bsT,asT) = the(AList.lookup (op =) (!bds) (HOLogic.listT xT)) + in (bds := AList.update (op =) (HOLogic.listT xT,(tl bsT,asT)) (!bds)) + end) ; + hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]))) end) | _ => da (s,ctxt)) in @@ -161,114 +130,151 @@ [] => tryabsdecomp (t,ctxt) | ((vns,cong)::congs) => ((let val cert = cterm_of thy - val (_, tmenv) = - Pattern.match thy - ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) - (Envir.type_env (Envir.empty 0),Term.Vartab.empty) - val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) - val (fts,its) = (map (snd o snd) fnvs, - map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) - in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate ([], its) cong)) - end) - handle MATCH => decomp_genreif da congs (t,ctxt))) - end; - -(* - fun decomp_genreif thy da ((vns,cong)::congs) t = - ((let - val cert = cterm_of thy - val (_, tmenv) = + val certy = ctyp_of thy + val (tyenv, tmenv) = Pattern.match thy ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) (Envir.type_env (Envir.empty 0),Term.Vartab.empty) val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) - val (fts,its) = (map (snd o snd) fnvs, - map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) - in (fts, FWD (instantiate ([], its) cong)) + val (fts,its) = + (map (snd o snd) fnvs, + map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) + val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) + in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong)) end) - handle MATCH => decomp_genreif thy da congs t) - | decomp_genreif thy da [] t = da t; - - (* We add the atoms here during reification *) -val env = ref ([]: (term list)); - -fun env_index t = - let val i = find_index_eq t (!env) - in if i = ~1 then (env:= (!env)@[t] ; (length (!env)) - 1) else i end; -*) - + handle MATCH => decomp_genreif da congs (t,ctxt))) + end; (* looks for the atoms equation and instantiates it with the right number *) fun mk_decompatom eqs (t,ctxt) = - let - val thy = ProofContext.theory_of ctxt - fun isateq (_$_$(Const("List.nth",_)$_$_)) = true - | isateq _ = false - in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of - NONE => raise REIF "Can not find the atoms equation" - | SOME th => - ([], - fn ths => - let val _ = print_thm th - val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt - val (Const("List.nth",_)$vs$_) = - (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th - val vsT = fastype_of vs - val Type("List.list",[vT]) = vsT - val cvs = cterm_of thy (foldr (fn (x,xs) => Const("List.list.Cons", vT --> vsT --> vsT)$x$xs) (Free(x,vsT)) (!bnds)) - val _ = print_thm (th RS sym) - val _ = print_cterm cvs - val th' = instantiate' [] - [SOME cvs, - SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))] - (th RS sym) - in hd (Variable.export ctxt' ctxt [th']) end) - end; + let + val tT = fastype_of t + fun isat eq = + let + val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd + in exists_Const + (fn (n,ty) => n="List.nth" + andalso + AList.defined (op =) (!bds) (domain_type ty)) rhs + andalso fastype_of rhs = tT + end + fun get_nth t = + case t of + Const("List.nth",_)$vs$n => (t,vs,n) + | t1$t2 => (get_nth t1 handle REIF "get_nth" => get_nth t2) + | Abs(_,_,t') => get_nth t' + | _ => raise REIF "get_nth" + val ([xn,vsn],ctxt') = Variable.invent_fixes ["x","vs"] ctxt + val thy = ProofContext.theory_of ctxt' + val cert = cterm_of thy + fun tryeqs [] = raise REIF "Can not find the atoms equation" + | tryeqs (eq::eqs) = (( + let + val rhs = eq |> prop_of |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq |> snd + val (nt,vs,n) = get_nth rhs + val ntT = fastype_of nt + val ntlT = HOLogic.listT ntT + val (bsT,asT) = the (AList.lookup (op =) (!bds) ntlT) + val x = Var ((xn,0),ntT) + val rhs_P = subst_free [(nt,x)] rhs + val (_, tmenv) = Pattern.match + thy (rhs_P, t) + (Envir.type_env (Envir.empty 0),Term.Vartab.empty) + val tml = Vartab.dest tmenv + val SOME (_,t') = AList.lookup (op =) tml (xn,0) + val cvs = + cert (foldr (fn (x,xs) => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs) + (Free(vsn,ntlT)) bsT) + val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) + (AList.delete (op =) (xn,0) tml) + val th = (instantiate + ([], + [(cert vs, cvs),(cert n, t' |> index_of |> HOLogic.mk_nat |> cert)] + @cts) eq) RS sym + in hd (Variable.export ctxt' ctxt [th]) + end) + handle MATCH => tryeqs eqs) + in ([], fn _ => tryeqs (filter isat eqs)) + end; -(* -fun mk_decompatom thy eqs = - let fun isateq (_$_$(Const("List.nth",_)$_$_)) = true - | isateq _ = false - in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of - NONE => raise REIF "Can not find the atoms equation" - | SOME th => - fn t => ([], - fn ths => - instantiate' [] [SOME(cterm_of thy (HOLogic.mk_nat(env_index t)))] - (th RS sym)) - end; +(* +fun mk_decompatom eqs (t,ctxt) = + let + val tT = fastype_of t + val tlT = HOLogic.listT tT + val (bsT,asT) = (the (AList.lookup (op =) (!bds) tlT) + handle Option => error "mk_decompatom: Type not found in the env.") + fun isateq (_$_$(Const("List.nth",_)$vs$_)) = (fastype_of vs = tlT) + | isateq _ = false + in case List.find (isateq o HOLogic.dest_Trueprop o prop_of) eqs of + NONE => raise REIF "Can not find the atoms equation" + | SOME th => + ([], + fn ths => + let + val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt + val cert = cterm_of (ProofContext.theory_of ctxt') + val (Const("List.nth",_)$(vs as Var((vsn,vsi),_))$n) = + (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th + val cvs = + cert (foldr (fn (x,xs) => Const("List.list.Cons", tT --> tlT --> tlT)$x$xs) + (Free(x,tlT)) bsT) + val th' = (instantiate ([], + [(cert vs, cvs), + (cert n, cert (HOLogic.mk_nat(index_of t)))]) th) + RS sym + in hd (Variable.export ctxt' ctxt [th']) end) + end; *) (* Generic reification procedure: *) (* creates all needed cong rules and then just uses the theorem synthesis *) + +fun mk_congs ctxt raw_eqs = + let + val fs = foldr (fn (eq,fns) => + (eq |> prop_of |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq |> fst |> strip_comb + |> fst) ins fns) [] raw_eqs + val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst) + union ts) [] fs + val _ = bds := AList.make (fn _ => ([],[])) tys + val (vs, ctxt') = Variable.invent_fixes (replicate (length tys) "vs") ctxt + val thy = ProofContext.theory_of ctxt' + val cert = cterm_of thy + val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) + (tys ~~ vs) + fun insteq eq ts = + let val itms = map (fn t => t|> (AList.lookup (op =) vstys) |> the) ts + in instantiate' [] itms eq + end + val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq |> fst |> strip_comb |> fst |> fastype_of + |> binder_types |> split_last |> fst + |> (insteq eq)) raw_eqs + val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) + in ps ~~ (Variable.export ctxt' ctxt congs) + end; + fun genreif ctxt raw_eqs t = - let val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt - val thy = ProofContext.theory_of ctxt' - val cert = cterm_of thy - val Const(fname,fT)$(Var(_,vT))$_ = - (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (hd raw_eqs) - val cv = cert (Free(x, vT)) - val eqs = map (instantiate' [] [SOME cv]) raw_eqs - val fs = - foldr (fn (eq,fns) => - let val f$_$_ = (fst o HOLogic.dest_eq o - HOLogic.dest_Trueprop o prop_of) eq - in f ins fns end) [] eqs - val congs = map (mk_congeq ctxt' fs) eqs - val congs = (map fst congs) ~~ (Variable.export ctxt' ctxt (map snd congs)) - val _ = (env := []) - val _ = (bnds := []) - val da = mk_decompatom raw_eqs - val th = divide_and_conquer (decomp_genreif da congs) (t,ctxt) - val cv' = cterm_of (ProofContext.theory_of ctxt) - (HOLogic.mk_list I (body_type fT) (!env)) - val _ = (env := []) - val _ = (bnds:= []) - val th' = instantiate' [] [SOME cv'] th - val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' - val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) - (fn _ => Simp_tac 1) - in FWD trans [th'',th'] - end; + let + val _ = bds := [] + val congs = mk_congs ctxt raw_eqs + val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) + val tys = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd + |> strip_comb |> fst |> fastype_of |> strip_type |> fst + |> split_last |> fst + val cert = cterm_of (ProofContext.theory_of ctxt) + val cvs = map (fn t => t |> (AList.lookup (op =) (!bds)) |> the |> snd + |> HOLogic.mk_list I (dest_listT t) |> cert |> SOME) + tys + val th' = (instantiate' [] cvs (th RS sym)) RS sym + val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' + val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) + (fn _ => Simp_tac 1) + val _ = bds := [] + in FWD trans [th'',th'] + end; fun genreflect ctxt corr_thm raw_eqs t = let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym] @@ -295,4 +301,4 @@ val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst in rtac th i st end); -end +end \ No newline at end of file