2152 @{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text |
2152 @{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text |
2153 "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh |
2153 "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh |
2154 for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume |
2154 for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume |
2155 all bound atoms from an assignment are fresh for @{text "c"} (fourth |
2155 all bound atoms from an assignment are fresh for @{text "c"} (fourth |
2156 line). In order to see how an instantiation for @{text "c"} in the |
2156 line). In order to see how an instantiation for @{text "c"} in the |
2157 conclusion `controls' the premises, you have to take into account that |
2157 conclusion `controls' the premises, one has to take into account that |
2158 Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated |
2158 Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated |
2159 with a pair, for example, then this type-constraint will be propagated to |
2159 with a pair, for example, then this type-constraint will be propagated to |
2160 the premises. The main point is that if @{text "c"} is instantiated |
2160 the premises. The main point is that if @{text "c"} is instantiated |
2161 appropriately, then the user can mimic the usual `pencil-and-paper' |
2161 appropriately, then the user can mimic the usual `pencil-and-paper' |
2162 reasoning employing the variable convention about bound and free variables |
2162 reasoning employing the variable convention about bound and free variables |