# HG changeset patch # User bulwahn # Date 1256729343 -3600 # Node ID b129e4c476d6db9c4b5a6b2ac39dc6ed07160be4 # Parent 1d93dd8a02c9a8a6e5837333ac24ea569a686b49 improved mode parser; added mode annotations to examples diff -r 1d93dd8a02c9 -r b129e4c476d6 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Oct 28 12:29:02 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Oct 28 12:29:03 2009 +0100 @@ -174,7 +174,8 @@ fun gen_parse_mode smode_parser = (Scan.optional - (P.enum "!" ((P.$$$ "X" >> K NONE) || (smode_parser >> SOME)) --| P.$$$ "!") []) -- smode_parser + ((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") []) + -- smode_parser val parse_mode = gen_parse_mode parse_smode @@ -193,8 +194,7 @@ val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> - code_pred_cmd) + OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd) end diff -r 1d93dd8a02c9 -r b129e4c476d6 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Oct 28 12:29:02 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Oct 28 12:29:03 2009 +0100 @@ -6,7 +6,7 @@ inductive False' :: "bool" -code_pred (mode: X ! []) False' . +code_pred (mode : []) False' . code_pred [depth_limited] False' . code_pred [rpred] False' . @@ -27,10 +27,10 @@ for r :: "'a \ 'a \ bool" code_pred -(* (mode: [] => [], [] => [1], [] => [2], [] => [1, 2], - [1] => [], [1] => [1], [1] => [2], [1] => [1, 2], - [2] => [], [2] => [1], [2] => [2], [2] => [1, 2], - [1, 2] => [], [1, 2] => [1], [1, 2] => [2], [1, 2] => [1, 2])*) + (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2], + [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2], + [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2], + [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2]) EmptyClosure . thm EmptyClosure.equation @@ -66,12 +66,12 @@ where "zerozero (0, 0)" -code_pred zerozero . +code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero . code_pred [rpred] zerozero . subsection {* Alternative Rules *} -datatype char = C | D | E | F | G +datatype char = C | D | E | F | G | H inductive is_C_or_D where @@ -130,7 +130,7 @@ text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} -code_pred is_FGH +code_pred (mode: [], [1]) is_FGH proof - case is_F_or_G from this(1) show thesis @@ -209,7 +209,7 @@ definition odd' where "odd' x == \ even x" -code_pred [inductify] odd' . +code_pred (mode: [1]) [inductify] odd' . code_pred [inductify, depth_limited] odd' . code_pred [inductify, rpred] odd' . @@ -221,7 +221,7 @@ where "n mod 2 = 0 \ is_even n" -code_pred is_even . +code_pred (mode: [1]) is_even . subsection {* append predicate *} @@ -258,7 +258,7 @@ lemmas [code_pred_intros] = append2_Nil append2.intros(2) -code_pred append2 +code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2 proof - case append2 from append2(1) show thesis @@ -329,8 +329,8 @@ "filter1 P [] []" | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" | "\ P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" -ML {* Scan.optional *} -code_pred ( mode : [1], [1, 2]) filter1 . + +code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 . code_pred [depth_limited] filter1 . code_pred [rpred] filter1 . @@ -353,7 +353,7 @@ where "List.filter P xs = ys ==> filter3 P xs ys" -code_pred filter3 . +code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 . code_pred [depth_limited] filter3 . thm filter3.depth_limited_equation @@ -361,7 +361,7 @@ where "List.filter P xs = ys ==> filter4 P xs ys" -code_pred filter4 . +code_pred (mode: [1, 2], [1, 2, 3]) filter4 . code_pred [depth_limited] filter4 . code_pred [rpred] filter4 . @@ -381,7 +381,7 @@ "tupled_rev ([], [])" | "tupled_rev (xs, xs') \ tupled_append (xs', [x], ys) \ tupled_rev (x#xs, ys)" -code_pred tupled_rev . +code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev . thm tupled_rev.equation subsection {* partition predicate *} @@ -392,7 +392,7 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . +code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition . code_pred [depth_limited] partition . code_pred [rpred] partition . @@ -407,7 +407,7 @@ | "f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, x # ys, zs)" | "\ f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, ys, x # zs)" -code_pred tupled_partition . +code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition . thm tupled_partition.equation @@ -418,7 +418,7 @@ subsection {* transitive predicate *} -code_pred tranclp +code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp proof - case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis