--- 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