Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Elimination.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      CTT/ex/Elimination.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Some examples taken from P. Martin-L\"of, Intuitionistic type theory
(Bibliopolis, 1984).
*)

section "Examples with elimination rules"

theory Elimination
imports "../CTT"
begin

text "This finds the functions fst and snd!"

schematic_goal [folded basic_defs]: "A type \ ?a : (A \ A) \ A"
apply pc
done

schematic_goal [folded basic_defs]: "A type \ ?a : (A \ A) \ A"
apply pc
back
done

text "Double negation of the Excluded Middle"
schematic_goal "A type \ ?a : ((A + (A\F)) \ F) \ F"
apply intr
apply (rule ProdE)
apply assumption
apply pc
done

schematic_goal "\A type; B type\ \ ?a : (A \ B) \ (B \ A)"
apply pc
done
(*The sequent version (ITT) could produce an interesting alternative
  by backtracking.  No longer.*)

text "Binary sums and products"
schematic_goal "\A type; B type; C type\ \ ?a : (A + B \ C) \ (A \ C) \ (B \ C)"
apply pc
done

(*A distributive law*)
schematic_goal "\A type; B type; C type\ \ ?a : A \ (B + C) \ (A \ B + A \ C)"
apply pc
done

(*more general version, same proof*)
schematic_goal
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\x. x:A \ C(x) type"
  shows "?a : (\x:A. B(x) + C(x)) \ (\x:A. B(x)) + (\x:A. C(x))"
apply (pc assms)
done

text "Construction of the currying functional"
schematic_goal "\A type; B type; C type\ \ ?a : (A \ B \ C) \ (A \ (B \ C))"
apply pc
done

(*more general goal with same proof*)
schematic_goal
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\z. z: (\x:A. B(x)) \ C(z) type"
  shows "?a : \f: (\z : (\x:A . B(x)) . C(z)).
                      (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))"
apply (pc assms)
done

text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
schematic_goal "\A type; B type; C type\ \ ?a : (A \ (B \ C)) \ (A \ B \ C)"
apply pc
done

(*more general goal with same proof*)
schematic_goal
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\z. z: (\x:A . B(x)) \ C(z) type"
  shows "?a : (\x:A . \y:B(x) . C())
        \<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
apply (pc assms)
done

text "Function application"
schematic_goal "\A type; B type\ \ ?a : ((A \ B) \ A) \ B"
apply pc
done

text "Basic test of quantifier reasoning"
schematic_goal
  assumes "A type"
    and "B type"
    and "\x y. \x:A; y:B\ \ C(x,y) type"
  shows
    "?a : (\y:B . \x:A . C(x,y))
          \<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"
apply (pc assms)
done

text "Martin-Löf (1984) pages 36-7: the combinator S"
schematic_goal
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\x y. \x:A; y:B(x)\ \ C(x,y) type"
  shows "?a : (\x:A. \y:B(x). C(x,y))
             \<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
apply (pc assms)
done

text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
schematic_goal
  assumes "A type"
    and "B type"
    and "\z. z: A+B \ C(z) type"
  shows "?a : (\x:A. C(inl(x))) \ (\y:B. C(inr(y)))
          \<longrightarrow> (\<Prod>z: A+B. C(z))"
apply (pc assms)
done

(*towards AXIOM OF CHOICE*)
schematic_goal [folded basic_defs]:
  "\A type; B type; C type\ \ ?a : (A \ B \ C) \ (A \ B) \ (A \ C)"
apply pc
done

(*Martin-Löf (1984) page 50*)
text "AXIOM OF CHOICE! Delicate use of elimination rules"
schematic_goal
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\x y. \x:A; y:B(x)\ \ C(x,y) type"
  shows "?a : (\x:A. \y:B(x). C(x,y)) \ (\f: (\x:A. B(x)). \x:A. C(x, f`x))"
apply (intr assms)
prefer 2 apply add_mp
prefer 2 apply add_mp
apply (erule SumE_fst)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (rule_tac [4] SumE_snd)
apply (typechk SumE_fst assms)
done

text "Axiom of choice. Proof without fst, snd. Harder still!"
schematic_goal [folded basic_defs]:
  assumes "A type"
    and "\x. x:A \ B(x) type"
    and "\x y. \x:A; y:B(x)\ \ C(x,y) type"
  shows "?a : (\x:A. \y:B(x). C(x,y)) \ (\f: (\x:A. B(x)). \x:A. C(x, f`x))"
apply (intr assms)
(*Must not use add_mp as subst_prodE hides the construction.*)
apply (rule ProdE [THEN SumE])
apply assumption
apply assumption
apply assumption
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (erule_tac [4] ProdE [THEN SumE])
apply (typechk assms)
apply (rule replace_type)
apply (rule subst_eqtyparg)
apply (rule comp_rls)
apply (typechk assms)
apply assumption
done

text "Example of sequent-style deduction"
(*When splitting z:A \<times> B, the assumption C(z) is affected;  ?a becomes
    \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w)     *)
schematic_goal
  assumes "A type"
    and "B type"
    and "\z. z:A \ B \ C(z) type"
  shows "?a : (\z:A \ B. C(z)) \ (\u:A. \v:B. C())"
apply (rule intr_rls)
apply (tactic \<open>biresolve_tac \<^context> safe_brls 2\<close>)
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
apply (rule_tac [2] a = "y" in ProdE)
apply (typechk assms)
apply (rule SumE, assumption)
apply intr
defer 1
apply assumption+
apply (typechk assms)
done

end

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