src/HOL/Decision_Procs/Ferrack.thy
changeset 61424 c3658c18b7bc
parent 60767 ad5b4771fc19
child 61586 5197a2ecb658
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -1129,7 +1129,7 @@
     1.4    by pat_completeness auto
     1.5  termination rsplit0 by (relation "measure num_size") simp_all
     1.6  
     1.7 -lemma rsplit0: "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
     1.8 +lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
     1.9  proof (induct t rule: rsplit0.induct)
    1.10    case (2 a b)
    1.11    let ?sa = "rsplit0 a"
    1.12 @@ -1140,8 +1140,8 @@
    1.13    let ?tb = "snd ?sb"
    1.14    from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
    1.15      by (cases "rsplit0 a") (auto simp add: Let_def split_def)
    1.16 -  have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =
    1.17 -    Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
    1.18 +  have "Inum bs ((case_prod (CN 0)) (rsplit0 (Add a b))) =
    1.19 +    Inum bs ((case_prod (CN 0)) ?sa)+Inum bs ((case_prod (CN 0)) ?sb)"
    1.20      by (simp add: Let_def split_def algebra_simps)
    1.21    also have "\<dots> = Inum bs a + Inum bs b"
    1.22      using 2 by (cases "rsplit0 a") auto
    1.23 @@ -1180,38 +1180,38 @@
    1.24    "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
    1.25      else (NEq (CN 0 (-c) (Neg t))))"
    1.26  
    1.27 -lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) =
    1.28 -  Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
    1.29 +lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod lt (rsplit0 t)) =
    1.30 +  Ifm bs (Lt t) \<and> isrlfm (case_prod lt (rsplit0 t))"
    1.31    using rsplit0[where bs = "bs" and t="t"]
    1.32    by (auto simp add: lt_def split_def, cases "snd(rsplit0 t)", auto,
    1.33      rename_tac nat a b, case_tac "nat", auto)
    1.34  
    1.35 -lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) =
    1.36 -  Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
    1.37 +lemma le: "numnoabs t \<Longrightarrow> Ifm bs (case_prod le (rsplit0 t)) =
    1.38 +  Ifm bs (Le t) \<and> isrlfm (case_prod le (rsplit0 t))"
    1.39    using rsplit0[where bs = "bs" and t="t"]
    1.40    by (auto simp add: le_def split_def, cases "snd(rsplit0 t)", auto,
    1.41      rename_tac nat a b, case_tac "nat", auto)
    1.42  
    1.43 -lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) =
    1.44 -  Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
    1.45 +lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod gt (rsplit0 t)) =
    1.46 +  Ifm bs (Gt t) \<and> isrlfm (case_prod gt (rsplit0 t))"
    1.47    using rsplit0[where bs = "bs" and t="t"]
    1.48    by (auto simp add: gt_def split_def, cases "snd(rsplit0 t)", auto,
    1.49      rename_tac nat a b, case_tac "nat", auto)
    1.50  
    1.51 -lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) =
    1.52 -  Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
    1.53 +lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (case_prod ge (rsplit0 t)) =
    1.54 +  Ifm bs (Ge t) \<and> isrlfm (case_prod ge (rsplit0 t))"
    1.55    using rsplit0[where bs = "bs" and t="t"]
    1.56    by (auto simp add: ge_def split_def, cases "snd(rsplit0 t)", auto,
    1.57      rename_tac nat a b, case_tac "nat", auto)
    1.58  
    1.59 -lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) =
    1.60 -  Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
    1.61 +lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod eq (rsplit0 t)) =
    1.62 +  Ifm bs (Eq t) \<and> isrlfm (case_prod eq (rsplit0 t))"
    1.63    using rsplit0[where bs = "bs" and t="t"]
    1.64    by (auto simp add: eq_def split_def, cases "snd(rsplit0 t)", auto,
    1.65      rename_tac nat a b, case_tac "nat", auto)
    1.66  
    1.67 -lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) =
    1.68 -  Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
    1.69 +lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod neq (rsplit0 t)) =
    1.70 +  Ifm bs (NEq t) \<and> isrlfm (case_prod neq (rsplit0 t))"
    1.71    using rsplit0[where bs = "bs" and t="t"]
    1.72    by (auto simp add: neq_def split_def, cases "snd(rsplit0 t)", auto,
    1.73      rename_tac nat a b, case_tac "nat", auto)
    1.74 @@ -1228,12 +1228,12 @@
    1.75    "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
    1.76    "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
    1.77    "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
    1.78 -  "rlfm (Lt a) = split lt (rsplit0 a)"
    1.79 -  "rlfm (Le a) = split le (rsplit0 a)"
    1.80 -  "rlfm (Gt a) = split gt (rsplit0 a)"
    1.81 -  "rlfm (Ge a) = split ge (rsplit0 a)"
    1.82 -  "rlfm (Eq a) = split eq (rsplit0 a)"
    1.83 -  "rlfm (NEq a) = split neq (rsplit0 a)"
    1.84 +  "rlfm (Lt a) = case_prod lt (rsplit0 a)"
    1.85 +  "rlfm (Le a) = case_prod le (rsplit0 a)"
    1.86 +  "rlfm (Gt a) = case_prod gt (rsplit0 a)"
    1.87 +  "rlfm (Ge a) = case_prod ge (rsplit0 a)"
    1.88 +  "rlfm (Eq a) = case_prod eq (rsplit0 a)"
    1.89 +  "rlfm (NEq a) = case_prod neq (rsplit0 a)"
    1.90    "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
    1.91    "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
    1.92    "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
    1.93 @@ -2430,7 +2430,7 @@
    1.94      using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm)
    1.95    also have "\<dots> = (Ifm (x#bs) ?res)"
    1.96      using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm \<circ> (usubst ?q)",symmetric]
    1.97 -    by (simp add: split_def pair_collapse)
    1.98 +    by (simp add: split_def prod.collapse)
    1.99    finally have lheq: "?lhs = Ifm bs (decr ?res)"
   1.100      using decr[OF nbth] by blast
   1.101    then have lr: "?lhs = ?rhs"