# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295647083 -3600
# Node ID da9bed7baf2323e05887835355395dbbc1419cfb
# Parent  abb6c3ac2df2080527e94b636a9491da6f922ebb
better flow of proofs and definitions and proof

diff -r abb6c3ac2df2 -r da9bed7baf23 Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Fri Jan 21 22:23:44 2011 +0100
+++ b/Tutorial/Tutorial1.thy	Fri Jan 21 22:58:03 2011 +0100
@@ -61,6 +61,7 @@
         \<bullet>    bullet    (permutation application)
 *}
 
+
 theory Tutorial1
 imports Lambda
 begin
@@ -178,25 +179,19 @@
 term "\<And>x. P x"
 
 
-
-section {* Inductive Definitions: Transitive Closures of Beta-Reduction *}
-
-text {*
-  The theory Lmabda already contains a definition for beta-reduction, written
-*}
-
-term "t \<longrightarrow>b t'"
+section {* Inductive Definitions: Evaluation Relation *}
 
 text {*
-  In this section we want to define inductively the transitive closure of
-  beta-reduction.
+  In this section we want to define inductively the evaluation
+  relation for lambda terms.
 
-  Inductive definitions in Isabelle start with the keyword "inductive" and a predicate 
-  name.  One can optionally provide a type for the predicate. Clauses of the inductive
-  predicate are introduced by "where" and more than two clauses need to be 
-  separated by "|". One can also give a name to each clause and indicate that it 
-  should be added to the hints database ("[intro]"). A typical clause has some 
-  premises and a conclusion. This is written in Isabelle as:
+  Inductive definitions in Isabelle start with the keyword "inductive" 
+  and a predicate name.  One can optionally provide a type for the predicate. 
+  Clauses of the inductive predicate are introduced by "where" and more than 
+  two clauses need to be separated by "|". One can also give a name to each 
+  clause and indicate that it should be added to the hints database ("[intro]"). 
+  A typical clause has some premises and a conclusion. This is written in 
+  Isabelle as:
 
    "premise \<Longrightarrow> conclusion"
    "premise1 \<Longrightarrow> premise2 \<Longrightarrow> \<dots> premisen \<Longrightarrow> conclusion"
@@ -213,18 +208,22 @@
 *}
 
 inductive
-  beta_star1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b* _" [60, 60] 60)
+  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
 where
-  bs1_refl: "t \<longrightarrow>b* t"
-| bs1_trans: "\<lbrakk>t1 \<longrightarrow>b t2; t2 \<longrightarrow>b* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b* t3"
+  e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
+| e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
 
 
+text {* 
+  Values are also defined using inductive. In our case values
+  are just lambda-abstractions. 
+*}
+
 inductive
-  beta_star2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b** _" [60, 60] 60)
+  val :: "lam \<Rightarrow> bool" 
 where
-  bs2_refl: "t \<longrightarrow>b** t"
-| bs2_step: "t1 \<longrightarrow>b t2 \<Longrightarrow> t1 \<longrightarrow>b** t2"
-| bs2_trans: "\<lbrakk>t1 \<longrightarrow>b** t2; t2 \<longrightarrow>b** t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b** t3"
+  v_Lam[intro]:   "val (Lam [x].t)"
+
 
 section {* Theorems *}
 
@@ -233,8 +232,8 @@
   database can be queried using 
 *}
 
-thm bs1_refl
-thm bs2_trans
+thm e_App
+thm e_Lam
 thm conjI
 thm conjunct1
 
@@ -248,8 +247,8 @@
   constitutes an induction over them. 
 *}
 
-thm beta_star1.intros
-thm beta_star2.induct
+thm eval.intros
+thm eval.induct
 
 
 section {* Lemmas / Theorems / Corollaries *}
@@ -267,8 +266,6 @@
   Examples are
 *}
 
-
-
 lemma alpha_equ:
   shows "Lam [x].Var x = Lam [y].Var y"
   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
