less customary term_of conversions;
authorhaftmann
Fri Feb 15 08:31:31 2013 +0100 (2013-02-15)
changeset 511440ede9e2266a8
parent 51143 0a2371e7ced3
child 51151 65b7ccb1d96a
less customary term_of conversions;
spurious side effect on method reflection
src/HOL/Code_Evaluation.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/ex/Reflection_Examples.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -133,50 +133,15 @@
     1.4    (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
     1.5       and "Term.Free/ ((_), (_))")
     1.6  
     1.7 +code_const "term_of \<Colon> integer \<Rightarrow> term"
     1.8 +  (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
     1.9 +  
    1.10  code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    1.11    (Eval "HOLogic.mk'_literal")
    1.12  
    1.13  code_reserved Eval HOLogic
    1.14  
    1.15  
    1.16 -subsubsection {* Numeric types *}
    1.17 -
    1.18 -definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
    1.19 -  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
    1.20 -
    1.21 -lemma (in term_syntax) term_of_num_semiring_code [code]:
    1.22 -  "term_of_num_semiring two k = (
    1.23 -    if k = 1 then termify Num.One
    1.24 -    else (if k mod two = 0
    1.25 -      then termify Num.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
    1.26 -      else termify Num.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
    1.27 -  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def)
    1.28 -
    1.29 -lemma (in term_syntax) term_of_nat_code [code]:
    1.30 -  "term_of (n::nat) = (
    1.31 -    if n = 0 then termify (0 :: nat)
    1.32 -    else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)"
    1.33 -  by (simp only: term_of_anything)
    1.34 -
    1.35 -lemma (in term_syntax) term_of_natural_code [code]:
    1.36 -  "term_of (k::natural) = (
    1.37 -    if k = 0 then termify (0 :: natural)
    1.38 -    else termify (numeral :: num \<Rightarrow> natural) <\<cdot>> term_of_num_semiring (2::natural) k)"
    1.39 -  by (simp only: term_of_anything)
    1.40 -
    1.41 -lemma (in term_syntax) term_of_integer_code [code]:
    1.42 -  "term_of (k::integer) = (if k = 0 then termify (0 :: integer)
    1.43 -    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) (- k)
    1.44 -    else termify (numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) k)"
    1.45 -  by (simp only: term_of_anything)
    1.46 -
    1.47 -lemma (in term_syntax) term_of_int_code [code]:
    1.48 -  "term_of (k::int) = (if k = 0 then termify (0 :: int)
    1.49 -    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) (- k)
    1.50 -    else termify (numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) k)"
    1.51 -  by (simp only: term_of_anything)
    1.52 -
    1.53 -
    1.54  subsubsection {* Obfuscation *}
    1.55  
    1.56  print_translation {*
    1.57 @@ -202,7 +167,7 @@
    1.58  
    1.59  
    1.60  hide_const dummy_term valapp
    1.61 -hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing
    1.62 +hide_const (open) Const App Abs Free termify valtermify term_of tracing
    1.63  
    1.64  end
    1.65  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     2.3 @@ -309,7 +309,14 @@
     2.4  definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
     2.5    "list s n = map s [0 ..< n]"
     2.6  
     2.7 -values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
     2.8 +values [expected "{[Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
     2.9 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    2.10 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
    2.11 +     )))))))))))))))))))))))))))))))))))))))),
    2.12 +   Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc   (Suc (Suc (Suc (Suc
    2.13 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    2.14 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
    2.15 +     )))))))))))))))))))))))))))))))))))))))))]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
    2.16  
    2.17  
    2.18  subsection {* CCS *}
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
     3.3 @@ -334,7 +334,7 @@
     3.4  code_pred [dseq] one_or_two .
     3.5  code_pred [random_dseq] one_or_two .
     3.6  thm one_or_two.dseq_equation
     3.7 -values [expected "{1::nat, 2::nat}"] "{x. one_or_two x}"
     3.8 +values [expected "{Suc 0, Suc (Suc 0)}"] "{x. one_or_two x}"
     3.9  values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
    3.10  
    3.11  inductive one_or_two' :: "nat => bool"
    3.12 @@ -387,9 +387,9 @@
    3.13  
    3.14  values [expected "{}" dseq 0] 8 "{x. even x}"
    3.15  values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
    3.16 -values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
    3.17 -values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
    3.18 -values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
    3.19 +values [expected "{0, Suc (Suc 0)}" dseq 3] 8 "{x. even x}"
    3.20 +values [expected "{0, Suc (Suc 0)}" dseq 4] 8 "{x. even x}"
    3.21 +values [expected "{0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))}" dseq 6] 8 "{x. even x}"
    3.22  
    3.23  values [random_dseq 1, 1, 0] 8 "{x. even x}"
    3.24  values [random_dseq 1, 1, 1] 8 "{x. even x}"
    3.25 @@ -442,7 +442,7 @@
    3.26  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
    3.27  
    3.28  values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.29 -values [expected "{(([]::nat list), [1, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.30 +values [expected "{(([]::nat list), [Suc 0, Suc (Suc 0), Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc 0))), Suc (Suc (Suc (Suc (Suc 0))))])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.31  values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.32  values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.33  values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
    3.34 @@ -553,9 +553,9 @@
    3.35  
    3.36  thm filter1.equation
    3.37  
    3.38 -values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    3.39 +values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    3.40  values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    3.41 -values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    3.42 +values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
    3.43  
    3.44  inductive filter2
    3.45  where
    3.46 @@ -1233,16 +1233,21 @@
    3.47  thm plus_nat_test.equation
    3.48  thm plus_nat_test.new_random_dseq_equation
    3.49  
    3.50 -values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
    3.51 -values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
    3.52 -values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
    3.53 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 4 5 z}"
    3.54 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 7 2 z}"
    3.55 +values [expected "{Suc (Suc (Suc (Suc 0)))}"] "{y. plus_nat_test 5 y 9}"
    3.56  values [expected "{}"] "{y. plus_nat_test 9 y 8}"
    3.57 -values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
    3.58 -values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
    3.59 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc 0)))))}"] "{y. plus_nat_test 1 y 7}"
    3.60 +values [expected "{Suc (Suc 0)}"] "{x. plus_nat_test x 7 9}"
    3.61  values [expected "{}"] "{x. plus_nat_test x 9 7}"
    3.62 -values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
    3.63 -values [expected "{(0::nat, 1::nat), (1, 0)}"] "{(x, y). plus_nat_test x y 1}"
    3.64 -values [expected "{(0::nat, 5::nat), (4, 1), (3, 2), (2, 3), (1, 4), (5, 0)}"]
    3.65 +values [expected "{(0::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 0}"
    3.66 +values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
    3.67 +values [expected "{(0, Suc (Suc (Suc (Suc (Suc 0))))),
    3.68 +                  (Suc 0, Suc (Suc (Suc (Suc 0)))),
    3.69 +                  (Suc (Suc 0), Suc (Suc (Suc 0))),
    3.70 +                  (Suc (Suc (Suc 0)), Suc (Suc 0)),
    3.71 +                  (Suc (Suc (Suc (Suc 0))), Suc 0),
    3.72 +                  (Suc (Suc (Suc (Suc (Suc 0)))), 0)}"]
    3.73    "{(x, y). plus_nat_test x y 5}"
    3.74  
    3.75  inductive minus_nat_test :: "nat => nat => nat => bool"
    3.76 @@ -1256,10 +1261,10 @@
    3.77  thm minus_nat_test.new_random_dseq_equation
    3.78  
    3.79  values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
    3.80 -values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
    3.81 -values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
    3.82 -values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
    3.83 -values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
    3.84 +values [expected "{Suc (Suc (Suc (Suc (Suc 0))))}"] "{z. minus_nat_test 7 2 z}"
    3.85 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 7 9}"
    3.86 +values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 9 7}"
    3.87 +values [expected "{0, Suc 0, Suc (Suc 0), Suc (Suc (Suc 0))}"] "{x. minus_nat_test x 3 0}"
    3.88  values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
    3.89  
    3.90  subsection {* Examples on int *}
     4.1 --- a/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     4.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     4.3 @@ -129,7 +129,6 @@
     4.4  text {* Now we specify on which subterm it should be applied *}
     4.5  lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
     4.6    apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
     4.7 -  apply code_simp
     4.8  oops
     4.9  
    4.10