theory "Value" imports "~~/src/HOL/HOLCF/HOLCF" begin subsubsection {* The semantic domain for values and environments *} domain Value = Fn (lazy "Value → Value") | B (lazy "bool discr") fixrec Fn_project :: "Value → Value → Value" where "Fn_project⋅(Fn⋅f) = f" abbreviation Fn_project_abbr (infix "↓Fn" 55) where "f ↓Fn v ≡ Fn_project⋅f⋅v" lemma [simp]: "⊥ ↓Fn x = ⊥" "(B⋅b) ↓Fn x = ⊥" by (fixrec_simp)+ fixrec B_project :: "Value → Value → Value → Value" where "B_project⋅(B⋅db)⋅v⇩1⋅v⇩2 = (if undiscr db then v⇩1 else v⇩2)" lemma [simp]: "B_project⋅(B⋅(Discr b))⋅v⇩1⋅v⇩2 = (if b then v⇩1 else v⇩2)" "B_project⋅⊥⋅v⇩1⋅v⇩2 = ⊥" "B_project⋅(Fn⋅f)⋅v⇩1⋅v⇩2 = ⊥" by fixrec_simp+ text {* A chain in the domain @{typ Value} is either always bottom, or eventually @{term "Fn"} of another chain *} lemma Value_chainE[consumes 1, case_names bot B Fn]: assumes "chain Y" obtains "Y = (λ _ . ⊥)" | n b where "Y = (λ m. (if m < n then ⊥ else B⋅b))" | n Y' where "Y = (λ m. (if m < n then ⊥ else Fn⋅(Y' (m-n))))" "chain Y'" proof(cases "Y = (λ _ . ⊥)") case True thus ?thesis by (rule that(1)) next case False hence "∃ i. Y i ≠ ⊥" by auto hence "∃ n. Y n ≠ ⊥ ∧ (∀m. Y m ≠ ⊥ ⟶ m ≥ n)" by (rule exE)(rule ex_has_least_nat) then obtain n where "Y n ≠ ⊥" and "∀m. m < n ⟶ Y m = ⊥" by fastforce hence "(∃ f. Y n = Fn⋅f) ∨ (∃ b. Y n = B⋅b)" by (metis Value.exhaust) thus ?thesis proof assume "(∃ f. Y n = Fn⋅f)" then obtain f where "Y n = Fn ⋅ f" by blast { fix i from `chain Y` have "Y n ⊑ Y (i+n)" by (metis chain_mono le_add2) with `Y n = _` have "∃ g. (Y (i+n) = Fn ⋅ g)" by (metis Value.dist_les(1) Value.exhaust below_bottom_iff) } then obtain Y' where Y': "⋀ i. Y (i + n) = Fn ⋅ (Y' i)" by metis have "Y = (λm. if m < n then ⊥ else Fn⋅(Y' (m - n)))" using `∀m. _` Y' by (metis add_diff_inverse add.commute) moreover have"chain Y'" using `chain Y` by (auto intro!:chainI elim: chainE simp add: Value.inverts[symmetric] Y'[symmetric] simp del: Value.inverts) ultimately show ?thesis by (rule that(3)) next assume "(∃ b. Y n = B⋅b)" then obtain b where "Y n = B⋅b" by blast { fix i from `chain Y` have "Y n ⊑ Y (i+n)" by (metis chain_mono le_add2) with `Y n = _` have "Y (i+n) = B⋅b" by (metis Value.dist_les(2) Value.exhaust Value.inverts(2) below_bottom_iff discrete_cpo) } hence Y': "⋀ i. Y (i + n) = B⋅b" by metis have "Y = (λm. if m < n then ⊥ else B⋅b)" using `∀m. _` Y' by (metis add_diff_inverse add.commute) thus ?thesis by (rule that(2)) qed qed end