src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43298 82d4874757df
parent 43297 e77baf329f48
child 43300 854f667df3d6
equal deleted inserted replaced
43297:e77baf329f48 43298:82d4874757df
    13 
    13 
    14   val hol_clause_from_metis :
    14   val hol_clause_from_metis :
    15     Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
    15     Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
    16     -> term
    16     -> term
    17   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    17   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    18   val untyped_aconv : term * term -> bool
    18   val metis_aconv_untyped : term * term -> bool
    19   val replay_one_inference :
    19   val replay_one_inference :
    20     Proof.context -> (string * term) list -> int Symtab.table
    20     Proof.context -> (string * term) list -> int Symtab.table
    21     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    21     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    22     -> (Metis_Thm.thm * thm) list
    22     -> (Metis_Thm.thm * thm) list
    23   val discharge_skolem_premises :
    23   val discharge_skolem_premises :
   226 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
   226 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
   227   | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   227   | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   228   | simp_not_not t = t
   228   | simp_not_not t = t
   229 
   229 
   230 (* Match untyped terms. *)
   230 (* Match untyped terms. *)
   231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
   231 fun metis_aconv_untyped (Const (a, _), Const(b, _)) = (a = b)
   232   | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
   232   | metis_aconv_untyped (Free (a, _), Free (b, _)) = (a = b)
   233   | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) =
   233   | metis_aconv_untyped (Var ((a, _), _), Var ((b, _), _)) =
   234     (a = b) (* ignore variable numbers *)
   234     a = b (* ignore variable numbers *)
   235   | untyped_aconv (Bound i, Bound j) = (i = j)
   235   | metis_aconv_untyped (Bound i, Bound j) = (i = j)
   236   | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
   236   | metis_aconv_untyped (Abs (_, _, t), Abs (_, _, u)) =
   237   | untyped_aconv (t1 $ t2, u1 $ u2) =
   237     metis_aconv_untyped (t, u)
   238     untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
   238   | metis_aconv_untyped (t1 $ t2, u1 $ u2) =
   239   | untyped_aconv _ = false
   239     metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
       
   240   | metis_aconv_untyped _ = false
   240 
   241 
   241 val normalize_literal = simp_not_not o Envir.eta_contract
   242 val normalize_literal = simp_not_not o Envir.eta_contract
   242 
   243 
   243 (* Find the relative location of an untyped term within a list of terms as a
   244 (* Find the relative location of an untyped term within a list of terms as a
   244    1-based index. Returns 0 in case of failure. *)
   245    1-based index. Returns 0 in case of failure. *)
   245 fun index_of_literal lit haystack =
   246 fun index_of_literal lit haystack =
   246   let
   247   let
   247     fun match_lit normalize =
   248     fun match_lit normalize =
   248       HOLogic.dest_Trueprop #> normalize
   249       HOLogic.dest_Trueprop #> normalize
   249       #> curry untyped_aconv (lit |> normalize)
   250       #> curry metis_aconv_untyped (lit |> normalize)
   250   in
   251   in
   251     (case find_index (match_lit I) haystack of
   252     (case find_index (match_lit I) haystack of
   252        ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
   253        ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
   253      | j => j) + 1
   254      | j => j) + 1
   254   end
   255   end
   449       th
   450       th
   450     else
   451     else
   451       let
   452       let
   452         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
   453         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
   453         val prems = prems0 |> map normalize_literal
   454         val prems = prems0 |> map normalize_literal
   454                            |> distinct untyped_aconv
   455                            |> distinct metis_aconv_untyped
   455         val goal = Logic.list_implies (prems, concl)
   456         val goal = Logic.list_implies (prems, concl)
   456         val tac = cut_rules_tac [th] 1
   457         val tac = cut_rules_tac [th] 1
   457                   THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
   458                   THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
   458                   THEN ALLGOALS assume_tac
   459                   THEN ALLGOALS assume_tac
   459       in
   460       in
   499   let
   500   let
   500     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   501     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   501     val prem = goal |> Logic.strip_assums_hyp |> hd
   502     val prem = goal |> Logic.strip_assums_hyp |> hd
   502     val concl = goal |> Logic.strip_assums_concl
   503     val concl = goal |> Logic.strip_assums_concl
   503     fun pair_untyped_aconv (t1, t2) (u1, u2) =
   504     fun pair_untyped_aconv (t1, t2) (u1, u2) =
   504       untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
   505       metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2)
   505     fun add_terms tp inst =
   506     fun add_terms tp inst =
   506       if exists (pair_untyped_aconv tp) inst then inst
   507       if exists (pair_untyped_aconv tp) inst then inst
   507       else tp :: map (apsnd (subst_atomic [tp])) inst
   508       else tp :: map (apsnd (subst_atomic [tp])) inst
   508     fun is_flex t =
   509     fun is_flex t =
   509       case strip_comb t of
   510       case strip_comb t of