diff options
author | Josh Chen | 2018-08-17 14:20:39 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-17 14:20:39 +0200 |
commit | 0c786e631f32c1f92c508d3fe8aad6f433bb5ce0 (patch) | |
tree | 658c32c489bf8e741884c9864cc45244b7127de4 | |
parent | 6608e0a3d48aae26f84087da5e4d60da8341bca5 (diff) |
Partway through updating proofs after the change of the function composition definition
Diffstat (limited to '')
-rw-r--r-- | ProdProps.thy | 57 |
1 files changed, 11 insertions, 46 deletions
diff --git a/ProdProps.thy b/ProdProps.thy index e48b3e6..2145bf9 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -15,22 +15,18 @@ begin section \<open>Composition\<close> text " - The proof of associativity is surprisingly intricate; it involves telling Isabelle to use the correct rule for \<Pi>-type judgmental equality, and the correct substitutions in the subgoals thereafter, among other things. + The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Pi>-type definitional equality, and the correct substitutions in the subgoals thereafter. " lemma compose_assoc: - assumes - "A \<rightarrow> B: U(i)" "B \<rightarrow> C: U(i)" and - "\<Prod>x:C. D(x): U(i)" and - "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)" + assumes "A: U(i)" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)" shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)" proof (subst (0 1 2 3) compose_def) - text "Compute the different bracketings and show they are equivalent:" - show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" proof (subst Prod_eq) - show "\<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" by simp + \<comment> \<open>Todo: set the Simplifier (or other simplification methods) up to use \<open>Prod_eq\<close>!\<close> + show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" proof compute show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" @@ -39,49 +35,18 @@ proof (subst (0 1 2 3) compose_def) qed show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (simple lems: assms) qed (simple lems: assms) - qed (wellformed lems: assms) - - text " - Finish off any remaining subgoals that Isabelle can't prove automatically. - These typically require the application of specific substitutions or computation rules. - " - show "g \<circ> f: A \<rightarrow> C" by (subst compose_def) (derive lems: assms) - - show "h \<circ> g: \<Prod>x:B. D(g`x)" - proof (subst compose_def) - show "\<^bold>\<lambda>x. h`(g`x): \<Prod>x:B. D(g`x)" - proof - show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" - proof - show "\<And>x. x: B \<Longrightarrow> g`x: C" by (simple lems: assms) - qed (simple lems: assms) - qed (wellformed lems: assms) - qed fact+ - - show "\<Prod>x:B. D (g`x): U(i)" - proof - show "\<And>x. x: B \<Longrightarrow> D(g`x): U(i)" - proof - - have *: "D: C \<longrightarrow> U(i)" by (wellformed lems: assms) - - fix x assume asm: "x: B" - have "g`x: C" by (simple lems: assms asm) - then show "D(g`x): U(i)" by (rule *) - qed - qed (wellformed lems: assms) - - have "A: U(i)" by (wellformed lems: assms) - moreover have "C: U(i)" by (wellformed lems: assms) - ultimately show "A \<rightarrow> C: U(i)" .. -qed (simple lems: assms) - + qed fact +qed -text "The following rule is correct, but we cannot prove it using just the rules of the theory." lemma compose_comp': assumes "A: U(i)" and "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)" shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" -oops +proof (subst compose_def, subst Prod_eq) + show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`x) \<equiv> \<^bold>\<lambda>x. c (b x)" + proof compute + + text "However we can derive a variant with more explicit premises:" |