1(* Title: HOL/Tools/reification.ML 2 Author: Amine Chaieb, TU Muenchen 3 4A trial for automatical reification. 5*) 6 7signature REIFICATION = 8sig 9 val conv: Proof.context -> thm list -> conv 10 val tac: Proof.context -> thm list -> term option -> int -> tactic 11 val lift_conv: Proof.context -> conv -> term option -> int -> tactic 12 val dereify: Proof.context -> thm list -> conv 13end; 14 15structure Reification : REIFICATION = 16struct 17 18fun dest_listT (Type (\<^type_name>\<open>list\<close>, [T])) = T; 19 20val FWD = curry (op OF); 21 22fun rewrite_with ctxt eqs = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps eqs); 23 24val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp} 25 26fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn {context = ctxt', concl, ...} => 27 let 28 val ct = 29 (case some_t of 30 NONE => Thm.dest_arg concl 31 | SOME t => Thm.cterm_of ctxt' t) 32 val thm = conv ct; 33 in 34 if Thm.is_reflexive thm then no_tac 35 else ALLGOALS (resolve_tac ctxt [pure_subst OF [thm]]) 36 end) ctxt; 37 38(* Make a congruence rule out of a defining equation for the interpretation 39 40 th is one defining equation of f, 41 i.e. th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" 42 Cp is a constructor pattern and P is a pattern 43 44 The result is: 45 [|?A1 = f ?t1 ; .. ; ?An= f ?tn |] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) 46 + the a list of names of the A1 .. An, Those are fresh in the ctxt *) 47 48fun mk_congeq ctxt fs th = 49 let 50 val Const (fN, _) = th |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq 51 |> fst |> strip_comb |> fst; 52 val ((_, [th']), ctxt') = Variable.import true [th] ctxt; 53 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')); 54 fun add_fterms (t as t1 $ t2) = 55 if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs 56 then insert (op aconv) t 57 else add_fterms t1 #> add_fterms t2 58 | add_fterms (t as Abs _) = 59 if exists_Const (fn (c, _) => c = fN) t 60 then K [t] 61 else K [] 62 | add_fterms _ = I; 63 val fterms = add_fterms rhs []; 64 val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'; 65 val tys = map fastype_of fterms; 66 val vs = map Free (xs ~~ tys); 67 val env = fterms ~~ vs; (*FIXME*) 68 fun replace_fterms (t as t1 $ t2) = 69 (case AList.lookup (op aconv) env t of 70 SOME v => v 71 | NONE => replace_fterms t1 $ replace_fterms t2) 72 | replace_fterms t = 73 (case AList.lookup (op aconv) env t of 74 SOME v => v 75 | NONE => t); 76 fun mk_def (Abs (x, xT, t), v) = 77 HOLogic.mk_Trueprop (HOLogic.all_const xT $ Abs (x, xT, HOLogic.mk_eq (v $ Bound 0, t))) 78 | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)); 79 fun tryext x = 80 (x RS @{lemma "(\<forall>x. f x = g x) \<Longrightarrow> f = g" by blast} handle THM _ => x); 81 val cong = 82 (Goal.prove ctxt'' [] (map mk_def env) 83 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) 84 (fn {context, prems, ...} => 85 Local_Defs.unfold0_tac context (map tryext prems) THEN resolve_tac ctxt'' [th'] 1)) RS sym; 86 val (cong' :: vars') = 87 Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Thm.cterm_of ctxt'') vs); 88 val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars'; 89 90 in (vs', cong') end; 91 92(* congs is a list of pairs (P,th) where th is a theorem for 93 [| f p1 = A1; ...; f pn = An|] ==> f (C p1 .. pn) = P *) 94 95fun rearrange congs = 96 let 97 fun P (_, th) = 98 let val \<^term>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ l $ _) = Thm.concl_of th 99 in can dest_Var l end; 100 val (yes, no) = List.partition P congs; 101 in no @ yes end; 102 103fun dereify ctxt eqs = 104 rewrite_with ctxt (eqs @ @{thms nth_Cons_0 nth_Cons_Suc}); 105 106fun index_of t bds = 107 let 108 val tt = HOLogic.listT (fastype_of t); 109 in 110 (case AList.lookup Type.could_unify bds tt of 111 NONE => error "index_of: type not found in environements!" 112 | SOME (tbs, tats) => 113 let 114 val i = find_index (fn t' => t' = t) tats; 115 val j = find_index (fn t' => t' = t) tbs; 116 in 117 if j = ~1 then 118 if i = ~1 119 then (length tbs + length tats, AList.update Type.could_unify (tt, (tbs, tats @ [t])) bds) 120 else (i, bds) 121 else (j, bds) 122 end) 123 end; 124 125(* Generic decomp for reification : matches the actual term with the 126 rhs of one cong rule. The result of the matching guides the 127 proof synthesis: The matches of the introduced Variables A1 .. An are 128 processed recursively 129 The rest is instantiated in the cong rule,i.e. no reification is needed *) 130 131(* da is the decomposition for atoms, ie. it returns ([],g) where g 132 returns the right instance f (AtC n) = t , where AtC is the Atoms 133 constructor and n is the number of the atom corresponding to t *) 134fun decomp_reify da cgns (ct, ctxt) bds = 135 let 136 val thy = Proof_Context.theory_of ctxt; 137 fun tryabsdecomp (ct, ctxt) bds = 138 (case Thm.term_of ct of 139 Abs (_, xT, ta) => 140 let 141 val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt; 142 val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta); (* FIXME !? *) 143 val x = Free (xn, xT); 144 val cx = Thm.cterm_of ctxt' x; 145 val cta = Thm.cterm_of ctxt' ta; 146 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of 147 NONE => error "tryabsdecomp: Type not found in the Environement" 148 | SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT, 149 (x :: bsT, atsT)) bds); 150 in (([(cta, ctxt')], 151 fn ([th], bds) => 152 (hd (Variable.export ctxt' ctxt [(Thm.forall_intr cx th) COMP allI]), 153 let 154 val (bsT, asT) = the (AList.lookup Type.could_unify bds (HOLogic.listT xT)); 155 in 156 AList.update Type.could_unify (HOLogic.listT xT, (tl bsT, asT)) bds 157 end)), 158 bds) 159 end 160 | _ => da (ct, ctxt) bds) 161 in 162 (case cgns of 163 [] => tryabsdecomp (ct, ctxt) bds 164 | ((vns, cong) :: congs) => 165 (let 166 val (tyenv, tmenv) = 167 Pattern.match thy 168 ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (Thm.concl_of cong), Thm.term_of ct) 169 (Vartab.empty, Vartab.empty); 170 val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv); 171 val (fts, its) = 172 (map (snd o snd) fnvs, 173 map (fn ((vn, vi), (tT, t)) => (((vn, vi), tT), Thm.cterm_of ctxt t)) invs); 174 val ctyenv = 175 map (fn ((vn, vi), (s, ty)) => (((vn, vi), s), Thm.ctyp_of ctxt ty)) 176 (Vartab.dest tyenv); 177 in 178 ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt, 179 apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds) 180 end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds)) 181 end; 182 183fun get_nths (t as (Const (\<^const_name>\<open>List.nth\<close>, _) $ vs $ n)) = 184 AList.update (op aconv) (t, (vs, n)) 185 | get_nths (t1 $ t2) = get_nths t1 #> get_nths t2 186 | get_nths (Abs (_, _, t')) = get_nths t' 187 | get_nths _ = I; 188 189fun tryeqs [] (ct, ctxt) bds = error "Cannot find the atoms equation" 190 | tryeqs (eq :: eqs) (ct, ctxt) bds = (( 191 let 192 val rhs = eq |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd; 193 val nths = get_nths rhs []; 194 val (vss, _) = fold_rev (fn (_, (vs, n)) => fn (vss, ns) => 195 (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([], []); 196 val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt; 197 val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt'; 198 val thy = Proof_Context.theory_of ctxt''; 199 val vsns_map = vss ~~ vsns; 200 val xns_map = fst (split_list nths) ~~ xns; 201 val subst = map (fn (nt, xn) => (nt, Var ((xn, 0), fastype_of nt))) xns_map; 202 val rhs_P = subst_free subst rhs; 203 val (tyenv, tmenv) = Pattern.match thy (rhs_P, Thm.term_of ct) (Vartab.empty, Vartab.empty); 204 val sbst = Envir.subst_term (tyenv, tmenv); 205 val sbsT = Envir.subst_type tyenv; 206 val subst_ty = 207 map (fn (n, (s, t)) => ((n, s), Thm.ctyp_of ctxt'' t)) (Vartab.dest tyenv) 208 val tml = Vartab.dest tmenv; 209 val (subst_ns, bds) = fold_map 210 (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds => 211 let 212 val name = snd (the (AList.lookup (op =) tml xn0)); 213 val (idx, bds) = index_of name bds; 214 in (apply2 (Thm.cterm_of ctxt'') (n, idx |> HOLogic.mk_nat), bds) end) subst bds; 215 val subst_vs = 216 let 217 fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) = 218 let 219 val cns = sbst (Const (\<^const_name>\<open>List.Cons\<close>, T --> lT --> lT)); 220 val lT' = sbsT lT; 221 val (bsT, _) = the (AList.lookup Type.could_unify bds lT); 222 val vsn = the (AList.lookup (op =) vsns_map vs); 223 val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT')); 224 in apply2 (Thm.cterm_of ctxt'') (vs, vs') end; 225 in map h subst end; 226 val cts = 227 map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt'') (Var ((vn, vi), tT), t)) 228 (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b)) 229 (map (fn n => (n, 0)) xns) tml); 230 val substt = 231 let 232 val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); 233 in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; 234 val th = 235 (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq) 236 RS sym; 237 in (hd (Variable.export ctxt'' ctxt [th]), bds) end) 238 handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); 239 240(* looks for the atoms equation and instantiates it with the right number *) 241 242fun mk_decompatom eqs (ct, ctxt) bds = (([], fn (_, bds) => 243 let 244 val tT = fastype_of (Thm.term_of ct); 245 fun isat eq = 246 let 247 val rhs = eq |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd; 248 in exists_Const 249 (fn (n, ty) => n = \<^const_name>\<open>List.nth\<close> 250 andalso AList.defined Type.could_unify bds (domain_type ty)) rhs 251 andalso Type.could_unify (fastype_of rhs, tT) 252 end; 253 in tryeqs (filter isat eqs) (ct, ctxt) bds end), bds); 254 255(* Generic reification procedure: *) 256(* creates all needed cong rules and then just uses the theorem synthesis *) 257 258fun mk_congs ctxt eqs = 259 let 260 val fs = fold_rev (fn eq => insert (op =) (eq |> Thm.prop_of |> HOLogic.dest_Trueprop 261 |> HOLogic.dest_eq |> fst |> strip_comb 262 |> fst)) eqs []; 263 val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs []; 264 val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt; 265 val subst = 266 the o AList.lookup (op =) 267 (map2 (fn T => fn v => (T, Thm.cterm_of ctxt' (Free (v, T)))) tys vs); 268 fun prep_eq eq = 269 let 270 val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop 271 |> HOLogic.dest_eq |> fst |> strip_comb; 272 val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs; 273 in Thm.instantiate ([], subst) eq end; 274 val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs; 275 val bds = AList.make (K ([], [])) tys; 276 in (ps ~~ Variable.export ctxt' ctxt congs, bds) end 277 278fun conv ctxt eqs ct = 279 let 280 val (congs, bds) = mk_congs ctxt eqs; 281 val congs = rearrange congs; 282 val (th, bds') = 283 apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds); 284 fun is_list_var (Var (_, t)) = can dest_listT t 285 | is_list_var _ = false; 286 val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd 287 |> strip_comb |> snd |> filter is_list_var; 288 val vs = map (fn Var (v as (_, T)) => 289 (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; 290 val th' = 291 Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th; 292 val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); 293 in Thm.transitive th'' th' end; 294 295fun tac ctxt eqs = 296 lift_conv ctxt (conv ctxt eqs); 297 298end; 299