# HG changeset patch # User wenzelm # Date 1154610185 -7200 # Node ID a8761e8568deba7608b9caa2ea53687a062f7404 # Parent 0e0ea63fe7689e6e05812b258c6cdad190d741c4 Generic reflection and reification (by Amine Chaieb). diff -r 0e0ea63fe768 -r a8761e8568de src/HOL/ex/Reflection.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Reflection.thy Thu Aug 03 15:03:05 2006 +0200 @@ -0,0 +1,27 @@ +(* + ID: $Id$ + Author: Amine Chaieb, TU Muenchen +*) + +header {* Generic reflection and reification *} + +theory Reflection +imports Main +uses "reflection.ML" +begin + +method_setup reify = {* + fn src => + Method.syntax (Attrib.thms -- + Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> + (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to)) +*} "partial automatic reification" + +method_setup reflection = {* + fn src => + Method.syntax (Attrib.thms -- + Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> + (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to)) +*} "reflection method" + +end diff -r 0e0ea63fe768 -r a8761e8568de src/HOL/ex/ReflectionEx.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/ReflectionEx.thy Thu Aug 03 15:03:05 2006 +0200 @@ -0,0 +1,252 @@ +(* + ID: $Id$ + Author: Amine Chaieb, TU Muenchen +*) + +header {* Examples for generic reflection and reification *} + +theory ReflectionEx +imports Reflection +begin + + + (* The type fm represents simple propositional formulae *) +datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat + +consts Ifm :: "bool list \ fm \ bool" +primrec + "Ifm vs (At n) = vs!n" + "Ifm bs (And p q) = (Ifm bs p \ Ifm bs q)" + "Ifm vs (Or p q) = (Ifm vs p \ Ifm vs q)" + "Ifm vs (Imp p q) = (Ifm vs p \ Ifm vs q)" + "Ifm vs (Iff p q) = (Ifm vs p = Ifm vs q)" + "Ifm vs (NOT p) = (\ (Ifm vs p))" + +consts fmsize :: "fm \ nat" +primrec + "fmsize (At n) = 1" + "fmsize (NOT p) = 1 + fmsize p" + "fmsize (And p q) = 1 + fmsize p + fmsize q" + "fmsize (Or p q) = 1 + fmsize p + fmsize q" + "fmsize (Imp p q) = 2 + fmsize p + fmsize q" + "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q" + + + + (* reify maps a bool to an fm, for this it needs the + semantics of fm (Ifm.simps)*) +lemma "Q \ (D & F & ((~ D) & (~ F)))" +apply (reify Ifm.simps) +oops + + (* You can also just pick up a subterm to reify \ *) +lemma "Q \ (D & F & ((~ D) & (~ F)))" +apply (reify Ifm.simps ("((~ D) & (~ F))")) +oops + + (* Let's perform NNF, A version that tends to disjunctions *) +consts nnf :: "fm \ fm" +recdef nnf "measure fmsize" + "nnf (At n) = At n" + "nnf (And p q) = And (nnf p) (nnf q)" + "nnf (Or p q) = Or (nnf p) (nnf q)" + "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)" + "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))" + "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))" + "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))" + "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))" + "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))" + "nnf (NOT (NOT p)) = nnf p" + "nnf (NOT p) = NOT p" + + (* nnf preserves the semantics of fm *) +lemma nnf: "Ifm vs (nnf p) = Ifm vs p" + by (induct p rule: nnf.induct) auto + + (* Now let's perform NNF using our function defined above. + reflection takes the correctness theorem (nnf) the semantics of fm + and applies the function to the corresponding of the formula *) +lemma "(\ (A = B)) \ (B \ (A \ (B | C \ (B \ A | D)))) \ A \ B \ D" +apply (reflection nnf Ifm.simps) +oops + + (* Here also you can just pick up a subterm \ *) +lemma "(\ (A = B)) \ (B \ (A \ (B | C \ (B \ A | D)))) \ A \ B \ D" +apply (reflection nnf Ifm.simps ("(B | C \ (B \ A | D))")) +oops + + + (* Example 2 : simple arithmetics formulae *) + + (* num reflects linear expressions over natural number *) +datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num + +consts num_size :: "num \ nat" +primrec + "num_size (C c) = 1" + "num_size (Var n) = 1" + "num_size (Add a b) = 1 + num_size a + num_size b" + "num_size (Mul c a) = 1 + num_size a" + "num_size (CN n c a) = 4 + num_size a " + + (* The semantics of num *) +consts Inum:: "nat list \ num \ nat" +primrec + Inum_C : "Inum vs (C i) = i" + Inum_Var: "Inum vs (Var n) = vs!n" + Inum_Add: "Inum vs (Add s t) = Inum vs s + Inum vs t" + Inum_Mul: "Inum vs (Mul c t) = c * Inum vs t" + Inum_CN : "Inum vs (CN n c t) = c*(vs!n) + Inum vs t" + + (* Let's reify some nat expressions \ *) +lemma "4 * (2*x + (y::nat)) \ 0" + apply (reify Inum.simps ("4 * (2*x + (y::nat))")) + (* We're in a bad situation!!*) +oops + (* So let's leave the Inum_C equation at the end and see what happens \*) +lemma "4 * (2*x + (y::nat)) \ 0" + apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))")) + (* We're still in a bad situation!!*) + (* BUT!! It's better\ Note that the reification depends on the order of the equations\ *) + (* The problem is that Inum_C has the form : Inum vs (C i) = i *) + (* So the right handside matches any term of type nat, which makes things bad. *) + (* We want only numerals \ So let's specialize Inum_C with numerals.*) +oops + +lemma Inum_number: "Inum vs (C (number_of t)) = number_of t" by simp +lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number + + (* Second trial *) +lemma "1 * (2*x + (y::nat)) \ 0" + apply (reify Inum_eqs ("1 * (2*x + (y::nat))")) +oops + (* That was fine, so let's try an other one\ *) + +lemma "1 * (2*x + (y::nat) + 0 + 1) \ 0" + apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)")) + (* Oh!! 0 is not a variable \ Oh! 0 is not a number_of .. thing *) + (* Tha same for 1, so let's add those equations too *) +oops + +lemma Inum_01: "Inum vs (C 0) = 0" "Inum vs (C 1) = 1" "Inum vs (C(Suc n)) = Suc n" + by simp+ +lemmas Inum_eqs'= Inum_eqs Inum_01 + (* Third Trial *) + +lemma "1 * (2*x + (y::nat) + 0 + 1) \ 0" + apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)")) + (* Okay *) +oops + + (* Some simplifications for num terms, you can skimm untill the main theorem linum *) +consts lin_add :: "num \ num \ num" +recdef lin_add "measure (\(x,y). ((size x) + (size y)))" + "lin_add (CN n1 c1 r1,CN n2 c2 r2) = + (if n1=n2 then + (let c = c1 + c2 + in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2)))) + else if n1 \ n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2))) + else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))" + "lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))" + "lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))" + "lin_add (C b1, C b2) = C (b1+b2)" + "lin_add (a,b) = Add a b" +lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)" +apply (induct t s rule: lin_add.induct, simp_all add: Let_def) +apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) +by (case_tac "n1 = n2", simp_all add: ring_eq_simps) + +consts lin_mul :: "num \ nat \ num" +recdef lin_mul "measure size " + "lin_mul (C j) = (\ i. C (i*j))" + "lin_mul (CN n c a) = (\ i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))" + "lin_mul t = (\ i. Mul i t)" + +lemma lin_mul: "\ i. Inum bs (lin_mul t i) = Inum bs (Mul i t)" +by (induct t rule: lin_mul.induct, auto simp add: ring_eq_simps) + +consts linum:: "num \ num" +recdef linum "measure num_size" + "linum (C b) = C b" + "linum (Var n) = CN n 1 (C 0)" + "linum (Add t s) = lin_add (linum t, linum s)" + "linum (Mul c t) = lin_mul (linum t) c" + "linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)" + +lemma linum : "Inum vs (linum t) = Inum vs t" +by (induct t rule: linum.induct, simp_all add: lin_mul lin_add) + + (* Now we can use linum to simplify nat terms using reflection *) +lemma "(Suc (Suc 1)) * ((x::nat) + (Suc 1)*y) = 3*x + 6*y" +apply (reflection linum Inum_eqs' ("(Suc (Suc 1)) * ((x::nat) + (Suc 1)*y)")) +oops + + (* Let's list this to formulae \ *) + +datatype aform = Lt num num | Eq num num | Ge num num | NEq num num | + Conj aform aform | Disj aform aform | NEG aform | T | F +consts linaformsize:: "aform \ nat" +recdef linaformsize "measure size" + "linaformsize T = 1" + "linaformsize F = 1" + "linaformsize (Lt a b) = 1" + "linaformsize (Ge a b) = 1" + "linaformsize (Eq a b) = 1" + "linaformsize (NEq a b) = 1" + "linaformsize (NEG p) = 2 + linaformsize p" + "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q" + "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q" + + +consts aform :: "nat list => aform => bool" +primrec + "aform vs T = True" + "aform vs F = False" + "aform vs (Lt a b) = (Inum vs a < Inum vs b)" + "aform vs (Eq a b) = (Inum vs a = Inum vs b)" + "aform vs (Ge a b) = (Inum vs a \ Inum vs b)" + "aform vs (NEq a b) = (Inum vs a \ Inum vs b)" + "aform vs (NEG p) = (\ (aform vs p))" + "aform vs (Conj p q) = (aform vs p \ aform vs q)" + "aform vs (Disj p q) = (aform vs p \ aform vs q)" + + (* Let's reify and do reflection .. *) +lemma "(3::nat)*x + t < 0 \ (2 * x + y \ 17)" +apply (reify Inum_eqs' aform.simps) +oops + +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")) +oops + + (* We now define a simple transformation on aform: NNF + linum on atoms *) +consts linaform:: "aform \ aform" +recdef linaform "measure linaformsize" + "linaform (Lt s t) = Lt (linum s) (linum t)" + "linaform (Eq s t) = Eq (linum s) (linum t)" + "linaform (Ge s t) = Ge (linum s) (linum t)" + "linaform (NEq s t) = NEq (linum s) (linum t)" + "linaform (Conj p q) = Conj (linaform p) (linaform q)" + "linaform (Disj p q) = Disj (linaform p) (linaform q)" + "linaform (NEG T) = F" + "linaform (NEG F) = T" + "linaform (NEG (Lt a b)) = Ge a b" + "linaform (NEG (Ge a b)) = Lt a b" + "linaform (NEG (Eq a b)) = NEq a b" + "linaform (NEG (NEq a b)) = Eq a b" + "linaform (NEG (NEG p)) = linaform p" + "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))" + "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))" + "linaform p = p" + +lemma linaform: "aform vs (linaform p) = aform vs p" + 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) (* ("Suc 0 + Suc 0< 0")) *) +oops + + (* etc etc \*) + + +end diff -r 0e0ea63fe768 -r a8761e8568de src/HOL/ex/reflection.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/reflection.ML Thu Aug 03 15:03:05 2006 +0200 @@ -0,0 +1,172 @@ +(* + ID: $Id$ + 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 -> term option -> int -> tactic +end; + +structure Reflection : REFLECTION += struct + + (* 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 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); + + (* 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 *) + + fun decomp_genreif thy da ((vns,cong)::congs) t = + ((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, FWD (instantiate ([], 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; + +exception REIF of string; + + (* looks for the atoms equation and instantiates it with the right number *) +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; + + (* Generic reification procedure: *) + (* creates all needed cong rules and then just uses the theorem synthesis *) +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 _ = (env := []) + val da = mk_decompatom thy eqs + val [th] = Variable.export ctxt' ctxt + [divide_and_conquer (decomp_genreif thy da congs) t] + val cv' = cterm_of (ProofContext.theory_of ctxt) + (HOLogic.mk_list I (body_type fT) (!env)) + val _ = (env := []) + 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; + +fun genreflect ctxt corr_thm raw_eqs t = + let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym] + val ft = (snd o Thm.dest_comb o snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) th + val rth = normalization_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 reflection_tac ctxt (corr_thm::raw_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 = (genreflect ctxt corr_thm raw_eqs t) RS ssubst + in rtac th i st end); + +end