48 definitely be inconsistent. |
48 definitely be inconsistent. |
49 *) |
49 *) |
50 basevars_def: "stvars vs == range vs = UNIV" |
50 basevars_def: "stvars vs == range vs = UNIV" |
51 |
51 |
52 |
52 |
53 lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c" |
53 lemma basevars: "\<And>vs. basevars vs ==> \<exists>u. vs u = c" |
54 apply (unfold basevars_def) |
54 apply (unfold basevars_def) |
55 apply (rule_tac b = c and f = vs in rangeE) |
55 apply (rule_tac b = c and f = vs in rangeE) |
56 apply auto |
56 apply auto |
57 done |
57 done |
58 |
58 |
59 lemma base_pair1: "!!x y. basevars (x,y) ==> basevars x" |
59 lemma base_pair1: "\<And>x y. basevars (x,y) ==> basevars x" |
60 apply (simp (no_asm) add: basevars_def) |
60 apply (simp (no_asm) add: basevars_def) |
61 apply (rule equalityI) |
61 apply (rule equalityI) |
62 apply (rule subset_UNIV) |
62 apply (rule subset_UNIV) |
63 apply (rule subsetI) |
63 apply (rule subsetI) |
64 apply (drule_tac c = "(xa, arbitrary) " in basevars) |
64 apply (drule_tac c = "(xa, arbitrary) " in basevars) |
65 apply auto |
65 apply auto |
66 done |
66 done |
67 |
67 |
68 lemma base_pair2: "!!x y. basevars (x,y) ==> basevars y" |
68 lemma base_pair2: "\<And>x y. basevars (x,y) ==> basevars y" |
69 apply (simp (no_asm) add: basevars_def) |
69 apply (simp (no_asm) add: basevars_def) |
70 apply (rule equalityI) |
70 apply (rule equalityI) |
71 apply (rule subset_UNIV) |
71 apply (rule subset_UNIV) |
72 apply (rule subsetI) |
72 apply (rule subsetI) |
73 apply (drule_tac c = "(arbitrary, xa) " in basevars) |
73 apply (drule_tac c = "(arbitrary, xa) " in basevars) |
74 apply auto |
74 apply auto |
75 done |
75 done |
76 |
76 |
77 lemma base_pair: "!!x y. basevars (x,y) ==> basevars x & basevars y" |
77 lemma base_pair: "\<And>x y. basevars (x,y) ==> basevars x & basevars y" |
78 apply (rule conjI) |
78 apply (rule conjI) |
79 apply (erule base_pair1) |
79 apply (erule base_pair1) |
80 apply (erule base_pair2) |
80 apply (erule base_pair2) |
81 done |
81 done |
82 |
82 |
87 lemma unit_base: "basevars (v::unit stfun)" |
87 lemma unit_base: "basevars (v::unit stfun)" |
88 apply (unfold basevars_def) |
88 apply (unfold basevars_def) |
89 apply auto |
89 apply auto |
90 done |
90 done |
91 |
91 |
92 lemma baseE: "[| basevars v; !!x. v x = c ==> Q |] ==> Q" |
92 lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> Q" |
93 apply (erule basevars [THEN exE]) |
93 apply (erule basevars [THEN exE]) |
94 apply blast |
94 apply blast |
95 done |
95 done |
96 |
96 |
97 |
97 |
98 (* ------------------------------------------------------------------------------- |
98 (* ------------------------------------------------------------------------------- |
99 The following shows that there should not be duplicates in a "stvars" tuple: |
99 The following shows that there should not be duplicates in a "stvars" tuple: |
100 *) |
100 *) |
101 |
101 |
102 lemma "!!v. basevars (v::bool stfun, v) ==> False" |
102 lemma "\<And>v. basevars (v::bool stfun, v) ==> False" |
103 apply (erule baseE) |
103 apply (erule baseE) |
104 apply (subgoal_tac "(LIFT (v,v)) x = (True, False)") |
104 apply (subgoal_tac "(LIFT (v,v)) x = (True, False)") |
105 prefer 2 |
105 prefer 2 |
106 apply assumption |
106 apply assumption |
107 apply simp |
107 apply simp |