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"
```