# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666804124 -3600
# Node ID 2510e6f7b11cc49b31a4e622773d7c33f232a1b0
# Parent  934d4aed8497a69b098fc35105e58e346f0116f7
Beautifying CTT a tiny bit

diff -r 934d4aed8497 -r 2510e6f7b11c src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Wed Oct 26 17:22:12 2022 +0100
+++ b/src/CTT/ex/Elimination.thy	Wed Oct 26 18:08:44 2022 +0100
@@ -19,17 +19,17 @@
 done
 
 schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
-apply pc
-back
-done
+  apply pc
+  back
+  done
 
 text "Double negation of the Excluded Middle"
 schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
-apply intr
-apply (rule ProdE)
-apply assumption
-apply pc
-done
+  apply intr
+  apply (rule ProdE)
+   apply assumption
+  apply pc
+  done
 
 schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
 apply pc
@@ -39,13 +39,12 @@
 
 text "Binary sums and products"
 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
+  apply pc
+  done
 
 (*A distributive law*)
 schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"
-apply pc
-done
+  by pc
 
 (*more general version, same proof*)
 schematic_goal
@@ -53,13 +52,13 @@
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     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
+  apply (pc assms)
+  done
 
 text "Construction of the currying functional"
 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
+  apply pc
+  done
 
 (*more general goal with same proof*)
 schematic_goal
@@ -68,13 +67,13 @@
     and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> C(z) type"
   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
+  apply (pc assms)
+  done
 
 text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
 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
+  apply pc
+  done
 
 (*more general goal with same proof*)
 schematic_goal
@@ -83,13 +82,13 @@
     and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"
   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
+  apply (pc assms)
+  done
 
 text "Function application"
 schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
-apply pc
-done
+  apply pc
+  done
 
 text "Basic test of quantifier reasoning"
 schematic_goal
@@ -99,8 +98,8 @@
   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
+  apply (pc assms)
+  done
 
 text "Martin-Löf (1984) pages 36-7: the combinator S"
 schematic_goal
@@ -109,8 +108,8 @@
     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
+  apply (pc assms)
+  done
 
 text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
 schematic_goal
@@ -119,14 +118,14 @@
     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)))
           \<longrightarrow> (\<Prod>z: A+B. C(z))"
-apply (pc assms)
-done
+  apply (pc assms)
+  done
 
 (*towards AXIOM OF CHOICE*)
 schematic_goal [folded basic_defs]:
   "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"
-apply pc
-done
+  apply pc
+  done
 
 
 (*Martin-Löf (1984) page 50*)
@@ -136,16 +135,16 @@
     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 (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
+  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]:
@@ -153,42 +152,42 @@
     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 (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
+  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
+  (*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 "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"
   shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"
-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
+  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
diff -r 934d4aed8497 -r 2510e6f7b11c src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Wed Oct 26 17:22:12 2022 +0100
+++ b/src/CTT/ex/Equality.thy	Wed Oct 26 18:08:44 2022 +0100
@@ -6,63 +6,62 @@
 section "Equality reasoning by rewriting"
 
 theory Equality
-imports "../CTT"
+  imports "../CTT"
 begin
 
 lemma split_eq: "p : Sum(A,B) \<Longrightarrow> split(p,pair) = p : Sum(A,B)"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+  apply (rule EqE)
+  apply (rule elim_rls, assumption)
+  apply rew
+  done
 
 lemma when_eq: "\<lbrakk>A type; B type; p : A+B\<rbrakk> \<Longrightarrow> when(p,inl,inr) = p : A + B"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+  apply (rule EqE)
+  apply (rule elim_rls, assumption)
+   apply rew
+  done
 
-(*in the "rec" formulation of addition, 0+n=n *)
+text \<open>in the "rec" formulation of addition, $0+n=n$\<close>
 lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(y)) = p : N"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+  apply (rule EqE)
+  apply (rule elim_rls, assumption)
+   apply rew
+  done
 
-(*the harder version, n+0=n: recursive, uses induction hypothesis*)
+text \<open>the harder version, $n+0=n$: recursive, uses induction hypothesis\<close>
 lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(z)) = p : N"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply hyp_rew
-done
+  apply (rule EqE)
+  apply (rule elim_rls, assumption)
+   apply hyp_rew
+  done
 
