# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1367495355 -3600
# Node ID 89ed51d72e4a77fa2941eaee19dba21ffa0a2bbc
# Parent  e113420a2fce01627e3cb6d0d32bcce670bb495d
eliminated explicit swap_lemmas

diff -r e113420a2fce -r 89ed51d72e4a thys/Recs.thy
--- a/thys/Recs.thy	Thu May 02 11:32:37 2013 +0100
+++ b/thys/Recs.thy	Thu May 02 12:49:15 2013 +0100
@@ -230,10 +230,7 @@
   "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
 
 definition 
-  "rec_power_swap = PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2])"
-
-definition
-  "rec_power = rec_swap rec_power_swap"
+  "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
 
 definition
   "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
@@ -242,10 +239,8 @@
   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_minus_swap = (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
+  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
-definition
-  "rec_minus = rec_swap rec_minus_swap"
 
 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
 
@@ -259,9 +254,7 @@
   @{text "rec_eq"} compares two arguments: returns @{text "1"}
   if they are equal; @{text "0"} otherwise. *}
 definition 
-  "rec_eq = CN rec_minus 
-             [CN (constn 1) [Id 2 0], 
-              CN rec_add [rec_minus, rec_swap rec_minus]]"
+  "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
 
 definition 
   "rec_noteq = CN rec_not [rec_eq]"
@@ -277,6 +270,7 @@
 
 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
   y otherwise *}
+
 definition 
   "rec_ifz = PR (Id 2 0) (Id 4 3)"
 
@@ -326,10 +320,8 @@
 text {* Dvd, Quotient, Reminder *}
 
 definition 
-  "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0]"  
-
-definition 
-  "rec_dvd = rec_swap rec_dvd_swap" 
+  "rec_dvd = 
+     rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
 
 definition
   "rec_quo = (let lhs = CN S [Id 3 0] in
@@ -359,13 +351,9 @@
   "rec_eval rec_mult [x, y] = x * y"
 by (induct x) (simp_all add: rec_mult_def)
 
-lemma power_swap_lemma [simp]: 
-  "rec_eval rec_power_swap [y, x] = x ^ y"
-by (induct y) (simp_all add: rec_power_swap_def)
-
 lemma power_lemma [simp]: 
   "rec_eval rec_power [x, y] = x ^ y"
-by (simp add: rec_power_def)
+by (induct y) (simp_all add: rec_power_def)
 
 lemma fact_lemma [simp]: 
   "rec_eval rec_fact [x] = fact x"
@@ -375,13 +363,9 @@
   "rec_eval rec_pred [x] =  x - 1"
 by (induct x) (simp_all add: rec_pred_def)
 
-lemma minus_swap_lemma [simp]: 
-  "rec_eval rec_minus_swap [x, y] = y - x"
-by (induct x) (simp_all add: rec_minus_swap_def)
-
 lemma minus_lemma [simp]: 
   "rec_eval rec_minus [x, y] = x - y"
-by (simp add: rec_minus_def)
+by (induct y) (simp_all add: rec_minus_def)
 
 lemma sign_lemma [simp]: 
   "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
@@ -468,15 +452,10 @@
 apply(auto)
 done
 
-lemma dvd_swap_lemma [simp]:
-  "rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)"
-unfolding dvd_alt_def
-by (auto simp add: rec_dvd_swap_def)
-
 lemma dvd_lemma [simp]:
   "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
-by (simp add: rec_dvd_def)
-
+unfolding dvd_alt_def
+by (auto simp add: rec_dvd_def)
 
 fun Quo where
   "Quo x 0 = 0"