summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 03 Apr 2012 16:53:32 +0200 | |

changeset 47295 | b77980afc975 |

parent 47294 | 008b7858f3c0 |

child 47296 | c82a0b2606a1 |

some context examples;

--- a/src/HOL/IsaMakefile Tue Apr 03 16:51:01 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 03 16:53:32 2012 +0200 @@ -1036,7 +1036,8 @@ $(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ - Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ + Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \ + Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \ Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ Isar_Examples/Mutilated_Checkerboard.thy \ Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 16:53:32 2012 +0200 @@ -0,0 +1,94 @@ +(* Title: HOL/Isar_Examples/Group_Context.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- theory context version *} + +theory Group_Context +imports Main +begin + +text {* hypothetical group axiomatization *} + +context + fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\<And>x. one ** x = x" + and left_inverse: "\<And>x. inverse x ** x = one" +begin + +text {* some consequences *} + +lemma right_inverse: "x ** inverse x = one" +proof - + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\<dots> = one ** x ** inverse x" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\<dots> = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\<dots> = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . +qed + +lemma right_one: "x ** one = x" +proof - + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\<dots> = x ** inverse x ** x" + by (simp only: assoc) + also have "\<dots> = one ** x" + by (simp only: right_inverse) + also have "\<dots> = x" + by (simp only: left_one) + finally show "x ** one = x" . +qed + +lemma one_equality: "e ** x = x \<Longrightarrow> one = e" +proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\<dots> = (e ** x) ** inverse x" + by (simp only: eq) + also have "\<dots> = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\<dots> = e ** one" + by (simp only: right_inverse) + also have "\<dots> = e" + by (simp only: right_one) + finally show "one = e" . +qed + +lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'" +proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\<dots> = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\<dots> = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\<dots> = x' ** one" + by (simp only: right_inverse) + also have "\<dots> = x'" + by (simp only: right_one) + finally show "inverse x = x'" . +qed + +end + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Apr 03 16:53:32 2012 +0200 @@ -0,0 +1,96 @@ +(* Title: HOL/Isar_Examples/Group_Notepad.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- proof notepad version *} + +theory Group_Notepad +imports Main +begin + +notepad +begin + txt {* hypothetical group axiomatization *} + + fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\<And>x. one ** x = x" + and left_inverse: "\<And>x. inverse x ** x = one" + + txt {* some consequences *} + + have right_inverse: "\<And>x. x ** inverse x = one" + proof - + fix x + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\<dots> = one ** x ** inverse x" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\<dots> = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\<dots> = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\<dots> = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . + qed + + have right_one: "\<And>x. x ** one = x" + proof - + fix x + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\<dots> = x ** inverse x ** x" + by (simp only: assoc) + also have "\<dots> = one ** x" + by (simp only: right_inverse) + also have "\<dots> = x" + by (simp only: left_one) + finally show "x ** one = x" . + qed + + have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e" + proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\<dots> = (e ** x) ** inverse x" + by (simp only: eq) + also have "\<dots> = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\<dots> = e ** one" + by (simp only: right_inverse) + also have "\<dots> = e" + by (simp only: right_one) + finally show "one = e" . + qed + + have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'" + proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\<dots> = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\<dots> = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\<dots> = x' ** one" + by (simp only: right_inverse) + also have "\<dots> = x'" + by (simp only: right_one) + finally show "inverse x = x'" . + qed + +end + +end