-(*Associativity of addition*)
+text \<open>Associativity of addition\<close>
 lemma "\<lbrakk>a:N; b:N; c:N\<rbrakk>
   \<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) =
     rec(a, rec(b, c, \<lambda>x y. succ(y)), \<lambda>x y. succ(y)) : N"
-apply (NE a)
-apply hyp_rew
-done
+  apply (NE a)
+    apply hyp_rew
+  done
 
-(*Martin-Löf (1984) page 62: pairing is surjective*)
+text \<open>Martin-Löf (1984) page 62: pairing is surjective\<close>
 lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>x y. y)> = p : Sum(A,B)"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
-done
+  apply (rule EqE)
+  apply (rule elim_rls, assumption)
+  apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
+  done
 
 lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"
-apply rew
-done
+  by rew
 
-(*a contrived, complicated simplication, requires sum-elimination also*)
+text \<open>a contrived, complicated simplication, requires sum-elimination also\<close>
 lemma "(\<^bold>\<lambda>f. \<^bold>\<lambda>x. f`(f`x)) ` (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) =
       \<^bold>\<lambda>x. x  :  \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"
-apply (rule reduction_rls)
-apply (rule_tac [3] intrL_rls)
-apply (rule_tac [4] EqE)
-apply (erule_tac [4] SumE)
-(*order of unifiers is essential here*)
-apply rew
-done
+  apply (rule reduction_rls)
+    apply (rule_tac [3] intrL_rls)
+     apply (rule_tac [4] EqE)
+     apply (erule_tac [4] SumE)
+    (*order of unifiers is essential here*)
+     apply rew
+  done
 
 end
diff -r 934d4aed8497 -r 2510e6f7b11c src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Wed Oct 26 17:22:12 2022 +0100
+++ b/src/CTT/ex/Synthesis.thy	Wed Oct 26 18:08:44 2022 +0100
@@ -6,40 +6,40 @@
 section "Synthesis examples, using a crude form of narrowing"
 
 theory Synthesis
-imports "../CTT"
+  imports "../CTT"
 begin
 
 text "discovery of predecessor function"
 schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
-apply intr
-apply eqintr
-apply (rule_tac [3] reduction_rls)
-apply (rule_tac [5] comp_rls)
-apply rew
-done
+  apply intr
+    apply eqintr
+    apply (rule_tac [3] reduction_rls)
+      apply (rule_tac [5] comp_rls)
+        apply rew
+  done
 
 text "the function fst as an element of a function type"
 schematic_goal [folded basic_defs]:
   "A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
-apply intr
-apply eqintr
-apply (rule_tac [2] reduction_rls)
-apply (rule_tac [4] comp_rls)
-apply typechk
-txt "now put in A everywhere"
-apply assumption+
-done
+  apply intr
+   apply eqintr
+   apply (rule_tac [2] reduction_rls)
+     apply (rule_tac [4] comp_rls)
+       apply typechk
+  txt "now put in A everywhere"
+   apply assumption+
+  done
 
 text "An interesting use of the eliminator, when"
