doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex

 %
 \endisadelimquoteme
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline

 \isadelimquoteme
 %
 \endisadelimquoteme
 %
 \begin{isamarkuptext}%
-\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
+\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
   \isa{attribute} which states that the given theorems should be
   considered as defining equations for a \isa{fun} statement --
   the corresponding constant is determined syntactically.  The resulting code:%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \verb|class (Semigroup a) => Monoid a where {|\newline%
 \verb|  neutral :: a;|\newline%
 \verb|};|\newline%
 \newline%
 \verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow Zero_nat a = neutral;|\newline%
 \verb|pow (Suc n) a = mult a (pow n a);|\newline%
-\verb|pow Zero_nat a = neutral;|\newline%
 \newline%
 \verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
 \verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
 \verb|plus_nat Zero_nat n = n;|\newline%
 \newline%
 \verb|neutral_nat :: Nat;|\newline%
 \verb|neutral_nat = Suc Zero_nat;|\newline%
 \newline%
 \verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
+\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
 \verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
-\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
 \newline%
 \verb|instance Semigroup Nat where {|\newline%
 \verb|  mult = mult_nat;|\newline%
 \verb|};|\newline%
 \newline%

 \newline%
 \verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline%
 \verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
 \verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
 \newline%
-\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
-\verb|  |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
+\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
+\verb|  |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
 \newline%
 \verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
 \verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
 \newline%
 \verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
 \newline%
-\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
-\verb|  |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
+\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
+\verb|  |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
 \newline%
 \verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
 \newline%
 \verb|val monoid_nat =|\newline%
 \verb|  {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline%

 %
 \endisadelimquoteme
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline

 %
 \endisadelimquoteme
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \isanewline
 \isacommand{declare}\isamarkupfalse%
 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
 \endisatagquoteme
 {\isafoldquoteme}%
 %
 \isadelimquoteme
 %

 %
 \isataginvisible
 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp%
 \endisataginvisible
 {\isafoldinvisible}%
 %
 \isadeliminvisible

 \verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
 \verb|fun eq (A_:'a eq) = #eq A_;|\newline%
 \newline%
 \verb|fun eqop A_ a b = eq A_ a b;|\newline%
 \newline%
-\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
-\verb|  |\verb,|,\verb| member A_ x [] = false;|\newline%
-\newline%
-\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
-\verb|  (if member A_ z xs|\newline%
-\verb|    then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
-\verb|           else collect_duplicates A_ xs (z :: ys) zs)|\newline%
-\verb|    else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
-\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
+\verb|fun member A_ x [] = false|\newline%
+\verb|  |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
+\newline%
+\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
+\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
+\verb|    (if member A_ z xs|\newline%
+\verb|      then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
+\verb|             else collect_duplicates A_ xs (z :: ys) zs)|\newline%
+\verb|      else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
 \newline%
 \verb|end; (*struct Example*)|%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 \isacommand{instantiation}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
 \ \isacommand{proof}\isamarkupfalse%
 \isanewline

 \isanewline
 \isacommand{end}\isamarkupfalse%
 \isanewline
 \isanewline
 \isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%

 %
 \endisadelimquoteme
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%

 %
 \endisadelimquoteme
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
 \endisatagquoteme

 \verb|structure Example = |\newline%
 \verb|struct|\newline%
 \newline%
 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
 \newline%
-\verb|fun null (x :: xs) = false|\newline%
-\verb|  |\verb,|,\verb| null [] = true;|\newline%
+\verb|fun null [] = true|\newline%
+\verb|  |\verb,|,\verb| null (x :: xs) = false;|\newline%
 \newline%
 \verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
 \verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
 \verb|  |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
 \verb|  |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%