src/CTT/ex/Elimination.thy

 
 Some examples taken from P. Martin-Löf, Intuitionistic type theory
 (Bibliopolis, 1984).
 *)
 
-section "Examples with elimination rules"
+section \<open>Examples with elimination rules\<close>
 
 theory Elimination
 imports "../CTT"
 begin
 
-text "This finds the functions fst and snd!"
+text \<open>This finds the functions fst and snd!\<close>
 
 schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
 apply pc
 done
 
 schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
   apply pc
   back
   done
 
-text "Double negation of the Excluded Middle"
+text \<open>Double negation of the Excluded Middle\<close>
 schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
   apply intr
   apply (rule ProdE)
    apply assumption
   apply pc
   done
+
+text \<open>Experiment: the proof above in Isar\<close>
+lemma
+  assumes "A type" shows "(\<^bold>\<lambda>f. f ` inr(\<^bold>\<lambda>y. f ` inl(y))) : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
+proof intr
+  fix f
+  assume f: "f : A + (A \<longrightarrow> F) \<longrightarrow> F" 
+  with assms have "inr(\<^bold>\<lambda>y. f ` inl(y)) : A + (A \<longrightarrow> F)"
+    by pc
+  then show "f ` inr(\<^bold>\<lambda>y. f ` inl(y)) : F" 
+    by (rule ProdE [OF f])
+qed (rule assms)+
 
 schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
 apply pc
 done
 (*The sequent version (ITT) could produce an interesting alternative
   by backtracking.  No longer.*)
 
-text "Binary sums and products"
+text \<open>Binary sums and products\<close>
 schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
   apply pc
   done
 
 (*A distributive law*)

     and "\<And>x. x:A \<Longrightarrow> C(x) type"
   shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))"
   apply (pc assms)
   done
 
-text "Construction of the currying functional"
+text \<open>Construction of the currying functional\<close>
 schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
   apply pc
   done
 
 (*more general goal with same proof*)

   shows "?a : \<Prod>f: (\<Prod>z : (\<Sum>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)"
+text \<open>Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)\<close>
 schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
   apply pc
   done
 
 (*more general goal with same proof*)

   shows "?a : (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))
         \<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
   apply (pc assms)
   done
 
-text "Function application"
+text \<open>Function application\<close>
 schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
   apply pc
   done
 
-text "Basic test of quantifier reasoning"
+text \<open>Basic test of quantifier reasoning\<close>
 schematic_goal
   assumes "A type"
     and "B type"
     and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
   shows
     "?a :     (\<Sum>y:B . \<Prod>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"
+text \<open>Martin-Löf (1984) pages 36-7: the combinator S\<close>
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   shows "?a :    (\<Prod>x:A. \<Prod>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"
+text \<open>Martin-Löf (1984) page 58: the axiom of disjunction elimination\<close>
 schematic_goal
   assumes "A type"
     and "B type"
     and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
   shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))

   apply pc
   done
 
 
 (*Martin-Löf (1984) page 50*)
-text "AXIOM OF CHOICE!  Delicate use of elimination rules"
+text \<open>AXIOM OF CHOICE!  Delicate use of elimination rules\<close>
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"

     by (rule ProdC [OF \<open>a : A\<close>]) (typechk SumE_fst f)
   ultimately show "snd(f`a) : C(a, (\<^bold>\<lambda>x. fst(f ` x)) ` a)"
     by (intro replace_type [OF subst_eqtyparg]) (typechk SumE_fst assms \<open>a : A\<close>)
 qed
 
-text "Axiom of choice.  Proof without fst, snd.  Harder still!"
+text \<open>Axiom of choice.  Proof without fst, snd.  Harder still!\<close>
 schematic_goal [folded basic_defs]:
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
   shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"

     apply (rule comp_rls)
       apply (typechk assms)
   apply assumption
   done
 
-text "Example of sequent-style deduction"
+text \<open>Example of sequent-style deduction\<close>
   (*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"