Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Rewrite_Examples.thy   Sprache: Isabelle

Original von: Isabelle©

theory Rewrite_Examples
imports Main "HOL-Library.Rewrite"
begin

section \<open>The rewrite Proof Method by Example\<close>

(* This file is intended to give an overview over
   the features of the pattern-based rewrite proof method.

   See also https://www21.in.tum.de/~noschinl/Pattern-2014/
*)

lemma
  fixes a::int and b::int and c::int
  assumes "P (b + a)"
  shows "P (a + b)"
by (rewrite at "a + b" add.commute)
   (rule assms)

(* Selecting a specific subterm in a large, ambiguous term. *)
lemma
  fixes a b c :: int
  assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c"
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
  by (rewrite in "f _ + f \ = _" diff_self) fact

lemma
  fixes a b c :: int
  assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
  by (rewrite at "f (_ + \) + f _ = _" diff_self) fact

lemma
  fixes a b c :: int
  assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c"
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
  by (rewrite in "f (\ + _) + _ = _" diff_self) fact

lemma
  fixes a b c :: int
  assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c"
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
  by (rewrite in "f (_ + \) + _ = _" diff_self) fact

lemma
  fixes x y :: nat
  shows"x + y > c \ y + x > c"
  by (rewrite at "\ > c" add.commute) assumption

(* We can also rewrite in the assumptions.  *)
lemma
  fixes x y :: nat
  assumes "y + x > c \ y + x > c"
  shows   "x + y > c \ y + x > c"
  by (rewrite in asm add.commute) fact

lemma
  fixes x y :: nat
  assumes "y + x > c \ y + x > c"
  shows   "x + y > c \ y + x > c"
  by (rewrite in "x + y > c" at asm add.commute) fact

lemma
  fixes x y :: nat
  assumes "y + x > c \ y + x > c"
  shows   "x + y > c \ y + x > c"
  by (rewrite at "\ > c" at asm add.commute) fact

lemma
  assumes "P {x::int. y + 1 = 1 + x}"
  shows   "P {x::int. y + 1 = x + 1}"
  by (rewrite at "x+1" in "{x::int. \ }" add.commute) fact

lemma
  assumes "P {x::int. y + 1 = 1 + x}"
  shows   "P {x::int. y + 1 = x + 1}"
  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \ }" add.commute)
   fact

lemma
  assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. s * t + y - 3)}"
  shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\s t. y + s * t - 3)}"
  by (rewrite at "b + d * e" in "\(a, b, c). _ = Q (\d e. \)" add.commute) fact

(* This is not limited to the first assumption *)
lemma
  assumes "PROP P \ PROP Q"
  shows "PROP R \ PROP P \ PROP Q"
    by (rewrite at asm assms)

lemma
  assumes "PROP P \ PROP Q"
  shows "PROP R \ PROP R \ PROP P \ PROP Q"
    by (rewrite at asm assms)

(* Rewriting "at asm" selects each full assumption, not any parts *)
lemma
  assumes "(PROP P \ PROP Q) \ (PROP S \ PROP R)"
  shows "PROP S \ (PROP P \ PROP Q) \ PROP R"
  apply (rewrite at asm assms)
  apply assumption
  done



(* Rewriting with conditional rewriting rules works just as well. *)
lemma test_theorem:
  fixes x :: nat
  shows "x \ y \ x \ y \ x = y"
  by (rule Orderings.order_antisym)

(* Premises of the conditional rule yield new subgoals. The
   assumptions of the goal are propagated into these subgoals
*)

lemma
  fixes f :: "nat \ nat"
  shows "f x \ 0 \ f x \ 0 \ f x = 0"
  apply (rewrite at "f x" to "0" test_theorem)
  apply assumption
  apply assumption
  apply (rule refl)
  done