@@ -361,100 +358,47 @@
        show \<dots>
      \<dots>
      qed
-*}
 
-
-subsection {* Exercise I *}
-
-text {*
-  Remove the sorries in the proof below and fill in the proper
-  justifications. 
+   Two very simple example proofs are as follows.
 *}
 
 
-lemma
-  assumes a: "t1 \<longrightarrow>b* t2" 
-  shows "t1 \<longrightarrow>b** t2"
-  using a
+lemma eval_val:
+  assumes a: "val t"
+  shows "t \<Down> t"
+using a
 proof (induct)
-  case (bs1_refl t)
-  show "t \<longrightarrow>b** t" using bs2_refl by blast
-next
-  case (bs1_trans t1 t2 t3)
-  have beta: "t1 \<longrightarrow>b t2" by fact
-  have ih: "t2 \<longrightarrow>b** t3" by fact
-  have a: "t1 \<longrightarrow>b** t2" using beta bs2_step by blast
-  show "t1 \<longrightarrow>b** t3" using a ih bs2_trans by blast
+  case (v_Lam x t)
+  show "Lam [x]. t \<Down> Lam [x]. t" sorry
 qed
 
-
-subsection {* Exercise II *}
-
-text {*
-  Again remove the sorries in the proof below and fill in the proper
-  justifications. 
-*}
-
-lemma bs1_trans2:
-  assumes a: "t1 \<longrightarrow>b* t2"
-  and     b: "t2 \<longrightarrow>b* t3"
-  shows "t1 \<longrightarrow>b* t3"
-using a b
+lemma eavl_to_val:
+  assumes a: "t \<Down> t'"
+  shows "val t'"
+using a
 proof (induct)
-  case (bs1_refl t1)
-  have a: "t1 \<longrightarrow>b* t3" by fact
-  show "t1 \<longrightarrow>b* t3" using a by blast
+  case (e_Lam x t)
+  show "val (Lam [x].t)" sorry
 next
