simplified setup
authorhaftmann
Mon Jun 05 15:59:45 2017 +0200 (2017-06-05)
changeset 66011f10bbfe07c41
parent 66010 2f7d39285a1a
child 66012 59bf29d2b3a1
simplified setup
src/HOL/Nitpick.thy
     1.1 --- a/src/HOL/Nitpick.thy	Mon Jun 05 15:59:41 2017 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Jun 05 15:59:45 2017 +0200
     1.3 @@ -119,36 +119,25 @@
     1.4  \<open>rat\<close> and \<open>real\<close>.
     1.5  \<close>
     1.6  
     1.7 -function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
     1.8 +fun nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
     1.9    "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
    1.10 -  by auto
    1.11 -termination
    1.12 -  apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
    1.13 -   apply auto
    1.14 -   apply (metis mod_less_divisor xt1(9))
    1.15 -  apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
    1.16 -  done
    1.17 -
    1.18 +  
    1.19  declare nat_gcd.simps [simp del]
    1.20  
    1.21  definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.22    "nat_lcm x y = x * y div (nat_gcd x y)"
    1.23  
    1.24 -definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.25 -  "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    1.26 -
    1.27 -definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.28 -  "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    1.29 -
    1.30 -lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
    1.31 +lemma gcd_eq_nitpick_gcd [nitpick_unfold]:
    1.32 +  "gcd x y = Nitpick.nat_gcd x y"
    1.33    by (induct x y rule: nat_gcd.induct)
    1.34      (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    1.35  
    1.36 -lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
    1.37 +lemma lcm_eq_nitpick_lcm [nitpick_unfold]:
    1.38 +  "lcm x y = Nitpick.nat_lcm x y"
    1.39    by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    1.40  
    1.41  definition Frac :: "int \<times> int \<Rightarrow> bool" where
    1.42 -  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
    1.43 +  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
    1.44  
    1.45  consts
    1.46    Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
    1.47 @@ -170,7 +159,7 @@
    1.48    "norm_frac a b =
    1.49      (if b < 0 then norm_frac (- a) (- b)
    1.50       else if a = 0 \<or> b = 0 then (0, 1)
    1.51 -     else let c = int_gcd a b in (a div c, b div c))"
    1.52 +     else let c = gcd a b in (a div c, b div c))"
    1.53    by pat_completeness auto
    1.54    termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto
    1.55  
    1.56 @@ -180,7 +169,7 @@
    1.57    "frac a b \<equiv> Abs_Frac (norm_frac a b)"
    1.58  
    1.59  definition plus_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.60 -  [nitpick_simp]: "plus_frac q r = (let d = int_lcm (denom q) (denom r) in
    1.61 +  [nitpick_simp]: "plus_frac q r = (let d = lcm (denom q) (denom r) in
    1.62      frac (num q * (d div denom q) + num r * (d div denom r)) d)"
    1.63  
    1.64  definition times_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.65 @@ -239,7 +228,7 @@
    1.66  \<close>
    1.67  
    1.68  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
    1.69 -  refl' wf' card' sum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.70 +  refl' wf' card' sum' fold_graph' nat_gcd nat_lcm Frac Abs_Frac Rep_Frac
    1.71    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac
    1.72    inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec'
    1.73  
    1.74 @@ -247,7 +236,7 @@
    1.75  
    1.76  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
    1.77    card'_def sum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    1.78 -  size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.79 +  size_list_simp nat_lcm_def Frac_def zero_frac_def one_frac_def
    1.80    num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
    1.81    number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
    1.82    wfrec'_def