(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
lemma
  assumes rewr: "PROP P \ PROP Q \ PROP R \ PROP R'"
  assumes A1: "PROP S \ PROP T \ PROP U \ PROP P"
  assumes A2: "PROP S \ PROP T \ PROP U \ PROP Q"
  assumes C: "PROP S \ PROP R' \ PROP T \ PROP U \ PROP V"
  shows "PROP S \ PROP R \ PROP T \ PROP U \ PROP V"
  apply (rewrite at asm rewr)
  apply (fact A1)
  apply (fact A2)
  apply (fact C)
  done


(*
   Instantiation.

   Since all rewriting is now done via conversions,
   instantiation becomes fairly easy to do.
*)


(* We first introduce a function f and an extended
   version of f that is annotated with an invariant. *)

fun f :: "nat \ nat" where "f n = n"
definition "f_inv (I :: nat \ bool) n \ f n"

lemma annotate_f: "f = f_inv I"
  by (simp add: f_inv_def fun_eq_iff)

(* We have a lemma with a bound variable n, and
   want to add an invariant to f. *)

lemma
  assumes "P (\n. f_inv (\_. True) n + 1) = x"
  shows "P (\n. f n + 1) = x"
  by (rewrite to "f_inv (\_. True)" annotate_f) fact

(* We can also add an invariant that contains the variable n bound in the outer context.
   For this, we need to bind this variable to an identifier. *)

lemma
  assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x"
  shows "P (\n. f n + 1) = x"
  by (rewrite in "\n. \" to "f_inv (\x. n < x + 1)" annotate_f) fact

(* Any identifier will work *)
lemma
  assumes "P (\n. f_inv (\x. n < x + 1) n + 1) = x"
  shows "P (\n. f n + 1) = x"
  by (rewrite in "\abc. \" to "f_inv (\x. abc < x + 1)" annotate_f) fact

(* The "for" keyword. *)
lemma
  assumes "P (2 + 1)"
  shows "\x y. P (1 + 2 :: nat)"
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact

lemma
  assumes "\x y. P (y + x)"
  shows "\x y. P (x + y :: nat)"
by (rewrite in "P (x + _)" at for (x y) add.commute) fact

lemma
  assumes "\x y z. y + x + z = z + y + (x::int)"
  shows   "\x y z. x + y + z = z + y + (x::int)"
by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact

lemma
  assumes "\x y z. z + (x + y) = z + y + (x::int)"
  shows   "\x y z. x + y + z = z + y + (x::int)"
by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact

lemma
  assumes "\x y z. x + y + z = y + z + (x::int)"
  shows   "\x y z. x + y + z = z + y + (x::int)"
by (rewrite at "\ + _" at "_ = \" in for () add.commute) fact

lemma
  assumes eq: "\x. P x \ g x = x"
  assumes f1: "\x. Q x \ P x"
  assumes f2: "\x. Q x \ x"
  shows "\x. Q x \ g x"
  apply (rewrite at "g x" in for (x) eq)
  apply (fact f1)
  apply (fact f2)
  done

(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
lemma
  assumes "(\(x::int). x < 1 + x)"
  and     "(x::int) + 1 > x"
  shows   "(\(x::int). x + 1 > x) \ (x::int) + 1 > x"
by (rewrite at "x + 1" in for (x) at asm add.commute)
   (rule assms)

(* The rewrite method also has an ML interface *)
lemma
  assumes "\a b. P ((a + 1) * (1 + b)) "
  shows "\a b :: nat. P ((a + 1) * (b + 1))"
  apply (tactic \<open>
    let
      val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
      (* Note that the pattern order is reversed *)
      val pat = [
        Rewrite.For [(x, SOME \<^typ>\<open>nat\<close>)],
        Rewrite.In,
        Rewrite.Term (@{const plus(nat)} $ Free (x, \<^typ>\<open>nat\<close>) $ \<^term>\<open>1 :: nat\<close>, [])]
      val to = NONE
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
  \<close>)
  apply (fact assms)
  done

lemma
  assumes "Q (\b :: int. P (\a. a + b) (\a. a + b))"
  shows "Q (\b :: int. P (\a. a + b) (\a. b + a))"
  apply (tactic \<open>
    let
      val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
      val pat = [
        Rewrite.Concl,
        Rewrite.In,
        Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
          $ Abs ("x"\<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
        Rewrite.In,
        Rewrite.Term (@{const plus(int)} $ Free (x, \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
        ]
      val to = NONE
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
  \<close>)
  apply (fact assms)
  done

(* There is also conversion-like rewrite function: *)
ML \<open>
  val ct = \<^cprop>\<open>Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))\<close>
  val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
  val pat = [
    Rewrite.Concl,
    Rewrite.In,
    Rewrite.Term (Free ("Q", (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) --> \<^typ>\<open>bool\<close>)
      $ Abs ("x"\<^typ>\<open>int\<close>, Rewrite.mk_hole 1 (\<^typ>\<open>int\<close> --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>\<open>int\<close>)]),
    Rewrite.In,
    Rewrite.Term (@{const plus(int)} $ Free (x, \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
    ]
  val to = NONE
  val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
\<close>

section \<open>Regression tests\<close>

ML \<open>
  val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>
  val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
  val pat = [
    Rewrite.In,
    Rewrite.Term (@{const plus(int)} $ Var (("c", 0), \<^typ>\<open>int\<close>) $ Var (("c", 0), \<^typ>\<open>int\<close>), [])
    ]
  val to = NONE
  val _ =
    case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of
      NONE => ()
    | _ => error "should not have matched anything"
\<close>

ML \<open>
  Rewrite.params_pconv (Conv.all_conv |> K |> K) \<^context> (Vartab.empty, []) \<^cterm>\<open>\<And>x. PROP A\<close>
\<close>

lemma
  assumes eq: "PROP A \ PROP B \ PROP C"
  assumes f1: "PROP D \ PROP A"
  assumes f2: "PROP D \ PROP C"
  shows "\x. PROP D \ PROP B"
  apply (rewrite eq)
  apply (fact f1)
  apply (fact f2)
  done

end

¤ Dauer der Verarbeitung: 0.2 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik