# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1309825580 -32400
# Node ID cc0605102f9537c4a25c8e55ce4f0c07e7ced10e
# Parent  dc003667cd174f65de058c6514cf7eaefc7227c4
Move If / Let with 'True' to the end of Lambda

diff -r dc003667cd17 -r cc0605102f95 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Jul 04 23:56:19 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 09:26:20 2011 +0900
@@ -722,48 +722,6 @@
 apply (rule, perm_simp, rule)
 oops
 
-text {* tests of functions containing if and case *}
-
-consts P :: "lam \<Rightarrow> bool"
-
-nominal_primrec  
-  A :: "lam => lam"
-where  
-  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
-| "A (Var x) = (Var x)" 
-| "A (App M N) = (if True then M else A N)"
-oops
-
-nominal_primrec  
-  C :: "lam => lam"
-where  
-  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
-| "C (Var x) = (Var x)" 
-| "C (App M N) = (if True then M else C N)"
-oops
-
-nominal_primrec  
-  A :: "lam => lam"
-where  
-  "A (Lam [x].M) = (Lam [x].M)"
-| "A (Var x) = (Var x)"
-| "A (App M N) = (if True then M else A N)"
-oops
-
-nominal_primrec  
-  B :: "lam => lam"
-where  
-  "B (Lam [x].M) = (Lam [x].M)"
-| "B (Var x) = (Var x)"
-| "B (App M N) = (if True then M else (B N))"
-unfolding eqvt_def
-unfolding B_graph_def
-apply(perm_simp)
-apply(rule allI)
-apply(rule refl)
-oops
-
-
 lemma test:
   assumes "t = s"
   and "supp p \<sharp>* t" "supp p \<sharp>* x"
@@ -831,6 +789,47 @@
 
 termination by lexicographic_order
 
+text {* tests of functions containing if and case *}
+
+consts P :: "lam \<Rightarrow> bool"
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
+| "A (Var x) = (Var x)" 
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  C :: "lam => lam"
+where  
+  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
+| "C (Var x) = (Var x)" 
+| "C (App M N) = (if True then M else C N)"
+oops
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (Lam [x].M) = (Lam [x].M)"
+| "A (Var x) = (Var x)"
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  B :: "lam => lam"
+where  
+  "B (Lam [x].M) = (Lam [x].M)"
+| "B (Var x) = (Var x)"
+| "B (App M N) = (if True then M else (B N))"
+unfolding eqvt_def
+unfolding B_graph_def
+apply(perm_simp)
+apply(rule allI)
+apply(rule refl)
+oops
+
 end