equal
deleted
inserted
replaced
61 |
61 |
62 lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)" |
62 lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)" |
63 by(auto simp: eq_st_def) |
63 by(auto simp: eq_st_def) |
64 |
64 |
65 instance |
65 instance |
66 proof |
66 proof (standard, goal_cases) |
67 case goal1 thus ?case |
67 case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1) |
68 by transfer (simp add: less_eq_st_rep_iff widen1) |
68 next |
69 next |
69 case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2) |
70 case goal2 thus ?case |
70 next |
71 by transfer (simp add: less_eq_st_rep_iff widen2) |
71 case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1) |
72 next |
72 next |
73 case goal3 thus ?case |
73 case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2) |
74 by transfer (simp add: less_eq_st_rep_iff narrow1) |
|
75 next |
|
76 case goal4 thus ?case |
|
77 by transfer (simp add: less_eq_st_rep_iff narrow2) |
|
78 qed |
74 qed |
79 |
75 |
80 end |
76 end |
81 |
77 |
82 |
78 |
92 "None \<triangle> x = None" | |
88 "None \<triangle> x = None" | |
93 "x \<triangle> None = None" | |
89 "x \<triangle> None = None" | |
94 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
90 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
95 |
91 |
96 instance |
92 instance |
97 proof |
93 proof (standard, goal_cases) |
98 case goal1 thus ?case |
94 case (1 x y) thus ?case |
99 by(induct x y rule: widen_option.induct)(simp_all add: widen1) |
95 by(induct x y rule: widen_option.induct)(simp_all add: widen1) |
100 next |
96 next |
101 case goal2 thus ?case |
97 case (2 x y) thus ?case |
102 by(induct x y rule: widen_option.induct)(simp_all add: widen2) |
98 by(induct x y rule: widen_option.induct)(simp_all add: widen2) |
103 next |
99 next |
104 case goal3 thus ?case |
100 case (3 x y) thus ?case |
105 by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
101 by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
106 next |
102 next |
107 case goal4 thus ?case |
103 case (4 y x) thus ?case |
108 by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
104 by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
109 qed |
105 qed |
110 |
106 |
111 end |
107 end |
112 |
108 |
548 permanent_interpretation Abs_Int_wn_measure |
544 permanent_interpretation Abs_Int_wn_measure |
549 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
545 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
550 and test_num' = in_ivl |
546 and test_num' = in_ivl |
551 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl |
547 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl |
552 and m = m_ivl and n = n_ivl and h = 3 |
548 and m = m_ivl and n = n_ivl and h = 3 |
553 proof |
549 proof (standard, goal_cases) |
554 case goal2 thus ?case by(rule m_ivl_anti_mono) |
550 case 2 thus ?case by(rule m_ivl_anti_mono) |
555 next |
551 next |
556 case goal1 thus ?case by(rule m_ivl_height) |
552 case 1 thus ?case by(rule m_ivl_height) |
557 next |
553 next |
558 case goal3 thus ?case by(rule m_ivl_widen) |
554 case 3 thus ?case by(rule m_ivl_widen) |
559 next |
555 next |
560 case goal4 from goal4(2) show ?case by(rule n_ivl_narrow) |
556 case 4 from 4(2) show ?case by(rule n_ivl_narrow) |
561 -- "note that the first assms is unnecessary for intervals" |
557 -- "note that the first assms is unnecessary for intervals" |
562 qed |
558 qed |
563 |
559 |
564 lemma iter_winden_step_ivl_termination: |
560 lemma iter_winden_step_ivl_termination: |
565 "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C" |
561 "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C" |