-(*The early implementation of unification caused non-rigid path in occur check
+  (*The early implementation of unification caused non-rigid path in occur check
   See following example.*)
 schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
                    \<times> Eq(?A, ?b(inr(i)), <succ(0), i>)"
-apply intr
-apply eqintr
-apply (rule comp_rls)
-apply rew
-done
+  apply intr
+   apply eqintr
+   apply (rule comp_rls)
+     apply rew
+  done
 
 (*Here we allow the type to depend on i.
  This prevents the cycle in the first unification (no longer needed).
@@ -47,58 +47,58 @@
  Simpler still: make ?A into a constant type N \<times> N.*)
 schematic_goal "?a : \<Prod>i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
                   \<times>  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
-oops
+  oops
 
-text "A tricky combination of when and split"
-(*Now handled easily, but caused great problems once*)
+  text "A tricky combination of when and split"
+    (*Now handled easily, but caused great problems once*)
 schematic_goal [folded basic_defs]:
   "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
                            \<times>  Eq(?A, ?b(inr(<i,j>)), j)"
-apply intr
-apply eqintr
-apply (rule PlusC_inl [THEN trans_elem])
-apply (rule_tac [4] comp_rls)
-apply (rule_tac [7] reduction_rls)
-apply (rule_tac [10] comp_rls)
-apply typechk
-done
+  apply intr
+   apply eqintr
+   apply (rule PlusC_inl [THEN trans_elem])
+      apply (rule_tac [4] comp_rls)
+        apply (rule_tac [7] reduction_rls)
+           apply (rule_tac [10] comp_rls)
+             apply typechk
+  done
 
 (*similar but allows the type to depend on i and j*)
 schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
                           \<times>   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
-oops
+  oops
 
 (*similar but specifying the type N simplifies the unification problems*)
 schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(N, ?b(inl(<i,j>)), i)
                           \<times>   Eq(N, ?b(inr(<i,j>)), j)"
-oops
+  oops
 
 
-text "Deriving the addition operator"
+  text "Deriving the addition operator"
 schematic_goal [folded arith_defs]:
   "?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
                   \<times>  (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
-apply intr
-apply eqintr
-apply (rule comp_rls)
-apply rew
-done
+  apply intr
+   apply eqintr
+   apply (rule comp_rls)
+    apply rew
+  done
 
 text "The addition function -- using explicit lambdas"
 schematic_goal [folded arith_defs]:
   "?c : \<Sum>plus : ?A .
          \<Prod>x:N. Eq(N, plus`0`x, x)
                 \<times>  (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
-apply intr
-apply eqintr
-apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
-apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
-apply (rule_tac [3] p = "y" in NC_succ)
-  (**  by (resolve_tac @{context} comp_rls 3);  caused excessive branching  **)
-apply rew
-done
+  apply intr
+    apply eqintr
+    apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+     apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
+         apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+          apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
+              apply (rule_tac [3] p = "y" in NC_succ)
+    (**  by (resolve_tac @{context} comp_rls 3);  caused excessive branching  **)
+                apply rew
+  done
 
 end
 
diff -r 934d4aed8497 -r 2510e6f7b11c src/CTT/ex/Typechecking.thy
--- a/src/CTT/ex/Typechecking.thy	Wed Oct 26 17:22:12 2022 +0100
+++ b/src/CTT/ex/Typechecking.thy	Wed Oct 26 18:08:44 2022 +0100
@@ -12,77 +12,69 @@
 subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
 
 schematic_goal "?A type"
-apply (rule form_rls)
-done
+  by (rule form_rls)
 
 schematic_goal "?A type"
-apply (rule form_rls)
-back
-apply (rule form_rls)
-apply (rule form_rls)
-done
+  apply (rule form_rls)
+  back
+   apply (rule form_rls)
+  apply (rule form_rls)
+  done
 
 schematic_goal "\<Prod>z:?A . N + ?B(z) type"
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-done
+  apply (rule form_rls)
+   apply (rule form_rls)
+  apply (rule form_rls)
+   apply (rule form_rls)
+  apply (rule form_rls)
+  done
 
 
 subsection \<open>Multi-step proofs: Type inference\<close>
 
 lemma "\<Prod>w:N. N + N type"
-apply form
-done
+  by form
 
 schematic_goal "<0, succ(0)> : ?A"
-apply intr
-done
+  apply intr done
 
 schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
-apply typechk
-done
+  apply typechk done
 
 schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
-apply typechk
-done
+  apply typechk done
 
 text "typechecking an application of fst"
 schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
-apply typechk
-done
+  apply typechk done
 
 text "typechecking the predecessor function"
 schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
-apply typechk
-done
+  apply typechk done
 
 text "typechecking the addition function"
 schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
-apply typechk
-done
+  apply typechk done
 
-(*Proofs involving arbitrary types.
-  For concreteness, every type variable left over is forced to be N*)
+text \<open>Proofs involving arbitrary types.
+  For concreteness, every type variable left over is forced to be @{term N}\<close>
 method_setup N =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
 
 schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
-apply typechk
-apply N
-done
+  apply typechk
+  apply N
+  done
 
 schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
-apply typechk
-apply N
-done
+  apply typechk
+   apply N
+  done
 
 text "typechecking fst (as a function object)"
 schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
-apply typechk
-apply N
-done
+  apply typechk 
+   apply N
+  done
 
 end