605 (* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *) |
605 (* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *) |
606 (* the T1,...,Tn depend on the types of the datatype's constructors) *) |
606 (* the T1,...,Tn depend on the types of the datatype's constructors) *) |
607 ((case last_elem (binder_types T) of |
607 ((case last_elem (binder_types T) of |
608 Type (s', _) => |
608 Type (s', _) => |
609 (case DatatypePackage.datatype_info thy s' of |
609 (case DatatypePackage.datatype_info thy s' of |
610 Some info => |
610 Some info => s mem (#rec_names info) |
611 (* TODO: I'm not quite sure if comparing the names is sufficient, or if *) |
611 | None => false) (* not an inductive datatype *) |
612 (* we should also check the type *) |
|
613 s mem (#rec_names info) |
|
614 | None => (* not an inductive datatype *) |
|
615 false) |
|
616 | _ => (* a (free or schematic) type variable *) |
612 | _ => (* a (free or schematic) type variable *) |
617 false) |
613 false) |
618 handle LIST "last_elem" => false) (* not even a function type *) |
614 handle LIST "last_elem" => false) (* not even a function type *) |
619 in |
615 in |
620 if is_IDT_constructor () then |
616 if is_IDT_constructor () then |
1346 Some (Node [FF, TT], model, args) |
1342 Some (Node [FF, TT], model, args) |
1347 | Const ("True", _) => (* redundant, since 'True' is also an IDT constructor *) |
1343 | Const ("True", _) => (* redundant, since 'True' is also an IDT constructor *) |
1348 Some (TT, model, args) |
1344 Some (TT, model, args) |
1349 | Const ("False", _) => (* redundant, since 'False' is also an IDT constructor *) |
1345 | Const ("False", _) => (* redundant, since 'False' is also an IDT constructor *) |
1350 Some (FF, model, args) |
1346 Some (FF, model, args) |
1351 | Const ("All", _) $ t1 => (* if 'All' occurs without an argument (i.e. *) |
1347 | Const ("All", _) $ t1 => |
1352 (* as argument to a higher-order function or *) |
1348 (* if "All" occurs without an argument (i.e. as argument to a higher-order *) |
1353 (* predicate), it is handled by the *) |
1349 (* function or predicate), it is handled by the 'stlc_interpreter' (i.e. *) |
1354 (* 'stlc_interpreter' (i.e. by unfolding its *) |
1350 (* by unfolding its definition) *) |
1355 (* definition) *) |
|
1356 let |
1351 let |
1357 val (i, m, a) = interpret thy model args t1 |
1352 val (i, m, a) = interpret thy model args t1 |
1358 in |
1353 in |
1359 case i of |
1354 case i of |
1360 Node xs => |
1355 Node xs => |
1365 Some (Leaf [fmTrue, fmFalse], m, a) |
1360 Some (Leaf [fmTrue, fmFalse], m, a) |
1366 end |
1361 end |
1367 | _ => |
1362 | _ => |
1368 raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function") |
1363 raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function") |
1369 end |
1364 end |
1370 | Const ("Ex", _) $ t1 => (* if 'Ex' occurs without an argument (i.e. as *) |
1365 | Const ("Ex", _) $ t1 => |
1371 (* argument to a higher-order function or *) |
1366 (* if "Ex" occurs without an argument (i.e. as argument to a higher-order *) |
1372 (* predicate), it is handled by the *) |
1367 (* function or predicate), it is handled by the 'stlc_interpreter' (i.e. *) |
1373 (* 'stlc_interpreter' (i.e. by unfolding its *) |
1368 (* by unfolding its definition) *) |
1374 (* definition) *) |
|
1375 let |
1369 let |
1376 val (i, m, a) = interpret thy model args t1 |
1370 val (i, m, a) = interpret thy model args t1 |
1377 in |
1371 in |
1378 case i of |
1372 case i of |
1379 Node xs => |
1373 Node xs => |