Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Simps_Case_Conv_Examples.thy Sprache: Isabelle

Original von: Isabelle^©

theory Simps_Case_Conv_Examples imports
  "HOL-Library.Simps_Case_Conv"
begin

section \<open>Tests for the Simps<->Case conversion tools\<close>

fun foo where
  "foo (x # xs) Nil = 0" |
  "foo (x # xs) (y # ys) = foo [] []" |
  "foo Nil (y # ys) = 1" |
  "foo Nil Nil = 3"

fun bar where
  "bar x 0 y = 0 + x" |
  "bar x (Suc n) y = n + x"

definition
  split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
where
"split_rule_test x f = f (case x of Inl af \ af 1
    | Inr (b, None) => inv f 0
    | Inr (b, Some g) => g b)"

definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)"

definition nosplit where "nosplit x = x @ (case x of [] \ [1] | xs \ xs)"

text \<open>Function with complete, non-overlapping patterns\<close>
case_of_simps foo_cases1: foo.simps
lemma
  fixes xs :: "'a list" and ys :: "'b list"
  shows "foo xs ys =
   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
  by (fact foo_cases1)

text \<open>Redundant equations are ignored\<close>
case_of_simps foo_cases2: foo.simps foo.simps
lemma
  fixes xs :: "'a list" and ys :: "'b list"
  shows "foo xs ys =
   (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
    | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
  by (fact foo_cases2)

text \<open>Variable patterns\<close>
case_of_simps bar_cases: bar.simps
lemma "bar x n y = (case n of 0 \ 0 + x | Suc n' \ n' + x)" by(fact bar_cases)

text \<open>Case expression not at top level\<close>
simps_of_case split_rule_test_simps: split_rule_test_def
lemma
  "split_rule_test (Inl x) f = f (x 1)"
  "split_rule_test (Inr (x, None)) f = f (inv f 0)"
  "split_rule_test (Inr (x, Some y)) f = f (y x)"
  by (fact split_rule_test_simps)+

text \<open>Argument occurs both as case parameter and seperately\<close>
simps_of_case nosplit_simps1: nosplit_def
lemma
  "nosplit [] = [] @ [1]"
  "nosplit (x # xs) = (x # xs) @ x # xs"
  by (fact nosplit_simps1)+

text \<open>Nested case expressions\<close>
simps_of_case test_simps1: test_def
lemma
  "test None [] = 1"
  "test None (x # xs) = 2"
  "test (Some x) y = x"
  by (fact test_simps1)+

text \<open>Single-constructor patterns\<close>
case_of_simps fst_conv_simps: fst_conv
lemma "fst x = (case x of (a,b) \ a)"
  by (fact fst_conv_simps)

text \<open>Partial split of case\<close>
simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
lemma
  "nosplit [] = [] @ [1]"
  "nosplit (x # xs) = (x # xs) @ x # xs"
  by (fact nosplit_simps1)+

simps_of_case test_simps2: test_def (splits: option.split)
lemma
  "test None y = (case y of [] \ 1 | x # xs \ 2)"
  "test (Some x) y = x"
  by (fact test_simps2)+

text \<open>Reversal\<close>
case_of_simps test_def1: test_simps1
lemma
  "test x y =
   (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
    | Some x' \ x')"
  by (fact test_def1)

text \<open>Case expressions on RHS\<close>
case_of_simps test_def2: test_simps2
lemma "test x y =
  (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
   | Some x' \ x')"
  by (fact test_def2)

text \<open>Partial split of simps\<close>
case_of_simps foo_cons_def: foo.simps(1,2)
lemma
  fixes xs :: "'a list" and ys :: "'b list"
  shows "foo (x # xs) ys = (case ys of [] \ 0 | _ # _ \ foo ([] :: 'a list) ([] :: 'b list))"
  by (fact foo_cons_def)

end

¤ Dauer der Verarbeitung: 0.16 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.