# HG changeset patch # User haftmann # Date 1233137085 -3600 # Node ID bd6fb191c00eb6104a5e37bbcce18d3fe25339f2 # Parent cc3958d31b1d5a098da96c69ebd2fa4283079a34# Parent ac31940cfb69b84298e34a4ab8c50d191a383de4 merged diff -r ac31940cfb69 -r bd6fb191c00e NEWS --- a/NEWS Wed Jan 28 11:03:42 2009 +0100 +++ b/NEWS Wed Jan 28 11:04:45 2009 +0100 @@ -193,6 +193,8 @@ *** HOL *** +* Theory "Reflection" now resides in HOL/Library. + * Entry point to Word library now simply named "Word". INCOMPATIBILITY. * Made source layout more coherent with logical distribution diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 28 11:03:42 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 28 11:04:45 2009 +0100 @@ -331,10 +331,11 @@ Library/Binomial.thy Library/Eval_Witness.thy \ Library/Code_Index.thy Library/Code_Char.thy \ Library/Code_Char_chr.thy Library/Code_Integer.thy \ - Library/Numeral_Type.thy \ + Library/Numeral_Type.thy Library/Reflection.thy \ Library/Boolean_Algebra.thy Library/Countable.thy \ Library/RBT.thy Library/Univ_Poly.thy \ - Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML + Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \ + Library/reify_data.ML Library/reflection.ML @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library @@ -809,14 +810,14 @@ ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML \ + ex/Quickcheck_Examples.thy \ ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ ex/Reflected_Presburger.thy ex/coopertac.ML \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ ex/Subarray.thy ex/Sublist.thy \ ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \ ex/Unification.thy ex/document/root.bib \ - ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy \ + ex/document/root.tex ex/Meson_Test.thy ex/set.thy \ ex/svc_funcs.ML ex/svc_test.thy \ ex/ImperativeQuicksort.thy \ ex/BigO_Complex.thy \ @@ -968,7 +969,7 @@ HOL-Word: HOL $(OUT)/HOL-Word -$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Infinite_Set.thy \ +$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \ Library/Boolean_Algebra.thy \ Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \ Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \ diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Jan 28 11:03:42 2009 +0100 +++ b/src/HOL/Library/Library.thy Wed Jan 28 11:04:45 2009 +0100 @@ -35,6 +35,7 @@ Quicksort Quotient Ramsey + Reflection RBT State_Monad Univ_Poly diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/Library/Reflection.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Reflection.thy Wed Jan 28 11:04:45 2009 +0100 @@ -0,0 +1,45 @@ +(* Title: HOL/Library/Reflection.thy + Author: Amine Chaieb, TU Muenchen +*) + +header {* Generic reflection and reification *} + +theory Reflection +imports Main +uses "reify_data.ML" ("reflection.ML") +begin + +setup {* Reify_Data.setup *} + +lemma ext2: "(\x. f x = g x) \ f = g" + by (blast intro: ext) + +use "reflection.ML" + +method_setup reify = {* fn src => + Method.syntax (Attrib.thms -- + Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #> + (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) +*} "partial automatic reification" + +method_setup reflection = {* +let + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); + val onlyN = "only"; + val rulesN = "rules"; + val any_keyword = keyword onlyN || keyword rulesN; + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + val terms = thms >> map (term_of o Drule.dest_term); + fun optional scan = Scan.optional scan []; +in fn src => + Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> + (fn (((eqs,ths),to), ctxt) => + let + val (ceqs,cths) = Reify_Data.get ctxt + val corr_thms = ths@cths + val raw_eqs = eqs@ceqs + in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) + end) end +*} "reflection method" + +end diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/Library/reflection.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/reflection.ML Wed Jan 28 11:04:45 2009 +0100 @@ -0,0 +1,327 @@ +(* Title: HOL/Library/reflection.ML + Author: Amine Chaieb, TU Muenchen + +A trial for automatical reification. +*) + +signature REFLECTION = +sig + val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic + val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic + val gen_reflection_tac: Proof.context -> (cterm -> thm) + -> thm list -> thm list -> term option -> int -> tactic +end; + +structure Reflection : REFLECTION = +struct + +val ext2 = @{thm ext2}; +val nth_Cons_0 = @{thm nth_Cons_0}; +val nth_Cons_Suc = @{thm nth_Cons_Suc}; + + (* Make a congruence rule out of a defining equation for the interpretation *) + (* th is one defining equation of f, i.e. + th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *) + (* Cp is a constructor pattern and P is a pattern *) + + (* The result is: + [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *) + (* + the a list of names of the A1 .. An, Those are fresh in the ctxt*) + + +fun mk_congeq ctxt fs th = + let + 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 + val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt + val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) + fun add_fterms (t as t1 $ t2) = + if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t + else add_fterms t1 #> add_fterms t2 + | add_fterms (t as Abs(xn,xT,t')) = + if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => []) + | add_fterms _ = I + val fterms = add_fterms rhs [] + val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt' + val tys = map fastype_of fterms + val vs = map Free (xs ~~ tys) + val env = fterms ~~ vs + (* FIXME!!!!*) + fun replace_fterms (t as t1 $ t2) = + (case AList.lookup (op aconv) env t of + SOME v => v + | NONE => replace_fterms t1 $ replace_fterms t2) + | replace_fterms t = (case AList.lookup (op aconv) env t of + SOME v => v + | NONE => t) + + 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))) + | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) + fun tryext x = (x RS ext2 handle THM _ => x) + 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) (map tryext (#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); + + (* da is the decomposition for atoms, ie. it returns ([],g) where g + returns the right instance f (AtC n) = t , where AtC is the Atoms + constructor and n is the number of the atom corresponding to t *) + +(* Generic decomp for reification : matches the actual term with the +rhs of one cong rule. The result of the matching guides the +proof synthesis: The matches of the introduced Variables A1 .. An are +processed recursively + The rest is instantiated in the cong rule,i.e. no reification is needed *) + +exception REIF of string; + +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 Type.could_unify (!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 Type.could_unify (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.variant_fixes ["x"] ctxt + val (xn,ta) = variant_abs (xn,xT,ta) + val x = Free(xn,xT) + val _ = (case AList.lookup Type.could_unify (!bds) (HOLogic.listT xT) + of NONE => error "tryabsdecomp: Type not found in the Environement" + | SOME (bsT,atsT) => + (bds := AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) (!bds))) + in ([(ta, ctxt')] , + fn [th] => ((let val (bsT,asT) = the(AList.lookup Type.could_unify (!bds) (HOLogic.listT xT)) + in (bds := AList.update Type.could_unify (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 + (case cgns of + [] => tryabsdecomp (t,ctxt) + | ((vns,cong)::congs) => ((let + val cert = cterm_of thy + 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), 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) + 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 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 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 Type.could_unify (!bds) (domain_type ty)) rhs + andalso Type.could_unify (fastype_of rhs, tT) + end + fun get_nths t acc = + case t of + Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc + | t1$t2 => get_nths t1 (get_nths t2 acc) + | Abs(_,_,t') => get_nths t' acc + | _ => acc + + fun + tryeqs [] = error "Can not find the atoms equation" + | tryeqs (eq::eqs) = (( + let + val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd + val nths = get_nths rhs [] + val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) => + (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[]) + val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt + val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt' + val thy = ProofContext.theory_of ctxt'' + val cert = cterm_of thy + val certT = ctyp_of thy + val vsns_map = vss ~~ vsns + val xns_map = (fst (split_list nths)) ~~ xns + val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map + val rhs_P = subst_free subst rhs + val (tyenv, tmenv) = Pattern.match + thy (rhs_P, t) + (Envir.type_env (Envir.empty 0), Vartab.empty) + val sbst = Envir.subst_vars (tyenv, tmenv) + val sbsT = Envir.typ_subst_TVars tyenv + val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) + (Vartab.dest tyenv) + val tml = Vartab.dest tmenv + val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) + val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) => + (cert n, snd (valOf (AList.lookup (op =) tml xn0)) + |> (index_of #> HOLogic.mk_nat #> cert))) + subst + val subst_vs = + let + fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T)) + fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = + let + val cns = sbst (Const("List.list.Cons", T --> lT --> lT)) + val lT' = sbsT lT + val (bsT,asT) = the (AList.lookup Type.could_unify (!bds) lT) + val vsn = valOf (AList.lookup (op =) vsns_map vs) + val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT'))) + in (cert vs, cvs) end + in map h subst end + val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) + (fold (AList.delete (fn (((a: string),_),(b,_)) => a = b)) + (map (fn n => (n,0)) xns) tml) + val substt = + let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[])) + in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end + val th = (instantiate (subst_ty, substt) eq) RS sym + in hd (Variable.export ctxt'' ctxt [th]) end) + handle MATCH => tryeqs eqs) +in ([], fn _ => tryeqs (filter isat eqs)) +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 = fold_rev (fn eq => + insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq |> fst |> strip_comb + |> fst)) raw_eqs [] + val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl) + union ts) fs [] + val _ = bds := AList.make (fn _ => ([],[])) tys + val (vs, ctxt') = Variable.variant_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) + val is_Var = can dest_Var + fun insteq eq vs = + let + val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t))) + (filter is_Var vs) + in Thm.instantiate ([],subst) eq + end + val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl + |> (insteq eq)) raw_eqs + val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) +in ps ~~ (Variable.export ctxt' ctxt congs) +end + +fun partition P [] = ([],[]) + | partition P (x::xs) = + let val (yes,no) = partition P xs + in if P x then (x::yes,no) else (yes, x::no) end + +fun rearrange congs = +let + fun P (_, th) = + let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th + in can dest_Var l end + val (yes,no) = partition P congs + in no @ yes end + + + +fun genreif ctxt raw_eqs t = + let + val congs = rearrange (mk_congs ctxt raw_eqs) + val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) + fun is_listVar (Var (_,t)) = can dest_listT t + | is_listVar _ = false + val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd + |> strip_comb |> snd |> filter is_listVar + val cert = cterm_of (ProofContext.theory_of ctxt) + val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars + val th' = instantiate ([], cvs) 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 (local_simpset_of ctxt) 1) + val _ = bds := [] +in FWD trans [th'',th'] +end + + +fun genreflect ctxt conv corr_thms raw_eqs t = +let + val reifth = genreif ctxt raw_eqs t + fun trytrans [] = error "No suitable correctness theorem found" + | trytrans (th::ths) = + (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths) + val th = trytrans corr_thms + val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th + val rth = conv ft +in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc]) + (simplify (HOL_basic_ss addsimps [rth]) th) +end + +fun genreify_tac ctxt eqs to i = (fn st => + let + val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)) + val t = (case to of NONE => P | SOME x => x) + val th = (genreif ctxt eqs t) RS ssubst + in rtac th i st + end); + + (* Reflection calls reification and uses the correctness *) + (* theorem assumed to be the dead of the list *) +fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st => + let + val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1)); + val t = the_default P to; + val th = genreflect ctxt conv corr_thms raw_eqs t + RS ssubst; + in (rtac th i THEN TRY(rtac TrueI i)) st end); + +fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv; + +end diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/Library/reify_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/reify_data.ML Wed Jan 28 11:04:45 2009 +0100 @@ -0,0 +1,39 @@ +(* Title: HOL/Library/reflection_data.ML + Author: Amine Chaieb, TU Muenchen + +Data for the reification and reflection methods. +*) + +signature REIFY_DATA = +sig + val get: Proof.context -> thm list * thm list + val add: attribute + val del: attribute + val radd: attribute + val rdel: attribute + val setup: theory -> theory +end; + +structure Reify_Data : REIFY_DATA = +struct + +structure Data = GenericDataFun +( + type T = thm list * thm list; + val empty = ([], []); + val extend = I; + fun merge _ = pairself Thm.merge_thms; +); + +val get = Data.get o Context.Proof; + +val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm); +val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm); +val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm); +val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm); + +val setup = Attrib.add_attributes + [("reify", Attrib.add_del_args add del, "Reify data"), + ("reflection", Attrib.add_del_args radd rdel, "Reflection data")]; + +end; diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Jan 28 11:03:42 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Jan 28 11:04:45 2009 +0100 @@ -63,7 +63,6 @@ "Dense_Linear_Order_Ex", "PresburgerEx", "Reflected_Presburger", - "Reflection", "ReflectionEx", "BinEx", "Sqrt", diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/ex/Reflection.thy --- a/src/HOL/ex/Reflection.thy Wed Jan 28 11:03:42 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* - ID: $Id$ - Author: Amine Chaieb, TU Muenchen -*) - -header {* Generic reflection and reification *} - -theory Reflection -imports Main - uses "reflection_data.ML" ("reflection.ML") -begin - -setup {* Reify_Data.setup*} - - -lemma ext2: "(\x. f x = g x) \ f = g" - by (blast intro: ext) - -use "reflection.ML" - -method_setup reify = {* - fn src => - Method.syntax (Attrib.thms -- - Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #> - (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) -*} "partial automatic reification" - -method_setup reflection = {* -let -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -val onlyN = "only"; -val rulesN = "rules"; -val any_keyword = keyword onlyN || keyword rulesN; -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map (term_of o Drule.dest_term); -fun optional scan = Scan.optional scan []; -in -fn src => - Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> - (fn (((eqs,ths),to), ctxt) => - let - val (ceqs,cths) = Reify_Data.get ctxt - val corr_thms = ths@cths - val raw_eqs = eqs@ceqs - in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) - end) end -*} "reflection method" -end diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Wed Jan 28 11:03:42 2009 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Wed Jan 28 11:04:45 2009 +0100 @@ -1,9 +1,9 @@ -(* - ID: $Id$ +(* Title: HOL/ex/ReflectionEx.thy Author: Amine Chaieb, TU Muenchen *) header {* Examples for generic reflection and reification *} + theory ReflectionEx imports Reflection begin diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/ex/reflection.ML --- a/src/HOL/ex/reflection.ML Wed Jan 28 11:03:42 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,325 +0,0 @@ -(* Author: Amine Chaieb, TU Muenchen - -A trial for automatical reification. -*) - -signature REFLECTION = -sig - val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic - val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic - val gen_reflection_tac: Proof.context -> (cterm -> thm) - -> thm list -> thm list -> term option -> int -> tactic -end; - -structure Reflection : REFLECTION = -struct - -val ext2 = thm "ext2"; -val nth_Cons_0 = thm "nth_Cons_0"; -val nth_Cons_Suc = thm "nth_Cons_Suc"; - - (* Make a congruence rule out of a defining equation for the interpretation *) - (* th is one defining equation of f, i.e. - th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *) - (* Cp is a constructor pattern and P is a pattern *) - - (* The result is: - [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *) - (* + the a list of names of the A1 .. An, Those are fresh in the ctxt*) - - -fun mk_congeq ctxt fs th = - let - 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 - val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt - val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) - fun add_fterms (t as t1 $ t2) = - if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t - else add_fterms t1 #> add_fterms t2 - | add_fterms (t as Abs(xn,xT,t')) = - if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => []) - | add_fterms _ = I - val fterms = add_fterms rhs [] - val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt' - val tys = map fastype_of fterms - val vs = map Free (xs ~~ tys) - val env = fterms ~~ vs - (* FIXME!!!!*) - fun replace_fterms (t as t1 $ t2) = - (case AList.lookup (op aconv) env t of - SOME v => v - | NONE => replace_fterms t1 $ replace_fterms t2) - | replace_fterms t = (case AList.lookup (op aconv) env t of - SOME v => v - | NONE => t) - - 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))) - | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) - fun tryext x = (x RS ext2 handle THM _ => x) - 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) (map tryext (#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); - - (* da is the decomposition for atoms, ie. it returns ([],g) where g - returns the right instance f (AtC n) = t , where AtC is the Atoms - constructor and n is the number of the atom corresponding to t *) - -(* Generic decomp for reification : matches the actual term with the -rhs of one cong rule. The result of the matching guides the -proof synthesis: The matches of the introduced Variables A1 .. An are -processed recursively - The rest is instantiated in the cong rule,i.e. no reification is needed *) - -exception REIF of string; - -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 Type.could_unify (!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 Type.could_unify (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.variant_fixes ["x"] ctxt - val (xn,ta) = variant_abs (xn,xT,ta) - val x = Free(xn,xT) - val _ = (case AList.lookup Type.could_unify (!bds) (HOLogic.listT xT) - of NONE => error "tryabsdecomp: Type not found in the Environement" - | SOME (bsT,atsT) => - (bds := AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) (!bds))) - in ([(ta, ctxt')] , - fn [th] => ((let val (bsT,asT) = the(AList.lookup Type.could_unify (!bds) (HOLogic.listT xT)) - in (bds := AList.update Type.could_unify (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 - (case cgns of - [] => tryabsdecomp (t,ctxt) - | ((vns,cong)::congs) => ((let - val cert = cterm_of thy - 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), 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) - 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 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 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 Type.could_unify (!bds) (domain_type ty)) rhs - andalso Type.could_unify (fastype_of rhs, tT) - end - fun get_nths t acc = - case t of - Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc - | t1$t2 => get_nths t1 (get_nths t2 acc) - | Abs(_,_,t') => get_nths t' acc - | _ => acc - - fun - tryeqs [] = error "Can not find the atoms equation" - | tryeqs (eq::eqs) = (( - let - val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd - val nths = get_nths rhs [] - val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) => - (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[]) - val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt - val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt' - val thy = ProofContext.theory_of ctxt'' - val cert = cterm_of thy - val certT = ctyp_of thy - val vsns_map = vss ~~ vsns - val xns_map = (fst (split_list nths)) ~~ xns - val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map - val rhs_P = subst_free subst rhs - val (tyenv, tmenv) = Pattern.match - thy (rhs_P, t) - (Envir.type_env (Envir.empty 0), Vartab.empty) - val sbst = Envir.subst_vars (tyenv, tmenv) - val sbsT = Envir.typ_subst_TVars tyenv - val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) - (Vartab.dest tyenv) - val tml = Vartab.dest tmenv - val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) - val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) => - (cert n, snd (valOf (AList.lookup (op =) tml xn0)) - |> (index_of #> HOLogic.mk_nat #> cert))) - subst - val subst_vs = - let - fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T)) - fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = - let - val cns = sbst (Const("List.list.Cons", T --> lT --> lT)) - val lT' = sbsT lT - val (bsT,asT) = the (AList.lookup Type.could_unify (!bds) lT) - val vsn = valOf (AList.lookup (op =) vsns_map vs) - val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT'))) - in (cert vs, cvs) end - in map h subst end - val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) - (fold (AList.delete (fn (((a: string),_),(b,_)) => a = b)) - (map (fn n => (n,0)) xns) tml) - val substt = - let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[])) - in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end - val th = (instantiate (subst_ty, substt) eq) RS sym - in hd (Variable.export ctxt'' ctxt [th]) end) - handle MATCH => tryeqs eqs) -in ([], fn _ => tryeqs (filter isat eqs)) -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 = fold_rev (fn eq => - insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq |> fst |> strip_comb - |> fst)) raw_eqs [] - val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl) - union ts) fs [] - val _ = bds := AList.make (fn _ => ([],[])) tys - val (vs, ctxt') = Variable.variant_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) - val is_Var = can dest_Var - fun insteq eq vs = - let - val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t))) - (filter is_Var vs) - in Thm.instantiate ([],subst) eq - end - val eqs = map (fn eq => eq |> prop_of |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl - |> (insteq eq)) raw_eqs - val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) -in ps ~~ (Variable.export ctxt' ctxt congs) -end - -fun partition P [] = ([],[]) - | partition P (x::xs) = - let val (yes,no) = partition P xs - in if P x then (x::yes,no) else (yes, x::no) end - -fun rearrange congs = -let - fun P (_, th) = - let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th - in can dest_Var l end - val (yes,no) = partition P congs - in no @ yes end - - - -fun genreif ctxt raw_eqs t = - let - val congs = rearrange (mk_congs ctxt raw_eqs) - val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) - fun is_listVar (Var (_,t)) = can dest_listT t - | is_listVar _ = false - val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd - |> strip_comb |> snd |> filter is_listVar - val cert = cterm_of (ProofContext.theory_of ctxt) - val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars - val th' = instantiate ([], cvs) 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 (local_simpset_of ctxt) 1) - val _ = bds := [] -in FWD trans [th'',th'] -end - - -fun genreflect ctxt conv corr_thms raw_eqs t = -let - val reifth = genreif ctxt raw_eqs t - fun trytrans [] = error "No suitable correctness theorem found" - | trytrans (th::ths) = - (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths) - val th = trytrans corr_thms - val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th - val rth = conv ft -in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc]) - (simplify (HOL_basic_ss addsimps [rth]) th) -end - -fun genreify_tac ctxt eqs to i = (fn st => - let - val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)) - val t = (case to of NONE => P | SOME x => x) - val th = (genreif ctxt eqs t) RS ssubst - in rtac th i st - end); - - (* Reflection calls reification and uses the correctness *) - (* theorem assumed to be the dead of the list *) -fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st => - let - val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1)); - val t = the_default P to; - val th = genreflect ctxt conv corr_thms raw_eqs t - RS ssubst; - in (rtac th i THEN TRY(rtac TrueI i)) st end); - -fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv; -end diff -r ac31940cfb69 -r bd6fb191c00e src/HOL/ex/reflection_data.ML --- a/src/HOL/ex/reflection_data.ML Wed Jan 28 11:03:42 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -(* Title: HOL/ex/reflection_data.ML - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Data for the reification and reflection methods. -*) - -signature REIFY_DATA = -sig - type entry = thm list * thm list - val get: Proof.context -> entry - val del: attribute - val add: attribute - val setup: theory -> theory -end; - -structure Reify_Data : REIFY_DATA = -struct - -type entry = thm list * thm list; - -structure Data = GenericDataFun -( - type T = entry - val empty = ([], []) - val extend = I - fun merge _ = pairself Thm.merge_thms -); - -val get = Data.get o Context.Proof; - -val add = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (apfst (Thm.add_thm th))) - -val del = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (apfst (Thm.del_thm th))) - -val radd = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (apsnd (Thm.add_thm th))) - -val rdel = Thm.declaration_attribute (fn th => fn context => - context |> Data.map (apsnd (Thm.del_thm th))) - -(* concrete syntax *) -(* -local -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); - -val constsN = "consts"; -val addN = "add"; -val delN = "del"; -val any_keyword = keyword constsN || keyword addN || keyword delN; -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map (term_of o Drule.dest_term); - -fun optional scan = Scan.optional scan []; - -in -val att_syntax = Attrib.syntax - ((Scan.lift (Args.$$$ "del") |-- thms) >> del || - optional (keyword addN |-- thms) >> add) -end; -*) - -(* theory setup *) - val setup = - Attrib.add_attributes [("reify", Attrib.add_del_args add del, "Reify data"), - ("reflection", Attrib.add_del_args radd rdel, "Reflection data")]; -end; diff -r ac31940cfb69 -r bd6fb191c00e src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Wed Jan 28 11:03:42 2009 +0100 +++ b/src/Pure/Tools/isabelle_process.scala Wed Jan 28 11:04:45 2009 +0100 @@ -118,10 +118,10 @@ /* process information */ - private var proc: Process = null - private var closing = false - private var pid: String = null - private var the_session: String = null + @volatile private var proc: Process = null + @volatile private var closing = false + @volatile private var pid: String = null + @volatile private var the_session: String = null def session = the_session