-  case (bs1_trans t1 t2 t3')
-  have ih1: "t1 \<longrightarrow>b t2" by fact
-  have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-  have asm: "t3' \<longrightarrow>b* t3" by fact
-  have a: "t2 \<longrightarrow>b* t3" using ih2 asm by blast
-  show "t1 \<longrightarrow>b* t3" using ih1 a beta_star1.bs1_trans by blast
+  case (e_App t1 x t t2 v v')
+  have "t1 \<Down> Lam [x].t" by fact
+  have ih1: "val (Lam [x]. t)" by fact
+  have "t2 \<Down> v" by fact
+  have ih2: "val v" by fact
+  have "t [x ::= v] \<Down> v'" by fact
+  have ih3: "val v'" by fact
+  show "val v'" sorry
 qed
   
-lemma
-  assumes a: "t1 \<longrightarrow>b** t2"
-  shows "t1 \<longrightarrow>b* t2"
-using a
-proof (induct)
-  case (bs2_refl t)
-  show "t \<longrightarrow>b* t" using bs1_refl by blast
-next
-  case (bs2_step t1 t2)
-  have ih: "t1 \<longrightarrow>b t2" by fact
-  have a: "t2 \<longrightarrow>b* t2" using bs1_refl by blast
-  show "t1 \<longrightarrow>b* t2" using ih a bs1_trans by blast
-next
-  case (bs2_trans t1 t2 t3)
-  have ih1: "t1 \<longrightarrow>b* t2" by fact
-  have ih2: "t2 \<longrightarrow>b* t3" by fact
-  show "t1 \<longrightarrow>b* t3" using ih1 ih2 bs1_trans2 by blast  
-qed
-  
+ 
 text {* 
   Just like gotos in the Basic programming language, labels often reduce 
   the readability of proofs. Therefore one can use in Isar the notation
   "then have" in order to feed a have-statement to the proof of 
   the next have-statement. This is used in teh second case below.
 *}
+ 
 
-lemma 
-  assumes a: "t1 \<longrightarrow>b* t2"
-  and     b: "t2 \<longrightarrow>b* t3"
-  shows "t1 \<longrightarrow>b* t3"
-using a b
-proof (induct)
-  case (bs1_refl t1)
-  show "t1 \<longrightarrow>b* t3" by fact
-next
-  case (bs1_trans t1 t2 t3')
-  have ih1: "t1 \<longrightarrow>b t2" by fact
-  have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-  have "t3' \<longrightarrow>b* t3" by fact
-  then have "t2 \<longrightarrow>b* t3" using ih2 by blast
-  then show "t1 \<longrightarrow>b* t3" using ih1 beta_star1.bs1_trans by blast
-qed
 
 text {* 
   The label ih2 cannot be got rid of in this way, because it is used 
@@ -474,26 +418,6 @@
   "statement". With this we can simplify our proof further to:
 *}
 
-lemma 
-  assumes a: "t1 \<longrightarrow>b* t2"
-  and     b: "t2 \<longrightarrow>b* t3"
-  shows "t1 \<longrightarrow>b* t3"
-using a b
-proof (induct)
-  case (bs1_refl t1)
-  show "t1 \<longrightarrow>b* t3" by fact
-next
-  case (bs1_trans t1 t2 t3')
-  have "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-  moreover
-  have "t3' \<longrightarrow>b* t3" by fact
-  ultimately 
-  have "t2 \<longrightarrow>b* t3" by blast
-  moreover 
-  have "t1 \<longrightarrow>b t2" by fact
-  ultimately show "t1 \<longrightarrow>b* t3" using beta_star1.bs1_trans by blast
-qed
-
 
 text {* 
   While automatic proof procedures in Isabelle are not able to prove statements
@@ -502,41 +426,7 @@
   and auto will take care of the rest. This means we can write:
 *}
 
-lemma
-  assumes a: "t1 \<longrightarrow>b* t2" 
-  shows "t1 \<longrightarrow>b** t2"
-  using a
-  by (induct) (auto intro: beta_star2.intros)
 
-lemma 
-  assumes a: "t1 \<longrightarrow>b* t2"
-  and     b: "t2 \<longrightarrow>b* t3"
-  shows "t1 \<longrightarrow>b* t3"
-  using a b
-  by (induct) (auto intro: beta_star1.intros)
-
-lemma
-  assumes a: "t1 \<longrightarrow>b** t2"
-  shows "t1 \<longrightarrow>b* t2"
-  using a
-  by (induct) (auto intro: bs1_trans2 beta_star1.intros)
-
-inductive
-  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
-where
-  e_Lam:  "Lam [x].t \<Down> Lam [x].t"
-| e_App:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
-
-declare eval.intros[intro]
-
-text {* 
-  Values are also defined using inductive. In our case values
-  are just lambda-abstractions. *}
-
-inductive
-  val :: "lam \<Rightarrow> bool" 
-where
-  v_Lam[intro]:   "val (Lam [x].t)"
 
 
 section {* Datatypes: Evaluation Contexts *}
@@ -655,7 +545,7 @@
   shows "<e1, Es1> \<mapsto>* <e3, Es3>"
 using a b by (induct) (auto)
 
-lemma eval_to_val:
+lemma eval_to_val:  (* fixme: done above *)
   assumes a: "t \<Down> t'"
   shows "val t'"
 using a by (induct) (auto)
diff -r abb6c3ac2df2 -r da9bed7baf23 Tutorial/Tutorial2.thy
--- a/Tutorial/Tutorial2.thy	Fri Jan 21 22:23:44 2011 +0100
+++ b/Tutorial/Tutorial2.thy	Fri Jan 21 22:58:03 2011 +0100
@@ -24,7 +24,6 @@
 
 type_synonym ty_ctx = "(name \<times> ty) list"
 
-
 inductive
   valid :: "ty_ctx \<Rightarrow> bool"
 where