src/HOL/ex/reflection.ML
changeset 23648 bccbf6138c30
parent 23643 32ee4111d1bc
child 23791 e105381d4140
equal deleted inserted replaced
23647:89286c4e7928 23648:bccbf6138c30
     5 A trial for automatical reification.
     5 A trial for automatical reification.
     6 *)
     6 *)
     7 
     7 
     8 signature REFLECTION = sig
     8 signature REFLECTION = sig
     9   val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
     9   val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
    10   val reflection_tac: Proof.context -> thm list -> term option -> int -> tactic
    10   val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
    11   val gen_reflection_tac: Proof.context -> (cterm -> thm)
    11   val gen_reflection_tac: Proof.context -> (cterm -> thm)
    12     -> thm list -> term option -> int -> tactic
    12     -> thm list -> thm list -> term option -> int -> tactic
    13 end;
    13 end;
    14 
    14 
    15 structure Reflection  : REFLECTION 
    15 structure Reflection : REFLECTION
    16 = struct
    16 = struct
    17 
    17 
    18 val ext2 = thm "ext2";
    18 val ext2 = thm "ext2";
    19 val nth_Cons_0 = thm "nth_Cons_0";
    19 val nth_Cons_0 = thm "nth_Cons_0";
    20 val nth_Cons_Suc = thm "nth_Cons_Suc";
    20 val nth_Cons_Suc = thm "nth_Cons_Suc";
   147 	val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
   147 	val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
   148     in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong))
   148     in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong))
   149     end)
   149     end)
   150       handle MATCH => decomp_genreif da congs (t,ctxt)))
   150       handle MATCH => decomp_genreif da congs (t,ctxt)))
   151   end;
   151   end;
   152           (* looks for the atoms equation and instantiates it with the right number *)
   152 
       
   153  (* looks for the atoms equation and instantiates it with the right number *)
   153 
   154 
   154 
   155 
   155 fun mk_decompatom eqs (t,ctxt) =
   156 fun mk_decompatom eqs (t,ctxt) =
   156 let 
   157 let 
   157  val tT = fastype_of t
   158  val tT = fastype_of t
   254 			     |> (insteq eq)) raw_eqs
   255 			     |> (insteq eq)) raw_eqs
   255   val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
   256   val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs)
   256 in ps ~~ (Variable.export ctxt' ctxt congs)
   257 in ps ~~ (Variable.export ctxt' ctxt congs)
   257 end
   258 end
   258 
   259 
       
   260 fun partition P [] = ([],[])
       
   261   | partition P (x::xs) = 
       
   262      let val (yes,no) = partition P xs
       
   263      in if P x then (x::yes,no) else (yes, x::no) end
       
   264 
       
   265 fun rearrange congs = 
       
   266 let 
       
   267  fun P (_, th) = 
       
   268   let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
       
   269   in can dest_Var l end
       
   270  val (yes,no) = partition P congs 
       
   271  in no @ yes end
       
   272 
       
   273 
       
   274 
   259 fun genreif ctxt raw_eqs t =
   275 fun genreif ctxt raw_eqs t =
   260  let 
   276  let 
   261   val congs = mk_congs ctxt raw_eqs 
   277   val congs = rearrange (mk_congs ctxt raw_eqs)
   262   val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt)
   278   val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt)
   263   fun is_listVar (Var (_,t)) = can dest_listT t
   279   fun is_listVar (Var (_,t)) = can dest_listT t
   264        | is_listVar _ = false
   280        | is_listVar _ = false
   265   val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
   281   val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
   266 	       |> strip_comb |> snd |> filter is_listVar
   282 	       |> strip_comb |> snd |> filter is_listVar
   272 			(fn _ => Simp_tac 1)
   288 			(fn _ => Simp_tac 1)
   273   val _ = bds := []
   289   val _ = bds := []
   274 in FWD trans [th'',th']
   290 in FWD trans [th'',th']
   275 end
   291 end
   276 
   292 
   277 fun genreflect ctxt conv corr_thm raw_eqs t =
   293 
   278     let val th = FWD trans [genreif ctxt raw_eqs t, corr_thm RS sym]
   294 fun genreflect ctxt conv corr_thms raw_eqs t =
   279         val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
   295 let 
   280         val rth = conv ft
   296   val reifth = genreif ctxt raw_eqs t
   281     in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
   297   fun trytrans [] = error "No suitable correctness theorem found"
   282                 (simplify (HOL_basic_ss addsimps [rth]) th)
   298     | trytrans (th::ths) = 
   283     end
   299          (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
       
   300   val th = trytrans corr_thms
       
   301   val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
       
   302   val rth = conv ft
       
   303 in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
       
   304            (simplify (HOL_basic_ss addsimps [rth]) th)
       
   305 end
   284 
   306 
   285 fun genreify_tac ctxt eqs to i = (fn st =>
   307 fun genreify_tac ctxt eqs to i = (fn st =>
   286   let
   308   let
   287     val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
   309     val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1))
   288     val t = (case to of NONE => P | SOME x => x)
   310     val t = (case to of NONE => P | SOME x => x)
   290   in rtac th i st
   312   in rtac th i st
   291   end);
   313   end);
   292 
   314 
   293     (* Reflection calls reification and uses the correctness *)
   315     (* Reflection calls reification and uses the correctness *)
   294         (* theorem assumed to be the dead of the list *)
   316         (* theorem assumed to be the dead of the list *)
   295 fun gen_reflection_tac ctxt conv (corr_thm :: raw_eqs) to i = (fn st =>
   317 fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
   296   let
   318   let
   297     val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
   319     val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
   298     val t = the_default P to;
   320     val t = the_default P to;
   299     val th = genreflect ctxt conv corr_thm raw_eqs t
   321     val th = genreflect ctxt conv corr_thms raw_eqs t
   300       RS ssubst;
   322       RS ssubst;
   301   in rtac th i st end);
   323   in rtac th i st end);
   302 
   324 
   303 fun reflection_tac ctxt = gen_reflection_tac ctxt NBE.normalization_conv;
   325 fun reflection_tac ctxt = gen_reflection_tac ctxt NBE.normalization_conv;
   304 end
   326 end