add isabelle program (#778)

knightking100 · Oct 31, 2018 · abd493b · abd493b
1 parent c0cbc1d
commit abd493b
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 0 deletions.
diff --git a/LANGUAGES.md b/LANGUAGES.md
@@ -787,6 +787,7 @@ You can also request a new language to be added to the list, just leave a commen
 - [ ] [Iota](http://esolangs.org/wiki/Iota)
 - [ ] [IRC](http://esolangs.org/wiki/IRC)
 - [ ] [Iris](http://esolangs.org/wiki/Iris)
+- [x] [isabelle](https://en.wikipedia.org/wiki/Isabelle_(proof_assistant))
 - [x] [ISCOM](http://esolangs.org/wiki/ISCOM)
 - [ ] [itflabtijtslwi](http://esolangs.org/wiki/Itflabtijtslwi)
 - [x] [IWBASIC](https://rosettacode.org/wiki/Hello_world/Text#IWBASIC)

diff --git a/examples/i/isabelle.thy b/examples/i/isabelle.thy
@@ -0,0 +1,18 @@
+theory isabelle
+imports Main
+
+begin
+theorem HelloWorld:
+assumes 1: "Meeting \<and> Greeting \<longrightarrow> Hello"
+assumes 2: "Greeting \<longrightarrow> Meeting"
+assumes 3: "Greeting"
+shows "Hello"
+proof - 
+{
+  from 2 3 have 4: "Meeting" by (rule mp)
+  from 4 3 have 5: "Meeting \<and> Greeting" by (rule conjI)
+  from 1 5 have 6: "Hello" by (rule mp)
+}
+thus ?thesis .
+qed
+end